jukebox-0.2.19: A first-order reasoning toolbox
Jukebox.Clausify
newtype ClausifyFlags Source #
Constructors
Fields
Instances
Methods
showsPrec :: Int -> ClausifyFlags -> ShowS #
show :: ClausifyFlags -> String #
showList :: [ClausifyFlags] -> ShowS #
clausifyFlags :: OptionParser ClausifyFlags Source #
clausify :: ClausifyFlags -> Problem Form -> CNF Source #
split :: Form -> [Form] Source #
clausForm :: String -> 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 #