Z3Model

public class Z3Model : Z3RefCountedObject

Model for the constraints asserted into the logical context.

  • The context this Z3Model belongs

    Declaration

    Swift

    public let context: Z3Context

  • Evaluate the AST node t in the given model. Returns the result in case of success, or nil in case of failure.

    If completion is true, 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 is false, 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.

    Declaration

    Swift

    public func eval<T>(_ t: Z3Ast<T>, completion: Bool = false) -> Z3Ast<T>? where T : SortKind

  • Evaluate the AST node t in the given model. Returns the result in case of success, or nil in case of failure.

    Type-erased version.

    If completion is true, 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 is false, 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.

    Declaration

    Swift

    public func evalAny(_ t: AnyZ3Ast, completion: Bool = false) -> AnyZ3Ast?

  • Return the interpretation (i.e., assignment) of constant a in the current model. Return nil, if the model does not assign an interpretation for a. That should be interpreted as: the value of a 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