1. New paramodulation function

2. goal narrowing works both on the current goal both before and after
demodulation

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index a3fd41e21b1d8c5a68a65f88ecc89984c7667ae0..7c934df1e59cd48373a65d5a66ff11d98237eb82 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -12,7 +12,7 @@
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
 (* let debug s = prerr_endline (Lazy.force s) ;; *)
-let debug _ = ();; 
+let debug _ = ();;  
 
 let monster = 100;;
     
@@ -53,6 +53,11 @@ module type Paramod =
       passives:t Terms.unit_clause list -> szsontology
     val fast_eq_check :
       state -> input* input -> szsontology
+    val nparamod :
+      useage:bool ->
+      max_steps:int ->
+      ?timeout:float ->
+      state -> input* input -> szsontology
   end
 
 module Paramod (B : Orderings.Blob) = struct
@@ -248,7 +253,7 @@ module Paramod (B : Orderings.Blob) = struct
       in
         debug (lazy "Performed infer_left step");
        let bag = Terms.replace_in_bag (g_current,false,iterno) bag in
-        bag, maxvar, actives, passives, g_current::g_actives,
+          bag, maxvar, actives, passives, g_current::g_actives,
     (add_passive_goals g_passives new_goals)
   ;;
 
@@ -278,6 +283,10 @@ module Paramod (B : Orderings.Blob) = struct
     let bag, maxvar, actives, new_clauses = 
       Sup.infer_right bag maxvar current actives 
     in
+      debug
+       (lazy 
+        ("New clauses :" ^ (String.concat ";\n" 
+           (List.map Pp.pp_unit_clause new_clauses)))); 
       debug (lazy "Demodulating goals with actives...");
       (* keep goals demodulated w.r.t. actives and check if solved *)
       let bag, g_actives = 
@@ -324,17 +333,16 @@ module Paramod (B : Orderings.Blob) = struct
   let last_chance (bag,maxvar,actives,passives,g_actives,g_passives) =
     debug (lazy("Last chance " ^ string_of_float
                  (Unix.gettimeofday())));
-    let active_t = snd actives in
+    let actives_l, active_t = actives in
     let passive_t,wset,_ = passives in
     let _ = debug
       (lazy 
-        ("Passive set :" ^ (String.concat ";\n" 
-           (List.map (fun _,cl -> Pp.pp_unit_clause cl) 
-              (WeightPassiveSet.elements wset))))) in
+        ("Actives :" ^ (String.concat ";\n" 
+           (List.map Pp.pp_unit_clause actives_l)))) in 
     let wset = IDX.elems passive_t in
     let _ = debug
       (lazy 
-        ("Passive table :" ^(String.concat ";\n" 
+        ("Passives:" ^(String.concat ";\n" 
            (List.map (fun _,cl -> Pp.pp_unit_clause cl)
               (IDX.ClauseSet.elements wset))))) in
     let g_passives = 
@@ -425,6 +433,21 @@ module Paramod (B : Orderings.Blob) = struct
         actives passives g_actives g_passives
   ;;
 
+  let check_and_infer ~no_demod iterno status current =
+    let bag,maxvar,actives,passives,g_actives,g_passives = status in
+    match 
+      Sup.simplify_goal 
+        ~no_demod:false maxvar (snd actives) bag g_actives current 
+    with
+      | None -> status
+      | Some (bag,g_current) -> 
+         let _ = 
+           debug (lazy("Infer on goal : " 
+                       ^ Pp.pp_unit_clause g_current)) 
+         in
+           backward_infer_step bag maxvar actives passives
+              g_actives g_passives g_current iterno
+
   (* similar to given_clause, but it merely works on goals, 
      in parallel, at each iteration *)
   let rec goal_narrowing iterno max_steps timeout status
@@ -446,19 +469,10 @@ module Paramod (B : Orderings.Blob) = struct
           let _ = 
             debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current)) 
           in
-           match 
-             Sup.simplify_goal 
-               ~no_demod:false maxvar (snd actives) bag g_actives current 
-           with
-             | None -> acc
-             | Some (bag,g_current) -> 
-                let _ = 
-                  debug (lazy("Demodulated goal : " 
-                              ^ Pp.pp_unit_clause g_current)) 
-                in
-                backward_infer_step bag maxvar actives passives
-                  g_actives g_passives g_current iterno)
-          status passive_goals
+            (* awe work both on the original goal and the demodulated one*)
+          let acc = check_and_infer ~no_demod:true iterno acc current
+          in check_and_infer ~no_demod:false iterno acc current)
+       status passive_goals
     in
       goal_narrowing iterno max_steps timeout newstatus
 
@@ -540,4 +554,18 @@ let fast_eq_check s goal =
     | Stop o -> o
   ;;
 
+let nparamod ~useage ~max_steps ?timeout s goal =
+  let bag,maxvar,actives,passives,g_actives,g_passives
+      = initialize_goal s goal in
+  if is_passive_g_set_empty g_passives then Error "not an equation" 
+  else
+    try given_clause ~useage ~noinfer:false
+      bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives
+  with
+    | Sup.Success (bag, _, (i,_,_,_),subst) ->
+       compute_result bag i subst
+    | Stop (Unsatisfiable _) -> Error "solution found!"
+    | Stop o -> o
+  ;;
+
 end

diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli
index 321d0f8971730f03a2d7b06ccce9e63d5634956a..1142b03c7ea47cc451abd48bcdfecc5f5e4a4266 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.mli
+++ b/helm/software/components/ng_paramodulation/paramod.mli
@@ -48,6 +48,13 @@ module type Paramod =
       passives:t Terms.unit_clause list -> szsontology
     val fast_eq_check :
       state -> input* input -> szsontology
+    val nparamod :
+      useage:bool ->
+      max_steps:int ->
+      ?timeout:float ->
+      state -> 
+      input* input -> 
+      szsontology
   end
 
 module Paramod ( B : Orderings.Blob ) : Paramod