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

Public Member Functions

def __init__ (self, m, ctx)
 
def __del__ (self)
 
def __repr__ (self)
 
def sexpr (self)
 
def eval
 
def evaluate
 
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)
 
def update_value (self, x, value)
 
def translate (self, target)
 
def __copy__ (self)
 
def __deepcopy__
 
- 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 6359 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  m,
  ctx 
)

Definition at line 6362 of file z3py.py.

6362  def __init__(self, m, ctx):
6363  assert ctx is not None
6364  self.model = m
6365  self.ctx = ctx
6366  Z3_model_inc_ref(self.ctx.ref(), self.model)
6367 
def __init__(self, m, ctx)
Definition: z3py.py:6362
void Z3_API Z3_model_inc_ref(Z3_context c, Z3_model m)
Increment the reference counter of the given model.
def __del__ (   self)

Definition at line 6368 of file z3py.py.

6368  def __del__(self):
6369  if self.ctx.ref() is not None and Z3_model_dec_ref is not None:
6370  Z3_model_dec_ref(self.ctx.ref(), self.model)
6371 
def __del__(self)
Definition: z3py.py:6368
void Z3_API Z3_model_dec_ref(Z3_context c, Z3_model m)
Decrement the reference counter of the given model.

Member Function Documentation

def __copy__ (   self)

Definition at line 6674 of file z3py.py.

6674  def __copy__(self):
6675  return self.translate(self.ctx)
6676 
def __copy__(self)
Definition: z3py.py:6674
def translate(self, target)
Definition: z3py.py:6666
def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 6677 of file z3py.py.

6677  def __deepcopy__(self, memo={}):
6678  return self.translate(self.ctx)
6679 
6680 
def __deepcopy__
Definition: z3py.py:6677
def translate(self, target)
Definition: z3py.py:6666
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 6580 of file z3py.py.

6580  def __getitem__(self, idx):
6581  """If `idx` is an integer, then the declaration at position `idx` in the model `self` is returned.
6582  If `idx` is a declaration, then the actual interpretation is returned.
6583 
6584  The elements can be retrieved using position or the actual declaration.
6585 
6586  >>> f = Function('f', IntSort(), IntSort())
6587  >>> x = Int('x')
6588  >>> s = Solver()
6589  >>> s.add(x > 0, x < 2, f(x) == 0)
6590  >>> s.check()
6591  sat
6592  >>> m = s.model()
6593  >>> len(m)
6594  2
6595  >>> m[0]
6596  x
6597  >>> m[1]
6598  f
6599  >>> m[x]
6600  1
6601  >>> m[f]
6602  [else -> 0]
6603  >>> for d in m: print("%s -> %s" % (d, m[d]))
6604  x -> 1
6605  f -> [else -> 0]
6606  """
6607  if _is_int(idx):
6608  if idx >= len(self):
6609  raise IndexError
6610  num_consts = Z3_model_get_num_consts(self.ctx.ref(), self.model)
6611  if (idx < num_consts):
6612  return FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, idx), self.ctx)
6613  else:
6614  return FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, idx - num_consts), self.ctx)
6615  if isinstance(idx, FuncDeclRef):
6616  return self.get_interp(idx)
6617  if is_const(idx):
6618  return self.get_interp(idx.decl())
6619  if isinstance(idx, SortRef):
6620  return self.get_universe(idx)
6621  if z3_debug():
6622  _z3_assert(False, "Integer, Z3 declaration, or Z3 constant expected")
6623  return None
6624 
Function Declarations.
Definition: z3py.py:718
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 get_universe(self, s)
Definition: z3py.py:6560
def is_const(a)
Definition: z3py.py:1287
def __getitem__(self, idx)
Definition: z3py.py:6580
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 z3_debug()
Definition: z3py.py:62
def get_interp(self, decl)
Definition: z3py.py:6453
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 6436 of file z3py.py.

6436  def __len__(self):
6437  """Return the number of constant and function declarations in the model `self`.
6438 
6439  >>> f = Function('f', IntSort(), IntSort())
6440  >>> x = Int('x')
6441  >>> s = Solver()
6442  >>> s.add(x > 0, f(x) != x)
6443  >>> s.check()
6444  sat
6445  >>> m = s.model()
6446  >>> len(m)
6447  2
6448  """
6449  num_consts = int(Z3_model_get_num_consts(self.ctx.ref(), self.model))
6450  num_funcs = int(Z3_model_get_num_funcs(self.ctx.ref(), self.model))
6451  return num_consts + num_funcs
6452 
def __len__(self)
Definition: z3py.py:6436
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.
def __repr__ (   self)

