Fixed conflicts due to problem when merging with UEQ implementation

[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 54f7e10466a2a3550d7c08fc50cead3246b60ba4..93468738b59242492a79bd15514f6b9a1c43d368 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -81,7 +81,7 @@ module Superposition (B : Orderings.Blob) =
       let rec aux bag pos ctx id = function
       | Terms.Leaf _ as t -> f bag t pos ctx id
       | Terms.Var _ as t -> bag,t,id
-      | Terms.Node l as t->
+      | Terms.Node (hd::l) as t->
           let bag,t,id1 = f bag t pos ctx id in
             if id = id1 then
               let bag, l, _, id = 
@@ -92,10 +92,11 @@ module Superposition (B : Orderings.Blob) =
                      let bag,newt,id = aux bag newpos newctx id t in
                        if post = [] then bag, pre@[newt], [], id
                        else bag, pre @ [newt], List.tl post, id)
-                  (bag, [], List.tl l, id) l
+                  (bag, [hd], List.tl l, id) l
               in
                 bag, Terms.Node l, id
             else bag,t,id1
+      | _ -> assert false
       in
         aux bag pos ctx id t
     ;;
@@ -136,7 +137,7 @@ module Superposition (B : Orderings.Blob) =
          (IDX.DT.retrieve_generalizations table) subterm 
       in
       list_first
-        (fun (dir, (id,lit,vl,_)) ->
+        (fun (dir, is_pos, pos, (id,nlit,plit,vl,_)) ->
            match lit with
            | Terms.Predicate _ -> assert false
            | Terms.Equation (l,r,_,o) ->
@@ -154,7 +155,7 @@ module Superposition (B : Orderings.Blob) =
                    prof_demod_s.HExtlib.profile 
                      (Subst.apply_subst subst) newside 
                  in
-                 if o = Terms.Incomparable then
+                 if o = Terms.Incomparable || o = Terms.Invertible then
                    let o = 
                      prof_demod_o.HExtlib.profile 
                       (Order.compare_terms newside) side in
@@ -629,7 +630,7 @@ module Superposition (B : Orderings.Blob) =
                  let subst = 
                    Unif.unification (* (varlist@vl)*)  [] subterm side 
                  in 
-                 if o = Terms.Incomparable then
+                 if o = Terms.Incomparable || o = Terms.Invertible 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
@@ -656,6 +657,7 @@ module Superposition (B : Orderings.Blob) =
             (all_positions [3] 
               (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
               r (superposition table vl))
+      | Terms.Equation (l,r,ty,Terms.Invertible)
       | Terms.Equation (l,r,ty,Terms.Gt) ->
           fold_build_new_clause bag maxvar id Terms.Superposition
             (fun _ -> true)
@@ -680,8 +682,8 @@ module Superposition (B : Orderings.Blob) =
            fold_build_new_clause bag maxvar id Terms.Superposition
               (filtering Terms.Lt)
               (all_positions [2] 
-                (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; l; x ])
-                r (superposition table vl))
+                (fun x -> Terms.Node [ Terms.Leaf B.eqP; ty; x; r ])
+                l (superposition table vl))
          in
            bag, maxvar, r_terms @ l_terms
       | _ -> assert false