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`

.