What4.Solver

The module reexports the most commonly used types and operations for interacting with solvers.

Solver Adapters

data SolverAdapter st

The main interface for interacting with a solver in an "offline" fashion, which means that a new solver process is started for each query.

Constructors

SolverAdapter

Fields

• solver_adapter_name :: !String
• solver_adapter_config_options :: ![ConfigDesc]

  Configuration options relevant to this solver adapter

• solver_adapter_check_sat :: !(forall t fs a. ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a)

  Operation to check the satisfiability of a formula. The final argument is a callback that calculates the ultimate result from a SatResult and operations for finding model values in the event of a SAT result. Note: the evaluation functions may cease to be avaliable after the callback completes, so any necessary information should be extracted from them before returning.

• solver_adapter_write_smt2 :: !(forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ())

  Write an SMTLib2 problem instance onto the given handle, incorporating any solver-specific tweaks appropriate to this solver

Instances

Eq (SolverAdapter st)

Defined in What4.Solver.Adapter

Methods

(==) :: SolverAdapter st -> SolverAdapter st -> Bool

(/=) :: SolverAdapter st -> SolverAdapter st -> Bool

Ord (SolverAdapter st)

Defined in What4.Solver.Adapter

Methods

compare :: SolverAdapter st -> SolverAdapter st -> Ordering

(<) :: SolverAdapter st -> SolverAdapter st -> Bool

(<=) :: SolverAdapter st -> SolverAdapter st -> Bool

(>) :: SolverAdapter st -> SolverAdapter st -> Bool

(>=) :: SolverAdapter st -> SolverAdapter st -> Bool

max :: SolverAdapter st -> SolverAdapter st -> SolverAdapter st

min :: SolverAdapter st -> SolverAdapter st -> SolverAdapter st

Show (SolverAdapter st)

Defined in What4.Solver.Adapter

Methods

showsPrec :: Int -> SolverAdapter st -> ShowS

show :: SolverAdapter st -> String

showList :: [SolverAdapter st] -> ShowS

type ExprRangeBindings t = RealExpr t -> IO (Maybe Rational, Maybe Rational)

Function that calculates upper and lower bounds for real-valued elements. This type is used for solvers (e.g., dReal) that give only approximate solutions.

defaultSolverAdapter :: ConfigOption (BaseStringType Unicode)

solverAdapterOptions :: [SolverAdapter st] -> IO ([ConfigDesc], IO (SolverAdapter st))

data LogData

A collection of operations for producing output from solvers. Solvers can produce messages at varying verbosity levels that might be appropriate for user output by using the logCallbackVerbose operation. If a logHandle is provided, the entire interaction sequence with the solver will be mirrored into that handle.

Constructors

LogData

Fields

• logCallbackVerbose :: Int -> String -> IO ()

  takes a verbosity and a message to log

• logVerbosity :: Int

  the default verbosity; typical default is 2

• logReason :: String

  the reason for performing the operation

• logHandle :: Maybe Handle

  handle on which to mirror solver input/responses

logCallback :: LogData -> String -> IO ()

defaultLogData :: LogData

smokeTest :: ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe SomeException)

Test the ability to interact with a solver by peforming a check-sat query on a trivially unsatisfiable problem.

module What4.SatResult

Boolector

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 :: Boolector -> ExprBuilder t st fs -> IO FilePath

defaultSolverArgs :: 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 :: Boolector -> AcknowledgementAction t (Writer Boolector) -> ProblemFeatures -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer Boolector))

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

runSolverInOverride :: 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

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 :: ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer Boolector))

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

boolectorAdapter :: SolverAdapter st

boolectorPath :: ConfigOption (BaseStringType Unicode)

Path to boolector

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.

boolectorOptions :: [ConfigDesc]

boolectorFeatures :: ProblemFeatures

CVC4

data CVC4

Constructors

CVC4

Instances

Show CVC4

Defined in What4.Solver.CVC4

Methods

showsPrec :: Int -> CVC4 -> ShowS

show :: CVC4 -> String

showList :: [CVC4] -> ShowS

SMTLib2GenericSolver CVC4

Defined in What4.Solver.CVC4

Methods

defaultSolverPath :: CVC4 -> ExprBuilder t st fs -> IO FilePath

defaultSolverArgs :: CVC4 -> ExprBuilder t st fs -> IO [String]

defaultFeatures :: CVC4 -> ProblemFeatures

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

supportsResetAssertions :: CVC4 -> Bool

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

newDefaultWriter :: CVC4 -> AcknowledgementAction t (Writer CVC4) -> ProblemFeatures -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer CVC4))

withSolver :: CVC4 -> AcknowledgementAction t (Writer CVC4) -> ProblemFeatures -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t CVC4 -> IO b) -> IO b

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

SMTLib2Tweaks CVC4

Defined in What4.Solver.CVC4

Methods

smtlib2tweaks :: CVC4

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 CVC4)

Defined in What4.Solver.CVC4

Methods

startSolverProcess :: ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer CVC4))

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

cvc4Adapter :: SolverAdapter st

