jukebox-0.1.2: A first-order reasoning toolbox

Safe HaskellNone

Jukebox.Clausify

Documentation

newtype ClausifyFlags Source

Constructors

ClausifyFlags 

Fields

splitting :: Bool
 

Instances

clausifyFlags :: OptionParser ClausifyFlagsSource

clausify :: ClausifyFlags -> Problem Form -> CNFSource

split :: Form -> [Form]Source

clausForm :: ByteString -> Form -> M [Input Clause]Source

miniscope :: Form -> M FormSource

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

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

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 FormSource

removeExpensiveOr :: Form -> M [Form]Source

type Cost = (Integer, Integer)Source

unitCost :: CostSource

andCost :: [Cost] -> CostSource

orCost :: [Cost] -> CostSource

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 aSource

skolemName :: Named a => String -> a -> M NameSource

nextSk :: M IntSource

withName :: Tag -> M a -> M aSource

getName :: M TagSource

skolem :: Variable -> NameMap Variable -> M TermSource

literal :: String -> NameMap Variable -> M AtomicSource