freescale porting

[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 b15503de4f1ba9497efd292f24bac9a97a15171c..7c934df1e59cd48373a65d5a66ff11d98237eb82 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
@@ -52,6 +53,11 @@ module type Paramod =
       passives:t Terms.unit_clause list -> szsontology
     val fast_eq_check :
       state -> input* input -> szsontology
+    val nparamod :
+      useage:bool ->
+      max_steps:int ->
+      ?timeout:float ->
+      state -> input* input -> szsontology
   end
 
 module Paramod (B : Orderings.Blob) = struct
@@ -80,7 +86,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
@@ -246,7 +253,7 @@ module Paramod (B : Orderings.Blob) = struct
       in
         debug (lazy "Performed infer_left step");
        let bag = Terms.replace_in_bag (g_current,false,iterno) bag in
-        bag, maxvar, actives, passives, g_current::g_actives,
+          bag, maxvar, actives, passives, g_current::g_actives,
     (add_passive_goals g_passives new_goals)
   ;;
 
@@ -276,6 +283,10 @@ module Paramod (B : Orderings.Blob) = struct
     let bag, maxvar, actives, new_clauses = 
       Sup.infer_right bag maxvar current actives 
     in
+      debug
+       (lazy 
+        ("New clauses :" ^ (String.concat ";\n" 
+           (List.map Pp.pp_unit_clause new_clauses)))); 
       debug (lazy "Demodulating goals with actives...");
       (* keep goals demodulated w.r.t. actives and check if solved *)
       let bag, g_actives = 
@@ -322,17 +333,16 @@ module Paramod (B : Orderings.Blob) = struct
   let last_chance (bag,maxvar,actives,passives,g_actives,g_passives) =
     debug (lazy("Last chance " ^ string_of_float
                  (Unix.gettimeofday())));
-    let active_t = snd actives in
+    let actives_l, active_t = actives 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
+        ("Actives :" ^ (String.concat ";\n" 
+           (List.map Pp.pp_unit_clause actives_l)))) in 
     let wset = IDX.elems passive_t in
     let _ = debug
       (lazy 
-        ("Passive table :" ^(String.concat ";\n" 
+        ("Passives:" ^(String.concat ";\n" 
            (List.map (fun _,cl -> Pp.pp_unit_clause cl)
               (IDX.ClauseSet.elements wset))))) in
     let g_passives = 
@@ -423,6 +433,21 @@ module Paramod (B : Orderings.Blob) = struct
         actives passives g_actives g_passives
   ;;
 
+  let check_and_infer ~no_demod iterno status current =
+    let bag,maxvar,actives,passives,g_actives,g_passives = status in
+    match 
+      Sup.simplify_goal 
+        ~no_demod:false maxvar (snd actives) bag g_actives current 
+    with
+      | None -> status
+      | Some (bag,g_current) -> 
+         let _ = 
+           debug (lazy("Infer on goal : " 
+                       ^ Pp.pp_unit_clause g_current)) 
+         in
+           backward_infer_step bag maxvar actives passives
+              g_actives g_passives g_current iterno
+
   (* similar to given_clause, but it merely works on goals, 
      in parallel, at each iteration *)
   let rec goal_narrowing iterno max_steps timeout status
@@ -444,23 +469,14 @@ module Paramod (B : Orderings.Blob) = struct
           let _ = 
             debug (lazy("Selected goal : " ^ Pp.pp_unit_clause current)) 
           in
-           match 
-             Sup.simplify_goal 
-               ~no_demod:false maxvar (snd actives) bag g_actives current 
-           with
-             | None -> acc
-             | Some (bag,g_current) -> 
-                let _ = 
-                  debug (lazy("Demodulated goal : " 
-                              ^ Pp.pp_unit_clause g_current)) 
-                in
-                backward_infer_step bag maxvar actives passives
-                  g_actives g_passives g_current iterno)
-          status passive_goals
+            (* awe work both on the original goal and the demodulated one*)
+          let acc = check_and_infer ~no_demod:true iterno acc current
+          in check_and_infer ~no_demod:false iterno acc current)
+       status passive_goals
     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
@@ -503,7 +519,7 @@ module Paramod (B : Orderings.Blob) = struct
                (fun x ->
                   let cl,_,_ = Terms.get_from_bag x bag in
                     Pp.pp_unit_clause cl) l))));
-        Unsatisfiable [ bag, i, l ]
+        Unsatisfiable [ bag, i, subst, l ]
 
   let paramod ~useage ~max_steps ?timeout (bag,maxvar) ~g_passives ~passives =
     let _initial_timestamp = Unix.gettimeofday () in
@@ -519,8 +535,8 @@ 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
+    | Sup.Success (bag, _, (i,_,_,_),subst) ->
+       compute_result bag i subst
     | Stop (Unsatisfiable _) -> Error "solution found!"
     | Stop o -> o
   ;;
@@ -532,8 +548,22 @@ let fast_eq_check s goal =
   try 
     goal_narrowing 0 2 None s
   with
-    | Sup.Success (bag, _, (i,_,_,_)) ->
-       compute_result bag i
+    | Sup.Success (bag, _, (i,_,_,_),subst) ->
+       compute_result bag i subst
+    | Stop (Unsatisfiable _) -> Error "solution found!"
+    | Stop o -> o
+  ;;
+
+let nparamod ~useage ~max_steps ?timeout s goal =
+  let bag,maxvar,actives,passives,g_actives,g_passives
+      = initialize_goal s goal in
+  if is_passive_g_set_empty g_passives then Error "not an equation" 
+  else
+    try given_clause ~useage ~noinfer:false
+      bag maxvar 0 0 max_steps timeout actives passives g_actives g_passives
+  with
+    | Sup.Success (bag, _, (i,_,_,_),subst) ->
+       compute_result bag i subst
     | Stop (Unsatisfiable _) -> Error "solution found!"
     | Stop o -> o
   ;;