Z3Goal
public class Z3Goal : Z3RefCountedObject
Set of formulas that can be solved and/or transformed using tactics and solvers.
-
The context this
Z3Goal
belongsDeclaration
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 formulafalse
.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 isfalse
, adding new formulas is a no-op. If the formulaast
istrue
, then nothing is added. If the formulaast
isfalse
, then the entire goal is replaced by the formulafalse
.Declaration
Swift
public func assert(_ ast: Z3Bool)
-
Erase all formulas from this goal.
Declaration
Swift
public func reset()
-
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