From: denes <??>
Date: Wed, 22 Jul 2009 11:13:45 +0000 (+0000)
Subject: Fixed conflicts due to problem when merging with UEQ implementation
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=39a2078b0e835d39895a5b6c0862d668ece544f3;p=helm.git

Fixed conflicts due to problem when merging with UEQ implementation
---

diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend
index c0099a604..6dc4150c1 100644
--- a/helm/software/components/ng_paramodulation/.depend
+++ b/helm/software/components/ng_paramodulation/.depend
@@ -5,7 +5,7 @@ foUtils.cmi: terms.cmi orderings.cmi
 index.cmi: terms.cmi orderings.cmi 
 foUnif.cmi: terms.cmi orderings.cmi 
 superposition.cmi: terms.cmi orderings.cmi index.cmi 
-stats.cmi: orderings.cmi 
+stats.cmi: terms.cmi orderings.cmi 
 paramod.cmi: terms.cmi orderings.cmi 
 nCicBlob.cmi: terms.cmi 
 cicBlob.cmi: terms.cmi 
@@ -20,8 +20,10 @@ orderings.cmo: terms.cmi pp.cmi orderings.cmi
 orderings.cmx: terms.cmx pp.cmx orderings.cmi 
 foUtils.cmo: terms.cmi orderings.cmi foSubst.cmi foUtils.cmi 
 foUtils.cmx: terms.cmx orderings.cmx foSubst.cmx foUtils.cmi 
-index.cmo: terms.cmi orderings.cmi foUtils.cmi index.cmi 
-index.cmx: terms.cmx orderings.cmx foUtils.cmx index.cmi 
+index.cmo: terms.cmi pp.cmi orderings.cmi foUtils.cmi foUnif.cmi foSubst.cmi \
+    index.cmi 
+index.cmx: terms.cmx pp.cmx orderings.cmx foUtils.cmx foUnif.cmx foSubst.cmx \
+    index.cmi 
 foUnif.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi foUnif.cmi 
 foUnif.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx foUnif.cmi 
 superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \
diff --git a/helm/software/components/ng_paramodulation/Makefile b/helm/software/components/ng_paramodulation/Makefile
index c9c869d82..6196ab1f9 100644
--- a/helm/software/components/ng_paramodulation/Makefile
+++ b/helm/software/components/ng_paramodulation/Makefile
@@ -2,7 +2,7 @@ PACKAGE = ng_paramodulation
 
 INTERFACE_FILES = \
 	terms.mli pp.mli foSubst.mli \
-	orderings.mli foUtils.mli index.mli foUnif.mli superposition.mli \
+	orderings.mli foUtils.mli foUnif.mli index.mli superposition.mli \
 	stats.mli paramod.mli nCicBlob.mli cicBlob.mli nCicProof.mli \
 	nCicParamod.mli
 
diff --git a/helm/software/components/ng_paramodulation/foUnif.ml b/helm/software/components/ng_paramodulation/foUnif.ml
index cb3045c19..61bbdcd8b 100644
--- a/helm/software/components/ng_paramodulation/foUnif.ml
+++ b/helm/software/components/ng_paramodulation/foUnif.ml
@@ -81,6 +81,7 @@ module Founif (B : Orderings.Blob) = struct
     subst
 ;;
 
+(* Sets of variables in s and t are assumed to be disjoint  *)
   let alpha_eq s t =
     let rec equiv subst s t =
       let s = match s with Terms.Var i -> Subst.lookup i subst | _ -> s
diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml
index 8c75baeea..6f36d5939 100644
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -91,8 +91,8 @@ module Utils (B : Orderings.Blob) = struct
           let p = Subst.apply_subst subst p in
           Terms.Predicate p
     in
-    let nlit = List.map apply_subst_on_lit nlit in
-    let plit = List.map apply_subst_on_lit plit in
+    let nlit = List.map (fun (l,s) -> (apply_subst_on_lit l,s)) nlit in
+    let plit = List.map (fun (l,s) -> (apply_subst_on_lit l,s)) plit in
     let proof =
       match proof with
       | Terms.Exact t -> Terms.Exact (Subst.apply_subst subst t)
