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