what4-1.6.3: Solver-agnostic symbolic values support for issuing queries

Copyright | (c) Galois Inc 2015-2020
License | BSD3
Maintainer | Rob Dockins <rdockins@galois.com>
Stability | provisional
Safe Haskell | None
Language | Haskell2010

What4.Solver.Z3

Description

Z3-specific tweaks to the basic SMTLib2 solver interface.

Synopsis

- data Z3 = Z3
- z3Adapter :: forall (st :: Type -> Type). SolverAdapter st
- z3Path :: ConfigOption (BaseStringType Unicode)
- z3Timeout :: ConfigOption BaseIntegerType
- z3Options :: [ConfigDesc]
- z3Tactic :: ConfigOption (BaseStringType Unicode)
- z3TacticDefault :: Text
- z3Features :: ProblemFeatures
- 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
- withZ3 :: forall t (st :: Type -> Type) fs a. ExprBuilder t st fs -> FilePath -> LogData -> (Session t Z3 -> IO a) -> IO a
- writeZ3SMT2File :: forall t (st :: Type -> Type) fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ()
- runZ3Horn :: forall sym t (st :: Type -> Type) fs. sym ~ ExprBuilder t st fs => sym -> Bool -> LogData -> [SomeSymFn sym] -> [BoolExpr t] -> IO (SatResult (MapF (SymFnWrapper sym) (SymFnWrapper sym)) ())
- writeZ3HornSMT2File :: forall sym t (st :: Type -> Type) fs. sym ~ ExprBuilder t st fs => sym -> Bool -> Handle -> [SomeSymFn sym] -> [BoolExpr t] -> IO ()

# Documentation

data Z3 Source #

Constructors

Z3 |

#### Instances

Instances details

Show Z3 Source # |
Instance details Defined in What4.Solver.Z3 Methods showsPrec :: Int -> Z3 -> ShowS Source # show :: Z3 -> String Source # showList :: [Z3] -> ShowS Source #
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

Methods

smtlib2tweaks :: Z3 Source #

smtlib2exitCommand :: Maybe Command Source #

smtlib2arrayType :: [Sort] -> Sort -> Sort Source #

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

smtlib2arraySelect :: Term -> [Term] -> Term Source #

smtlib2arrayUpdate :: Term -> [Term] -> Term -> Term Source #

smtlib2StringSort :: Sort Source #

smtlib2StringTerm :: Text -> Term Source #

smtlib2StringLength :: Term -> Term Source #

smtlib2StringAppend :: [Term] -> Term Source #

smtlib2StringContains :: Term -> Term -> Term Source #

smtlib2StringIndexOf :: Term -> Term -> Term -> Term Source #

smtlib2StringIsPrefixOf :: Term -> Term -> Term Source #

smtlib2StringIsSuffixOf :: Term -> Term -> Term Source #

smtlib2StringSubstring :: Term -> Term -> Term -> Term Source #

smtlib2StructSort :: [Sort] -> Sort Source #

smtlib2StructCtor :: [Term] -> Term Source #

smtlib2StructProj :: Int -> Int -> Term -> Term Source #

smtlib2declareStructCmd :: Int -> Maybe Command Source #

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 #

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

z3Path :: ConfigOption (BaseStringType Unicode) Source #

Path to Z3

z3Timeout :: ConfigOption BaseIntegerType Source #

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

z3Options :: [ConfigDesc] Source #

z3Tactic :: ConfigOption (BaseStringType Unicode) Source #

Z3 tactic

z3TacticDefault :: Text Source #

z3Features :: ProblemFeatures 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.

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

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

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 :: forall sym t (st :: Type -> Type) fs. sym ~ ExprBuilder t st fs => sym -> Bool -> Handle -> [SomeSymFn sym] -> [BoolExpr t] -> IO () Source #