- type SAT a = WriterT [Clause] (State Accu) a
- data Boolean
- type Booleans = [Boolean]
- boolean :: SAT Boolean
- exists :: SAT Boolean
- forall :: SAT Boolean
- constant :: Bool -> SAT Boolean
- not :: Boolean -> Boolean
- assert :: [Boolean] -> SAT ()
- monadic :: Monad m => ([a] -> m b) -> [m a] -> m b
- constant :: Bool -> SAT Boolean
- and :: [Boolean] -> SAT Boolean
- or :: [Boolean] -> SAT Boolean
- xor :: [Boolean] -> SAT Boolean
- fun2 :: (Bool -> Bool -> Bool) -> Boolean -> Boolean -> SAT Boolean
- fun3 :: (Bool -> Bool -> Bool -> Bool) -> Boolean -> Boolean -> Boolean -> SAT Boolean
- monadic :: Monad m => ([a] -> m b) -> [m a] -> m b
Documentation
fun2 :: (Bool -> Bool -> Bool) -> Boolean -> Boolean -> SAT BooleanSource
implement the function by giving a full CNF that determines the outcome