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 :: sym ~ ExprBuilder t st fs => sym -> 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.

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