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 e747d6693bc228227cb8c037801a4538957f9f45..e9726116e2fc44fa2029e71aeee45f3b27e304e7 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -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
@@ -96,8 +92,9 @@ let nparamod rdb metasenv subst context t table =
       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
       let ctable = IDX.index_unit_clause IDX.DT.empty current in
@@ -132,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