Portability | GHC only |
---|---|
Maintainer | Simon Meier <iridcode@gmail.com> |
Safe Haskell | None |
This is the public interface for constructing and deconstructing constraint systems. The interface for performing constraint solving provided by Theory.Constraint.Solver.
- data Contradiction
- substCreatesNonNormalTerms :: MaudeHandle -> System -> LNSubst -> LNSubstVFresh -> Bool
- contradictions :: ProofContext -> System -> [Contradiction]
- contradictorySystem :: ProofContext -> System -> Bool
- prettyContradiction :: Document d => Contradiction -> d
Contradictory constraint systems
data Contradiction Source
Reasons why a constraint System
can be contradictory.
Cyclic | The paths are cyclic. |
NonNormalTerms | Has terms that are not in normal form. | NonLastNode -- ^ Has a non-silent node after the last node. |
ForbiddenExp | Forbidden Exp-down rule instance |
ForbiddenBP | Forbidden bilinear pairing rule instance |
ForbiddenKD | has forbidden KD-fact |
ImpossibleChain | has impossible chain |
NonInjectiveFactInstance (NodeId, NodeId, NodeId) | Contradicts that certain facts have unique instances. |
IncompatibleEqs | Incompatible equalities. |
FormulasFalse | False in formulas |
SuperfluousLearn LNTerm NodeId | A term is derived both before and after a learn |
NodeAfterLast (NodeId, NodeId) | There is a node after the last node. |
substCreatesNonNormalTerms :: MaudeHandle -> System -> LNSubst -> LNSubstVFresh -> BoolSource
contradictions :: ProofContext -> System -> [Contradiction]Source
All CR-rules reducing a constraint system to *⟂* represented as a list of trivial contradictions. Note that some constraint systems are also removed because they have no unifier. This is part of unification. Note also that *S_{¬@}* is handled as part of *S_∀*.
contradictorySystem :: ProofContext -> System -> BoolSource
True
if the constraint system is contradictory.
Pretty-printing
prettyContradiction :: Document d => Contradiction -> dSource
Pretty-print a Contradiction
.