snaphost: supright almost done

[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 b002dce33a05c4be5bc2f823d31f0c952293ed31..64cc35bd4e3a41e8331bb0ec071bbb9e5f30826f 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -17,11 +17,12 @@ module Superposition (B : Terms.Blob) =
     module Unif = FoUnif.Founif(B)
     module Subst = FoSubst.Subst(B)
     module Order = Orderings.Orderings(B)
+    module Utils = FoUtils.Utils(B)
 
-    let all_positions t f =
+    let all_positions pos ctx t f =
       let rec aux pos ctx = function
-      | Terms.Leaf a as t -> f t pos ctx 
-      | Terms.Var i -> []
+      | Terms.Leaf _ as t -> f t pos ctx 
+      | Terms.Var _ -> []
       | Terms.Node l as t-> 
           let acc, _, _ = 
             List.fold_left
@@ -34,7 +35,7 @@ module Superposition (B : Terms.Blob) =
           in
            acc
       in
-        aux [] (fun x -> x) t
+        aux pos ctx t
     ;;
 
     let superposition_right table varlist subterm pos context =
@@ -44,38 +45,85 @@ module Superposition (B : Terms.Blob) =
            match lit with
            | Terms.Predicate _ -> assert false
            | Terms.Equation (l,r,_,o) ->
+               assert(o <> Terms.Eq);
                let side, newside = if dir=Terms.Left2Right then l,r else r,l in
                try 
                  let subst, varlist = 
                    Unif.unification (varlist@vl) [] subterm side 
                  in
-                 Some (context newside, subst, varlist, id, pos, dir)
+                 if o = Terms.Incomparable then
+                   let side = Subst.apply_subst subst side in
+                   let newside = Subst.apply_subst subst newside in
+                   let o = Order.compare_terms side newside in
+                   (* XXX: check Riazanov p. 33 (iii) *)
+                   if o <> Terms.Lt && o <> Terms.Eq then  
+                     Some (context newside, subst, varlist, id, pos, dir)
+                   else 
+                     None
+                 else
+                   Some (context newside, subst, varlist, id, pos, dir)
                with FoUnif.UnificationFailure _ -> None)
         (IDX.ClauseSet.elements cands)
     ;;
 
-    let superposition_right_step bag (id,selected,vl,_) table =
+    let build_new_clause bag maxvar filter t subst vl id id2 pos dir =
+      let maxvar, vl, relocsubst = Utils.relocate maxvar vl in
+      let subst = Subst.concat relocsubst subst in
+      let proof = Terms.Step(Terms.SuperpositionRight,id,id2,dir,pos,subst) in
+      let t = Subst.apply_subst subst t in
+      if filter t then
+        let literal = 
+          match t with
+          | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
+               let o = Order.compare_terms l r in
+               Terms.Equation (l, r, ty, o)
+          | t -> Terms.Predicate t
+        in
+        let bag, uc = 
+          Utils.add_to_bag bag (0, literal, vl, proof)
+        in
+        Some (bag, maxvar, uc)
+      else
+        None
+    ;;
+
+    let fold_build_new_clause bag maxvar id filter res =
+      let maxvar, bag, new_clauses = 
+        List.fold_left
+          (fun (maxvar, bag, acc) (t,subst,vl,id2,pos,dir) -> 
+             match build_new_clause bag maxvar filter t subst vl id id2 pos dir
+             with Some (bag, maxvar, uc) -> maxvar, bag, uc::acc
+                | None -> maxvar, bag, acc)
+          (maxvar, bag, []) res
+      in
+      bag, maxvar, new_clauses
+    ;;
+
+    let superposition_right_with_table bag maxvar (id,selected,vl,_) table =
       match selected with 
       | Terms.Predicate _ -> assert false
-      | Terms.Equation (l,r,ty,Terms.Lt) -> 
-          let res = all_positions r (superposition_right table vl) in
-          let _new_clauses = 
-            List.map
-              (fun (r,subst,vl,id2,pos,dir) -> 
-                 let proof = 
-                   Terms.Step(Terms.SuperpositionRight,id,id2, dir, pos, subst)
-                 in
-                 let r = Subst.apply_subst subst r in
-                 let l = Subst.apply_subst subst l in
-                 let ty = Subst.apply_subst subst ty in
-                 let o = Order.compare_terms l r in
-                 (* can unif compute the right vl for both sides? *)
-                 (0, Terms.Equation (l,r,ty,o), vl, proof))
-              res
-          in
-          (* fresh ID and metas and compute orientataion of new_clauses *)
-          assert false
-      | Terms.Equation (l,r,_,Terms.Gt) -> assert false
+      | Terms.Equation (l,r,ty,Terms.Lt) ->
+          fold_build_new_clause bag maxvar id (fun _ -> true)
+            (all_positions [3] 
+              (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
+              r (superposition_right table vl))          
+      | Terms.Equation (l,r,ty,Terms.Gt) ->
+          fold_build_new_clause bag maxvar id (fun _ -> true)
+            (all_positions [2] 
+              (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
+              l (superposition_right table vl))
+      | Terms.Equation (l,r,ty,Terms.Incomparable) -> 
+          fold_build_new_clause bag maxvar id
+            (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)) @         
+             (all_positions [2] 
+               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
+               l (superposition_right table vl)))
       | _ -> assert false
     ;;