class Z3::Model

Defined in:

z3/model.cr

Constructors

Instance Method Summary

Constructor Detail

def self.new(model : LibZ3::Model) #

[View source]

Instance Method Detail

def [](expr) #

[View source]
def consts : Array(FuncDecl) #

The declarations of the variables the model assigned - #each_const is what yields the variables themselves


[View source]
def each(&) #

Constants first, then functions - so what's yielded is a variable and its value, or a declaration and its interpretation, and both halves are unions


[View source]
def each_const(&) #

Yields each constant in the model as a {variable, value} pair, sorted by name


[View source]
def each_func(&) #

Yields each function as a {declaration, interpretation} pair, sorted by name


[View source]
def eval(expr : BoolExpr, complete = false) #

[View source]
def eval(expr : IntExpr, complete = false) #

[View source]
def eval(expr : BitvecExpr, complete = false) #

[View source]
def eval(expr : CharExpr, complete = false) #

[View source]
def eval(expr : FloatExpr, complete = false) #

[View source]
def eval(expr : RealExpr, complete = false) #

[View source]
def eval(expr : StringExpr, complete = false) #

[View source]
def eval(expr : SeqExpr, complete = false) #

[View source]
def eval(expr : RoundingModeExpr, complete = false) #

[View source]
def func_interp(decl : FuncDecl) : FuncInterp #

[View source]
def funcs : Array(FuncDecl) #

The uninterpreted functions the model decided the meaning of.

Recursive definitions are left out. Z3 puts every one made in the context into every model, of every solver, whether or not the query so much as mentioned it - define-fun-rec is context-global the way it is in an SMT-LIB script. It isn't something this model decided, it's the definition handed straight back, and its else branch is a body over de Bruijn variables which no Expr can hold.


[View source]
def has_interp?(decl : FuncDecl) #

Whether the model says anything at all about this variable or function. It's the question #model_eval can't answer: without completion an unassigned variable evaluates to itself, and with it Z3 invents a value rather than telling you it had to.


[View source]
def has_interp?(var : AnyExpr) #

[View source]
def model_eval(expr, complete = false) : AnyExpr #

#eval without the sort coming back with it, for the cases where the expression's class isn't known statically - an argument of a FuncDecl, say


[View source]
def negate #

A formula asserting the model must differ somewhere - useful for enumerating all solutions.

Only constants are negated. Saying "some function differs somewhere" needs a quantifier, so a model with functions in it can repeat under this.


[View source]
def num_consts #

[View source]
def num_funcs #

[View source]
def to_s(io) #

This needs to go eventually


[View source]
def to_unsafe : LibZ3::Model #

[View source]