Model/Solution of a satisfiability problem (aka system of constraints).
Definition at line 5940 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 interpretation 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]
[else -> 0]
>>> for d in m: print("%s -> %s" % (d, m[d]))
x -> 1
f -> [else -> 0]
Definition at line 6139 of file z3py.py.
6139 def __getitem__(self, idx):
6140 """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 interpretation is returned. 6142 The elements can be retrieved using position or the actual declaration. 6144 >>> f = Function('f', IntSort(), IntSort()) 6147 >>> s.add(x > 0, x < 2, f(x) == 0) 6161 >>> for d in m: print("%s -> %s" % (d, m[d])) 6166 if idx >= len(self):
6169 if (idx < num_consts):
6173 if isinstance(idx, FuncDeclRef):
6174 return self.get_interp(idx)
6176 return self.get_interp(idx.decl())
6177 if isinstance(idx, SortRef):
6178 return self.get_universe(idx)
6180 _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 5960 of file z3py.py.
5960 def eval(self, t, model_completion=False):
5961 """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`. 5965 >>> s.add(x > 0, x < 2) 5978 >>> m.eval(y, model_completion=True) 5980 >>> # Now, m contains an interpretation for y 5985 if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r):
5986 return _to_expr_ref(r[0], self.ctx)
5987 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, bool model_completion, Z3_ast *v)
Evaluate the AST node t in the given model. Return 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 5989 of file z3py.py.
5989 def evaluate(self, t, model_completion=False):
5990 """Alias for `eval`. 5994 >>> s.add(x > 0, x < 2) 5998 >>> m.evaluate(x + 1) 6000 >>> m.evaluate(x == 1) 6003 >>> m.evaluate(y + x) 6007 >>> m.evaluate(y, model_completion=True) 6009 >>> # Now, m contains an interpretation for y 6010 >>> m.evaluate(y + x) 6013 return self.eval(t, model_completion)
def get_sort |
( |
|
self, |
|
|
|
idx |
|
) |
| |
Return the uninterpreted 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 6079 of file z3py.py.
6079 def get_sort(self, idx):
6080 """Return the uninterpreted sort at position `idx` < self.num_sorts(). 6082 >>> A = DeclareSort('A') 6083 >>> B = DeclareSort('B') 6084 >>> a1, a2 = Consts('a1 a2', A) 6085 >>> b1, b2 = Consts('b1 b2', B) 6087 >>> s.add(a1 != a2, b1 != b2) 6098 if idx >= self.num_sorts():
6100 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 6102 of file z3py.py.
6103 """Return all uninterpreted sorts that have an interpretation in the model `self`. 6105 >>> A = DeclareSort('A') 6106 >>> B = DeclareSort('B') 6107 >>> a1, a2 = Consts('a1 a2', A) 6108 >>> b1, b2 = Consts('b1 b2', B) 6110 >>> s.add(a1 != a2, b1 != b2) 6117 return [ self.get_sort(i)
for i
in range(self.num_sorts()) ]
expr range(expr const &lo, expr const &hi)