Final subst returned by superposition and passed around.

[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 b06d8a654f4b083dce71d08db77a6abc90decedf..a3fd41e21b1d8c5a68a65f88ecc89984c7667ae0 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -11,7 +11,7 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
-(* let debug s = prerr_endline (Lazy.force s) ;; *) 
+(* 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
@@ -460,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
@@ -503,7 +505,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 +521,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 +534,8 @@ 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
   ;;