Implemented check for duplicates (in goals)

[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 fc44be0486e990d399f1dd48a9e382fb0b0dea93..e9726116e2fc44fa2029e71aeee45f3b27e304e7 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -1,7 +1,7 @@
 (* LOOPING : COL057-1.ma *)
 
 let debug s =
-   prerr_endline s
+   () (* prerr_endline s *)
 ;;
 
 let nparamod rdb metasenv subst context t table =
@@ -53,14 +53,10 @@ let nparamod rdb metasenv subst context t table =
            (true,snd g_cl,passives,PassiveSet.remove g_cl g_passives)
   in
 
-  let backward_infer_step bag maxvar actives passives g_actives g_passives g_current =
+  let backward_infer_step bag maxvar actives passives
+                          g_actives g_passives g_current =
     (* superposition left, simplifications on goals *)
       debug "infer_left step...";
-    debug ("Selected goal : " ^ Pp.pp_unit_clause g_current);
-    let bag, g_current = 
-      Sup.simplify_goal maxvar (snd actives) bag g_current
-    in
-      debug "Simplified goal";
       let bag, maxvar, new_goals = 
         Sup.infer_left bag maxvar g_current actives 
       in
@@ -92,18 +88,15 @@ let nparamod rdb metasenv subst context t table =
       Sup.infer_right bag maxvar current actives 
     in
       debug "Demodulating goals with actives...";
-      debug ("Current : " ^ (Pp.pp_unit_clause current));
-      debug ("Active goal : " ^ (Pp.pp_unit_clause (List.hd g_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) 
+            match Sup.simplify_goal maxvar (snd actives) bag acc c with
+              | None -> bag, acc
+              | Some (bag,c) -> bag,c::acc)
           (bag,[]) g_actives 
       in
-      debug (Pp.pp_unit_clause current);
-      debug (Pp.pp_unit_clause (List.hd g_actives));
       let ctable = IDX.index_unit_clause IDX.DT.empty current in
       let bag, maxvar, new_goals = 
        List.fold_left 
@@ -117,8 +110,6 @@ let nparamod rdb metasenv subst context t table =
        PassiveSet.empty new_clauses in
       let new_goals = List.fold_left add_passive_clause
        PassiveSet.empty new_goals in
-       debug (string_of_int (PassiveSet.cardinal new_goals));
-       debug (string_of_int (PassiveSet.cardinal g_passives));
        bag, maxvar, actives,
     PassiveSet.union new_clauses passives, g_actives,
     PassiveSet.union new_goals g_passives
@@ -138,8 +129,11 @@ let nparamod rdb metasenv subst context t table =
     let rec aux_select passives g_passives =
       let backward,current,passives,g_passives = select passives g_passives in
        if backward then
-         backward_infer_step bag maxvar actives passives
-                             g_actives g_passives current
+        match Sup.simplify_goal maxvar (snd actives) bag g_actives current with
+           | None -> aux_select passives g_passives
+           | Some x -> let bag,g_current = x in
+               backward_infer_step bag maxvar actives passives
+                 g_actives g_passives g_current
        else
          (* debug ("Selected fact : " ^ Pp.pp_unit_clause current); *)
           match Sup.keep_simplified current actives bag maxvar with
@@ -153,7 +147,6 @@ let nparamod rdb metasenv subst context t table =
     let bag,maxvar,actives,passives,g_actives,g_passives =      
       aux_select passives g_passives
     in
-      assert (PassiveSet.cardinal g_passives < 2);
       debug
        (Printf.sprintf "Number of active goals : %d"
           (List.length g_actives));
@@ -221,7 +214,7 @@ let nparamod rdb metasenv subst context t table =
               let metasenv,i,_,_=NCicMetaSubst.mk_meta metasenv context `Term in
               metasenv, NCic.Meta (i,(k,NCic.Irl (List.length context)))
           | t -> NCicUntrusted.map_term_fold_a 
-                  (fun _ k -> k+1) k aux metasenv t                 
+                  (fun _ k -> k+1) k aux metasenv t
         in
          aux 0 metasenv proofterm
       in
@@ -231,6 +224,8 @@ let nparamod rdb metasenv subst context t table =
           metasenv subst context proofterm None
       in
       proofterm, metasenv, subst
-  | Failure _ -> prerr_endline
+  | Failure s -> 
+      prerr_endline s;
+      prerr_endline
       (Printf.sprintf "FAILURE in %d iterations" !nb_iter); assert false
 ;;