| Portability | unportable |
|---|---|
| Stability | unstable |
| Maintainer | Martin Avanzini <martin.avanzini@uibk.ac.at> |
| Safe Haskell | Safe-Infered |
Tct.Encoding.UsableRules
Description
This module implements a SAT encoding of usable rules with respect to the argument filtering encoding, cf. module Tct.Encoding.ArgumentFiltering.
- validUsableRulesEncoding :: (Eq l, Ord l, Monad s, Solver s l) => Problem -> (Symbol -> Int -> PropFormula l) -> Memo Term s l (PropFormula l)
- usable :: NGBoolean b UsableAtom => Problem -> Rule -> b
- initialUsables :: Problem -> [Symbol]
Documentation
validUsableRulesEncoding :: (Eq l, Ord l, Monad s, Solver s l) => Problem -> (Symbol -> Int -> PropFormula l) -> Memo Term s l (PropFormula l)
Add this constraint for a valid SAT encoding.
Propositional formula that holds if the given rule is usable.
initialUsables :: Problem -> [Symbol]
Initial left-hand side roots symbols of usable rules.