Documentation

newtype ClausifyFlags Source #

clausifyFlags :: OptionParser ClausifyFlags Source #

clausify :: ClausifyFlags -> Problem Form -> CNF Source #

split :: Form -> [Form] Source #

clausForm :: AxKind -> Input Form -> M [Input Clause] Source #

miniscope :: Form -> M Form Source #

forAll :: Set Variable -> Form -> M Form Source #

forAllOr :: Set Variable -> [(Form, Set Variable)] -> M Form Source #

removeEquiv :: Form -> M [Form] Source #

removeEquivAux :: Bool -> Form -> M ([Form], Form, Form) Source #

makeCopyable :: Bool -> Form -> Form -> M ([Form], Form, Form) Source #

removeExists :: Form -> M Form Source #

removeExpensiveOr :: Form -> M [Form] Source #

type Cost = (Integer, Integer) Source #

unitCost :: Cost Source #

andCost :: [Cost] -> Cost Source #

orCost :: [Cost] -> Cost Source #

removeExpensiveOrAux :: Form -> M ([Form], Form, Cost) Source #

makeOr :: [(Form, Cost)] -> M ([Form], Form, Cost) Source #

cnf :: Form -> [[Literal]] Source #

cross :: [[[Literal]]] -> [[Literal]] Source #

simplifyCNF :: [[Literal]] -> [[Literal]] Source #

type M = ReaderT Tag NameM Source #

run :: M a -> NameM a Source #

skolemName :: Named a => String -> a -> M Name Source #

withName :: Tag -> M a -> M a Source #

getName :: M Tag Source #

skolem :: Variable -> Set Variable -> M Term Source #

literal :: String -> Set Variable -> M Atomic Source #