@@ -109,8 +109,8 @@ module Utils (B : Orderings.Blob) = struct
       match ty with
       | Terms.Node [ Terms.Leaf eq ; ty; l; r ] when B.eq B.eqP eq ->
            let o = Order.compare_terms l r in
-           (vars,Terms.Equation (l, r, ty, o)::literals)
-      | _ -> (vars,Terms.Predicate ty::literals)
+           (vars,(Terms.Equation (l, r, ty, o),false)::literals)
+      | _ -> (vars,(Terms.Predicate ty,false)::literals)
     in
     let varlist = Terms.vars_of_term proofterm in
     let (varlist,nlit) = List.fold_left foterm_to_lit (varlist,[]) nlit in
diff --git a/helm/software/components/ng_paramodulation/index.ml b/helm/software/components/ng_paramodulation/index.ml
index c7a0edcca..633c32854 100644
--- a/helm/software/components/ng_paramodulation/index.ml
+++ b/helm/software/components/ng_paramodulation/index.ml
@@ -16,16 +16,22 @@ module Index(B : Orderings.Blob) = struct
 
   module ClauseOT =
     struct 
-      type t = Terms.direction * B.t Terms.clause
+      type t = Terms.direction * (* direction if it is an equality *)
+	  bool *                 (* true if indexed literal is positive *)
+	  int *                  (* position of literal in clause *)
+	  B.t Terms.clause
  
-      let compare (d1,uc1) (d2,uc2) = 
-        let c = Pervasives.compare d1 d2 in
+      let compare (d1,p1,pos1,uc1) (d2,p2,pos2,uc2) = 
+        let c = Pervasives.compare (d1,p1,pos1) (d2,p2,pos2) in
         if c <> 0 then c else U.compare_clause uc1 uc2
       ;;
     end
 
   module ClauseSet : 
-    Set.S with type elt = Terms.direction * B.t Terms.clause
+    Set.S with type elt = Terms.direction * (* direction if it is an equality *)
+                          bool *       (* true if indexed literal is positive *)
+			  int *        (* position of literal in clause *)
+			  B.t Terms.clause
     = Set.Make(ClauseOT)
 
   open Discrimination_tree
@@ -79,18 +85,26 @@ module Index(B : Orderings.Blob) = struct
       type dataset = ClauseSet.t
     = Make(FotermIndexable)(ClauseSet)
 
-  let index_clause t = function
-    | (_,Terms.Equation (l,_,_,Terms.Gt),_,_) as c -> 
-          DT.index t l (Terms.Left2Right, c)
-    | (_,Terms.Equation (_,r,_,Terms.Lt),_,_) as c -> 
-          DT.index t r (Terms.Right2Left, c)
-    | (_,Terms.Equation (l,r,_,Terms.Incomparable),_,_) as c ->  
-          DT.index  
-           (DT.index t l (Terms.Left2Right, c))
-           r (Terms.Right2Left, c)
-    | (_,Terms.Equation (_,r,_,Terms.Eq),_,_)  -> assert false
-    | (_,Terms.Predicate p,_,_) as c ->
-          DT.index t p (Terms.Nodir, c)
+  let index_literal t c is_pos pos = function
+    | Terms.Equation (l,_,_,Terms.Gt) -> 
+          DT.index t l (Terms.Left2Right,is_pos,pos,c)
+    | Terms.Equation (_,r,_,Terms.Lt) ->
+          DT.index t r (Terms.Right2Left,is_pos,pos,c)
+    | Terms.Equation (l,r,_,Terms.Incomparable) ->
+          DT.index
+           (DT.index t l (Terms.Left2Right,is_pos,pos,c))
+           r (Terms.Right2Left,is_pos,pos,c)
+    | Terms.Equation (_,_,_,Terms.Eq) -> assert false
+    | Terms.Predicate p ->
+          DT.index t p (Terms.Nodir,is_pos,pos,c)
+  ;;
+
+  let index_clause t (_,nlit,plit,_,_ as c) =
+    let index_iter is_pos  (t,pos) (lit,sel) =
+      if sel then index_literal t c is_pos pos lit,pos+1 else t,pos+1
+    in
+    let (res,_) = List.fold_left (index_iter false) (t,0) nlit in
+      fst (List.fold_left (index_iter true) (res,0) plit)
   ;;
 
   type active_set = B.t Terms.clause list * DT.t
