|
Z3
|
|
All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
|
Z3
|
|
Inheritance diagram for ModelRef:Public Member Functions | |
| def | __init__ |
| def | __del__ |
| def | __repr__ |
| def | sexpr |
| def | eval |
| def | evaluate |
| def | __len__ |
| def | get_interp |
| def | num_sorts |
| def | get_sort |
| def | sorts |
| def | get_universe |
| def | __getitem__ |
| def | decls |
| Public Member Functions inherited from Z3PPObject | |
| def | use_pp |
Data Fields | |
| model | |
| ctx | |
Model/Solution of a satisfiability problem (aka system of constraints).
| def __del__ | ( | self | ) |
| def __getitem__ | ( | self, | |
| idx | |||
| ) |
If `idx` is an integer, then the declaration at position `idx` in the model `self` is returned. If `idx` is a declaration, then the actual interpreation is returned.
The elements can be retrieved using position or the actual declaration.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2, f(x) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> len(m)
2
>>> m[0]
x
>>> m[1]
f
>>> m[x]
1
>>> m[f]
[1 -> 0, else -> 0]
>>> for d in m: print("%s -> %s" % (d, m[d]))
x -> 1
f -> [1 -> 0, else -> 0]
Definition at line 5526 of file z3py.py.
| def __len__ | ( | self | ) |
Return the number of constant and function declarations in the model `self`.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, f(x) != x)
>>> s.check()
sat
>>> m = s.model()
>>> len(m)
2
Definition at line 5405 of file z3py.py.
| def __repr__ | ( | self | ) |
| def decls | ( | self | ) |
Return a list with all symbols that have an interpreation in the model `self`.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2, f(x) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> m.decls()
[x, f]
Definition at line 5570 of file z3py.py.
| def eval | ( | self, | |
| t, | |||
model_completion = False |
|||
| ) |
Evaluate the expression `t` in the model `self`. If `model_completion` is enabled, then a default interpretation is automatically added for symbols that do not have an interpretation in the model `self`.
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2)
>>> s.check()
sat
>>> m = s.model()
>>> m.eval(x + 1)
2
>>> m.eval(x == 1)
True
>>> y = Int('y')
>>> m.eval(y + x)
1 + y
>>> m.eval(y)
y
>>> m.eval(y, model_completion=True)
0
>>> # Now, m contains an interpretation for y
>>> m.eval(y + x)
1
Definition at line 5350 of file z3py.py.
| def evaluate | ( | self, | |
| t, | |||
model_completion = False |
|||
| ) |
Alias for `eval`.
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2)
>>> s.check()
sat
>>> m = s.model()
>>> m.evaluate(x + 1)
2
>>> m.evaluate(x == 1)
True
>>> y = Int('y')
>>> m.evaluate(y + x)
1 + y
>>> m.evaluate(y)
y
>>> m.evaluate(y, model_completion=True)
0
>>> # Now, m contains an interpretation for y
>>> m.evaluate(y + x)
1
Definition at line 5379 of file z3py.py.
| def get_interp | ( | self, | |
| decl | |||
| ) |
Return the interpretation for a given declaration or constant.
>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> s = Solver()
>>> s.add(x > 0, x < 2, f(x) == 0)
>>> s.check()
sat
>>> m = s.model()
>>> m[x]
1
>>> m[f]
[1 -> 0, else -> 0]
Definition at line 5420 of file z3py.py.
Referenced by ModelRef.__getitem__().
| def get_sort | ( | self, | |
| idx | |||
| ) |
Return the unintepreted sort at position `idx` < self.num_sorts().
>>> A = DeclareSort('A')
>>> B = DeclareSort('B')
>>> a1, a2 = Consts('a1 a2', A)
>>> b1, b2 = Consts('b1 b2', B)
>>> s = Solver()
>>> s.add(a1 != a2, b1 != b2)
>>> s.check()
sat
>>> m = s.model()
>>> m.num_sorts()
2
>>> m.get_sort(0)
A
>>> m.get_sort(1)
B
Definition at line 5466 of file z3py.py.
| def get_universe | ( | self, | |
| s | |||
| ) |
Return the intepretation for the uninterpreted sort `s` in the model `self`.
>>> A = DeclareSort('A')
>>> a, b = Consts('a b', A)
>>> s = Solver()
>>> s.add(a != b)
>>> s.check()
sat
>>> m = s.model()
>>> m.get_universe(A)
[A!val!0, A!val!1]
Definition at line 5506 of file z3py.py.
Referenced by ModelRef.__getitem__().
| def num_sorts | ( | self | ) |
Return the number of unintepreted sorts that contain an interpretation in the model `self`.
>>> A = DeclareSort('A')
>>> a, b = Consts('a b', A)
>>> s = Solver()
>>> s.add(a != b)
>>> s.check()
sat
>>> m = s.model()
>>> m.num_sorts()
1
Definition at line 5451 of file z3py.py.
Referenced by ModelRef.get_sort().
| def sexpr | ( | self | ) |
Return a textual representation of the s-expression representing the model.
Definition at line 5346 of file z3py.py.
Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().
| def sorts | ( | self | ) |
Return all uninterpreted sorts that have an interpretation in the model `self`.
>>> A = DeclareSort('A')
>>> B = DeclareSort('B')
>>> a1, a2 = Consts('a1 a2', A)
>>> b1, b2 = Consts('b1 b2', B)
>>> s = Solver()
>>> s.add(a1 != a2, b1 != b2)
>>> s.check()
sat
>>> m = s.model()
>>> m.sorts()
[A, B]
Definition at line 5489 of file z3py.py.
| ctx |
Definition at line 5337 of file z3py.py.
Referenced by Probe.__eq__(), Probe.__ge__(), ModelRef.__getitem__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), ApplyResult.convert_model(), ModelRef.decls(), ModelRef.eval(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), ModelRef.get_interp(), Fixedpoint.get_rules(), ModelRef.get_sort(), ModelRef.get_universe(), Optimize.model(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), and Fixedpoint.update_rule().
| model |
Definition at line 5336 of file z3py.py.
Referenced by ModelRef.__del__(), ModelRef.__getitem__(), ModelRef.__len__(), ModelRef.decls(), ModelRef.eval(), ModelRef.get_interp(), ModelRef.get_sort(), ModelRef.get_universe(), ModelRef.num_sorts(), and ModelRef.sexpr().
1.8.5