jukebox-0.1.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 :: ByteString -> Form -> M [Input Clause] Source

miniscope :: Form -> M Form Source

forAll :: NameMap Variable -> Form -> M Form Source

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

removeEquiv :: Form -> M [Form] Source

removeEquivAux :: Bool -> Form -> M (Seq Form, Form, Form) Source

makeCopyable :: Bool -> Form -> Form -> M (Seq 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 (Seq Form, Form, Cost) Source

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

cnf :: Form -> Seq (Seq Literal) Source

cross :: Seq (Seq (Seq Literal)) -> Seq (Seq Literal) Source

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

type M = ReaderT Tag (StateT Int NameM) Source

run :: M a -> NameM a Source

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

nextSk :: M Int Source

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

getName :: M Tag Source

skolem :: Variable -> NameMap Variable -> M Term Source

literal :: String -> NameMap Variable -> M Atomic Source