diff --git a/helm/software/components/ng_paramodulation/index.mli b/helm/software/components/ng_paramodulation/index.mli
index 51934d1b1..93517597f 100644
--- a/helm/software/components/ng_paramodulation/index.mli
+++ b/helm/software/components/ng_paramodulation/index.mli
@@ -14,7 +14,11 @@
 module Index (B : Orderings.Blob) : 
   sig
     module ClauseSet : Set.S with 
-      type elt = Terms.direction * B.t Terms.clause
+      type elt =
+          Terms.direction * (* direction if it is an equality *)
+	  bool *            (* true if indexed literal is positive *)
+	  int *             (* position of literal in clause *)
+	  B.t Terms.clause
 
     module FotermIndexable : Discrimination_tree.Indexable with 
       type constant_name = B.t and
@@ -27,7 +31,7 @@ module Index (B : Orderings.Blob) :
       type dataset = ClauseSet.t
     
     val index_clause :
-          DT.t -> B.t Terms.clause -> DT.t 
+          DT.t -> B.t Terms.clause -> DT.t
 
     type active_set = B.t Terms.clause list * DT.t
 
diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index be7e140f3..8c740a0e4 100644
--- a/helm/software/components/ng_paramodulation/nCicParamod.ml
+++ b/helm/software/components/ng_paramodulation/nCicParamod.ml
@@ -33,7 +33,7 @@ let nparamod rdb metasenv subst context t table =
     HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t]
   in
   match 
-    P.paramod ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0) 
+    P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0) 
       ~g_passives:goals ~passives (bag,maxvar) 
   with 
   | P.Error _ | P.GaveUp | P.Timeout _ -> []
diff --git a/helm/software/components/ng_paramodulation/orderings.ml b/helm/software/components/ng_paramodulation/orderings.ml
index f2151528f..f8e1d4231 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 
@@ -88,14 +88,15 @@ let compute_literal_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)
 ;;
 
 let compute_clause_weight (_,nl,pl,_,_) =
-  List.fold_left (fun acc lit -> compute_literal_weight lit + acc) 0 (nl@pl)
+  List.fold_left (fun acc (lit,_) -> compute_literal_weight lit + acc) 0 (nl@pl)
 
 let compute_goal_weight = compute_clause_weight;;
   
@@ -181,6 +182,7 @@ let compare_terms o x y =
       | XGT -> Terms.Gt
       | XLT -> Terms.Lt
       | XEQ -> Terms.Eq
+      | XINVERTIBLE -> Terms.Invertible
       | _ -> assert false
 ;;
 
@@ -204,7 +206,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
   ;;
 
@@ -267,6 +271,7 @@ module KBO (B : Terms.Blob) = struct
         let r = aux t1 t2 in
         if r = XEQ then (
           match t1, t2 with
+	  | Terms.Var i, Terms.Var j when i=j -> XEQ
           | Terms.Node (_::tl1), Terms.Node (_::tl2) -> cmp tl1 tl2
           | _, _ ->  XINCOMPARABLE
         ) else r 
diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index f3afc16f4..137cb4586 100644
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -28,7 +28,8 @@ module type Paramod =
     type bag = t Terms.bag * int
     val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
     val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
-    val paramod : 
+    val paramod :
+      useage:bool ->
       max_steps:int ->
       ?timeout:float ->
       bag -> 
@@ -184,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
@@ -341,12 +343,12 @@ module Paramod (B : Orderings.Blob) = struct
       debug
         (Printf.sprintf "Number of passives : %d"
            (passive_set_cardinal passives));
-      given_clause ~noinfer
+      given_clause ~useage ~noinfer
         bag maxvar iterno weight_picks max_steps timeout 
         actives passives g_actives g_passives
   ;;
 
