X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2Forderings.mli;h=84a3cf9f5236daaee3b0a91274745127486a9c3d;hb=38c54dd8e2234836d5f3e8011c478daf7d59fa25;hp=f2f6a1678ba249bdadfc5d74cbfd41eb7ab659e2;hpb=6c4056ea40b96039f24eeda9a1e1900c95bad7c8;p=helm.git

diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli
index f2f6a1678..84a3cf9f5 100644
--- a/helm/software/components/ng_paramodulation/orderings.mli
+++ b/helm/software/components/ng_paramodulation/orderings.mli
@@ -11,7 +11,31 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-module Orderings (B : Terms.Blob) :
+module type Blob =
   sig 
-    val compare_terms : B.t Terms.foterm -> B.t Terms.foterm -> Terms.comparison
+    include Terms.Blob 
+
+    (* This order relation should be:
+     * - stable for instantiation
+     * - total on ground terms
+     *
+     *)
+    val compare_terms : 
+          t Terms.foterm -> t Terms.foterm -> Terms.comparison
+
+    (* 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 name : string
+
   end
+
+module NRKBO (B : Terms.Blob) : Blob 
+with type t = B.t 
+
+module KBO (B : Terms.Blob) : Blob 
+with type t = B.t 
+
+module LPO (B : Terms.Blob) : Blob
+with type t = B.t