+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_unit_clause_weight : 't Terms.unit_clause -> int
+ val compute_goal_weight : '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