Definition at line 6372 of file z3py.py.

6372  def __repr__(self):
6373  return obj_to_string(self)
6374 
def __repr__(self)
Definition: z3py.py:6372
def decls (   self)
Return a list with all symbols that have an interpretation 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 6625 of file z3py.py.

6625  def decls(self):
6626  """Return a list with all symbols that have an interpretation in the model `self`.
6627  >>> f = Function('f', IntSort(), IntSort())
6628  >>> x = Int('x')
6629  >>> s = Solver()
6630  >>> s.add(x > 0, x < 2, f(x) == 0)
6631  >>> s.check()
6632  sat
6633  >>> m = s.model()
6634  >>> m.decls()
6635  [x, f]
6636  """
6637  r = []
6638  for i in range(Z3_model_get_num_consts(self.ctx.ref(), self.model)):
6639  r.append(FuncDeclRef(Z3_model_get_const_decl(self.ctx.ref(), self.model, i), self.ctx))
6640  for i in range(Z3_model_get_num_funcs(self.ctx.ref(), self.model)):
6641  r.append(FuncDeclRef(Z3_model_get_func_decl(self.ctx.ref(), self.model, i), self.ctx))
6642  return r
6643 
Function Declarations.
Definition: z3py.py:718
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
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.
def decls(self)
Definition: z3py.py:6625
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 6379 of file z3py.py.

6379  def eval(self, t, model_completion=False):
6380  """Evaluate the expression `t` in the model `self`.
6381  If `model_completion` is enabled, then a default interpretation is automatically added
6382  for symbols that do not have an interpretation in the model `self`.
6383 
6384  >>> x = Int('x')
6385  >>> s = Solver()
6386  >>> s.add(x > 0, x < 2)
6387  >>> s.check()
6388  sat
6389  >>> m = s.model()
6390  >>> m.eval(x + 1)
6391  2
6392  >>> m.eval(x == 1)
6393  True
6394  >>> y = Int('y')
6395  >>> m.eval(y + x)
6396  1 + y
6397  >>> m.eval(y)
6398  y
6399  >>> m.eval(y, model_completion=True)
6400  0
6401  >>> # Now, m contains an interpretation for y
6402  >>> m.eval(y + x)
6403  1
6404  """
6405  r = (Ast * 1)()
6406  if Z3_model_eval(self.ctx.ref(), self.model, t.as_ast(), model_completion, r):
6407  return _to_expr_ref(r[0], self.ctx)
6408  raise Z3Exception("failed to evaluate expression in the model")
6409 
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 eval
Definition: z3py.py:6379
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 6410 of file z3py.py.

6410  def evaluate(self, t, model_completion=False):
6411  """Alias for `eval`.
6412 
6413  >>> x = Int('x')
6414  >>> s = Solver()
6415  >>> s.add(x > 0, x < 2)
6416  >>> s.check()
6417  sat
6418  >>> m = s.model()
6419  >>> m.evaluate(x + 1)
6420  2
6421  >>> m.evaluate(x == 1)
6422  True
6423  >>> y = Int('y')
6424  >>> m.evaluate(y + x)
6425  1 + y
6426  >>> m.evaluate(y)
6427  y
6428  >>> m.evaluate(y, model_completion=True)
6429  0
6430  >>> # Now, m contains an interpretation for y
6431  >>> m.evaluate(y + x)
6432  1
6433  """
6434  return self.eval(t, model_completion)
6435 
def evaluate
Definition: z3py.py:6410
def eval
Definition: z3py.py:6379
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]
[else -> 0]

Definition at line 6453 of file z3py.py.

Referenced by ModelRef.__getitem__().

