;;
module Utils (B : Terms.Blob) = struct
- module Subst = FoSubst.Subst(B) ;;
+ module Subst = FoSubst;; (*.Subst(B) ;;*)
module Order = Orderings.Orderings(B) ;;
let rec eq_foterm x y =
let empty_bag = Terms.M.empty ;;
+ let mk_passive_clause cl =
+ (Order.compute_unit_clause_weight cl, cl)
+ ;;
+
+ let compare_passive_clauses (w1,(id1,_,_,_)) (w2,(id2,_,_,_)) =
+ if w1 = w2 then id1 - id2
+ else w1 - w2
+ ;;
+
end