|Maintainer||Simon Meier <email@example.com>|
The constraint reduction rules, which are not enforced as invariants in Theory.Constraint.Solver.Reduction.
A goal represents a possible application of a rule that may result in
multiple cases or even non-termination (if applied repeatedly). These goals
are computed as the list of
Theory.Constraint.Solver.ProofMethod for the public interface to solving
goals and the implementation of heuristics.
A goal that is likely to result in progress.
A goal that is delayed to avoid immediate termination.
A goal that is likely to be constructible by the adversary.
A message that is deducible for the current solution.
Goals annotated with their number and usefulness.
The list of goals that must be solved before a solution can be extracted. Each goal is annotated with its age and an indicator for its usefulness.