Z3Solver
public class Z3Solver : Z3RefCountedObject
Incremental solver, possibly specialized by a particular tactic or logic.
-
The context this
Z3Solver
belongsDeclaration
Swift
public let context: Z3Context
-
Return a string describing all solver available parameters.
Seealso
getParamDescrs
Seealso
setParams
Declaration
Swift
public func getHelp() -> String
-
Set this solver using the given parameters.
Seealso
getHelp
Seealso
getParamDescrs
Declaration
Swift
public func setParams(_ params: Z3Params)
-
Return the parameter description set for this solver object.
Declaration
Swift
public func getParamDescrs() -> Z3ParamDescrs
-
Ad-hoc method for importing model conversion from solver.
This method is used for scenarios where
other
has been used to solve a set of formulas and was interrupted. Theself
solver may be a strengthening ofother
obtained from cubing (assigning a subset of literals or adding constraints over the assertions available inother
). Ifself
ends up being satisfiable, the model forself
may not correspond to a model of the original formula due to inprocessing inother
. This method is used to take the side-effect of inprocessing into account when returning a model forself
.Declaration
Swift
public func importModelConverter(from other: Z3Solver)
-
Solver local interrupt.
Normally you should use
Z3Context.interrupt()
to cancel solvers because only one solver is enabled concurrently per context. However, per GitHub issue #1006, there are use cases where it is more convenient to cancel a specific solver. Solvers that are not selected for interrupts are left alone.Declaration
Swift
public func interrupt()
-
Create a backtracking point.
The solver contains a stack of assertions.
Seealso
getNumScopes()
Seealso
pop()
Declaration
Swift
public func push()
-
Backtrack
n
backtracking points.Precondition
n <= getNumScopes()
Seealso
getNumScopes()
Seealso
push()
Declaration
Swift
public func pop(_ n: UInt32)
-
Remove all assertions from the solver.
Seealso
assert()
Seealso
assertAndTrack()
Declaration
Swift
public func reset()
-
Declaration
Swift
public func getNumScopes() -> UInt32
-
Assert a constraint into the solver.
The methods
check
andcheckAssumptions
should be used to check whether the logical context is consistent or not.Declaration
Swift
public func assert(_ exp: Z3Bool)
-
Assert a list of constraints into the solver.
The methods
check
andcheckAssumptions
should be used to check whether the logical context is consistent or not.Declaration
Swift
public func assert(_ constraints: [Z3Bool])
-
Assert a constraint
a
into the solver, and track it (in the unsat) core using the Boolean constantp
.This API is an alternative to
checkAssumptions
for extracting unsat cores. Both APIs can be used in the same solver. The unsat core will contain a combination of the Boolean variables provided usingassertAndTrack
and the Boolean literals provided usingcheckAssumptions
.Precondition
a
must be a Boolean expressionPrecondition
p
must be a Boolean constant (aka variable).Seealso
assert()
Seealso
reset()
-
Declaration
Swift
public func fromFile(_ fileName: String) throws
-
Declaration
Swift
public func fromString(_ s: String) throws
-
Return the set of asserted formulas on the solver.
Declaration
Swift
public func getAssertions() -> Z3AstVector
-
Return the set of units modulo model conversion.
Declaration
Swift
public func getUnits() -> Z3AstVector
-
Return the trail modulo model conversion, in order of decision level The decision level can be retrieved using
getLevel()
based on the trail.Declaration
Swift
public func getTrail() -> Z3AstVector
-
Return the set of non units in the solver state.
Declaration
Swift
public func getNonUnits() -> Z3AstVector
-
retrieve the decision depth of Boolean literals (variables or their negations). Assumes a check-sat call and no other calls (to extract models) have been invoked.
Declaration
Swift
public func getLevels(_ literals: Z3AstVector, count: UInt32) -> [UInt32]
-
Check whether the assertions in a given solver are consistent or not.
The method
getModel()
retrieves a model if the assertions is satisfiable (i.e., the result isStatus.satisfiable
) and model construction is enabled.Note that if the call returns
Status.unknown
, Z3 does not ensure that calls togetModel()
succeed and any models produced in this case are not guaranteed to satisfy the assertions.The function
getProof()
retrieves a proof if proof generation was enabled when the context was created, and the assertions are unsatisfiable (i.e., the result isStatus.unsatisfiable
).Declaration
Swift
public func check() -> Status
-
Check whether the assertions in the given solver and optional assumptions are consistent or not.
The function
getUnsatCore()
retrieves the subset of the assumptions used in the unsatisfiability proof produced by Z3. -
Retrieve consequences from solver that determine values of the supplied function symbols.
Declaration
Swift
public func getConsequences(assumptions: [Z3Bool], variables: [AnyZ3Ast], consequences: Z3AstVector) -> Status
-
Retrieve the proof for the last
check()
orcheckAssumptions()
The error handler is invoked if proof generation is not enabled, or if the commands above were not invoked for the given solver, or if the result was different from
Status.unsatisfiable
.Declaration
Swift
public func getProof() -> AnyZ3Ast?
-
Retrieve the unsat core for the last
checkAssumptions()
The unsat core is a subset of the assumptions
a
.By default, the unsat core will not be minimized. Generation of a minimized unsat core can be enabled via the
"sat.core.minimize"
and"smt.core.minimize"
settings for SAT and SMT cores respectively. Generation of minimized unsat cores will be more expensive.Declaration
Swift
public func getUnsatCore() -> Z3AstVector
-
Return a brief justification for an “unknown” result (i.e.,
Status.unknown
) for the commandscheck
andcheckAssumptions
Declaration
Swift
public func getReasonUnknown() -> String
-
Return statistics for the given solver.
Declaration
Swift
public func getStatistics() -> Z3Stats
-
Convert a solver into a string.
Seealso
fromFile()
Seealso
fromString()
Declaration
Swift
public func toString() -> String
-
Convert a solver into a DIMACS formatted string.
Seealso
Z3_goal_to_diamcs_string
for requirements.Declaration
Swift
public func toDimacsString(includeNames: Bool) -> String