From 8863adcc7dc67d3f4f6ba96c2424698cd6b21446 Mon Sep 17 00:00:00 2001
From: denes <??>
Date: Tue, 23 Jun 2009 10:30:55 +0000
Subject: [PATCH] Fixed nasty bug in maxvar updating

---
 .../components/ng_paramodulation/nCicBlob.ml       |  5 +++--
 .../components/ng_paramodulation/paramod.ml        | 11 +++++------
 helm/software/components/ng_paramodulation/pp.ml   | 14 ++++++++------
 .../components/ng_paramodulation/superposition.ml  |  2 +-
 4 files changed, 17 insertions(+), 15 deletions(-)

diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml
index dcc2aba30..208d6d533 100644
--- 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 4968d3290..d01292790 100644
--- 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 2e95e7a95..537ad02c1 100644
--- 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 554028fa7..aef672c14 100644
--- 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 -> 
-- 
2.39.2