module WeightFun: sig .. end
Weight functions
type C.t -> int
attribute a weight to a clause. The smaller, the better (lightweight
clauses will be favored). A weight must always be positive;
the weight of the empty clause should alwyays be 0.
val default : t
Use Literal.heuristic_weight
val penalty : t
Returns the penalty of the clause
val favor_all_neg : t
Favor clauses with only negative ground lits
val favor_non_all_neg : t
Favor clauses that have at least one non-(ground negative) lit
val favor_ground : t
val favor_horn : t
val favor_goal : t
The closest a clause is from the initial goal, the lowest its weight.
Some threshold is used for clauses that are too far away
val combine : (t * int) list -> t
Combine a list of pairs w, coeff where w is a weight function,
and coeff a strictly positive number. This is a weighted sum
of weights.