Implemented handling of Invertible equalities

[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 27361859bffbfb6e5f2e7d192d1c84d0ce1082b4..6037354794d61963bce35c0c22c586a894bb4f17 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -155,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
@@ -630,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
@@ -657,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)
@@ -681,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