EVM.Solvers

Documentation

data Solver

Supported solvers

Constructors

Z3

CVC5

Bitwuzla

Custom Text

Instances

Show Solver

Defined in EVM.Solvers

Methods

showsPrec :: Int -> Solver -> ShowS

show :: Solver -> String

showList :: [Solver] -> ShowS

data SolverInstance

A running solver instance

Constructors

SolverInstance

Fields

• solvertype :: Solver
• stdin :: Handle
• stdout :: Handle
• stderr :: Handle
• process :: ProcessHandle

newtype SolverGroup

A channel representing a group of solvers

Constructors

SolverGroup (Chan Task)

data Task

A script to be executed, a list of models to be extracted in the case of a sat result, and a channel where the result should be written

Constructors

Task

Fields

• script :: SMT2
• resultChan :: Chan CheckSatResult

data CheckSatResult

The result of a call to (check-sat)

Constructors

Sat SMTCex

Unsat

Unknown

Error Text

Instances

Show CheckSatResult

Defined in EVM.Solvers

Methods

showsPrec :: Int -> CheckSatResult -> ShowS

show :: CheckSatResult -> String

showList :: [CheckSatResult] -> ShowS

Eq CheckSatResult

Defined in EVM.Solvers

Methods

(==) :: CheckSatResult -> CheckSatResult -> Bool

(/=) :: CheckSatResult -> CheckSatResult -> Bool

isSat :: CheckSatResult -> Bool

isErr :: CheckSatResult -> Bool

isUnsat :: CheckSatResult -> Bool

checkSat :: SolverGroup -> SMT2 -> IO CheckSatResult

withSolvers :: Solver -> Natural -> Maybe Natural -> (SolverGroup -> IO a) -> IO a

getModel :: SolverInstance -> CexVars -> IO SMTCex

mkTimeout :: Maybe Natural -> Text

solverArgs :: Solver -> Maybe Natural -> [Text]

Arguments used when spawing a solver instance

spawnSolver :: Solver -> Maybe Natural -> IO SolverInstance

Spawns a solver instance, and sets the various global config options that we use for our queries

stopSolver :: SolverInstance -> IO ()

Cleanly shutdown a running solver instnace

sendScript :: SolverInstance -> SMT2 -> IO (Either Text ())

Sends a list of commands to the solver. Returns the first error, if there was one.

sendCommand :: SolverInstance -> Text -> IO Text

Sends a single command to the solver, returns the first available line from the output buffer

sendLine :: SolverInstance -> Text -> IO Text

Sends a string to the solver and appends a newline, returns the first available line from the output buffer

sendLine' :: SolverInstance -> Text -> IO ()

Sends a string to the solver and appends a newline, doesn't return stdout

getValue :: SolverInstance -> Text -> IO Text

Returns a string representation of the model for the requested variable

readSExpr :: Handle -> IO [Text]

Reads lines from h until we have a balanced sexpr