Z3
Public Member Functions | Data Fields
ModelRef Class Reference
+ Inheritance diagram for ModelRef:

Public Member Functions

def __init__ (self, m, ctx)
 
def __deepcopy__ (self, memo={})
 
def __del__ (self)
 
def __repr__ (self)
 
def sexpr (self)
 
def eval (self, t, model_completion=False)
 
def evaluate (self, t, model_completion=False)
 
def __len__ (self)
 
def get_interp (self, decl)
 
def num_sorts (self)
 
def get_sort (self, idx)
 
def sorts (self)
 
def get_universe (self, s)
 
def __getitem__ (self, idx)
 
def decls (self)
 
- Public Member Functions inherited from Z3PPObject
def use_pp (self)
 

Data Fields

 model
 
 ctx
 

Detailed Description

Model/Solution of a satisfiability problem (aka system of constraints).

Definition at line 5573 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  m,
  ctx 
)

Definition at line 5576 of file z3py.py.

5576  def __init__(self, m, ctx):
5577  assert ctx is not None
5578  self.model = m
5579  self.ctx = ctx
5580  Z3_model_inc_ref(self.ctx.ref(), self.model)
5581 
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.

◆ __del__()

def __del__ (   self)

Definition at line 5585 of file z3py.py.

5585  def __del__(self):
5586  if self.ctx.ref() is not None:
5587  Z3_model_dec_ref(self.ctx.ref(), self.model)
5588 
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.

Member Function Documentation

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 5582 of file z3py.py.

5582  def __deepcopy__(self, memo={}):
5583  return ModelRef(self.m, self.ctx)
5584 

◆ __getitem__()

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 5775 of file z3py.py.

5775  def __getitem__(self, idx):
5776  """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.
5777 
5778  The elements can be retrieved using position or the actual declaration.
5779 
5780  >>> f = Function('f', IntSort(), IntSort())
5781  >>> x = Int('x')
5782  >>> s = Solver()
5783  >>> s.add(x > 0, x < 2, f(x) == 0)
5784  >>> s.check()
5785  sat
5786  >>> m = s.model()
5787  >>> len(m)
5788  2
5789  >>> m[0]
5790  x
5791  >>> m[1]
5792  f
5793  >>> m[x]
5794  1
5795  >>> m[f]
5796  [1 -> 0, else -> 0]
5797  >>> for d in m: print("%s -> %s" % (d, m[d]))
5798  x -> 1
5799  f -> [1 -> 0, else -> 0]
5800  """
5801  if _is_int(idx):
5802  if idx >= len(self):
5803  raise IndexError
5804  num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model)
5805  if (idx < num_consts):
5806  return FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, idx), self.ctx)
5807  else:
5808  return FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, idx - num_consts), self.ctx)
5809  if isinstance(idx, FuncDeclRef):
5810  return self.get_interp(idx)
5811  if is_const(idx):
5812  return self.get_interp(idx.decl())
5813  if isinstance(idx, SortRef):
5814  return self.get_universe(idx)
5815  if __debug__:
5816  _z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected")
5817  return None
5818 
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.
def is_const(a)
Definition: z3py.py:1080
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.

◆ __len__()

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 5651 of file z3py.py.

5651  def __len__(self):
5652  """Return the number of constant and function declarations in the model `self`.
5653 
5654  >>> f = Function('f', IntSort(), IntSort())
5655  >>> x = Int('x')
5656  >>> s = Solver()
5657  >>> s.add(x > 0, f(x) != x)
5658  >>> s.check()
5659  sat
5660  >>> m = s.model()
5661  >>> len(m)
5662  2
5663  """
5664  return int(Z3_model_get_num_consts(self.ctx.ref(), self.model)) + int(Z3_model_get_num_funcs(self.ctx.ref(), self.model))
5665 
unsigned Z3_API Z3_model_get_num_consts(Z3_context c, Z3_model m)
Return the number of constants assigned by the given model.
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.

◆ __repr__()

def __repr__ (   self)

Definition at line 5589 of file z3py.py.

5589  def __repr__(self):
5590  return obj_to_string(self)
5591 

◆ decls()

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 5819 of file z3py.py.

