Exported forward_inference_step

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.ml b/helm/software/components/ng_paramodulation/nCicParamod.ml
index 846a576c7861f9268aada91cc4642b98150d4e72..6096d88dae1bfd358d4593abe95081c40c196594 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicParamod.ml
+++ b/helm/software/components/ng_paramodulation/nCicParamod.ml
@@ -11,19 +11,23 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
+
+module B(C : NCicBlob.NCicContext): Orderings.Blob 
+  with type t = NCic.term and type input = NCic.term 
+  = Orderings.LPO(NCicBlob.NCicBlob(C))
+
+module NCicParamod(C : NCicBlob.NCicContext) = Paramod.Paramod(B(C))
+
 let nparamod rdb metasenv subst context t table =
-  let module C = 
-    struct
+  let module C =
+    struct 
       let metasenv = metasenv
       let subst = subst
-      let context = context
-    end
-  in
-  let module B : Orderings.Blob 
-      with type t = NCic.term and type input = NCic.term 
-    = Orderings.LPO(NCicBlob.NCicBlob(C))
+      let context = context 
+    end 
   in
-  let module P = Paramod.Paramod(B) in
+  let module B = B(C) in
+  let module P = NCicParamod(C) in
   let module Pp = Pp.Pp(B) in
   let bag, maxvar = Terms.empty_bag, 0 in
   let (bag,maxvar), goals = 

diff --git a/helm/software/components/ng_paramodulation/nCicParamod.mli b/helm/software/components/ng_paramodulation/nCicParamod.mli
index d24e5b57f0ee94abf77f2346647d1987a08bb534..067235158043fda321e20fecebe08a458ffc8f12 100644 (file)
--- a/helm/software/components/ng_paramodulation/nCicParamod.mli
+++ b/helm/software/components/ng_paramodulation/nCicParamod.mli
@@ -11,6 +11,9 @@
 
 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
 
+module NCicParamod(C : NCicBlob.NCicContext) : Paramod.Paramod
+with type t = NCic.term and type input = NCic.term 
+
 val nparamod :
   #NRstatus.status ->
   NCic.metasenv -> NCic.substitution -> NCic.context -> 

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
     
 

diff --git a/helm/software/components/ng_paramodulation/paramod.mli b/helm/software/components/ng_paramodulation/paramod.mli
index 9cffd9d2889af4958d8dc8254ce1af33e31dc18d..b195e80c945221e4f942fd0bf77c1a72987e6b02 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.mli
+++ b/helm/software/components/ng_paramodulation/paramod.mli
@@ -15,14 +15,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 ->