What4.Solver.Z3

Z3-specific tweaks to the basic SMTLib2 solver interface.

Documentation

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

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

defaultFeatures :: Z3 -> ProblemFeatures

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

supportsResetAssertions :: Z3 -> Bool

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

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

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

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

SMTLib2Tweaks Z3

Defined in What4.Solver.Z3

Methods

smtlib2tweaks :: Z3

smtlib2exitCommand :: Maybe Command

smtlib2arrayType :: [Sort] -> Sort -> Sort

smtlib2arrayConstant :: Maybe ([Sort] -> Sort -> Term -> Term)

smtlib2arraySelect :: Term -> [Term] -> Term

smtlib2arrayUpdate :: Term -> [Term] -> Term -> Term

smtlib2StringSort :: Sort

smtlib2StringTerm :: Text -> 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 :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer Z3))

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

z3Adapter :: SolverAdapter st

z3Path :: ConfigOption (BaseStringType Unicode)

Path to Z3

z3Timeout :: ConfigOption BaseIntegerType

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

z3Options :: [ConfigDesc]

z3Tactic :: ConfigOption (BaseStringType Unicode)

Z3 tactic

z3TacticDefault :: Text

z3Features :: ProblemFeatures

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.

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

runZ3Horn :: forall sym t st fs. sym ~ ExprBuilder t st fs => sym -> Bool -> LogData -> [SomeSymFn sym] -> [BoolExpr t] -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())

Check the satisfiability of a set of constrained Horn clauses (CHCs).

CHCs are represented as pure SMT-LIB2 implications. For more information, see the Z3 guide.

There are two ways to solve the CHCs: either by directly solving the problem as is, or by transforming the problem into a set of linear integer arithmetic (LIA) CHCs and solving that instead. The latter is done by replacing all bitvector (BV) operations with LIA operations, and replacing all BV variables with LIA variables. This transformation is not sound, but in practice it is a useful heuristic. Then the result is transformed back into a BV result, and checked for satisfiability. The satisfiability check is necessary because the transformation is not sound, so LIA solution may not be a solution to the BV CHCs.

writeZ3HornSMT2File :: sym ~ ExprBuilder t st fs => sym -> Bool -> Handle -> [SomeSymFn sym] -> [BoolExpr t] -> IO ()