attempt to run a last chance procedure after the timeout

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

diff --git a/helm/software/components/ng_paramodulation/superposition.ml b/helm/software/components/ng_paramodulation/superposition.ml
index c1c0612b1e39d39c7b166357670a3fc9c180b01d..9ccd934e1a8213dd2ab0f15bae92e091b48a3d68 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -313,13 +313,13 @@ module Superposition (B : Terms.Blob) =
              | (false,acc) ->
                  let (res,acc) = orphan_murder bag acc i2 in
                  if res then res,acc else res,i::acc
-;;
+    ;;
 
     let orphan_murder bag cl =
       let (id,_,_,_) = cl in
       let (res,_) = orphan_murder bag [] id in
        if res then debug "Orphan murdered"; res
-;;
+    ;;
 
     (* demodulate and check for subsumption *)
     let simplify table maxvar bag clause = 
@@ -338,7 +338,7 @@ module Superposition (B : Terms.Blob) =
        | bag, None -> let (id,_,_,_) = clause in
            Terms.M.add id (clause,true) bag, None
        | bag, Some clause -> bag, Some clause
-;;
+    ;;
 
     let one_pass_simplification new_clause (alist,atable) bag maxvar =
       match simplify atable maxvar bag new_clause with
@@ -439,11 +439,13 @@ module Superposition (B : Terms.Blob) =
 ;;
 
     (* this is like simplify but raises Success *)
-    let simplify_goal maxvar table bag g_actives clause = 
-      let bag, clause = demodulate bag clause table in
+    let simplify_goal ~no_demod maxvar table bag g_actives clause = 
+      let bag, clause = 
+       if no_demod then bag, clause else demodulate bag clause table 
+      in
+      if List.exists (are_alpha_eq clause) g_actives then None else
       if (is_identity_clause ~unify:true clause)
       then raise (Success (bag, maxvar, clause))
-
       else   
        let (id,lit,vl,_) = clause in 
        let l,r,ty = 
@@ -453,20 +455,17 @@ module Superposition (B : Terms.Blob) =
        in
        match deep_eq ~unify:true l r ty [] (fun x -> x) (fun x -> x) 
          table (Some(bag,maxvar,clause,Subst.id_subst)) with
-       | None -> 
-           if List.exists (are_alpha_eq clause) g_actives then None
-           else Some (bag, clause)
+       | None -> Some (bag,clause)
        | Some (bag,maxvar,cl,subst) -> 
            prerr_endline "Goal subsumed";
            raise (Success (bag,maxvar,cl))
-           (*
+(*
       else match is_subsumed ~unify:true bag maxvar clause table with
-       | None -> 
-           if List.exists (are_alpha_eq clause) g_actives then None
-           else Some (bag, clause)
+       | None -> Some (bag, clause)
        | Some ((bag,maxvar),c) -> 
            prerr_endline "Goal subsumed";
-           raise (Success (bag,maxvar,c))*) 
+           raise (Success (bag,maxvar,c))
+*) 
     ;;
 
     (* =================== inference ===================== *)
@@ -593,7 +592,7 @@ module Superposition (B : Terms.Blob) =
       let bag, new_goals = 
         List.fold_left
          (fun (bag, acc) g -> 
-           match simplify_goal maxvar atable bag [] g with
+           match simplify_goal ~no_demod:false maxvar atable bag [] g with
              | None -> assert false
              | Some (bag,g) -> bag,g::acc)
          (bag, []) new_goals