what4-1.6.3: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2015-2020
LicenseBSD3
MaintainerRob Dockins <rdockins@galois.com>
Safe HaskellNone
LanguageHaskell2010

What4.Solver

Description

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

Synopsis

Solver Adapters

data SolverAdapter (st :: Type -> Type) Source #

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

Instances

Instances details
Show (SolverAdapter st) Source # 
Instance details

Defined in What4.Solver.Adapter

Methods

showsPrec :: Int -> SolverAdapter st -> ShowS

show :: SolverAdapter st -> String

showList :: [SolverAdapter st] -> ShowS

Eq (SolverAdapter st) Source # 
Instance details

Defined in What4.Solver.Adapter

Methods

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

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

Ord (SolverAdapter st) Source # 
Instance details

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

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

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.

solverAdapterOptions :: forall (st :: Type -> Type). [SolverAdapter st] -> IO ([ConfigDesc], IO (SolverAdapter st)) Source #

data LogData Source #

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

smokeTest :: forall t (st :: Type -> Type) fs. ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe SomeException) Source #

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

ABC (external, via SMT-Lib2)

data ExternalABC Source #

Constructors

ExternalABC 

Instances

Instances details
Show ExternalABC Source # 
Instance details

Defined in What4.Solver.ExternalABC

Methods

showsPrec :: Int -> ExternalABC -> ShowS

show :: ExternalABC -> String

showList :: [ExternalABC] -> ShowS

SMTLib2GenericSolver ExternalABC Source # 
Instance details

Defined in What4.Solver.ExternalABC

Methods

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

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

defaultFeatures :: ExternalABC -> ProblemFeatures Source #

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

supportsResetAssertions :: ExternalABC -> Bool Source #

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

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

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

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

SMTLib2Tweaks ExternalABC Source # 
Instance details

Defined in What4.Solver.ExternalABC

externalABCAdapter :: forall (st :: Type -> Type). SolverAdapter st Source #

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

writeABCSMT2File :: forall t (st :: Type -> Type) fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO () Source #

Bitwuzla

data Bitwuzla Source #

Constructors

Bitwuzla 

Instances

Instances details
Show Bitwuzla Source # 
Instance details

Defined in What4.Solver.Bitwuzla

Methods

showsPrec :: Int -> Bitwuzla -> ShowS

show :: Bitwuzla -> String

showList :: [Bitwuzla] -> ShowS

SMTLib2GenericSolver Bitwuzla Source # 
Instance details

Defined in What4.Solver.Bitwuzla

Methods

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

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

defaultFeatures :: Bitwuzla -> ProblemFeatures Source #

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

supportsResetAssertions :: Bitwuzla -> Bool Source #

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

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

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

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

SMTLib2Tweaks Bitwuzla Source # 
Instance details

Defined in What4.Solver.Bitwuzla

OnlineSolver (Writer Bitwuzla) Source # 
Instance details

Defined in What4.Solver.Bitwuzla

Methods

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

shutdownSolverProcess :: SolverProcess scope (Writer Bitwuzla) -> IO (ExitCode, Text) Source #

bitwuzlaAdapter :: forall (st :: Type -> Type). SolverAdapter st Source #

bitwuzlaTimeout :: ConfigOption BaseIntegerType Source #

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

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

withBitwuzla Source #

Arguments

:: forall t (st :: Type -> Type) fs a. ExprBuilder t st fs 
-> FilePath

Path to Bitwuzla executable

-> LogData 
-> (Session t Bitwuzla -> IO a)

Action to run

-> IO a 

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

Boolector

data Boolector Source #

Constructors

Boolector 

Instances

Instances details
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 :: 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

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 #

boolectorAdapter :: forall (st :: Type -> Type). SolverAdapter st Source #

boolectorTimeout :: ConfigOption BaseIntegerType Source #

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

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

withBoolector Source #

Arguments

:: forall t (st :: Type -> Type) fs a. 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.

CVC4

data CVC4 Source #

Constructors

CVC4 

Instances

Instances details
Show CVC4 Source # 
Instance details

Defined in What4.Solver.CVC4

Methods

showsPrec :: Int -> CVC4 -> ShowS

show :: CVC4 -> String

showList :: [CVC4] -> ShowS

SMTLib2GenericSolver CVC4 Source # 
Instance details

Defined in What4.Solver.CVC4

Methods

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

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

defaultFeatures :: CVC4 -> ProblemFeatures Source #

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

supportsResetAssertions :: CVC4 -> Bool Source #

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

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

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

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

SMTLib2Tweaks CVC4 Source # 
Instance details

Defined in What4.Solver.CVC4

OnlineSolver (Writer CVC4) Source # 
Instance details

Defined in What4.Solver.CVC4

Methods

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

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

