Jukebox.Tools.Clausify

Documentation

newtype ClausifyFlags

Constructors

ClausifyFlags

Fields

• splitting :: Bool

Instances

Show ClausifyFlags

Defined in Jukebox.Tools.Clausify

Methods

showsPrec :: Int -> ClausifyFlags -> ShowS

show :: ClausifyFlags -> String

showList :: [ClausifyFlags] -> ShowS

clausifyFlags :: OptionParser ClausifyFlags

clausify :: ClausifyFlags -> Problem Form -> CNF

split :: Form -> [Form]

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

miniscope :: Form -> M Form

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

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

removeEquiv :: Form -> M [Form]

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

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

removeExists :: Form -> M Form

removeExpensiveOr :: Form -> M [Form]

type Cost = (Integer, Integer)

unitCost :: Cost

andCost :: [Cost] -> Cost

orCost :: [Cost] -> Cost

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

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

cnf :: Form -> [[Literal]]

cross :: [[[Literal]]] -> [[Literal]]

simplifyCNF :: [[Literal]] -> [[Literal]]

type M = ReaderT Tag NameM

run :: M a -> NameM a

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

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

getName :: M Tag

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

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