| Portability | unportable |
|---|---|
| Stability | unstable |
| Maintainer | Martin Avanzini <martin.avanzini@uibk.ac.at> |
| Safe Haskell | Safe-Infered |
Tct.Encoding.Precedence
Contents
Description
This module implements a SAT encoding of quasi precedences.
- validPrecedenceM :: (Eq l, Monad s, Solver s l) => [Symbol] -> SatSolver s l (PropFormula l)
- restrictRecDepthM :: (Eq l, Monad s, Solver s l) => [Symbol] -> Int -> SatSolver s l (PropFormula l)
- precGt :: Eq l => Symbol -> Symbol -> PropFormula l
- precEq :: Eq l => Symbol -> Symbol -> PropFormula l
- initial :: Signature -> Precedence
- newtype RecursiveSymbols = RS (Set Symbol)
- initialRecursiveSymbols :: RecursiveSymbols
- isRecursive :: Eq l => Symbol -> PropFormula l
Documentation
validPrecedenceM :: (Eq l, Monad s, Solver s l) => [Symbol] -> SatSolver s l (PropFormula l)
Add this constraint for a valid SAT encoding.
restrictRecDepthM :: (Eq l, Monad s, Solver s l) => [Symbol] -> Int -> SatSolver s l (PropFormula l)
Restrict the recursion depth to a given bound
precGt :: Eq l => Symbol -> Symbol -> PropFormula l
'f `precGt` g` asserts that f is strictly
above g in the precedence
precEq :: Eq l => Symbol -> Symbol -> PropFormula l
Assert equivalence in the precedence.
initial :: Signature -> Precedence
The initial argument filtering.
Recursive Symbols
This is used by Tct.Method.PopStar to obtain a more precise complexity certificate
isRecursive :: Eq l => Symbol -> PropFormula l