sig
type t = C.t -> int
val default : ClauseQueue_intf.S.WeightFun.t
val penalty : ClauseQueue_intf.S.WeightFun.t
val favor_all_neg : ClauseQueue_intf.S.WeightFun.t
val favor_non_all_neg : ClauseQueue_intf.S.WeightFun.t
val favor_ground : ClauseQueue_intf.S.WeightFun.t
val favor_horn : ClauseQueue_intf.S.WeightFun.t
val favor_goal : ClauseQueue_intf.S.WeightFun.t
val combine :
(ClauseQueue_intf.S.WeightFun.t * int) list ->
ClauseQueue_intf.S.WeightFun.t
end