What4.Solver.Boolector

This module provides an interface for running Boolector and parsing the results back.

Documentation

data Boolector

Constructors

Boolector

Instances

Show Boolector

Defined in What4.Solver.Boolector

Methods

showsPrec :: Int -> Boolector -> ShowS

show :: Boolector -> String

showList :: [Boolector] -> ShowS

SMTLib2GenericSolver Boolector

Defined in What4.Solver.Boolector

Methods

defaultSolverPath :: forall t (st :: Type -> Type) fs. Boolector -> ExprBuilder t st fs -> IO FilePath

defaultSolverArgs :: forall t (st :: Type -> Type) fs. Boolector -> ExprBuilder t st fs -> IO [String]

defaultFeatures :: Boolector -> ProblemFeatures

getErrorBehavior :: Boolector -> WriterConn t (Writer Boolector) -> InputStream Text -> IO ErrorBehavior

supportsResetAssertions :: Boolector -> Bool

setDefaultLogicAndOptions :: WriterConn t (Writer Boolector) -> IO ()

newDefaultWriter :: forall t (st :: Type -> Type) fs. Boolector -> AcknowledgementAction t (Writer Boolector) -> ProblemFeatures -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer Boolector))

withSolver :: forall t (st :: Type -> Type) fs b. Boolector -> AcknowledgementAction t (Writer Boolector) -> ProblemFeatures -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t Boolector -> IO b) -> IO b

runSolverInOverride :: forall t (st :: Type -> Type) fs b. Boolector -> AcknowledgementAction t (Writer Boolector) -> ProblemFeatures -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b

SMTLib2Tweaks Boolector

Defined in What4.Solver.Boolector

Methods

smtlib2tweaks :: Boolector

smtlib2exitCommand :: Maybe Command

smtlib2arrayType :: [Sort] -> Sort -> Sort

smtlib2arrayConstant :: Maybe ([Sort] -> Sort -> Term -> Term)

smtlib2arraySelect :: Term -> [Term] -> Term

smtlib2arrayUpdate :: Term -> [Term] -> Term -> Term

smtlib2StringSort :: Sort

smtlib2StringTerm :: ByteString -> Term

smtlib2StringLength :: Term -> Term

smtlib2StringAppend :: [Term] -> Term

smtlib2StringContains :: Term -> Term -> Term

smtlib2StringIndexOf :: Term -> Term -> Term -> Term

smtlib2StringIsPrefixOf :: Term -> Term -> Term

smtlib2StringIsSuffixOf :: Term -> Term -> Term

smtlib2StringSubstring :: Term -> Term -> Term -> Term

smtlib2StructSort :: [Sort] -> Sort

smtlib2StructCtor :: [Term] -> Term

smtlib2StructProj :: Int -> Int -> Term -> Term

smtlib2declareStructCmd :: Int -> Maybe Command

OnlineSolver (Writer Boolector)

Defined in What4.Solver.Boolector

Methods

startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer Boolector))

shutdownSolverProcess :: SolverProcess scope (Writer Boolector) -> IO (ExitCode, Text)

boolectorPath :: ConfigOption (BaseStringType Unicode)

Path to boolector

boolectorOptions :: [ConfigDesc]

boolectorAdapter :: SolverAdapter st

runBoolectorInOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a

withBoolector

Arguments

:: ExprBuilder t st fs

-> FilePath

Path to Boolector executable

-> LogData

-> (Session t Boolector -> IO a)

Action to run

-> IO a

Run Boolector in a session. Boolector will be configured to produce models, but otherwise left with the default configuration.

boolectorFeatures :: ProblemFeatures