First attempt for refined goal selection strategy

[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 c7f67aa09313fb1ec9127856ec9f8d06b7c3338e..ab5c1897bbbfc5785204bbf54d8a7ec35d98f742 100644 (file)
--- a/helm/software/components/ng_paramodulation/orderings.mli
+++ b/helm/software/components/ng_paramodulation/orderings.mli
@@ -18,9 +18,14 @@ module Orderings (B : Terms.Blob) :
      * - stable for instantiation
      * - total on ground terms
      *
-     * The output can range only on Eq, Lt, Gt, Incomparable
      *)
     val compare_terms : 
           B.t Terms.foterm -> B.t Terms.foterm -> Terms.comparison
 
+    val compute_unit_clause_weight :
+      B.t Terms.unit_clause -> int
+
+    val compute_goal_weight :
+      B.t Terms.unit_clause -> int
+
   end