Z3Goal

public class Z3Goal : Z3RefCountedObject

Set of formulas that can be solved and/or transformed using tactics and solvers.

  • The context this Z3Goal belongs

    Declaration

    Swift

    public let context: Z3Context

  • Return the depth of this goal. It tracks how many transformations were applied to it.

    Declaration

    Swift

    public var depth: UInt32 { get }

  • Returns true if this goal contains the formula false.

    Declaration

    Swift

    public var isInconsistent: Bool { get }

  • Return the number of formulas in this goal.

    Declaration

    Swift

    public var size: UInt32 { get }

  • Return a formula from this goal at a given index.

    Precondition

    index < size

    Declaration

    Swift

    public subscript(index: UInt32) -> Z3Bool { get }

  • Return a formula from this goal at a given index.

    Precondition

    index < size

    Declaration

    Swift

    public subscript(index: Int) -> Z3Bool { get }

  • Return the number of formulas, subformulas and terms in the given goal.

    Declaration

    Swift

    public var expressionCount: UInt32 { get }

  • Return true if the goal is empty, and it is precise or the product of a under approximation.

    Declaration

    Swift

    public var isDecidedSat: Bool { get }

  • Return true if the goal contains false, and it is precise or the product of an over approximation.

    Declaration

    Swift

    public var isDecidedUnsat: Bool { get }

  • Add a new formula ast to the given goal. The formula is split according to the following procedure that is applied until a fixed-point: Conjunctions are split into separate formulas. Negations are distributed over disjunctions, resulting in separate formulas. If the goal is false, adding new formulas is a no-op. If the formula ast is true, then nothing is added. If the formula ast is false, then the entire goal is replaced by the formula false.

    Declaration

    Swift

    public func assert(_ ast: Z3Bool)

  • Erase all formulas from this goal.

    Declaration

    Swift

    public func reset()

  • Convert a model of the formulas of a goal to a model of an original goal. The model may be nil, in which case the returned model is valid if the goal was established satisfiable.

    Declaration

    Swift

    public func convertModel(_ model: Z3Model?) -> Z3Model

  • Convert this goal into a string.

    Declaration

    Swift

    public func toString() -> String

  • Convert this goal into a DIMACS formatted string.

    The goal must be in CNF. You can convert a goal to CNF by applying the tseitin-cnf tactic. Bit-vectors are not automatically converted to Booleans either, so if the caller intends to preserve satisfiability, it should apply bit-blasting tactics. Quantifiers and theory atoms will not be encoded.

    Declaration

    Swift

    public func toDimacsString(includeNames: Bool) -> String

  • Copy this goal from the context source to the context newContext target.

    Declaration

    Swift

    public func translate(to newContext: Z3Context) -> Z3Goal