| Portability | unportable |
|---|---|
| Stability | unstable |
| Maintainer | Martin Avanzini <martin.avanzini@uibk.ac.at> |
| Safe Haskell | Safe-Infered |
Tct.Encoding.ArgumentFiltering
Description
This module provides a SAT encoding of argument filterings. By convention, n-ary function symbols admit argument positions '[1..n]'.
- validSafeArgumentFiltering :: (Eq l, Ord l) => [Symbol] -> Signature -> PropFormula l
- isCollapsing :: (Eq l, Ord l) => Symbol -> PropFormula l
- isInFilter :: (Eq l, Ord l) => Symbol -> Int -> PropFormula l
- initial :: Signature -> ArgumentFiltering
- data AFAtom
Documentation
validSafeArgumentFiltering :: (Eq l, Ord l) => [Symbol] -> Signature -> PropFormula l
Add this constraint for a valid SAT encoding.
isCollapsing :: (Eq l, Ord l) => Symbol -> PropFormula l
This formula holds if the argument filtering collapses on the symbol.
isInFilter :: (Eq l, Ord l) => Symbol -> Int -> PropFormula l
The formula isInFilter f i holds if the ith argument
filtering is in the filtering.
Initial argument filtering.