6453  def get_interp(self, decl):
6454  """Return the interpretation for a given declaration or constant.
6455 
6456  >>> f = Function('f', IntSort(), IntSort())
6457  >>> x = Int('x')
6458  >>> s = Solver()
6459  >>> s.add(x > 0, x < 2, f(x) == 0)
6460  >>> s.check()
6461  sat
6462  >>> m = s.model()
6463  >>> m[x]
6464  1
6465  >>> m[f]
6466  [else -> 0]
6467  """
6468  if z3_debug():
6469  _z3_assert(isinstance(decl, FuncDeclRef) or is_const(decl), "Z3 declaration expected")
6470  if is_const(decl):
6471  decl = decl.decl()
6472  try:
6473  if decl.arity() == 0:
6474  _r = Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast)
6475  if _r.value is None:
6476  return None
6477  r = _to_expr_ref(_r, self.ctx)
6478  if is_as_array(r):
6479  fi = self.get_interp(get_as_array_func(r))
6480  if fi is None:
6481  return fi
6482  e = fi.else_value()
6483  if e is None:
6484  return fi
6485  if fi.arity() != 1:
6486  return fi
6487  srt = decl.range()
6488  dom = srt.domain()
6489  e = K(dom, e)
6490  i = 0
6491  sz = fi.num_entries()
6492  n = fi.arity()
6493  while i < sz:
6494  fe = fi.entry(i)
6495  e = Store(e, fe.arg_value(0), fe.value())
6496  i += 1
6497  return e
6498  else:
6499  return r
6500  else:
6501  return FuncInterp(Z3_model_get_func_interp(self.ctx.ref(), self.model, decl.ast), self.ctx)
6502  except Z3Exception:
6503  return None
6504 
def Store(a, args)
Definition: z3py.py:4782
def is_const(a)
Definition: z3py.py:1287
def get_as_array_func(n)
Definition: z3py.py:6691
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 z3_debug()
Definition: z3py.py:62
def get_interp(self, decl)
Definition: z3py.py:6453
def is_as_array(n)
Definition: z3py.py:6686
def K(dom, v)
Definition: z3py.py:4838
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 6520 of file z3py.py.

6520  def get_sort(self, idx):
6521  """Return the uninterpreted sort at position `idx` < self.num_sorts().
6522 
6523  >>> A = DeclareSort('A')
6524  >>> B = DeclareSort('B')
6525  >>> a1, a2 = Consts('a1 a2', A)
6526  >>> b1, b2 = Consts('b1 b2', B)
6527  >>> s = Solver()
6528  >>> s.add(a1 != a2, b1 != b2)
6529  >>> s.check()
6530  sat
6531  >>> m = s.model()
6532  >>> m.num_sorts()
6533  2
6534  >>> m.get_sort(0)
6535  A
6536  >>> m.get_sort(1)
6537  B
6538  """
6539  if idx >= self.num_sorts():
6540  raise IndexError
6541  return _to_sort_ref(Z3_model_get_sort(self.ctx.ref(), self.model, idx), self.ctx)
6542 
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.
def num_sorts(self)
Definition: z3py.py:6505
def get_sort(self, idx)
Definition: z3py.py:6520
def get_universe (   self,
  s 
)
Return the interpretation 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!1, A!val!0]

Definition at line 6560 of file z3py.py.

Referenced by ModelRef.__getitem__().

6560  def get_universe(self, s):
6561  """Return the interpretation for the uninterpreted sort `s` in the model `self`.
6562 
6563  >>> A = DeclareSort('A')
6564  >>> a, b = Consts('a b', A)
6565  >>> s = Solver()
6566  >>> s.add(a != b)
6567  >>> s.check()
6568  sat
6569  >>> m = s.model()
6570  >>> m.get_universe(A)
6571  [A!val!1, A!val!0]
6572  """
6573  if z3_debug():
6574  _z3_assert(isinstance(s, SortRef), "Z3 sort expected")
6575  try:
6576  return AstVector(Z3_model_get_sort_universe(self.ctx.ref(), self.model, s.ast), self.ctx)
6577  except Z3Exception:
6578  return None
6579 
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...
def get_universe(self, s)
Definition: z3py.py:6560
def z3_debug()
Definition: z3py.py:62
def num_sorts (   self)
Return the number of uninterpreted 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 6505 of file z3py.py.

Referenced by ModelRef.get_sort().

6505  def num_sorts(self):
6506  """Return the number of uninterpreted sorts that contain an interpretation in the model `self`.
6507 
6508  >>> A = DeclareSort('A')
6509  >>> a, b = Consts('a b', A)
6510  >>> s = Solver()
6511  >>> s.add(a != b)
6512  >>> s.check()
6513  sat
6514  >>> m = s.model()
6515  >>> m.num_sorts()
6516  1
6517  """
6518  return int(Z3_model_get_num_sorts(self.ctx.ref(), self.model))
6519 
unsigned Z3_API Z3_model_get_num_sorts(Z3_context c, Z3_model m)
Return the number of uninterpreted sorts that m assigns an interpretation to.
def num_sorts(self)
Definition: z3py.py:6505
def sexpr (   self)
Return a textual representation of the s-expression representing the model.

