X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=e9726116e2fc44fa2029e71aeee45f3b27e304e7;hb=eca915d2656084f1e58149a476a2d305758b00f9;hp=e747d6693bc228227cb8c037801a4538957f9f45;hpb=158c113b8713291b4162f4c76d587bc42cdb25b7;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index e747d6693..e9726116e 100644
--- 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