Model/Solution of a satisfiability problem (aka system of constraints).
Definition at line 5455 of file z3py.py.
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 5654 of file z3py.py.
5654 def __getitem__(self, idx):
5655 """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. 5657 The elements can be retrieved using position or the actual declaration. 5659 >>> f = Function('f', IntSort(), IntSort()) 5662 >>> s.add(x > 0, x < 2, f(x) == 0) 5676 >>> for d in m: print("%s -> %s" % (d, m[d])) 5678 f -> [1 -> 0, else -> 0] 5681 if idx >= len(self):
5684 if (idx < num_consts):
5688 if isinstance(idx, FuncDeclRef):
5689 return self.get_interp(idx)
5691 return self.get_interp(idx.decl())
5692 if isinstance(idx, SortRef):
5693 return self.get_universe(idx)
5695 _z3_assert(
False,
"Integer, Z3 declaration, or Z3 constant expected")
Z3_func_decl Z3_API Z3_model_get_func_decl(Z3_context c, Z3_model m, unsigned i)
Return the declaration of the i-th function in the given model.
Z3_func_decl Z3_API Z3_model_get_const_decl(Z3_context c, Z3_model m, unsigned i)
Return the i-th constant in the given model.
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.
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 5475 of file z3py.py.
5475 def eval(self, t, model_completion=False):
5476 """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`. 5480 >>> s.add(x > 0, x < 2) 5493 >>> m.eval(y, model_completion=True) 5495 >>> # Now, m contains an interpretation for y 5500 if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r):
5501 return _to_expr_ref(r[0], self.ctx)
5502 raise Z3Exception(
"failed to evaluate expression in the model")
Z3_bool Z3_API Z3_model_eval(Z3_context c, Z3_model m, Z3_ast t, Z3_bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return Z3_TRUE if succeeded, and store the result in v...
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 5504 of file z3py.py.
5504 def evaluate(self, t, model_completion=False):
5505 """Alias for `eval`. 5509 >>> s.add(x > 0, x < 2) 5513 >>> m.evaluate(x + 1) 5515 >>> m.evaluate(x == 1) 5518 >>> m.evaluate(y + x) 5522 >>> m.evaluate(y, model_completion=True) 5524 >>> # Now, m contains an interpretation for y 5525 >>> m.evaluate(y + x) 5528 return self.eval(t, model_completion)
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 5594 of file z3py.py.
5594 def get_sort(self, idx):
5595 """Return the unintepreted sort at position `idx` < self.num_sorts(). 5597 >>> A = DeclareSort('A') 5598 >>> B = DeclareSort('B') 5599 >>> a1, a2 = Consts('a1 a2', A) 5600 >>> b1, b2 = Consts('b1 b2', B) 5602 >>> s.add(a1 != a2, b1 != b2) 5613 if idx >= self.num_sorts():
5615 return _to_sort_ref(
Z3_model_get_sort(self.ctx.ref(), self.model, idx), self.ctx)
Z3_sort Z3_API Z3_model_get_sort(Z3_context c, Z3_model m, unsigned i)
Return a uninterpreted sort that m assigns an interpretation.
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 5617 of file z3py.py.
5618 """Return all uninterpreted sorts that have an interpretation in the model `self`. 5620 >>> A = DeclareSort('A') 5621 >>> B = DeclareSort('B') 5622 >>> a1, a2 = Consts('a1 a2', A) 5623 >>> b1, b2 = Consts('b1 b2', B) 5625 >>> s.add(a1 != a2, b1 != b2) 5632 return [ self.get_sort(i)
for i
in range(self.num_sorts()) ]