Rewrote the main loop for paramodulation

[helm.git] / helm / software / components / ng_paramodulation / superposition.ml

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index aef672c144f5b2ba307626217ce5d122260a8812..82fe83037b0a92ebe287dcd4114aa716b2d99c0c 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -120,7 +120,7 @@ module Superposition (B : Terms.Blob) =
                    let newside = Subst.apply_subst subst newside in
                    let o = Order.compare_terms newside side in
                    (* Riazanov, pp. 45 (ii) *)
-                   if o = Terms.Lt then  
+                   if o = Terms.Lt then
                      Some (context newside, subst, varlist, id, pos, dir)
                    else 
                      ((*prerr_endline ("Filtering: " ^ 
@@ -133,20 +133,25 @@ module Superposition (B : Terms.Blob) =
         (IDX.ClauseSet.elements cands)
     ;;
 
-    (* XXX: possible optimization, if the literal has a "side" already
-     * in normal form we should not traverse it again *)
-    let demodulate_once bag (id, literal, vl, pr) table =
+    let demodulate_once ~jump_to_right bag (id, literal, vl, pr) table =
       (* debug ("Demodulating : " ^ (Pp.pp_unit_clause (id, literal, vl, pr)));*)
       match literal with
       | Terms.Predicate t -> assert false
       | Terms.Equation (l,r,ty,_) ->
-        match first_position [2]
-         (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) l
-         (demod table vl)
-       with
+       let left_position = if jump_to_right then None else
+         first_position [2]
+           (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ]) l
+           (demod table vl)
+       in
+        match left_position with
          | Some (newt, subst, varlist, id2, pos, dir) ->
-             build_clause bag (fun _ -> true) Terms.Demodulation 
-               newt subst varlist id id2 pos dir
+             begin
+               match build_clause bag (fun _ -> true) Terms.Demodulation 
+                 newt subst varlist id id2 pos dir
+               with
+                 | None -> assert false
+                 | Some x -> Some (x,false)
+             end
          | None ->
              match first_position
                [3] (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ]) r
@@ -154,14 +159,22 @@ module Superposition (B : Terms.Blob) =
              with
                | None -> None
                | Some (newt, subst, varlist, id2, pos, dir) ->
-                   build_clause bag (fun _ -> true) Terms.Demodulation 
-                     newt subst varlist id id2 pos dir
+                   match build_clause bag (fun _ -> true)
+                     Terms.Demodulation newt subst varlist id id2 pos dir
+                   with
+                       | None -> assert false
+                       | Some x -> Some (x,true)
     ;;
 
-    let rec demodulate bag clause table =
-      match demodulate_once bag clause table with
+    let rec demodulate ~jump_to_right bag clause table =
+      match demodulate_once ~jump_to_right bag clause table with
       | None -> bag, clause
-      | Some (bag, clause) -> demodulate bag clause table
+      | Some ((bag, clause),r) -> demodulate ~jump_to_right:r
+         bag clause table
+    ;;
+
+    let demodulate bag clause table = demodulate ~jump_to_right:false
+      bag clause table
     ;;
 
     (* move away *)
@@ -438,6 +451,8 @@ module Superposition (B : Terms.Blob) =
       in
        debug "Another superposition";
       let new_clauses = new_clauses @ additional_new_clauses in
+       debug (Printf.sprintf "Demodulating %d clauses"
+                (List.length new_clauses));
       let bag, new_clauses = 
         HExtlib.filter_map_acc (simplify atable maxvar) bag new_clauses
       in
@@ -451,15 +466,15 @@ module Superposition (B : Terms.Blob) =
         superposition_with_table bag maxvar goal atable 
       in
        debug "Superposed goal with active clauses";
-       (* We demodulate the new goals with active clauses *)
+       (* We simplify the new goals with active clauses *)
       let bag, new_goals = 
         List.fold_left
          (fun (bag, acc) g -> 
-            let bag, g = demodulate bag g atable in
-            bag, g :: acc) 
+            let bag, g = simplify_goal maxvar atable bag g in
+             bag,g::acc)
          (bag, []) new_goals
       in
-       debug "Demodulated goal with active clauses";
+       debug "Simplified new goals with active clauses";
       bag, maxvar, List.rev new_goals
     ;;