Moved compare in a different file.

[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 f7bc2eac9d5f237b3181fc7d42e23da39c9a4d47..de32ab5ddf8b7e0fe1b8984ed4bdad4e4d4c3970 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -12,8 +12,8 @@
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
 let print s = prerr_endline (Lazy.force s) ;; 
-(* let debug = print *) 
-let debug s = ();; 
+let noprint s = ();;  
+let debug = noprint;;
 
 let monster = 100;;
     
@@ -52,6 +52,8 @@ module type Paramod =
       bag -> 
       g_passives:t Terms.unit_clause list -> 
       passives:t Terms.unit_clause list -> szsontology
+    val demod :
+      state -> input* input -> szsontology
     val fast_eq_check :
       state -> input* input -> szsontology
     val nparamod :
@@ -346,12 +348,12 @@ module Paramod (B : Orderings.Blob) = struct
                  (Unix.gettimeofday())));
     let actives_l, active_t = actives in
     let passive_t,wset,_ = passives in
-    let _ = debug
+    let _ = noprint
       (lazy 
         ("Actives :" ^ (String.concat ";\n" 
            (List.map Pp.pp_unit_clause actives_l)))) in 
     let wset = IDX.elems passive_t in
-    let _ = debug
+    let _ = noprint
       (lazy 
         ("Passives:" ^(String.concat ";\n" 
            (List.map (fun _,cl -> Pp.pp_unit_clause cl)
@@ -367,13 +369,15 @@ module Paramod (B : Orderings.Blob) = struct
       (List.iter
        (fun x -> 
            ignore 
-             (Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x))
+            (debug (lazy("ckecking goal vs a: " ^ Pp.pp_unit_clause x));
+               Sup.simplify_goal ~no_demod:true maxvar active_t bag [] x))
        g_passives); 
       ignore
       (List.iter
         (fun x -> 
            ignore 
-             (Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x))
+             (debug (lazy("ckecking goal vs p: " ^ Pp.pp_unit_clause x));
+       Sup.simplify_goal ~no_demod:true maxvar passive_t bag [] x))
         (g_actives@g_passives)); 
     raise (Stop (Timeout (maxvar,bag)))
 
@@ -450,7 +454,7 @@ module Paramod (B : Orderings.Blob) = struct
       Sup.simplify_goal 
         ~no_demod maxvar (snd actives) bag g_actives current 
     with
-      | None -> status
+      | None -> debug (lazy "None"); status
       | Some (bag,g_current) -> 
          let _ = 
            debug (lazy("Infer on goal : " 
@@ -552,6 +556,14 @@ module Paramod (B : Orderings.Blob) = struct
     | Stop o -> o
   ;;
 
+let demod s goal =
+  let bag,maxvar,actives,passives,g_actives,g_passives = s in
+  let (bag,maxvar), g = mk_goal (bag,maxvar) goal in
+  if Terms.is_eq_clause g then 
+    let bag, ((i,_,_,_) as g1) = Sup.demodulate bag g (snd actives) in
+      if g1 = g then GaveUp else compute_result bag i []
+  else GaveUp
+
 let fast_eq_check s goal =
   let (_,_,_,_,_,g_passives) as s = initialize_goal s goal in
   if is_passive_g_set_empty g_passives then Error "not an equation"