Theory.Constraint.Solver.Goals

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 openGoals. See Theory.Constraint.Solver.ProofMethod for the public interface to solving goals and the implementation of heuristics.

Documentation

data Usefulness

Constructors

Useful

A goal that is likely to result in progress.

LoopBreaker

A goal that is delayed to avoid immediate termination.

ProbablyConstructible

A goal that is likely to be constructible by the adversary.

CurrentlyDeducible

A message that is deducible for the current solution.

Instances

Eq Usefulness

Ord Usefulness

Show Usefulness

type AnnotatedGoal = (Goal, (Integer, Usefulness))

Goals annotated with their number and usefulness.

openGoals :: System -> [AnnotatedGoal]

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.

solveGoal :: Goal -> Reduction String

solveGoal rules goal enumerates all possible cases of how this goal could be solved in the context of the given rules. For each case, a sensible case-name is returned.