Exported forward_inference_step

[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 0dbd6260aede1286d79976ea364a17e40d1ca5b1..6f76e2ad4221c7257b04e6f1e60bd29e4c1d36d6 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -20,14 +20,21 @@ module type Paramod =
   sig
     type t
     type input
+    type state
     type szsontology = 
       | Unsatisfiable of (t Terms.bag * int * int list) list
       | GaveUp 
       | Error of string 
       | Timeout of int * t Terms.bag
     type bag = t Terms.bag * int
+    val empty_state : state
     val mk_passive : bag -> input * input -> bag * t Terms.unit_clause
     val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
+    val forward_infer_step : 
+      state ->
+      t Terms.unit_clause ->
+      int ->
+      state
     val paramod :
       useage:bool ->
       max_steps:int ->
@@ -38,15 +45,6 @@ module type Paramod =
   end
 
 module Paramod (B : Orderings.Blob) = struct
-  type t = B.t
-  type input = B.input
-  type szsontology = 
-    | Unsatisfiable of (B.t Terms.bag * int * int list) list
-    | GaveUp 
-    | Error of string 
-    | Timeout of int * B.t Terms.bag
-  exception Stop of szsontology
-  type bag = B.t Terms.bag * int
   module Pp = Pp.Pp (B) 
   module FU = FoUnif.Founif(B) 
   module IDX = Index.Index(B) 
@@ -68,6 +66,32 @@ module Paramod (B : Orderings.Blob) = struct
   module WeightPassiveSet = Set.Make(WeightOrderedPassives)
   module AgePassiveSet = Set.Make(AgeOrderedPassives)
 
+  type t = B.t
+  type input = B.input
+  type state = 
+      B.t Terms.bag 
+      * int 
+      * Index.Index(B).active_set 
+      * (WeightPassiveSet.t * AgePassiveSet.t) 
+      * B.t Terms.unit_clause list 
+      * (WeightPassiveSet.t * AgePassiveSet.t)
+  type szsontology = 
+    | Unsatisfiable of (B.t Terms.bag * int * int list) list
+    | GaveUp 
+    | Error of string 
+    | Timeout of int * B.t Terms.bag
+  exception Stop of szsontology
+  type bag = B.t Terms.bag * int
+
+  let empty_state = 
+    Terms.empty_bag,
+    0,
+    ([],IDX.DT.empty),
+    (WeightPassiveSet.empty,AgePassiveSet.empty),
+    [],
+    (WeightPassiveSet.empty,AgePassiveSet.empty)
+;;
+
   let add_passive_clause ?(no_weight=false) (passives_w,passives_a) cl =
     let cl = if no_weight then (0,cl)
     else Utils.mk_passive_clause cl in
@@ -172,8 +196,8 @@ module Paramod (B : Orderings.Blob) = struct
     (add_passive_goals g_passives new_goals)
   ;;
 
-  let forward_infer_step bag maxvar actives passives g_actives
-                         g_passives current iterno =
+  let forward_infer_step (bag,maxvar,actives,passives,g_actives,g_passives)  
+      current iterno =
     (* forward step *)
     
     (* e = select P           *
@@ -321,8 +345,9 @@ module Paramod (B : Orderings.Blob) = struct
                     in
                     bag,maxvar,actives,passives,g_actives,g_passives
                   else
-                    forward_infer_step bag maxvar actives passives
-                      g_actives g_passives current iterno
+                    forward_infer_step 
+                     (bag,maxvar,actives,passives,g_actives,g_passives)
+                     current iterno
     in