Fixed nasty bug in maxvar updating

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index dcc2aba30310678b83bfcf10b3504f9158554213..208d6d533cb39e28c60df3776a3b8178d7a81a65 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicBlob.ml
+++ b/helm/software/components/ng_paramodulation/nCicBlob.ml
@@ -263,8 +263,9 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct
                   l,r,eq_ind
               in
                NCic.LetIn ("clause_" ^ string_of_int id, 
-                 (*close_with_forall vl (extract amount vl lit)*) NCic.Implicit `Type,
-                 close_with_lambdas vl
+                 close_with_forall vl (extract amount vl lit),
+                          (* NCic.Implicit `Type, *)
+                 close_with_lambdas vl 
                    (NCic.Appl [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
                  aux ongoal 
                    ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 4968d3290030c7e1b47441bf79d2b9242006db7f..d0129279065f1ec620d4aa9d824a6fa978f301b0 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -6,7 +6,7 @@ let debug s =
 
 let nparamod rdb metasenv subst context t table =
   let max_nb_iter = 999999999 in
-  let amount_of_time = 10.0 in
+  let amount_of_time = 300.0 in
   let module C = struct
     let metasenv = metasenv
     let subst = subst
@@ -42,12 +42,11 @@ let nparamod rdb metasenv subst context t table =
   in
   let rec given_clause bag maxvar actives      
       passives g_actives g_passives =
-    
-    incr nb_iter; if !nb_iter = max_nb_iter then 
-      (*(prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag);
+    (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag);
       prerr_endline "Active table :"; 
        (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
-         (fst actives));*)
+         (fst actives)); *)
+    incr nb_iter; if !nb_iter = max_nb_iter then       
       raise (Failure "No iterations left !");
     if Unix.gettimeofday () > timeout then
       raise (Failure "Timeout !");
@@ -124,7 +123,7 @@ let nparamod rdb metasenv subst context t table =
        let bag, maxvar, new_goals = 
          List.fold_left 
            (fun (bag,m,acc) g -> 
-              let bag, m, ng = Sup.infer_left bag maxvar g
+              let bag, m, ng = Sup.infer_left bag m g
                 ([current],ctable) in
                 bag,m,ng@acc) 
            (bag,maxvar,[]) g_actives 

diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml
index 2e95e7a95316c0c158e3e36bc9629f883d0a11e5..537ad02c13e849e6044a1d7a4512f55da4b33d2f 100644 (file)
--- a/helm/software/components/ng_paramodulation/pp.ml
+++ b/helm/software/components/ng_paramodulation/pp.ml
@@ -47,12 +47,14 @@ let string_of_direction = function
 ;;
 
 let pp_substitution ~formatter:f subst =
-     (List.iter
-       (fun (i, t) ->
-          (Format.fprintf f "?%d -> " i;
-          pp_foterm f t)
-       )
-       subst)
+  Format.fprintf f "@[<v 2>";
+  List.iter
+    (fun (i, t) ->
+       (Format.fprintf f "?%d -> " i;
+       pp_foterm f t;
+       Format.fprintf f "@;"))
+    subst;
+  Format.fprintf f "@]";
 ;;
 
 let pp_proof bag ~formatter:f p =

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index 554028fa75b857c3c10ccadf73d6d5cf825404a7..aef672c144f5b2ba307626217ce5d122260a8812 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -451,7 +451,7 @@ module Superposition (B : Terms.Blob) =
         superposition_with_table bag maxvar goal atable 
       in
        debug "Superposed goal with active clauses";
-       (* We demodulate the goal with active clauses *)
+       (* We demodulate the new goals with active clauses *)
       let bag, new_goals = 
         List.fold_left
          (fun (bag, acc) g ->