5819  def decls(self):
5820  """Return a list with all symbols that have an interpreation in the model `self`.
5821  >>> f = Function('f', IntSort(), IntSort())
5822  >>> x = Int('x')
5823  >>> s = Solver()
5824  >>> s.add(x > 0, x < 2, f(x) == 0)
5825  >>> s.check()
5826  sat
5827  >>> m = s.model()
5828  >>> m.decls()
5829  [x, f]
5830  """
5831  r = []
5832  for i in range(Z3_model_get_num_consts(self.ctx.ref(), self.model)):
5833  r.append(FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, i), self.ctx))
5834  for i in range(Z3_model_get_num_funcs(self.ctx.ref(), self.model)):
5835  r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx))
5836  return r
5837 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813
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.
unsigned Z3_API Z3_model_get_num_funcs(Z3_context c, Z3_model m)
Return the number of function interpretations in the given model.

◆ eval()

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 5596 of file z3py.py.

5596  def eval(self, t, model_completion=False):
5597  """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`.
5598 
5599  >>> x = Int('x')
5600  >>> s = Solver()
5601  >>> s.add(x > 0, x < 2)
5602  >>> s.check()
5603  sat
5604  >>> m = s.model()
5605  >>> m.eval(x + 1)
5606  2
5607  >>> m.eval(x == 1)
5608  True
5609  >>> y = Int('y')
5610  >>> m.eval(y + x)
5611  1 + y
5612  >>> m.eval(y)
5613  y
5614  >>> m.eval(y, model_completion=True)
5615  0
5616  >>> # Now, m contains an interpretation for y
5617  >>> m.eval(y + x)
5618  1
5619  """
5620  r = (Ast * 1)()
5621  if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r):
5622  return _to_expr_ref(r[0], self.ctx)
5623  raise Z3Exception("failed to evaluate expression in the model")
5624 
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...

◆ evaluate()

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 5625 of file z3py.py.

5625  def evaluate(self, t, model_completion=False):
5626  """Alias for `eval`.
5627 
5628  >>> x = Int('x')
5629  >>> s = Solver()
5630  >>> s.add(x > 0, x < 2)
5631  >>> s.check()
5632  sat
5633  >>> m = s.model()
5634  >>> m.evaluate(x + 1)
5635  2
5636  >>> m.evaluate(x == 1)
5637  True
5638  >>> y = Int('y')
5639  >>> m.evaluate(y + x)
5640  1 + y
5641  >>> m.evaluate(y)
5642  y
5643  >>> m.evaluate(y, model_completion=True)
5644  0
5645  >>> # Now, m contains an interpretation for y
5646  >>> m.evaluate(y + x)
5647  1
5648  """
5649  return self.eval(t, model_completion)
5650 

◆ get_interp()

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 5666 of file z3py.py.

5666  def get_interp(self, decl):
5667  """Return the interpretation for a given declaration or constant.
5668 
5669  >>> f = Function('f', IntSort(), IntSort())
5670  >>> x = Int('x')
5671  >>> s = Solver()
5672  >>> s.add(x > 0, x < 2, f(x) == 0)
5673  >>> s.check()
5674  sat
5675  >>> m = s.model()
5676  >>> m[x]
5677  1
5678  >>> m[f]
5679  [1 -> 0, else -> 0]
5680  """
5681  if __debug__:
5682  _z3_assert(isinstance(decl, FuncDeclRef) or is_const(decl), "Z3 declaration expected")
5683  if is_const(decl):
5684  decl = decl.decl()
5685  try:
5686  if decl.arity() == 0:
5687  _r = Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast)
5688  if _r.value is None:
5689  return None
5690  r = _to_expr_ref(_r, self.ctx)
5691  if is_as_array(r):
5692  return self.get_interp(get_as_array_func(r))
5693  else:
5694  return r
5695  else:
5696  return FuncInterp(Z3_model_get_func_interp(self.ctx.ref(), self.model, decl.ast), self.ctx)
5697  except Z3Exception:
5698  return None
5699 
def is_const(a)
Definition: z3py.py:1080
def get_as_array_func(n)
Definition: z3py.py:5842
Z3_func_interp Z3_API Z3_model_get_func_interp(Z3_context c, Z3_model m, Z3_func_decl f)
Return the interpretation of the function f in the model m. Return NULL, if the model does not assign...
Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a)
Return the interpretation (i.e., assignment) of constant a in the model m. Return NULL...
def is_as_array(n)
Definition: z3py.py:5838

