Portability | GHC only |
---|---|
Maintainer | Simon Meier <iridcode@gmail.com> |
Safe Haskell | None |
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.
- data Usefulness
- type AnnotatedGoal = (Goal, (Integer, Usefulness))
- openGoals :: System -> [AnnotatedGoal]
- solveGoal :: Goal -> Reduction String
Documentation
data Usefulness Source
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. |
type AnnotatedGoal = (Goal, (Integer, Usefulness))Source
Goals annotated with their number and usefulness.
openGoals :: System -> [AnnotatedGoal]Source
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.