class
Z3::Model
- Z3::Model
- Reference
- Object
Defined in:
z3/model.crConstructors
Instance Method Summary
- #[](expr)
- #consts
-
#each(&)
Yields each constant in the model as a
{variable, value}pair, sorted by name. - #eval(expr : BoolExpr, complete = false)
- #eval(expr : IntExpr, complete = false)
- #eval(expr : BitvecExpr, complete = false)
- #eval(expr : RealExpr, complete = false)
-
#negate
A formula asserting the model must differ somewhere - useful for enumerating all solutions.
- #num_consts
-
#to_s(io)
This needs to go eventually
- #to_unsafe : LibZ3::Model
Constructor Detail
Instance Method Detail
def each(&)
#
Yields each constant in the model as a {variable, value} pair, sorted by
name. We have no FuncDecl wrapper yet, so we rebuild the variable from the
const's name and range sort.
def negate
#
A formula asserting the model must differ somewhere - useful for enumerating all solutions.