module WeightFun: sig
.. end
Weight functions
type
t = 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
val age : t
Returns the age of the clause (or 0 for the empty 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.