Definition at line 6375 of file z3py.py.

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

6375  def sexpr(self):
6376  """Return a textual representation of the s-expression representing the model."""
6377  return Z3_model_to_string(self.ctx.ref(), self.model)
6378 
def sexpr(self)
Definition: z3py.py:6375
Z3_string Z3_API Z3_model_to_string(Z3_context c, Z3_model m)
Convert the given model into a string.
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 6543 of file z3py.py.

6543  def sorts(self):
6544  """Return all uninterpreted sorts that have an interpretation in the model `self`.
6545 
6546  >>> A = DeclareSort('A')
6547  >>> B = DeclareSort('B')
6548  >>> a1, a2 = Consts('a1 a2', A)
6549  >>> b1, b2 = Consts('b1 b2', B)
6550  >>> s = Solver()
6551  >>> s.add(a1 != a2, b1 != b2)
6552  >>> s.check()
6553  sat
6554  >>> m = s.model()
6555  >>> m.sorts()
6556  [A, B]
6557  """
6558  return [self.get_sort(i) for i in range(self.num_sorts())]
6559 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
def sorts(self)
Definition: z3py.py:6543
def num_sorts(self)
Definition: z3py.py:6505
def get_sort(self, idx)
Definition: z3py.py:6520
def translate (   self,
  target 
)
Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.

Definition at line 6666 of file z3py.py.

Referenced by ModelRef.__copy__(), and ModelRef.__deepcopy__().

6666  def translate(self, target):
6667  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
6668  """
6669  if z3_debug():
6670  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
6671  model = Z3_model_translate(self.ctx.ref(), self.model, target.ref())
6672  return ModelRef(model, target)
6673 
Z3_model Z3_API Z3_model_translate(Z3_context c, Z3_model m, Z3_context dst)
translate model from context c to context dst.
def z3_debug()
Definition: z3py.py:62
def translate(self, target)
Definition: z3py.py:6666
def update_value (   self,
  x,
  value 
)
Update the interpretation of a constant

Definition at line 6644 of file z3py.py.

6644  def update_value(self, x, value):
6645  """Update the interpretation of a constant"""
6646  if is_expr(x):
6647  x = x.decl()
6648  if is_func_decl(x) and x.arity() != 0 and isinstance(value, FuncInterp):
6649  fi1 = value.f
6650  fi2 = Z3_add_func_interp(x.ctx_ref(), self.model, x.ast, value.else_value().ast);
6651  fi2 = FuncInterp(fi2, x.ctx)
6652  for i in range(value.num_entries()):
6653  e = value.entry(i)
6654  n = Z3_func_entry_get_num_args(x.ctx_ref(), e.entry)
6655  v = AstVector()
6656  for j in range(n):
6657  v.push(e.arg_value(j))
6658  val = Z3_func_entry_get_value(x.ctx_ref(), e.entry)
6659  Z3_func_interp_add_entry(x.ctx_ref(), fi2.f, v.vector, val)
6660  return
6661  if not is_func_decl(x) or x.arity() != 0:
6662  raise Z3Exception("Expecting 0-ary function or constant expression")
6663  value = _py2expr(value)
6664  Z3_add_const_interp(x.ctx_ref(), self.model, x.ast, value.ast)
6665 
void Z3_API Z3_add_const_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast a)
Add a constant interpretation.
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
Z3_func_interp Z3_API Z3_add_func_interp(Z3_context c, Z3_model m, Z3_func_decl f, Z3_ast default_value)
Create a fresh func_interp object, add it to a model for a specified function. It has reference count...
def update_value(self, x, value)
Definition: z3py.py:6644
Z3_ast Z3_API Z3_func_entry_get_value(Z3_context c, Z3_func_entry e)
Return the value of this point.
unsigned Z3_API Z3_func_entry_get_num_args(Z3_context c, Z3_func_entry e)
Return the number of arguments in a Z3_func_entry object.
void Z3_API Z3_func_interp_add_entry(Z3_context c, Z3_func_interp fi, Z3_ast_vector args, Z3_ast value)
add a function entry to a function interpretation.
def is_expr(a)
Definition: z3py.py:1238
def is_func_decl(a)
Definition: z3py.py:846

Field Documentation

ctx
model