cvc4Adapter :: forall (st :: Type -> Type). SolverAdapter st Source #

cvc4Timeout :: ConfigOption BaseIntegerType Source #

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

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

writeCVC4SMT2File :: forall t (st :: Type -> Type) fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO () Source #

withCVC4 Source #

Arguments

:: forall t (st :: Type -> Type) fs a. 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.

CVC5

data CVC5 Source #

Constructors

CVC5 

Instances

Instances details
Show CVC5 Source # 
Instance details

Defined in What4.Solver.CVC5

Methods

showsPrec :: Int -> CVC5 -> ShowS

show :: CVC5 -> String

showList :: [CVC5] -> ShowS

SMTLib2GenericSolver CVC5 Source # 
Instance details

Defined in What4.Solver.CVC5

Methods

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

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

defaultFeatures :: CVC5 -> ProblemFeatures Source #

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

supportsResetAssertions :: CVC5 -> Bool Source #

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

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

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

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

SMTLib2Tweaks CVC5 Source # 
Instance details

Defined in What4.Solver.CVC5

OnlineSolver (Writer CVC5) Source # 
Instance details

Defined in What4.Solver.CVC5

Methods

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

shutdownSolverProcess :: SolverProcess scope (Writer CVC5) -> IO (ExitCode, Text) Source #

cvc5Adapter :: forall (st :: Type -> Type). SolverAdapter st Source #

cvc5Timeout :: ConfigOption BaseIntegerType Source #

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

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

writeCVC5SMT2File :: forall t (st :: Type -> Type) fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO () Source #

withCVC5 Source #

Arguments

:: forall t (st :: Type -> Type) fs a. ExprBuilder t st fs 
-> FilePath

Path to cvc5 executable

-> LogData 
-> (Session t CVC5 -> IO a)

Action to run

-> IO a 

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

DReal

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

drealAdapter :: forall (st :: Type -> Type). SolverAdapter st Source #

runDRealInOverride Source #

Arguments

:: forall t (st :: Type -> Type) fs a. ExprBuilder t st fs 
-> LogData 
-> [BoolExpr t]

propositions to check

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

writeDRealSMT2File :: forall t (st :: Type -> Type) fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO () Source #

STP

data STP Source #

Constructors

STP 

Instances

Instances details
Show STP Source # 
Instance details

Defined in What4.Solver.STP

Methods

showsPrec :: Int -> STP -> ShowS

show :: STP -> String

showList :: [STP] -> ShowS

SMTLib2GenericSolver STP Source # 
Instance details

Defined in What4.Solver.STP

Methods

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

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

defaultFeatures :: STP -> ProblemFeatures Source #

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

supportsResetAssertions :: STP -> Bool Source #

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

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

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

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

SMTLib2Tweaks STP Source # 
Instance details

Defined in What4.Solver.STP

OnlineSolver (Writer STP) Source # 
Instance details

Defined in What4.Solver.STP

Methods

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

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

stpAdapter :: forall (st :: Type -> Type). SolverAdapter st Source #

stpTimeout :: ConfigOption BaseIntegerType Source #

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

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

withSTP Source #

Arguments

:: forall t (st :: Type -> Type) fs a. 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.

Yices

yicesAdapter :: forall (t :: Type -> Type). SolverAdapter t Source #

yicesEnableInteractive :: ConfigOption BaseBoolType Source #

Enable interactive mode (necessary for per-goal timeouts)

yicesGoalTimeout :: ConfigOption BaseIntegerType Source #

Set a per-goal timeout in seconds.

runYicesInOverride :: forall t (st :: Type -> Type) fs a. ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t) () -> IO a) -> IO a Source #

Run writer and get a yices result.

writeYicesFile Source #

Arguments

:: forall t (st :: Type -> Type) fs. 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.

Z3

data Z3 Source #

Constructors

Z3 

Instances

Instances details
Show Z3 Source # 
Instance details

Defined in What4.Solver.Z3

Methods

showsPrec :: Int -> Z3 -> ShowS

show :: Z3 -> String

showList :: [Z3] -> ShowS

SMTLib2GenericSolver Z3 Source # 
Instance details

Defined in What4.Solver.Z3

Methods

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

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

defaultFeatures :: Z3 -> ProblemFeatures Source #

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

supportsResetAssertions :: Z3 -> Bool Source #

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

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

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

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

SMTLib2Tweaks Z3 Source # 
Instance details

Defined in What4.Solver.Z3

OnlineSolver (Writer Z3) Source # 
Instance details

Defined in What4.Solver.Z3

Methods

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

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

z3Timeout :: ConfigOption BaseIntegerType Source #

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

z3Adapter :: forall (st :: Type -> Type). SolverAdapter st Source #

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

withZ3 Source #

Arguments

:: forall t (st :: Type -> Type) fs a. 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.