First attempt for refined goal selection strategy

[helm.git] / helm / software / components / ng_paramodulation / foUtils.ml

diff --git a/helm/software/components/ng_paramodulation/foUtils.ml b/helm/software/components/ng_paramodulation/foUtils.ml
index 4c99f5b9cbe3b546c4896dd54beb71880c9b13d3..a970bb6f0c51ee67870e6577b9797daf45b1abca 100644 (file)
--- a/helm/software/components/ng_paramodulation/foUtils.ml
+++ b/helm/software/components/ng_paramodulation/foUtils.ml
@@ -140,6 +140,10 @@ module Utils (B : Terms.Blob) = struct
     (Order.compute_unit_clause_weight cl, cl)
   ;;
 
+  let mk_passive_goal g =
+    (Order.compute_goal_weight g, g)
+  ;;
+
   let compare_passive_clauses_weight (w1,(id1,_,_,_)) (w2,(id2,_,_,_)) =
     if w1 = w2 then id1 - id2
     else w1 - w2