Z3Solver

public class Z3Solver : Z3RefCountedObject

Incremental solver, possibly specialized by a particular tactic or logic.

  • The context this Z3Solver belongs

    Declaration

    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. The self solver may be a strengthening of other obtained from cubing (assigning a subset of literals or adding constraints over the assertions available in other). If self ends up being satisfiable, the model for self may not correspond to a model of the original formula due to inprocessing in other. This method is used to take the side-effect of inprocessing into account when returning a model for self.

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

  • Return the number of backtracking points.

    Seealso

    push()

    Seealso

    pop()

    Declaration

    Swift

    public func getNumScopes() -> UInt32

  • Retrieve the model for the last check() or checkAssumptions()

    The error handler is invoked if a model is not available because the commands above were not invoked for the given solver, or if the result was .unsatisfiable.

    Declaration

    Swift

    public func getModel() -> Z3Model?

  • Assert a constraint into the solver.

    The methods check and checkAssumptions 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 and checkAssumptions 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 constant p.

    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 using assertAndTrack and the Boolean literals provided using checkAssumptions.

    Precondition

    a must be a Boolean expression

    Precondition

    p must be a Boolean constant (aka variable).

    Seealso

    assert()

    Seealso

    reset()

    Declaration

    Swift

    public func assertAndTrack(_ a: Z3Bool, _ p: Z3Bool)

  • Load solver assertions from a file.

    Seealso

    fromString()

    Seealso

    toString()

    Declaration

    Swift

    public func fromFile(_ fileName: String) throws

  • Load solver assertions from a string.

    Seealso

    fromFile()

    Seealso

    toString()

    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 is Status.satisfiable) and model construction is enabled.

    Note that if the call returns Status.unknown, Z3 does not ensure that calls to getModel() 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 is Status.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.

    Declaration

    Swift

    public func checkAssumptions(_ assumptions: [AnyZ3Ast]) -> Status

  • 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() or checkAssumptions()

    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 commands check and checkAssumptions

    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