matitaprover is now flexible enough to allow the computation of statistics on

[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 1cdb9eb5cdc75f1890a258ed1aa6f0b6a55a1182..f3afc16f46e1047615f089808d648d485623bf34 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -16,7 +16,29 @@ let debug _ = ();;
 
 let monster = 100;;
     
+module type Paramod =
+  sig
+    type t
+    type input
+    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 mk_passive : bag -> input * input -> bag * t Terms.unit_clause
+    val mk_goal : bag -> input * input -> bag * t Terms.unit_clause
+    val paramod : 
+      max_steps:int ->
+      ?timeout:float ->
+      bag -> 
+      g_passives:t Terms.unit_clause list -> 
+      passives:t Terms.unit_clause list -> szsontology
+  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