Model/Solution of a satisfiability problem (aka system of constraints).
Definition at line 5897 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 6096 of file z3py.py.
6096 def __getitem__(self, idx):
6097 """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. 6099 The elements can be retrieved using position or the actual declaration. 6101 >>> f = Function('f', IntSort(), IntSort()) 6104 >>> s.add(x > 0, x < 2, f(x) == 0) 6118 >>> for d in m: print("%s -> %s" % (d, m[d])) 6123 if idx >= len(self):
6126 if (idx < num_consts):
6130 if isinstance(idx, FuncDeclRef):
6131 return self.get_interp(idx)
6133 return self.get_interp(idx.decl())
6134 if isinstance(idx, SortRef):
6135 return self.get_universe(idx)
6137 _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 5917 of file z3py.py.
5917 def eval(self, t, model_completion=False):
5918 """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`. 5922 >>> s.add(x > 0, x < 2) 5935 >>> m.eval(y, model_completion=True) 5937 >>> # Now, m contains an interpretation for y 5942 if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r):
5943 return _to_expr_ref(r[0], self.ctx)
5944 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 5946 of file z3py.py.
5946 def evaluate(self, t, model_completion=False):
5947 """Alias for `eval`. 5951 >>> s.add(x > 0, x < 2) 5955 >>> m.evaluate(x + 1) 5957 >>> m.evaluate(x == 1) 5960 >>> m.evaluate(y + x) 5964 >>> m.evaluate(y, model_completion=True) 5966 >>> # Now, m contains an interpretation for y 5967 >>> m.evaluate(y + x) 5970 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 6036 of file z3py.py.
6036 def get_sort(self, idx):
6037 """Return the uninterpreted sort at position `idx` < self.num_sorts(). 6039 >>> A = DeclareSort('A') 6040 >>> B = DeclareSort('B') 6041 >>> a1, a2 = Consts('a1 a2', A) 6042 >>> b1, b2 = Consts('b1 b2', B) 6044 >>> s.add(a1 != a2, b1 != b2) 6055 if idx >= self.num_sorts():
6057 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 6059 of file z3py.py.
6060 """Return all uninterpreted sorts that have an interpretation in the model `self`. 6062 >>> A = DeclareSort('A') 6063 >>> B = DeclareSort('B') 6064 >>> a1, a2 = Consts('a1 a2', A) 6065 >>> b1, b2 = Consts('b1 b2', B) 6067 >>> s.add(a1 != a2, b1 != b2) 6074 return [ self.get_sort(i)
for i
in range(self.num_sorts()) ]
expr range(expr const &lo, expr const &hi)