◆ get_sort()

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 5715 of file z3py.py.

5715  def get_sort(self, idx):
5716  """Return the unintepreted sort at position `idx` < self.num_sorts().
5717 
5718  >>> A = DeclareSort('A')
5719  >>> B = DeclareSort('B')
5720  >>> a1, a2 = Consts('a1 a2', A)
5721  >>> b1, b2 = Consts('b1 b2', B)
5722  >>> s = Solver()
5723  >>> s.add(a1 != a2, b1 != b2)
5724  >>> s.check()
5725  sat
5726  >>> m = s.model()
5727  >>> m.num_sorts()
5728  2
5729  >>> m.get_sort(0)
5730  A
5731  >>> m.get_sort(1)
5732  B
5733  """
5734  if idx >= self.num_sorts():
5735  raise IndexError
5736  return _to_sort_ref(Z3_model_get_sort(self.ctx.ref(), self.model, idx), self.ctx)
5737 
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.

◆ get_universe()

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 5755 of file z3py.py.

5755  def get_universe(self, s):
5756  """Return the intepretation for the uninterpreted sort `s` in the model `self`.
5757 
5758  >>> A = DeclareSort('A')
5759  >>> a, b = Consts('a b', A)
5760  >>> s = Solver()
5761  >>> s.add(a != b)
5762  >>> s.check()
5763  sat
5764  >>> m = s.model()
5765  >>> m.get_universe(A)
5766  [A!val!0, A!val!1]
5767  """
5768  if __debug__:
5769  _z3_assert(isinstance(s, SortRef), "Z3 sort expected")
5770  try:
5771  return AstVector(Z3_model_get_sort_universe(self.ctx.ref(), self.model, s.ast), self.ctx)
5772  except Z3Exception:
5773  return None
5774 
Z3_ast_vector Z3_API Z3_model_get_sort_universe(Z3_context c, Z3_model m, Z3_sort s)
Return the finite set of distinct values that represent the interpretation for sort s...

◆ num_sorts()

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 5700 of file z3py.py.

Referenced by ModelRef.get_sort().

5700  def num_sorts(self):
5701  """Return the number of unintepreted sorts that contain an interpretation in the model `self`.
5702 
5703  >>> A = DeclareSort('A')
5704  >>> a, b = Consts('a b', A)
5705  >>> s = Solver()
5706  >>> s.add(a != b)
5707  >>> s.check()
5708  sat
5709  >>> m = s.model()
5710  >>> m.num_sorts()
5711  1
5712  """
5713  return int(Z3_model_get_num_sorts(self.ctx.ref(), self.model))
5714 
unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m)
Return the number of uninterpreted sorts that m assigs an interpretation to.

◆ sexpr()

def sexpr (   self)
Return a textual representation of the s-expression representing the model.

Definition at line 5592 of file z3py.py.

Referenced by Fixedpoint.__repr__(), and Optimize.__repr__().

5592  def sexpr(self):
5593  """Return a textual representation of the s-expression representing the model."""
5594  return Z3_model_to_string(self.ctx.ref(), self.model)
5595 
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.

◆ sorts()

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 5738 of file z3py.py.

5738  def sorts(self):
5739  """Return all uninterpreted sorts that have an interpretation in the model `self`.
5740 
5741  >>> A = DeclareSort('A')
5742  >>> B = DeclareSort('B')
5743  >>> a1, a2 = Consts('a1 a2', A)
5744  >>> b1, b2 = Consts('b1 b2', B)
5745  >>> s = Solver()
5746  >>> s.add(a1 != a2, b1 != b2)
5747  >>> s.check()
5748  sat
5749  >>> m = s.model()
5750  >>> m.sorts()
5751  [A, B]
5752  """
5753  return [ self.get_sort(i) for i in range(self.num_sorts()) ]
5754 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:2813

Field Documentation

◆ ctx

ctx

Definition at line 5579 of file z3py.py.

Referenced by Probe.__call__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), ApplyResult.__len__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.check(), ApplyResult.convert_model(), Optimize.from_file(), Optimize.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.pop(), Optimize.pop(), Fixedpoint.push(), Optimize.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), Fixedpoint.register_relation(), Fixedpoint.set(), Optimize.set(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), and Fixedpoint.update_rule().

◆ model

model

Definition at line 5578 of file z3py.py.