From: denes <??>
Date: Tue, 21 Jul 2009 15:38:17 +0000 (+0000)
Subject: Implemented handling of Invertible equalities
X-Git-Tag: make_still_working~3643
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=5642a453e8b4bbe228d126aa0c44d31e101969ec;p=helm.git

Implemented handling of Invertible equalities
Fixed nasty bug in inferences for Incomparable equalities
---

diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index 3179f0000..4db4584a4 100644
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -80,12 +80,6 @@ module Index(B : Orderings.Blob) = struct
       type data = ClauseSet.elt and 
       type dataset = ClauseSet.t
     = Make(FotermIndexable)(ClauseSet)
-
-  let are_invertible maxvar varlist l r =
-    let _,_,subst = U.relocate maxvar varlist FoSubst.id_subst in
-    let l = FoSubst.apply_subst subst l in
-      try (ignore(Unif.alpha_eq l r);true) with
-	  FoUnif.UnificationFailure _ -> false
   
   let index_unit_clause maxvar t = function
     | (_,Terms.Equation (l,_,_,Terms.Gt),_,_) as c -> 
@@ -101,6 +95,8 @@ module Index(B : Orderings.Blob) = struct
           DT.index  
            (DT.index t l (Terms.Left2Right, c))
            r (Terms.Right2Left, c)
+    | (_,Terms.Equation (l,r,_,Terms.Invertible),vl,_) as c ->
+	DT.index t l (Terms.Left2Right, c)
     | (_,Terms.Equation (_,r,_,Terms.Eq),_,_)  -> assert false
     | (_,Terms.Predicate p,_,_) as c ->
           DT.index t p (Terms.Nodir, c)
diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index 4ca5a62d3..4c6e0a977 100644
--- a/helm/software/components/ng_paramodulation/orderings.ml
+++ b/helm/software/components/ng_paramodulation/orderings.ml
@@ -11,7 +11,7 @@
 
 (* $Id$ *)
 
-type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE
+type aux_comparison = XEQ | XLE | XGE | XLT | XGT | XINCOMPARABLE | XINVERTIBLE
 
 module type Blob =
   sig 
@@ -90,7 +90,8 @@ let compute_unit_clause_weight (_,l, _, _) =
         let w, m = weight_of_term x in 
         weight_of_polynomial w m
     | Terms.Equation (l,r,_,Terms.Eq) 
-    | Terms.Equation (l,r,_,Terms.Incomparable) ->
+    | Terms.Equation (l,r,_,Terms.Incomparable) 
+    | Terms.Equation (l,r,_,Terms.Invertible) ->
         let wl, ml = weight_of_term l in 
         let wr, mr = weight_of_term r in 
         weight_of_polynomial (wl+wr) (ml@mr)
@@ -198,6 +199,7 @@ let compare_terms o x y =
       | XGT -> Terms.Gt
       | XLT -> Terms.Lt
       | XEQ -> Terms.Eq
+      | XINVERTIBLE -> Terms.Invertible
       | _ -> assert false
 ;;
 
@@ -209,6 +211,51 @@ module NRKBO (B : Terms.Blob) = struct
 
   let eq_foterm = eq_foterm B.eq;;
 
