added (but not active) last chance idea

[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..8070b4b5db69a2334ccc1e536009ae38895136ea 100644 (file)
--- a/helm/software/components/ng_paramodulation/superposition.ml
+++ b/helm/software/components/ng_paramodulation/superposition.ml
@@ -22,7 +22,7 @@ module Superposition (B : Terms.Blob) =
     
     exception Success of B.t Terms.bag * int * B.t Terms.unit_clause
 
-(*    let debug s = prerr_endline s;;*)
+    let debug s = prerr_endline s;;
     let debug _ = ();;
 
     let rec list_first f = function
@@ -313,18 +313,19 @@ 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 orphan_murder bag actives cl =
       let (id,_,_,_) = cl in
-      let (res,_) = orphan_murder bag [] id in
+      let actives = List.map (fun (i,_,_,_) -> i) actives in
+      let (res,_) = orphan_murder bag actives id in
        if res then debug "Orphan murdered"; res
-;;
+    ;;
 
     (* demodulate and check for subsumption *)
     let simplify table maxvar bag clause = 
       if is_identity_clause ~unify:false clause then bag,None
-      (* else if orphan_murder bag clause then bag,None *)
+      (* else if orphan_murder bag actives clause then bag,None *)
       else let bag, clause = demodulate bag clause table in
       if is_identity_clause ~unify:false clause then bag,None
       else
@@ -338,7 +339,11 @@ 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 (id,_,_,_) = clause in
+           if orphan_murder bag clause then
+             Terms.M.add id (clause,true) bag, Some clause
+           else bag, Some clause*)
+    ;;
 
     let one_pass_simplification new_clause (alist,atable) bag maxvar =
       match simplify atable maxvar bag new_clause with
@@ -366,7 +371,8 @@ module Superposition (B : Terms.Blob) =
        (* Simplification of new_clause with :      *
         * - actives and cl if new_clause is not cl *
         * - only actives otherwise                 *)
-       match simplify atable1 maxvar bag new_clause with
+       match
+         simplify atable1 maxvar bag new_clause with
          | bag,None -> bag,(Some cl, None) (* new_clause has been discarded *)
          | bag,Some clause ->
              (* Simplification of each active clause with clause *
@@ -439,11 +445,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 +461,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 +598,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