Added optionnal one pass simplification (instead of keep_simplified)

[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 36adca45413def9a1fa5214571a84c92edcbfbca..8903ec02fc1c24082fe54d53ddbb32006ec761c4 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -1,9 +1,9 @@
-let debug s = ()
-(*  prerr_endline s *)
+let debug s =
+  () (* prerr_endline s *)
 ;;
 
 let nparamod rdb metasenv subst context t table =
-  let nb_iter = ref 100 in
+  let nb_iter = ref 200 in
   prerr_endline "========================================";
   let module C = struct
     let metasenv = metasenv
@@ -39,19 +39,16 @@ let nparamod rdb metasenv subst context t table =
   let rec given_clause bag maxvar actives      
       passives g_actives g_passives =
     
-    decr nb_iter; if !nb_iter = 0 then raise (Failure "Timeout !");
+    decr nb_iter; if !nb_iter = 0 then 
+      (*(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));*)
+    raise (Failure "Timeout !");
+
 
-    (* keep goals demodulated w.r.t. actives and check if solved *)
-    (* we may move this at the end of infer_right *) 
-    let bag, g_actives = 
-      List.fold_left 
-        (fun (bag,acc) c -> 
-           let bag, c = Sup.simplify_goal maxvar (snd actives) bag c in
-             bag, c::acc) 
-        (bag,[]) g_actives 
-    in
       
-      (* superposition left, simplifications on goals *)
+    (* superposition left, simplifications on goals *)
       debug "infer_left step...";
       let bag, maxvar, g_actives, g_passives =
        match select g_passives with
@@ -95,16 +92,26 @@ let nparamod rdb metasenv subst context t table =
          | Some (current, passives) -> 
              debug ("Selected fact : " ^ Pp.pp_unit_clause current);
               match Sup.keep_simplified current actives bag with
+             (* match Sup.one_pass_simplification current actives bag with *)
                | None -> aux_simplify passives
-               | Some x -> x
+               | Some x -> x,passives
       in
-      let (current, bag, actives) = aux_simplify passives
+      let (current, bag, actives),passives = aux_simplify passives
       in                   
        debug ("Fact after simplification :"
               ^ Pp.pp_unit_clause current);
        let bag, maxvar, actives, new_clauses = 
           Sup.infer_right bag maxvar current actives 
        in
+  debug "Demodulating goals with actives...";
+         (* keep goals demodulated w.r.t. actives and check if solved *)
+       let bag, g_actives = 
+         List.fold_left 
+            (fun (bag,acc) c -> 
+               let bag, c = Sup.simplify_goal maxvar (snd actives) bag c in
+                bag, c::acc) 
+            (bag,[]) g_actives 
+       in
        let ctable = IDX.index_unit_clause IDX.DT.empty current in
        let bag, maxvar, new_goals = 
          List.fold_left