Fixed nasty bug in superposition and freshing of clauses

diff --git a/helm/software/components/ng_paramodulation/.depend b/helm/software/components/ng_paramodulation/.depend
index 489a80a1a45f9d4d4a582bf0eb7b122480d700c6..8ffa24a0f8eeaaea45d7c8c05a8bc3238ec0bf6d 100644 (file)
--- a/helm/software/components/ng_paramodulation/.depend
+++ b/helm/software/components/ng_paramodulation/.depend
@@ -3,7 +3,7 @@ foSubst.cmi: terms.cmi
 foUtils.cmi: terms.cmi 
 foUnif.cmi: terms.cmi 
 orderings.cmi: terms.cmi 
-clauses.cmi: orderings.cmi 
+clauses.cmi: terms.cmi orderings.cmi 
 index.cmi: terms.cmi orderings.cmi 
 superposition.cmi: terms.cmi orderings.cmi index.cmi 
 stats.cmi: terms.cmi orderings.cmi 
@@ -21,22 +21,26 @@ foUtils.cmo: terms.cmi foSubst.cmi foUtils.cmi
 foUtils.cmx: terms.cmx foSubst.cmx foUtils.cmi 
 foUnif.cmo: terms.cmi foUtils.cmi foSubst.cmi foUnif.cmi 
 foUnif.cmx: terms.cmx foUtils.cmx foSubst.cmx foUnif.cmi 
-orderings.cmo: terms.cmi pp.cmi foUnif.cmi foSubst.cmi orderings.cmi 
-orderings.cmx: terms.cmx pp.cmx foUnif.cmx foSubst.cmx orderings.cmi 
-clauses.cmo: terms.cmi orderings.cmi foUtils.cmi foSubst.cmi clauses.cmi 
-clauses.cmx: terms.cmx orderings.cmx foUtils.cmx foSubst.cmx clauses.cmi 
-index.cmo: terms.cmi orderings.cmi foUtils.cmi index.cmi 
-index.cmx: terms.cmx orderings.cmx foUtils.cmx index.cmi 
+orderings.cmo: terms.cmi pp.cmi foUtils.cmi foUnif.cmi foSubst.cmi \
+    orderings.cmi 
+orderings.cmx: terms.cmx pp.cmx foUtils.cmx foUnif.cmx foSubst.cmx \
+    orderings.cmi 
+clauses.cmo: terms.cmi orderings.cmi foUtils.cmi foUnif.cmi foSubst.cmi \
+    clauses.cmi 
+clauses.cmx: terms.cmx orderings.cmx foUtils.cmx foUnif.cmx foSubst.cmx \
+    clauses.cmi 
+index.cmo: terms.cmi orderings.cmi foUtils.cmi clauses.cmi index.cmi 
+index.cmx: terms.cmx orderings.cmx foUtils.cmx clauses.cmx index.cmi 
 superposition.cmo: terms.cmi pp.cmi orderings.cmi index.cmi foUtils.cmi \
-    foUnif.cmi foSubst.cmi superposition.cmi 
+    foUnif.cmi foSubst.cmi clauses.cmi superposition.cmi 
 superposition.cmx: terms.cmx pp.cmx orderings.cmx index.cmx foUtils.cmx \
-    foUnif.cmx foSubst.cmx superposition.cmi 
+    foUnif.cmx foSubst.cmx clauses.cmx superposition.cmi 
 stats.cmo: terms.cmi pp.cmi stats.cmi 
 stats.cmx: terms.cmx pp.cmx stats.cmi 
 paramod.cmo: terms.cmi superposition.cmi pp.cmi orderings.cmi index.cmi \
-    foUtils.cmi foUnif.cmi paramod.cmi 
+    foUtils.cmi foUnif.cmi clauses.cmi paramod.cmi 
 paramod.cmx: terms.cmx superposition.cmx pp.cmx orderings.cmx index.cmx \
-    foUtils.cmx foUnif.cmx paramod.cmi 
+    foUtils.cmx foUnif.cmx clauses.cmx paramod.cmi 
 nCicBlob.cmo: terms.cmi foUtils.cmi nCicBlob.cmi 
 nCicBlob.cmx: terms.cmx foUtils.cmx nCicBlob.cmi 
 cicBlob.cmo: terms.cmi cicBlob.cmi 

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 4a688620590f94506e4ae07c7ec47bb5fe281269..8bbf6e1606162c47eca6f15a8490e1ba2f7fa3f3 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -12,7 +12,7 @@
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
 let debug s = prerr_endline (Lazy.force s) ;;
-(* let debug _ = ();; *)
+let debug _ = ();;
 
 let monster = 100;;
     
@@ -66,14 +66,16 @@ module Paramod (B : Orderings.Blob) = struct
 
   let add_passive_clause ?(bonus_weight=0) (passives_w,passives_a) cl =
     let (w,cl) = Clauses.mk_passive_clause cl in
-    let cl = (w+bonus_weight,cl) in
-    WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
+    (* let cl = (w+bonus_weight,cl) in *)
+    let cl = if bonus_weight = 0 then (w,cl) else (0,cl) in
+   WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
   ;;
 
   let add_passive_goal ?(bonus_weight=0) (passives_w,passives_a) g =
     let (w,g) = Clauses.mk_passive_goal g in
