jukebox-0.2.3: A first-order reasoning toolbox

Safe HaskellNone
LanguageHaskell98

Jukebox.Clausify

Documentation

newtype ClausifyFlags Source

Constructors

ClausifyFlags 

Fields

splitting :: Bool
 

Instances

clausifyFlags :: OptionParser ClausifyFlags Source

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

split :: Form -> [Form] Source

clausForm :: String -> 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