X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Fparamod.ml;h=3491f40196f9a21d8c522d564a49554a1b71be63;hb=ee9a771a3cf2124ef65906ae75eb0ba7e2e4303b;hp=f156ff0ffae30fe93d6318363f74387072da736b;hpb=016f069da6221053873b4d505716ef1bd80f08b6;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index f156ff0ff..3491f4019 100644
--- 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 Paramod (B : Terms.Blob) = struct
+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 
@@ -29,7 +51,7 @@ module Paramod (B : Terms.Blob) = struct
   module IDX = Index.Index(B) 
   module Sup = Superposition.Superposition(B) 
   module Utils = FoUtils.Utils(B) 
-  module Order = Orderings.Orderings(B)
+  module Order = B
   module WeightOrderedPassives =
       struct
         type t = B.t Terms.passive_clause
@@ -229,7 +251,7 @@ module Paramod (B : Terms.Blob) = struct
           end
         else raise (Stop (Timeout (maxvar,bag)));
 
-    let use_age = weight_picks = (iterno / 6 + 1) in
+    let use_age = false && (weight_picks = (iterno / 6 + 1)) in
     let weight_picks = if use_age then 0 else weight_picks+1
     in