]> matita.cs.unibo.it Git - helm.git/commitdiff
Implemented orphan murder test (clauses are not discarded for now)
authordenes <??>
Fri, 26 Jun 2009 09:46:23 +0000 (09:46 +0000)
committerdenes <??>
Fri, 26 Jun 2009 09:46:23 +0000 (09:46 +0000)
Re-enabled zero weight trick

helm/software/components/ng_paramodulation/paramod.ml
helm/software/components/ng_paramodulation/superposition.ml
helm/software/components/ng_paramodulation/superposition.mli

index d85c5627a4e4b4e97d1a9e667253dac41cd7aecb..51bd67286f0dc498886df771a0ae18cd2f91a8a8 100644 (file)
@@ -11,7 +11,7 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
-let debug s = prerr_endline s ;;
+(* let debug s = prerr_endline s ;;*)
 let debug _ = ();;
     
 module Paramod (B : Terms.Blob) = struct
@@ -49,8 +49,10 @@ module Paramod (B : Terms.Blob) = struct
       passives_w,passives_a
   ;;
 
-  let add_passive_clauses (passives_w,passives_a) new_clauses =
-    let new_clauses_w,new_clauses_a = List.fold_left add_passive_clause
+  let add_passive_clauses ?(no_weight=false)
+      (passives_w,passives_a) new_clauses =
+    let new_clauses_w,new_clauses_a =
+      List.fold_left (add_passive_clause ~no_weight)
       (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
     in
       (WeightPassiveSet.union new_clauses_w passives_w,
@@ -172,22 +174,22 @@ module Paramod (B : Terms.Blob) = struct
 
     let use_age = iterno mod 10 = 0 in
 
-    let rec aux_select passives g_passives =
+    let rec aux_select bag passives g_passives =
       let backward,current,passives,g_passives =
        select ~use_age:false passives g_passives
       in
        if backward then
         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
+           | None -> aux_select bag passives g_passives
+           | Some (bag,g_current) ->
                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
        (*  match Sup.one_pass_simplification current actives bag maxvar with*)
-             | None -> aux_select passives g_passives
-             | Some x -> let (current, bag, actives) = x in
+             | bag,None -> aux_select bag passives g_passives
+             | bag,Some (current,actives) ->
                  forward_infer_step bag maxvar actives passives
                                     g_actives g_passives current
     in
@@ -198,7 +200,7 @@ module Paramod (B : Terms.Blob) = struct
          (fst actives)); *)
 
     let bag,maxvar,actives,passives,g_actives,g_passives =      
