Branched paramodulation for CNF (Horn clauses)

[helm.git] / helm / software / components / ng_paramodulation / orderings.mli

diff --git a/helm/software/components/ng_paramodulation/orderings.mli b/helm/software/components/ng_paramodulation/orderings.mli
index 59cfde124c3468adbbbc7d567fb02d53d4b88880..7c66cc40bced62d6e3a889a38164627513a41064 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.mli
+++ b/helm/software/components/ng_paramodulation/orderings.mli
@@ -11,4 +11,31 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-val compare_terms : 'a Terms.foterm -> 'a Terms.foterm -> Terms.comparison
+module type Blob =
+  sig 
+    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 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