Copyright	(c) Galois Inc 2014-2020
License	BSD3
Maintainer	Rob Dockins <rdockins@galois.com>
Stability	provisional
Safe Haskell	None
Language	Haskell2010

What4.Solver.Boolector

Description

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

Synopsis

data Boolector = Boolector
boolectorPath :: ConfigOption (BaseStringType Unicode)
boolectorOptions :: [ConfigDesc]
boolectorAdapter :: SolverAdapter st
runBoolectorInOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a
withBoolector :: ExprBuilder t st fs -> FilePath -> LogData -> (Session t Boolector -> IO a) -> IO a
boolectorFeatures :: ProblemFeatures

Documentation

data Boolector Source #

Constructors

Boolector

Instances

Show Boolector Source #
Instance details Defined in What4.Solver.Boolector Methods showsPrec :: Int -> Boolector -> ShowS # show :: Boolector -> String # showList :: [Boolector] -> ShowS #
SMTLib2GenericSolver Boolector Source #
Instance details Defined in What4.Solver.Boolector Methods defaultSolverPath :: Boolector -> ExprBuilder t st fs -> IO FilePath Source # defaultSolverArgs :: Boolector -> ExprBuilder t st fs -> IO [String] Source # defaultFeatures :: Boolector -> ProblemFeatures Source # getErrorBehavior :: Boolector -> WriterConn t (Writer Boolector) -> InputStream Text -> IO ErrorBehavior Source # supportsResetAssertions :: Boolector -> Bool Source # setDefaultLogicAndOptions :: WriterConn t (Writer Boolector) -> IO () Source # newDefaultWriter :: Boolector -> AcknowledgementAction t (Writer Boolector) -> ProblemFeatures -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer Boolector)) Source # withSolver :: Boolector -> AcknowledgementAction t (Writer Boolector) -> ProblemFeatures -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t Boolector -> IO b) -> IO b Source # runSolverInOverride :: Boolector -> AcknowledgementAction t (Writer Boolector) -> ProblemFeatures -> ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO b) -> IO b Source #
SMTLib2Tweaks Boolector Source #
Instance details Defined in What4.Solver.Boolector Methods smtlib2tweaks :: Boolector Source # smtlib2arrayType :: [Sort] -> Sort -> Sort Source # smtlib2arrayConstant :: Maybe ([Sort] -> Sort -> Term -> Term) Source # smtlib2arraySelect :: Term -> [Term] -> Term Source # smtlib2arrayUpdate :: Term -> [Term] -> Term -> Term Source # smtlib2StringSort :: Sort Source # smtlib2StringTerm :: ByteString -> Term Source # smtlib2StringLength :: Term -> Term Source # smtlib2StringAppend :: [Term] -> Term Source # smtlib2StringContains :: Term -> Term -> Term Source # smtlib2StringIndexOf :: Term -> Term -> Term -> Term Source # smtlib2StringIsPrefixOf :: Term -> Term -> Term Source # smtlib2StringIsSuffixOf :: Term -> Term -> Term Source # smtlib2StringSubstring :: Term -> Term -> Term -> Term Source # smtlib2StructSort :: [Sort] -> Sort Source # smtlib2StructCtor :: [Term] -> Term Source # smtlib2StructProj :: Int -> Int -> Term -> Term Source # smtlib2declareStructCmd :: Int -> Maybe Command Source #
OnlineSolver (Writer Boolector) Source #
Instance details Defined in What4.Solver.Boolector Methods startSolverProcess :: ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer Boolector)) Source # shutdownSolverProcess :: SolverProcess scope (Writer Boolector) -> IO (ExitCode, Text) Source #

boolectorPath :: ConfigOption (BaseStringType Unicode) Source #

Path to boolector

boolectorOptions :: [ConfigDesc] Source #

boolectorAdapter :: SolverAdapter st Source #

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

withBoolector Source #

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 Source #