-  let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
+  let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
     let initial_timestamp = Unix.gettimeofday () in
     let passives =
       add_passive_clauses ~no_weight:true passive_empty_set passives
@@ -357,7 +359,7 @@ module Paramod (B : Orderings.Blob) = struct
     let g_actives = [] in
     let actives = [], IDX.DT.empty in
     try 
-     given_clause ~noinfer:false
+     given_clause ~useage ~noinfer:false
       bag maxvar 0  0 max_steps timeout actives passives g_actives g_passives
     with 
     | Sup.Success (bag, _, (i,_,_,_)) ->
diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli
index e133036af..9cffd9d28 100644
--- a/helm/software/components/ng_paramodulation/paramod.mli
+++ b/helm/software/components/ng_paramodulation/paramod.mli
@@ -24,6 +24,7 @@ module type Paramod =
     val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
     val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
     val paramod : 
+      useage:bool ->
       max_steps:int ->
       ?timeout:float ->
       bag -> 
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/stats.ml b/helm/software/components/ng_paramodulation/stats.ml
index 0f9f45d96..fd68f0fe7 100644
--- a/helm/software/components/ng_paramodulation/stats.ml
+++ b/helm/software/components/ng_paramodulation/stats.ml
@@ -83,6 +83,12 @@ module Stats (B : Terms.Blob) =
 			(t,occ,ar,goal_occ_nbr t goal,goal_pos t goal)::acc) res []
     ;;
 
+    let rec leaf_count = function
+      | Terms.Node l -> List.fold_left (fun acc x -> acc + (leaf_count x)) 0 l
+      | Terms.Leaf _ -> 1
+      | _ -> 0
+    ;;
+
     let rec dependencies op clauses acc =
       match clauses with
 	| [] -> acc
@@ -109,10 +115,21 @@ module Stats (B : Terms.Blob) =
 			    else
 			      dependencies op tl acc
 			else dependencies op tl acc
+                    | ((Terms.Node (Terms.Leaf op1::t) as x),y)
+                    | (y,(Terms.Node (Terms.Leaf op1::t) as x)) when leaf_count x > leaf_count y ->
+                         let rec term_leaves = function
+                           | Terms.Node l -> List.fold_left (fun acc x -> acc @ (term_leaves x)) [] l
+                           | Terms.Leaf x -> [x]
+                           | _ -> []
+                         in
+                         if List.mem op (List.filter (fun z -> not (B.eq op1 z)) (term_leaves x)) then 
+                           dependencies op tl (op1::acc)
+                         else
+                           dependencies op tl acc
 		    | _ -> dependencies op tl acc
     ;;
 
-    let dependencies op clauses = dependencies op clauses [];;
+    let dependencies op clauses = HExtlib.list_uniq (List.sort Pervasives.compare (dependencies op clauses []));;
 
     (* let max_weight_hyp = *)
 
diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 54f7e1046..93468738b 100644
--- 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
diff --git a/helm/software/components/ng_paramodulation/terms.ml b/helm/software/components/ng_paramodulation/terms.ml
index db4c8cad6..a7173b1b9 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
@@ -46,8 +46,10 @@ type 'a unit_clause =
 
 type 'a clause =
     int
-    * 'a literal list (* left hand side of the arrow *)
-    * 'a literal list (* right hand side of the arrow *)
+    * ('a literal * bool) list (* left hand side of the arrow,
+				  with flag for selection *)
+    * ('a literal * bool) list (* right hand side of the arrow,
+				  with flag for selection *)
     * varlist
     * 'a proof
 
diff --git a/helm/software/components/ng_paramodulation/terms.mli b/helm/software/components/ng_paramodulation/terms.mli
index dfed661d4..6ef3eeed8 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
 
@@ -52,8 +52,10 @@ type 'a unit_clause =
 
 type 'a clause =
     int
-    * 'a literal list (* left hand side of the arrow *)
-    * 'a literal list (* right hand side of the arrow *)
+    * ('a literal * bool) list (* left hand side of the arrow,
+				  with flag for selection *)
+    * ('a literal * bool) list (* right hand side of the arrow,
+				  with flag for selection *)
     * varlist
     * 'a proof