-      aux_select passives g_passives
+      aux_select bag passives g_passives
     in
       debug
        (Printf.sprintf "Number of active goals : %d"
@@ -218,8 +220,12 @@ module Paramod (B : Terms.Blob) = struct
 
   let paramod ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
     let initial_timestamp = Unix.gettimeofday () in
-    let passives = add_passive_clauses passive_empty_set passives in
-    let g_passives = add_passive_clauses passive_empty_set g_passives in
+    let passives =
+      add_passive_clauses ~no_weight:true passive_empty_set passives
+    in
+    let g_passives =
+      add_passive_clauses ~no_weight:true passive_empty_set g_passives
+    in
     let g_actives = [] in
     let actives = [], IDX.DT.empty in
     try 
index 3957e925e469d895f08ba866517e8a89497e54a3..d058be2533fd83faf8e99a31fd4b0e99d0a58331 100644 (file)
@@ -22,9 +22,8 @@ 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
       | [] -> None
@@ -296,9 +295,30 @@ module Superposition (B : Terms.Blob) =
                   | _,_ -> None
     ;;
 
+    let rec orphan_murder bag acc i =
+      match Terms.M.find i bag with
+       | (_,_,_,Terms.Exact _),discarded -> (discarded,acc)
+       | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),true -> (true,acc)
+       | (_,_,_,Terms.Step (_,i1,i2,_,_,_)),false ->
+            if (List.mem i acc) then (false,acc)
+            else match orphan_murder bag acc i1 with
+             | (true,acc) -> (true,acc)
+             | (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 = 
-      let bag, clause = demodulate bag clause table in
+      if is_identity_clause ~unify:false clause then bag,None
+      (* else if orphan_murder bag clause then bag,None *)
+      else let bag, clause = demodulate bag clause table in
       if is_identity_clause ~unify:false clause then bag,None
       else
         match is_subsumed ~unify:false bag maxvar clause table with
@@ -306,21 +326,29 @@ module Superposition (B : Terms.Blob) =
          | Some _ -> bag, None
     ;;
 
+    let simplify table maxvar bag clause =
+      match simplify table maxvar bag clause with
+       | 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
-       | bag,None -> None (* new_clause has been discarded *)
+       | bag,None -> bag,None (* new_clause has been discarded *)
        | bag,(Some clause) ->
            let ctable = IDX.index_unit_clause IDX.DT.empty clause in
            let bag, alist, atable = 
              List.fold_left 
-               (fun (bag, alist, atable as acc) c ->
+               (fun (bag, alist, atable) c ->
                   match simplify ctable maxvar bag c with
-                    |bag,None -> acc (* an active clause as been discarded *)
+                    |bag,None -> (bag,alist,atable)
+                       (* an active clause as been discarded *)
                     |bag,Some c1 ->
                        bag, c :: alist, IDX.index_unit_clause atable c)
                (bag,[],IDX.DT.empty) alist
            in
-             Some (clause, bag, (alist,atable))
+             bag, Some (clause, (alist,atable))
     ;;
 
     let simplification_step ~new_cl cl (alist,atable) bag maxvar new_clause =
@@ -332,16 +360,17 @@ module Superposition (B : Terms.Blob) =
         * - actives and cl if new_clause is not cl *
         * - only actives otherwise                 *)
        match simplify atable1 maxvar bag new_clause with
-         | bag,None -> (Some cl, None) (* new_clause has been discarded *)
+         | bag,None -> bag,(Some cl, None) (* new_clause has been discarded *)
          | bag,Some clause ->
              (* Simplification of each active clause with clause *
               * which is the simplified form of new_clause       *)
               let ctable = IDX.index_unit_clause IDX.DT.empty clause in
              let bag, newa, alist, atable = 
                List.fold_left 
-                 (fun (bag, newa, alist, atable as acc) c ->
+                 (fun (bag, newa, alist, atable) c ->
                     match simplify ctable maxvar bag c with
-                      |bag,None -> acc (* an active clause as been discarded *)
+                      |bag,None -> (bag, newa, alist, atable)
+                         (* an active clause as been discarded *)
                       |bag,Some c1 ->
                            if (c1 == c) then 
                              bag, newa, c :: alist,
@@ -351,37 +380,37 @@ module Superposition (B : Terms.Blob) =
                  (bag,[],[],IDX.DT.empty) alist
              in
                if new_cl then
-                 (Some cl, Some (clause, (alist,atable), newa, bag))
+                 bag, (Some cl, Some (clause, (alist,atable), newa))
                else
                  (* if new_clause is not cl, we simplify cl with clause *)
                  match simplify ctable maxvar bag cl with
                    | bag,None ->
                        (* cl has been discarded *)
-                       (None, Some (clause, (alist,atable), newa, bag))
+                       bag,(None, Some (clause, (alist,atable), newa))
                    | bag,Some cl1 ->
-                       (Some cl1, Some (clause, (alist,atable), newa, bag))
+                       bag,(Some cl1, Some (clause, (alist,atable), newa))
     ;;
 
     let keep_simplified cl (alist,atable) bag maxvar =
       let rec keep_simplified_aux ~new_cl cl (alist,atable) bag newc =
        if new_cl then
          match simplification_step ~new_cl cl (alist,atable) bag maxvar cl with
-           | (None, _) -> assert false
-           | (Some _, None) -> None
-           | (Some _, Some (clause, (alist,atable), newa, bag)) ->
+           | _,(None, _) -> assert false
+           | bag,(Some _, None) -> bag,None
+           | bag,(Some _, Some (clause, (alist,atable), newa)) ->
                keep_simplified_aux ~new_cl:(cl!=clause) clause (alist,atable)
                  bag (newa@newc)
        else
          match newc with
-           | [] -> Some (cl, bag, (alist,atable))
+           | [] -> bag, Some (cl, (alist,atable))
            | hd::tl ->
                match simplification_step ~new_cl cl
                  (alist,atable) bag maxvar hd with
-                 | (None,None) -> assert false
-                 | (Some _,None) ->
+                 | _,(None,None) -> assert false
+                 | bag,(Some _,None) ->
                      keep_simplified_aux ~new_cl cl (alist,atable) bag tl
-                 | (None, Some _) -> None
-                 | (Some cl1, Some (clause, (alist,atable), newa, bag)) ->
+                 | bag,(None, Some _) -> bag,None
+                 | bag,(Some cl1, Some (clause, (alist,atable), newa)) ->
                      let alist,atable =
                        (clause::alist, IDX.index_unit_clause atable clause)
                      in
index e3e2f8b9f2f6f15d12c791a4351309f022139ccd..a7badaba4a5bb32769af0cc4f7bad2322fda7f4b 100644 (file)
@@ -58,7 +58,7 @@ module Superposition (B : Terms.Blob) :
       Index.Index(B).active_set ->
       B.t Terms.bag ->
       int ->
-      (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option
+      B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
 
 
     val keep_simplified:
@@ -66,7 +66,7 @@ module Superposition (B : Terms.Blob) :
       Index.Index(B).active_set ->
       B.t Terms.bag ->
       int ->
-      (B.t Terms.unit_clause * B.t Terms.bag * Index.Index(B).active_set) option
+      B.t Terms.bag * (B.t Terms.unit_clause * Index.Index(B).active_set) option
 
 
   end