Extended is_identity test

First step towards age selection

diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml
index f56cccd89933b5dde4a4da6b434fb5b9c9312a39..26b7f6fa4b2e1abec80070352d5dbb502d1f99b8 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -140,9 +140,13 @@ module Utils (B : Terms.Blob) = struct
     (Order.compute_unit_clause_weight cl, cl)
   ;;
 
-  let compare_passive_clauses (w1,(id1,_,_,_)) (w2,(id2,_,_,_)) =
+  let compare_passive_clauses_weight (w1,(id1,_,_,_)) (w2,(id2,_,_,_)) =
     if w1 = w2 then id1 - id2
     else w1 - w2
   ;;
 
+  let compare_passive_clauses_age (_,(id1,_,_,_)) (_,(id2,_,_,_)) =
+    id1 - id2
+  ;;
+
 end

diff --git a/helm/software/components/ng_paramodulation/foUtils.mli b/helm/software/components/ng_paramodulation/foUtils.mli
index d0fb30367e6547451383e5bc574d695e480dacab..5cbe461a06ddb3c2baf79ec529f7bea1597a356b 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUtils.mli
+++ b/helm/software/components/ng_paramodulation/foUtils.mli
@@ -46,7 +46,10 @@ module Utils (B : Terms.Blob) :
 
     val empty_bag : B.t Terms.bag
 
-    val compare_passive_clauses :
+    val compare_passive_clauses_weight :
+      B.t Terms.passive_clause -> B.t Terms.passive_clause -> int
+
+    val compare_passive_clauses_age :
       B.t Terms.passive_clause -> B.t Terms.passive_clause -> int
 
   end

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index 208d6d533cb39e28c60df3776a3b8178d7a81a65..e611266d92cfad1c330a13c98b7834d084e95f94 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -198,9 +198,8 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
           let lit,vl,proof = get_literal id in
           if not ongoal && id = mp then
             ((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
-            assert (vl = []);  
              NCic.LetIn ("clause_" ^ string_of_int id, 
-                extract amount vl lit, 
+                extract amount [] lit, 
                 (NCic.Appl [eq_refl;NCic.Implicit `Type;NCic.Implicit `Term]),
                 aux true ((id,([],lit))::seen) (id::tl)))
           else

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index e9726116e2fc44fa2029e71aeee45f3b27e304e7..1c91ee54ecdc8141b7fe2c0a037572b565b7d3e9 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -1,7 +1,5 @@
-(* LOOPING : COL057-1.ma *)
-
 let debug s =
-   () (* prerr_endline s *)
+   prerr_endline s
 ;;
 
 let nparamod rdb metasenv subst context t table =
@@ -21,36 +19,76 @@ let nparamod rdb metasenv subst context t table =
   let module Sup = Superposition.Superposition(B) in
   let module Utils = FoUtils.Utils(B) in
     
-  let module OrderedPassives =
+  let module WeightOrderedPassives =
+      struct
+       type t = B.t Terms.passive_clause
+           
+       let compare = Utils.compare_passive_clauses_weight
+      end
+  in
+  let module AgeOrderedPassives =
       struct
        type t = B.t Terms.passive_clause
            
-       let compare = Utils.compare_passive_clauses
+       let compare = Utils.compare_passive_clauses_age
       end
   in
-  let module PassiveSet = Set.Make(OrderedPassives)
+  let module WeightPassiveSet = Set.Make(WeightOrderedPassives) in
+  let module AgePassiveSet = Set.Make(AgeOrderedPassives) in
+  let add_passive_clause (passives_w,passives_a) cl =
+    let cl = Utils.mk_passive_clause cl in
+    WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
   in
-  let add_passive_clause passives cl =
-    PassiveSet.add (Utils.mk_passive_clause cl) passives
+  let remove_passive_clause (passives_w,passives_a) cl =
+    let passives_w = WeightPassiveSet.remove cl passives_w in
+    let passives_a = AgePassiveSet.remove cl passives_a in
+      passives_w,passives_a
+  in
+  let add_passive_clauses (passives_w,passives_a) new_clauses =
+    let new_clauses_w,new_clauses_a = List.fold_left add_passive_clause
+      (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
+    in
+      (WeightPassiveSet.union new_clauses_w passives_w,
+       AgePassiveSet.union new_clauses_a passives_a)
+  in
+  let is_passive_set_empty (passives_w,passives_a) =
+    if (WeightPassiveSet.is_empty passives_w) then begin
+      assert (AgePassiveSet.is_empty passives_a); true
+    end else begin
+      assert (not (AgePassiveSet.is_empty passives_a)); false
+    end
+  in
+  let passive_set_cardinal (passives_w,_) =
+    WeightPassiveSet.cardinal passives_w
+  in
+  let passive_singleton cl =
+    (WeightPassiveSet.singleton cl,AgePassiveSet.singleton cl)
+  in
+  let passive_empty_set =
+    (WeightPassiveSet.empty,AgePassiveSet.empty)
+  in
+  let pick_min_passive use_age (passives_w,passives_a) =
+    if use_age then AgePassiveSet.min_elt passives_a
+    else WeightPassiveSet.min_elt passives_w
   in
   let timeout = Unix.gettimeofday () +. amount_of_time in 
 
-    (* TODO : fairness condition *)
+    (* TODO : global age over facts and goals (without comparing weights) *)
   let select passives g_passives =
-    if PassiveSet.is_empty passives then begin
-      assert (not (PassiveSet.is_empty g_passives));
-      let g_cl = PassiveSet.min_elt g_passives in
-       (true,snd g_cl,passives,PassiveSet.remove g_cl g_passives)
+    if is_passive_set_empty passives then begin
+      assert (not (is_passive_set_empty g_passives));
+      let g_cl = pick_min_passive false g_passives in
+       (true,snd g_cl,passives,remove_passive_clause g_passives g_cl)
     end
-    else let cl = PassiveSet.min_elt passives in
-      if PassiveSet.is_empty g_passives then
-       (false,snd cl,PassiveSet.remove cl passives,g_passives)
+    else let cl = pick_min_passive false passives in
+      if is_passive_set_empty g_passives then
+       (false,snd cl,remove_passive_clause passives cl,g_passives)
       else
-       let g_cl = PassiveSet.min_elt g_passives in
+       let g_cl = pick_min_passive false g_passives in
          if (fst cl <= fst g_cl) then
-           (false,snd cl,PassiveSet.remove cl passives,g_passives)
+           (false,snd cl,remove_passive_clause passives cl,g_passives)
          else
-           (true,snd g_cl,passives,PassiveSet.remove g_cl g_passives)
+           (true,snd g_cl,passives,remove_passive_clause g_passives g_cl)
   in
 
   let backward_infer_step bag maxvar actives passives
@@ -61,11 +99,8 @@ let nparamod rdb metasenv subst context t table =
         Sup.infer_left bag maxvar g_current actives 
       in
        debug "Performed infer_left step";
-       let new_goals = List.fold_left add_passive_clause
-         PassiveSet.empty new_goals
-       in
-          bag, maxvar, actives, passives, g_current::g_actives,
-    (PassiveSet.union new_goals g_passives)
+        bag, maxvar, actives, passives, g_current::g_actives,
+    (add_passive_clauses g_passives new_goals)
   in
 
   let forward_infer_step bag maxvar actives passives g_actives
@@ -106,13 +141,9 @@ let nparamod rdb metasenv subst context t table =
               bag,m,ng@acc) 
          (bag,maxvar,[]) g_actives 
       in
-      let new_clauses = List.fold_left add_passive_clause
-       PassiveSet.empty new_clauses in
-      let new_goals = List.fold_left add_passive_clause
-       PassiveSet.empty new_goals in
        bag, maxvar, actives,
-    PassiveSet.union new_clauses passives, g_actives,
-    PassiveSet.union new_goals g_passives
+    add_passive_clauses passives new_clauses, g_actives,
+    add_passive_clauses g_passives new_goals
   in
 
   let rec given_clause bag maxvar actives passives g_actives g_passives =
@@ -152,12 +183,12 @@ let nparamod rdb metasenv subst context t table =
           (List.length g_actives));
       debug
        (Printf.sprintf "Number of passive goals : %d"
-          (PassiveSet.cardinal g_passives));
+          (passive_set_cardinal g_passives));
       debug
        (Printf.sprintf "Number of actives : %d" (List.length (fst actives)));
       debug
        (Printf.sprintf "Number of passives : %d"
-          (PassiveSet.cardinal passives));
+          (passive_set_cardinal passives));
       given_clause bag maxvar actives passives g_actives g_passives
   in
 
