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

What4.Solver.Z3

Description

Z3-specific tweaks to the basic SMTLib2 solver interface.

Synopsis

data Z3 = Z3
z3Adapter :: SolverAdapter st
z3Path :: ConfigOption (BaseStringType Unicode)
z3Timeout :: ConfigOption BaseIntegerType
z3Options :: [ConfigDesc]
z3Tactic :: ConfigOption (BaseStringType Unicode)
z3TacticDefault :: Text
z3Features :: ProblemFeatures
runZ3InOverride :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a
withZ3 :: ExprBuilder t st fs -> FilePath -> LogData -> (Session t Z3 -> IO a) -> IO a
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)) ())
writeZ3HornSMT2File :: 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 # 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 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 :: 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 :: ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a Source #

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 #

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