cvc4Path :: ConfigOption (BaseStringType Unicode)

Path to cvc4

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

writeCVC4SMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()

withCVC4

Arguments

:: ExprBuilder t st fs

-> FilePath

Path to CVC4 executable

-> LogData

-> (Session t CVC4 -> IO a)

Action to run

-> IO a

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

cvc4Options :: [ConfigDesc]

cvc4Features :: ProblemFeatures

DReal

data DReal

Constructors

DReal

Instances

Show DReal

Defined in What4.Solver.DReal

Methods

showsPrec :: Int -> DReal -> ShowS

show :: DReal -> String

showList :: [DReal] -> ShowS

SMTLib2Tweaks DReal

Defined in What4.Solver.DReal

Methods

smtlib2tweaks :: DReal

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

type DRealBindings = Map Text (Either Bool (Maybe Rational, Maybe Rational))

drealAdapter :: SolverAdapter st

drealPath :: ConfigOption (BaseStringType Unicode)

Path to dReal

runDRealInOverride

Arguments

:: ExprBuilder t st fs

-> LogData

-> [BoolExpr t]

propositions to check

-> (SatResult (WriterConn t (Writer DReal), DRealBindings) () -> IO a)

-> IO a

writeDRealSMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()

STP

data STP

Constructors

STP

Instances

Show STP

Defined in What4.Solver.STP

Methods

showsPrec :: Int -> STP -> ShowS

show :: STP -> String

showList :: [STP] -> ShowS

SMTLib2GenericSolver STP

Defined in What4.Solver.STP

Methods

defaultSolverPath :: STP -> ExprBuilder t st fs -> IO FilePath

defaultSolverArgs :: STP -> ExprBuilder t st fs -> IO [String]

defaultFeatures :: STP -> ProblemFeatures

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

supportsResetAssertions :: STP -> Bool

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

newDefaultWriter :: STP -> AcknowledgementAction t (Writer STP) -> ProblemFeatures -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer STP))

withSolver :: STP -> AcknowledgementAction t (Writer STP) -> ProblemFeatures -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t STP -> IO b) -> IO b

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

SMTLib2Tweaks STP

Defined in What4.Solver.STP

Methods

smtlib2tweaks :: STP

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 STP)

Defined in What4.Solver.STP

Methods

startSolverProcess :: ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer STP))

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

stpAdapter :: SolverAdapter st

stpPath :: ConfigOption (BaseStringType Unicode)

Path to stp

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

withSTP

Arguments

:: ExprBuilder t st fs

-> FilePath

Path to STP executable

-> LogData

-> (Session t STP -> IO a)

Action to run

-> IO a

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

stpOptions :: [ConfigDesc]

stpFeatures :: ProblemFeatures

Yices

yicesAdapter :: SolverAdapter t

yicesPath :: ConfigOption (BaseStringType Unicode)

Path to yices

runYicesInOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t) () -> IO a) -> IO a

Run writer and get a yices result.

writeYicesFile

Arguments

:: ExprBuilder t st fs

Builder for getting current bindings.

-> FilePath

Path to file

-> BoolExpr t

Predicate to check

-> IO ()

Write a yices file that checks the satisfiability of the given predicate.

yicesOptions :: [ConfigDesc]

yicesDefaultFeatures :: ProblemFeatures

Z3

data Z3

Constructors

Z3

Instances

Show Z3

Defined in What4.Solver.Z3

Methods

showsPrec :: Int -> Z3 -> ShowS

show :: Z3 -> String

showList :: [Z3] -> ShowS

SMTLib2GenericSolver Z3

Defined in What4.Solver.Z3

Methods

defaultSolverPath :: Z3 -> ExprBuilder t st fs -> IO FilePath

defaultSolverArgs :: Z3 -> ExprBuilder t st fs -> IO [String]

defaultFeatures :: Z3 -> ProblemFeatures

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

supportsResetAssertions :: Z3 -> Bool

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

newDefaultWriter :: Z3 -> AcknowledgementAction t (Writer Z3) -> ProblemFeatures -> ExprBuilder t st fs -> OutputStream Text -> InputStream Text -> IO (WriterConn t (Writer Z3))

withSolver :: Z3 -> AcknowledgementAction t (Writer Z3) -> ProblemFeatures -> ExprBuilder t st fs -> FilePath -> LogData -> (Session t Z3 -> IO b) -> IO b

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

SMTLib2Tweaks Z3

Defined in What4.Solver.Z3

Methods

smtlib2tweaks :: Z3

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 Z3)

Defined in What4.Solver.Z3

Methods

startSolverProcess :: ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer Z3))

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

z3Path :: ConfigOption (BaseStringType Unicode)

Path to Z3

z3Adapter :: SolverAdapter st

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

withZ3

Arguments

:: ExprBuilder t st fs

-> FilePath

Path to Z3 executable

-> LogData

-> (Session t Z3 -> IO a)

Action to run

-> IO a

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

z3Options :: [ConfigDesc]

z3Features :: ProblemFeatures