Z3Model
public class Z3Model : Z3RefCountedObject
Model for the constraints asserted into the logical context.
-
The context this
Z3Model
belongsDeclaration
Swift
public let context: Z3Context
-
Evaluate the AST node
t
in the given model. Returns the result in case of success, ornil
in case of failure.If
completion
istrue
, then Z3 will assign an interpretation for any constant or function that does not have an interpretation in this model. These constants and functions were essentially don’t cares.If
completion
isfalse
, then Z3 will not assign interpretations to constants for functions that do not have interpretations in this model. Evaluation behaves as the identify function in this case.The evaluation may fail for the following reasons:
t
contains a quantifier.the current model is partial, that is, it doesn’t have a complete interpretation for uninterpreted functions. That is, the option
MODEL_PARTIAL=true
was used.t
is type incorrect.Z3Context.interrupt()
was invoked during evaluation.
-
Evaluate the AST node
t
in the given model. Returns the result in case of success, ornil
in case of failure.Type-erased version.
If
completion
istrue
, then Z3 will assign an interpretation for any constant or function that does not have an interpretation in this model. These constants and functions were essentially don’t cares.If
completion
isfalse
, then Z3 will not assign interpretations to constants for functions that do not have interpretations in this model. Evaluation behaves as the identify function in this case.The evaluation may fail for the following reasons:
t
contains a quantifier.the current model is partial, that is, it doesn’t have a complete interpretation for uninterpreted functions. That is, the option
MODEL_PARTIAL=true
was used.t
is type incorrect.Z3Context.interrupt()
was invoked during evaluation.
-
Return the interpretation (i.e., assignment) of constant
a
in the current model. Returnnil
, if the model does not assign an interpretation fora
. That should be interpreted as: the value ofa
does not matter.Precondition
a.arity == 0
Declaration
Swift
public func getConstInterp(_ a: Z3FuncDecl) -> AnyZ3Ast?
-
Test if there exists an interpretation (i.e., assignment) for
a
in the current model.Declaration
Swift
public func hasInterp(_ a: Z3FuncDecl) -> Bool
-
Convert the given model into a string.
Declaration
Swift
public func toString() -> String
-
Evaluates expression to a double, assuming it is a numeral already
Type-erased version.
Returns 0, in case of failure
Declaration
Swift
public func doubleAny(_ expr: AnyZ3Ast) -> Double
-
Evaluates expression to a double, assuming it is a numeral already
Returns 0, in case of failure
Declaration
Swift
public func double<T>(_ expr: Z3Ast<T>) -> Double where T : FloatingSort
-
Evaluates expression to a double, assuming it is a numeral already
Returns 0, in case of failure
Declaration
Swift
public func double<T>(_ expr: Z3Ast<T>) -> Double where T : ArithmeticSort
-
Evaluates expression to an integer, assuming it is a numeral already
Type-erased version.
Returns 0, in case of failure
Declaration
Swift
public func intAny(_ expr: AnyZ3Ast) -> Int32
-
Evaluates expression to an integer, assuming it is a numeral already
Type-erased version.
Returns 0, in case of failure
Declaration
Swift
public func int64Any(_ expr: AnyZ3Ast) -> Int64
-
Evaluates expression to an integer, assuming it is a numeral already
Returns 0, in case of failure
Declaration
Swift
public func int(_ expr: Z3Int) -> Int32
-
Evaluates expression to an integer, assuming it is a numeral already
Returns 0, in case of failure
Declaration
Swift
public func int64(_ expr: Z3Int) -> Int64
-
Evaluates expression to an integer, assuming it is a numeral already
Returns 0, in case of failure
Declaration
Swift
public func int(_ expr: Z3BitVector32) -> Int32
-
Evaluates expression to an integer, assuming it is a numeral already
Returns 0, in case of failure
Declaration
Swift
public func int64(_ expr: Z3BitVector64) -> Int64