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

What4.Solver.Z3

Description

Z3-specific tweaks to the basic SMTLib2 solver interface.

Synopsis

Documentation

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

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)

withZ3 Source #

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.

writeZ3SMT2File :: ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO () Source #