Categorical stuff postponed.

[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 3af1a38e448c459369a0bead452a7b4c84cc6363..a3fd41e21b1d8c5a68a65f88ecc89984c7667ae0 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -11,8 +11,8 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
-let debug s = prerr_endline (Lazy.force s) ;; 
-(* let debug _ = ();; *)
+(* let debug s = prerr_endline (Lazy.force s) ;; *)
+let debug _ = ();; 
 
 let monster = 100;;
     
@@ -21,7 +21,8 @@ module type Paramod =
     type t
     type input
     type szsontology = 
-      | Unsatisfiable of (t Terms.bag * int * int list) list
+      | Unsatisfiable of 
+         (t Terms.bag * int * t Terms.substitution * int list) list
       | GaveUp 
       | Error of string 
       | Timeout of int * t Terms.bag
@@ -80,7 +81,8 @@ module Paramod (B : Orderings.Blob) = struct
   type input = B.input
   type bag = B.t Terms.bag * int 
   type szsontology = 
-    | Unsatisfiable of (B.t Terms.bag * int * int list) list
+    | Unsatisfiable of 
+       (B.t Terms.bag * int * B.t Terms.substitution * int list) list
     | GaveUp 
     | Error of string 
     | Timeout of int * B.t Terms.bag
@@ -204,7 +206,12 @@ module Paramod (B : Orderings.Blob) = struct
   let initialize_goal (bag,maxvar,actives,passives,_,_) t = 
     let (bag,maxvar), g = mk_goal (bag,maxvar) t in
     let g_passives = g_passive_empty_set in
-    let g_passives = add_passive_goal g_passives g in
+    (* if the goal is not an equation we returns an empty
+       passive set *)
+    let g_passives =
+      if Terms.is_eq_clause g then add_passive_goal g_passives g
+      else g_passives 
+    in
       (bag,maxvar,actives,passives,[],g_passives)
 
 
@@ -318,7 +325,18 @@ module Paramod (B : Orderings.Blob) = struct
     debug (lazy("Last chance " ^ string_of_float
                  (Unix.gettimeofday())));
     let active_t = snd actives in
-    let passive_t,_,_ = passives in
+    let passive_t,wset,_ = passives in
+    let _ = debug
+      (lazy 
+        ("Passive set :" ^ (String.concat ";\n" 
+           (List.map (fun _,cl -> Pp.pp_unit_clause cl) 
+              (WeightPassiveSet.elements wset))))) in
+    let wset = IDX.elems passive_t in
+    let _ = debug
+      (lazy 
+        ("Passive table :" ^(String.concat ";\n" 
+           (List.map (fun _,cl -> Pp.pp_unit_clause cl)
+              (IDX.ClauseSet.elements wset))))) in
     let g_passives = 
       WeightPassiveSet.fold 
        (fun (_,x) acc ->
@@ -444,7 +462,7 @@ module Paramod (B : Orderings.Blob) = struct
     in
       goal_narrowing iterno max_steps timeout newstatus
 
-    let compute_result bag i =
+    let compute_result bag i subst =
       let l =
         let rec traverse ongoal (accg,acce) i =
           match Terms.get_from_bag i bag with
@@ -462,14 +480,13 @@ module Paramod (B : Orderings.Blob) = struct
         let gsteps,esteps = traverse true ([],[]) i in
           (List.rev esteps)@gsteps
       in
-      prerr_endline ("steps: " ^ (string_of_int (List.length l)));
+      debug (lazy ("steps: " ^ (string_of_int (List.length l))));
       let max_w = 
        List.fold_left 
          (fun acc i ->
             let (cl,_,_) = Terms.get_from_bag i bag in
               max acc (Order.compute_unit_clause_weight cl)) 0 l in
-       prerr_endline "Statistics :";
-       prerr_endline ("Max weight : " ^ (string_of_int max_w));
+       debug (lazy ("Max weight : " ^ (string_of_int max_w)));
 (*       List.iter (fun id -> let ((_,lit,_,proof as cl),d,it) =
            Terms.get_from_bag id bag in
              if d then
@@ -482,12 +499,13 @@ module Paramod (B : Orderings.Blob) = struct
                (Printf.sprintf "Id : %d, selected at %d, weight %d by %s"
                   id it (Order.compute_unit_clause_weight cl) 
                   (Pp.pp_proof_step proof))) l;*)
-        prerr_endline "Proof:"; 
-        List.iter 
-         (fun x ->
-            let cl,_,_ = Terms.get_from_bag x bag in
-             prerr_endline (Pp.pp_unit_clause cl)) l;
-        Unsatisfiable [ bag, i, l ]
+        debug (lazy ("Proof:" ^
+          (String.concat "\n" 
+            (List.map 
+               (fun x ->
+                  let cl,_,_ = Terms.get_from_bag x bag in
+                    Pp.pp_unit_clause cl) l))));
+        Unsatisfiable [ bag, i, subst, l ]
 
   let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
     let _initial_timestamp = Unix.gettimeofday () in
@@ -503,20 +521,22 @@ module Paramod (B : Orderings.Blob) = struct
      given_clause ~useage ~noinfer:false
       bag maxvar 0  0 max_steps timeout actives passives g_actives g_passives
     with 
-    | Sup.Success (bag, _, (i,_,_,_)) ->
-       compute_result bag i
-    | Stop (Unsatisfiable _) -> Error "stop bug solution found!"
+    | Sup.Success (bag, _, (i,_,_,_),subst) ->
+       compute_result bag i subst
+    | Stop (Unsatisfiable _) -> Error "solution found!"
     | Stop o -> o
   ;;
 
 let fast_eq_check s goal =
-  let s = initialize_goal s goal in
+  let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in
+  if is_passive_g_set_empty g_passives then Error "not an equation" 
+  else
   try 
     goal_narrowing 0 2 None s
   with
-    | Sup.Success (bag, _, (i,_,_,_)) ->
-       compute_result bag i
-    | Stop (Unsatisfiable _) -> Error "stop bug solution found!"
+    | Sup.Success (bag, _, (i,_,_,_),subst) ->
+       compute_result bag i subst
+    | Stop (Unsatisfiable _) -> Error "solution found!"
     | Stop o -> o
   ;;