Various fixes

[helm.git] / helm / software / components / ng_paramodulation / paramod.ml

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index 105f5c86b11ad6ecb0a2f46d8d5f8b11f795684f..47975fb3b7b7aca845e1121d6ef1444f08f70f71 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -11,7 +11,7 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
-(* let debug s = prerr_endline s ;;*)
+ (*let debug s = prerr_endline s ;;*)
  let debug _ = ();;
     
 let max_nb_iter = 999999999 ;;
@@ -174,7 +174,7 @@ module Paramod (B : Terms.Blob) = struct
 
     let rec aux_select passives g_passives =
       let backward,current,passives,g_passives =
-       select ~use_age passives g_passives
+       select ~use_age:false passives g_passives
       in
        if backward then
         match Sup.simplify_goal maxvar (snd actives) bag g_actives current with
@@ -224,10 +224,10 @@ module Paramod (B : Terms.Blob) = struct
         let l =
           let rec traverse ongoal (accg,acce) i =
             match Terms.M.find i bag with
-              | (id,_,_,Terms.Exact _) ->
+              | (id,_,_,Terms.Exact _),_ ->
                if ongoal then [i],acce else
                  if (List.mem i acce) then accg,acce else accg,acce@[i]
-              | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) ->
+              | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),_ ->
                if (not ongoal) && (List.mem i acce) then accg,acce
                else
                     let accg,acce = 
@@ -241,9 +241,9 @@ module Paramod (B : Terms.Blob) = struct
         prerr_endline 
           (Printf.sprintf "Found proof, %fs" 
             (Unix.gettimeofday() -. timeout +. amount_of_time));
-        prerr_endline "Proof:"; 
+        (* prerr_endline "Proof:"; 
         List.iter (fun x -> prerr_endline (string_of_int x);
-                prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;
+                prerr_endline (Pp.pp_unit_clause (fst (Terms.M.find x bag)))) l;*)
         [ bag, i, l ]
     | Failure (msg,_bag,_maxvar,nb_iter) -> 
         prerr_endline msg;