X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.mli;h=7c66cc40bced62d6e3a889a38164627513a41064;hb=8e4367191fdfd125596658e35d4b99cd3047a5bc;hp=ab5c1897bbbfc5785204bbf54d8a7ec35d98f742;hpb=07fb52e761b192a97c6fe00c657e670b2d1fc2f1;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli
index ab5c1897b..7c66cc40b 100644
--- a/helm/software/components/ng_paramodulation/orderings.mli
+++ b/helm/software/components/ng_paramodulation/orderings.mli
@@ -11,8 +11,9 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-module Orderings (B : Terms.Blob) :
+module type Blob =
   sig 
+    include Terms.Blob 
 
     (* This order relation should be:
      * - stable for instantiation
@@ -20,12 +21,21 @@ module Orderings (B : Terms.Blob) :
      *
      *)
     val compare_terms : 
-          B.t Terms.foterm -> B.t Terms.foterm -> Terms.comparison
+          t Terms.foterm -> t Terms.foterm -> Terms.comparison
 
-    val compute_unit_clause_weight :
-      B.t Terms.unit_clause -> int
+    (* these could be outside the module, but to ease experimentation
+     * we allow them to be tied with the ordering *)
+    val compute_clause_weight : 't Terms.clause -> int
 
-    val compute_goal_weight :
-      B.t Terms.unit_clause -> int
+    val name : string
 
   end
+
+module NRKBO (B : Terms.Blob) : Blob 
+with type t = B.t and type input = B.input
+
+module KBO (B : Terms.Blob) : Blob 
+with type t = B.t and type input = B.input
+
+module LPO (B : Terms.Blob) : Blob 
+with type t = B.t and type input = B.input