+exception UnificationFailure of string Lazy.t;;
+
+
+(* DUPLICATE CODE FOR TESTS (see FoUnif)  *)
+  let alpha_eq s t =
+    let rec equiv subst s t =
+      let s = match s with Terms.Var i -> FoSubst.lookup i subst | _ -> s
+      and t = match t with Terms.Var i -> FoSubst.lookup i subst | _ -> t
+        
+      in
+      match s, t with
+        | s, t when eq_foterm s t -> subst
+        | Terms.Var i, Terms.Var j
+            when (not (List.exists (fun (_,k) -> k=t) subst)) ->
+            let subst = FoSubst.build_subst i t subst in
+              subst
+        | Terms.Node l1, Terms.Node l2 -> (
+            try
+              List.fold_left2
+                (fun subst' s t -> equiv subst' s t)
+                subst l1 l2
+            with Invalid_argument _ ->
+              raise (UnificationFailure (lazy "Inference.unification.unif"))
+          )
+        | _, _ ->
+            raise (UnificationFailure (lazy "Inference.unification.unif"))
+    in
+      equiv FoSubst.id_subst s t
+;;
+
+let relocate maxvar varlist subst =
+    List.fold_right
+      (fun i (maxvar, varlist, s) -> 
+         maxvar+1, maxvar::varlist, FoSubst.build_subst i (Terms.Var maxvar) s)
+      varlist (maxvar+1, [], subst)
+  ;;
+
+  let are_invertible l r =
+    let varlist = Terms.vars_of_term l in
+    let maxvar = List.fold_left max 0 varlist in
+    let _,_,subst = relocate maxvar varlist FoSubst.id_subst in
+    let l = FoSubst.apply_subst subst l in
+      try (ignore(alpha_eq l r);true) with
+	  UnificationFailure _ -> false
+
   let compute_unit_clause_weight = compute_unit_clause_weight;;
   let compute_goal_weight = compute_goal_weight;;
   
@@ -221,7 +268,9 @@ module NRKBO (B : Terms.Blob) = struct
         if aux_ordering B.compare t1 t2 = XLT then XLT else XINCOMPARABLE
     | XGE -> 
         if aux_ordering B.compare t1 t2 = XGT then XGT else XINCOMPARABLE
-    | XEQ -> aux_ordering B.compare t1 t2
+    | XEQ -> let res = aux_ordering B.compare t1 t2 in
+	if res = XINCOMPARABLE && are_invertible t1 t2 then XINVERTIBLE
+	else res
     | res -> res
   ;;
 
diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index ac73df2d0..520d52396 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -185,6 +185,7 @@ module Paramod (B : Orderings.Blob) = struct
      * new'= demod A'' new    *
      * P' = P + new'          *)
     debug "Forward infer step...";
+    debug ("Number of actives : " ^ (string_of_int (List.length (fst actives))));
     let bag, maxvar, actives, new_clauses = 
       Sup.infer_right bag maxvar current actives 
     in
@@ -209,6 +210,7 @@ module Paramod (B : Orderings.Blob) = struct
           (bag,maxvar,[]) g_actives 
       in
       let bag = Terms.replace_in_bag (current,false,iterno) bag in
+	(* prerr_endline (Pp.pp_bag bag); *)
     bag, maxvar, actives,
     add_passive_clauses passives new_clauses, g_actives,
     add_passive_goals g_passives new_goals
diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml
index 625de5c31..ddf5726c4 100644
--- a/helm/software/components/ng_paramodulation/pp.ml
+++ b/helm/software/components/ng_paramodulation/pp.ml
@@ -85,6 +85,7 @@ let string_of_comparison = function
   | Terms.Gt -> "=>="
   | Terms.Eq -> "==="
   | Terms.Incomparable -> "=?="
+  | Terms.Invertible -> "=<->="
 
 let pp_unit_clause ~formatter:f c =
   let (id, l, vars, proof) = c in
diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 27361859b..603735479 100644
--- 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
diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml
index 9a225fd27..3947107ea 100644
--- a/helm/software/components/ng_paramodulation/terms.ml
+++ b/helm/software/components/ng_paramodulation/terms.ml
@@ -18,7 +18,7 @@ type 'a foterm =
 
 type 'a substitution = (int * 'a foterm) list
 
-type comparison = Lt | Eq | Gt | Incomparable
+type comparison = Lt | Eq | Gt | Incomparable | Invertible
 
 type rule = Superposition | Demodulation
 type direction = Left2Right | Right2Left | Nodir
diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli
index 47295035c..0146dba2c 100644
--- a/helm/software/components/ng_paramodulation/terms.mli
+++ b/helm/software/components/ng_paramodulation/terms.mli
@@ -18,7 +18,7 @@ type 'a foterm =
 
 type 'a substitution = (int * 'a foterm) list
 
-type comparison = Lt | Eq | Gt | Incomparable
+type comparison = Lt | Eq | Gt | Incomparable | Invertible
 
 type rule = Superposition | Demodulation