-    let g = (w+bonus_weight,g) in
-    WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
+    (* let g = (w+bonus_weight,g) in *)
+    let g = if bonus_weight = 0 then (w,g) else (0,g) in
+   WeightPassiveSet.add g passives_w, AgePassiveSet.add g passives_a
   ;;
 
   let remove_passive_clause (passives_w,passives_a) cl =

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 63507aea6b4aeda4c0eb16f00e52fadf09b2452a..51269d2b3956fdbcd3ec4f9cc0300ff640eea823 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -24,7 +24,7 @@ module Superposition (B : Orderings.Blob) =
     exception Success of B.t Terms.bag * int * B.t Terms.clause
 
     let debug s = prerr_endline (Lazy.force s);;
-    (* let debug _ = ();; *)
+    let debug _ = ();;
     let enable = true;;
 
     let rec list_first f = function
@@ -118,10 +118,10 @@ module Superposition (B : Orderings.Blob) =
         let vl = Clauses.vars_of_clause cl in
         let cl,maxvar = 
             if fresh then Clauses.fresh_clause ~subst maxvar (0, nlit, plit, vl, proof) 
-            else cl,maxvar
+            else (0,nlit,plit,vl,proof),maxvar
         in
         let bag, cl = 
-          Terms.add_to_bag (0, nlit, plit, vl, proof) bag
+          Terms.add_to_bag cl bag
         in
         Some (bag, maxvar, cl, literal)
       else
@@ -287,6 +287,7 @@ module Superposition (B : Orderings.Blob) =
       | _ -> false
 
     let fold_build_new_clause bag maxvar id rule filter res clause_ctx =
+      debug (lazy (string_of_int (List.length res)));
       let (bag, maxvar), res =
        HExtlib.filter_map_acc 
          (fun (bag, maxvar) (t,subst,id2,pos,dir) ->
@@ -334,6 +335,7 @@ module Superposition (B : Orderings.Blob) =
 
     let is_subsumed ~unify bag maxvar (id, nlit, plit, vl, _) table =
       match nlit,plit with
+      |  [Terms.Equation (l,r,ty,_) ,_],[] 
       | [],[Terms.Equation (l,r,ty,_) ,_]-> 
           (match rewrite_eq ~unify l r ty vl table with
             | None -> None
@@ -566,7 +568,6 @@ module Superposition (B : Orderings.Blob) =
         if no_demod then bag, clause else demodulate bag clause table 
       in
       if List.exists (Clauses.are_alpha_eq_cl clause) g_actives then None else
-      (debug (lazy (Pp.pp_clause clause));
       if (is_goal_trivial clause)
       then raise (Success (bag, maxvar, clause))
       else   
@@ -583,7 +584,7 @@ module Superposition (B : Orderings.Blob) =
          | None -> Some (bag,clause)
          | Some (bag,maxvar,cl,subst) -> 
              prerr_endline "Goal subsumed";
-             raise (Success (bag,maxvar,cl)))
+             raise (Success (bag,maxvar,cl))
 (*
       else match is_subsumed ~unify:true bag maxvar clause table with
         | None -> Some (bag, clause)
@@ -603,11 +604,13 @@ module Superposition (B : Orderings.Blob) =
     (* this is OK for both the sup_left and sup_right inference steps *)
     let superposition table varlist is_pos subterm pos context =
       let cands = IDX.DT.retrieve_unifiables table subterm in
-      HExtlib.filter_map
+      let res = HExtlib.filter_map
         (fun (dir, is_cand_pos, _, (id,nlit,plit,vl,_ (*as uc*))) ->
            match nlit,plit with
            | [],[Terms.Equation (l,r,_,o),_] ->
                (let side, newside = if dir=Terms.Left2Right then l,r else r,l in
+               debug (lazy (Pp.pp_foterm subterm));
+               debug (lazy (Pp.pp_foterm side));
                try 
                  let subst = 
                    Unif.unification (* (varlist@vl)*)  [] subterm side 
@@ -620,14 +623,16 @@ module Superposition (B : Orderings.Blob) =
                    if o <> Terms.Lt && o <> Terms.Eq then  
                      Some (context newside, subst, id, pos, dir)
                    else 
-                     ((*prerr_endline ("Filtering: " ^ 
-                        Pp.pp_foterm side ^ " =(< || =)" ^ 
-                        Pp.pp_foterm newside);*)None)
+                     (debug (lazy "Filtering out..."); None)
                  else
                    Some (context newside, subst, id, pos, dir)
                with FoUnif.UnificationFailure _ -> None)
             | _ -> assert false)
         (IDX.ClauseSet.elements cands)
+        in
+        debug (lazy (string_of_int (List.length (IDX.ClauseSet.elements cands)) ^ " candidates"));
+        debug (lazy (string_of_int (List.length res) ^ " results"));
+        res
     ;;
 
     (* Superposes selected equation with equalities in table *)
@@ -765,7 +770,7 @@ module Superposition (B : Orderings.Blob) =
         List.fold_left (superpose_literal id vl atable false)
             (bag,maxvar,[],List.tl nlit,[]) nlit
       in
-        debug (lazy "Superposed goal with active clauses");
+        debug (lazy (string_of_int (List.length new_goals) ^ " new goals"));
         (* We simplify the new goals with active clauses *)
       let bag, new_goals = 
         List.fold_left