1) added simplification of actives w.r.t. selected

[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 1729919af30556c5e48f78b844bb92be93a4f03c..4015d4b6d4a37444ce4b0f2ec6bda3473fce8cbb 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -19,6 +19,8 @@ module Superposition (B : Terms.Blob) =
     module Order = Orderings.Orderings(B)
     module Utils = FoUtils.Utils(B)
     module Pp = Pp.Pp(B)
+    
+    exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
 
     let rec list_first f = function
       | [] -> None
@@ -181,9 +183,17 @@ module Superposition (B : Terms.Blob) =
         else Some (bag, clause)
     ;;
 
+    (* this is like forward_simplify but raises Success *)
+    let backward_simplify maxvar table bag clause = 
+      let bag, clause = demodulate bag clause table in
+      if is_identity_clause clause then raise (Success (bag, maxvar, clause))
+      else bag, clause
+    ;;
+
     (* =================== inference ===================== *)
 
-    let superposition_right table varlist subterm pos context =
+    (* this is OK for both the sup_left and sup_right inference steps *)
+    let superposition table varlist subterm pos context =
       let cands = IDX.DT.retrieve_unifiables table subterm in
       HExtlib.filter_map
         (fun (dir, (id,lit,vl,_ (*as uc*))) ->
@@ -232,33 +242,33 @@ module Superposition (B : Terms.Blob) =
        bag, maxvar, res
     ;;
 
-    let superposition_right_with_table bag maxvar (id,selected,vl,_) table =
+    let superposition_with_table bag maxvar (id,selected,vl,_) table =
       match selected with 
       | Terms.Predicate _ -> assert false
       | Terms.Equation (l,r,ty,Terms.Lt) ->
-          fold_build_new_clause bag maxvar id Terms.SuperpositionRight 
+          fold_build_new_clause bag maxvar id Terms.Superposition
             (fun _ -> true)
             (all_positions [3] 
               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
-              r (superposition_right table vl))          
+              r (superposition table vl))          
       | Terms.Equation (l,r,ty,Terms.Gt) ->
-          fold_build_new_clause bag maxvar id Terms.SuperpositionRight
+          fold_build_new_clause bag maxvar id Terms.Superposition
             (fun _ -> true)
             (all_positions [2] 
               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
-              l (superposition_right table vl))
+              l (superposition table vl))
       | Terms.Equation (l,r,ty,Terms.Incomparable) -> 
-          fold_build_new_clause bag maxvar id Terms.SuperpositionRight
+          fold_build_new_clause bag maxvar id Terms.Superposition
             (function (* Riazanov: p.33 condition (iv) *)
               | Terms.Node [Terms.Leaf eq; ty; l; r ] when B.eq B.eqP eq -> 
                   Order.compare_terms l r <> Terms.Eq
               | _ -> assert false)
             ((all_positions [3] 
                (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
-               r (superposition_right table vl)) @         
+               r (superposition table vl)) @         
              (all_positions [2] 
                (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
-               l (superposition_right table vl)))
+               l (superposition table vl)))
       | _ -> assert false
     ;;
 
@@ -266,11 +276,17 @@ module Superposition (B : Terms.Blob) =
      * (and is not the identity) *)
     let infer_right bag maxvar current (alist,atable) = 
       let ctable = IDX.index_unit_clause IDX.DT.empty current in
+      let bag, (alist, atable) = 
+        let bag, alist = 
+          HExtlib.filter_map_acc (forward_simplify ctable) bag alist
+        in
+        bag, (alist, List.fold_left IDX.index_unit_clause IDX.DT.empty alist)
+      in
       let bag, maxvar, new_clauses =
         List.fold_left 
           (fun (bag, maxvar, acc) active ->
              let bag, maxvar, newc = 
-               superposition_right_with_table bag maxvar active ctable 
+               superposition_with_table bag maxvar active ctable 
              in
              bag, maxvar, newc @ acc)
           (bag, maxvar, []) alist
@@ -280,7 +296,7 @@ module Superposition (B : Terms.Blob) =
       in
       let fresh_current, maxvar = Utils.fresh_unit_clause maxvar current in
       let bag, maxvar, additional_new_clauses =
-        superposition_right_with_table bag maxvar fresh_current atable 
+        superposition_with_table bag maxvar fresh_current atable 
       in
       let new_clauses = new_clauses @ additional_new_clauses in
       let bag, new_clauses = 
@@ -289,6 +305,20 @@ module Superposition (B : Terms.Blob) =
       bag, maxvar, (alist, atable), new_clauses
     ;;
 
+    let infer_left bag maxvar goal (_alist, atable) =
+      let bag, maxvar, new_goals =
+        superposition_with_table bag maxvar goal atable 
+      in
+      let bag, new_goals = 
+        List.fold_left
+         (fun (bag, acc) g -> 
+            let bag, g = demodulate bag g atable in
+            bag, g :: acc) 
+         (bag, []) new_goals
+      in
+      bag, maxvar, List.rev new_goals
+    ;;
+
   end