what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

Copyright | (c) Galois Inc 2014-2020
License | BSD3
Maintainer | Rob Dockins <rdockins@galois.com>
Stability | provisional
Safe Haskell | Safe-Inferred
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)
- boolectorTimeout :: ConfigOption BaseIntegerType
- 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

Instances details

Show Boolector Source # |
Instance details Defined in What4.Solver.Boolector Methods showsPrec :: Int -> Boolector -> ShowS Source # show :: Boolector -> String Source # showList :: [Boolector] -> ShowS Source #
SMTLib2GenericSolver Boolector Source # |

Instance details

Defined in What4.Solver.Boolector

Methods

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

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

defaultFeatures :: Boolector -> ProblemFeatures Source #

getErrorBehavior :: Boolector -> WriterConn t (Writer Boolector) -> IO ErrorBehavior Source #

supportsResetAssertions :: Boolector -> Bool Source #

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

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

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

runSolverInOverride :: forall t (st :: Type -> Type) fs b. Boolector -> AcknowledgementAction t (Writer Boolector) -> ProblemFeatures -> Maybe (ConfigOption BaseBoolType) -> 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 #

smtlib2exitCommand :: Maybe Command 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 :: Text -> 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 :: forall scope (st :: Type -> Type) fs. 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

boolectorTimeout :: ConfigOption BaseIntegerType Source #

Per-check timeout, in milliseconds (zero is none)

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 #