@@ -169,13 +200,15 @@ let nparamod rdb metasenv subst context t table =
   in
   let bag, maxvar, goal = mk_clause Terms.M.empty 0 t in
   let g_actives = [] in
-  let g_passives = PassiveSet.singleton (Utils.mk_passive_clause goal) in
+  let g_passives =
+    passive_singleton (Utils.mk_passive_clause goal)
+  in
   let passives, bag, maxvar = 
     List.fold_left
       (fun (cl, bag, maxvar) t -> 
          let bag, maxvar, c = mk_clause bag maxvar t in
          (add_passive_clause cl c), bag, maxvar)
-      (PassiveSet.empty, bag, maxvar) table 
+      (passive_empty_set, bag, maxvar) table 
   in
   let actives = [], IDX.DT.empty in
   try given_clause bag maxvar actives passives g_actives g_passives

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index ffca04b96c7ff7b2c84f2cdde3953ed97b787df2..891c8dcacafaec6553e6884983448838fab7da1e 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -180,8 +180,10 @@ module Superposition (B : Terms.Blob) =
     (* move away *)
     let is_identity_clause = function
       | _, Terms.Equation (_,_,_,Terms.Eq), _, _ -> true
-      | _, Terms.Predicate _, _, _ -> assert false
-      | _ -> false
+      | _, Terms.Equation (l,r,_,_), vl, proof ->
+         (try ignore(Unif.unification vl [] l r); true
+         with FoUnif.UnificationFailure _ -> false)
+      | _, Terms.Predicate _, _, _ -> assert false       
     ;;
 
     let build_new_clause bag maxvar filter rule t subst vl id id2 pos dir =