Model/Solution of a satisfiability problem (aka system of constraints).
Definition at line 5891 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 6090 of file z3py.py.
6090 def __getitem__(self, idx):
6091 """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. 6093 The elements can be retrieved using position or the actual declaration. 6095 >>> f = Function('f', IntSort(), IntSort()) 6098 >>> s.add(x > 0, x < 2, f(x) == 0) 6112 >>> for d in m: print("%s -> %s" % (d, m[d])) 6117 if idx >= len(self):
6120 if (idx < num_consts):
6124 if isinstance(idx, FuncDeclRef):
6125 return self.get_interp(idx)
6127 return self.get_interp(idx.decl())
6128 if isinstance(idx, SortRef):
6129 return self.get_universe(idx)
6131 _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 5911 of file z3py.py.
5911 def eval(self, t, model_completion=False):
5912 """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`. 5916 >>> s.add(x > 0, x < 2) 5929 >>> m.eval(y, model_completion=True) 5931 >>> # Now, m contains an interpretation for y 5936 if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r):
5937 return _to_expr_ref(r[0], self.ctx)
5938 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 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 5940 of file z3py.py.
5940 def evaluate(self, t, model_completion=False):
5941 """Alias for `eval`. 5945 >>> s.add(x > 0, x < 2) 5949 >>> m.evaluate(x + 1) 5951 >>> m.evaluate(x == 1) 5954 >>> m.evaluate(y + x) 5958 >>> m.evaluate(y, model_completion=True) 5960 >>> # Now, m contains an interpretation for y 5961 >>> m.evaluate(y + x) 5964 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 6030 of file z3py.py.
6030 def get_sort(self, idx):
6031 """Return the uninterpreted sort at position `idx` < self.num_sorts(). 6033 >>> A = DeclareSort('A') 6034 >>> B = DeclareSort('B') 6035 >>> a1, a2 = Consts('a1 a2', A) 6036 >>> b1, b2 = Consts('b1 b2', B) 6038 >>> s.add(a1 != a2, b1 != b2) 6049 if idx >= self.num_sorts():
6051 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 6053 of file z3py.py.
6054 """Return all uninterpreted sorts that have an interpretation in the model `self`. 6056 >>> A = DeclareSort('A') 6057 >>> B = DeclareSort('B') 6058 >>> a1, a2 = Consts('a1 a2', A) 6059 >>> b1, b2 = Consts('b1 b2', B) 6061 >>> s.add(a1 != a2, b1 != b2) 6068 return [ self.get_sort(i)
for i
in range(self.num_sorts()) ]
expr range(expr const &lo, expr const &hi)