| Portability | unportable |
|---|---|
| Stability | unstable |
| Maintainer | Martin Avanzini <martin.avanzini@uibk.ac.at> |
| Safe Haskell | Safe-Infered |
Tct.Encoding.SafeMapping
Contents
Description
This module implements safe mapping, together with a a SAT encoding. By convention, n-ary function symbols admit argument positions '[1..n]'.
- data SafeMapping
- empty :: Signature -> Set Symbol -> SafeMapping
- isSafe :: SafeMapping -> Symbol -> Int -> Bool
- setSafe :: Symbol -> Int -> SafeMapping -> SafeMapping
- setSafes :: Symbol -> [Int] -> SafeMapping -> SafeMapping
- safeArgumentPositions :: Symbol -> SafeMapping -> [Int]
- validSafeMapping :: Eq l => [Symbol] -> Signature -> PropFormula l
- isSafeP :: Eq l => Symbol -> Int -> PropFormula l
Safe Mappings
data SafeMapping
Instances
| Show SafeMapping | |
| PrettyPrintable SafeMapping | |
| Decoder SafeMapping SafePosition | |
| PrettyPrintable (Trs, Signature, Variables, SafeMapping) |
empty :: Signature -> Set Symbol -> SafeMapping
The empty safe argument filtering.
isSafe :: SafeMapping -> Symbol -> Int -> Bool
Predicate that checks wether the given argument position of the given symbol is safe.
setSafe :: Symbol -> Int -> SafeMapping -> SafeMapping
Set ith argument position of given symbol safe.
setSafes :: Symbol -> [Int] -> SafeMapping -> SafeMapping
List version of setSafe.
safeArgumentPositions :: Symbol -> SafeMapping -> [Int]
Returns the list of safe argument positions.
Sat Encoding
validSafeMapping :: Eq l => [Symbol] -> Signature -> PropFormula l
Add this constraint for a valid SAT encoding.
isSafeP :: Eq l => Symbol -> Int -> PropFormula l
The Formula 'isSafeP f i' reflects
that the ith argument position of f is safe.