Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
Public Member Functions | Data Fields
AstRef Class Reference
+ Inheritance diagram for AstRef:

Public Member Functions

def __init__
 
def __del__
 
def __deepcopy__
 
def __str__
 
def __repr__
 
def __eq__
 
def __hash__
 
def __nonzero__
 
def __bool__
 
def sexpr
 
def as_ast
 
def get_id
 
def ctx_ref
 
def eq
 
def translate
 
def __copy__
 
def hash
 
- Public Member Functions inherited from Z3PPObject
def use_pp
 

Data Fields

 ast
 
 ctx
 

Detailed Description

AST are Direct Acyclic Graphs (DAGs) used to represent sorts, declarations and expressions.

Definition at line 296 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  ast,
  ctx = None 
)

Definition at line 298 of file z3py.py.

299  def __init__(self, ast, ctx=None):
300  self.ast = ast
301  self.ctx = _get_ctx(ctx)
302  Z3_inc_ref(self.ctx.ref(), self.as_ast())
def __init__
Definition: z3py.py:298
def as_ast
Definition: z3py.py:344
void Z3_API Z3_inc_ref(Z3_context c, Z3_ast a)
Increment the reference counter of the given AST. The context c should have been created using Z3_mk_...
def __del__ (   self)

Definition at line 303 of file z3py.py.

304  def __del__(self):
305  if self.ctx.ref() is not None:
306  Z3_dec_ref(self.ctx.ref(), self.as_ast())
def __del__
Definition: z3py.py:303
void Z3_API Z3_dec_ref(Z3_context c, Z3_ast a)
Decrement the reference counter of the given AST. The context c should have been created using Z3_mk_...
def as_ast
Definition: z3py.py:344

Member Function Documentation

def __bool__ (   self)

Definition at line 325 of file z3py.py.

Referenced by AstRef.__nonzero__().

326  def __bool__(self):
327  if is_true(self):
328  return True
329  elif is_false(self):
330  return False
331  elif is_eq(self) and self.num_args() == 2:
332  return self.arg(0).eq(self.arg(1))
333  else:
334  raise Z3Exception("Symbolic expressions cannot be cast to concrete Boolean values.")
def __bool__
Definition: z3py.py:325
def is_eq
Definition: z3py.py:1503
def is_true
Definition: z3py.py:1429
def eq
Definition: z3py.py:356
def is_false
Definition: z3py.py:1446
def __copy__ (   self)

Definition at line 389 of file z3py.py.

390  def __copy__(self):
391  return self.translate(self.ctx)
def __copy__
Definition: z3py.py:389
def translate
Definition: z3py.py:373
def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 307 of file z3py.py.

308  def __deepcopy__(self, memo={}):
309  return _to_ast_ref(self.ast, self.ctx)
def __deepcopy__
Definition: z3py.py:307
def __eq__ (   self,
  other 
)

Definition at line 316 of file z3py.py.

Referenced by Probe.__ne__().

317  def __eq__(self, other):
318  return self.eq(other)
def eq
Definition: z3py.py:356
def __eq__
Definition: z3py.py:316
def __hash__ (   self)

Definition at line 319 of file z3py.py.

320  def __hash__(self):
321  return self.hash()
def __hash__
Definition: z3py.py:319
def hash
Definition: z3py.py:392
def __nonzero__ (   self)

Definition at line 322 of file z3py.py.

323  def __nonzero__(self):
324  return self.__bool__()
def __bool__
Definition: z3py.py:325
def __nonzero__
Definition: z3py.py:322
def __repr__ (   self)

Definition at line 313 of file z3py.py.

314  def __repr__(self):
315  return obj_to_string(self)
def __repr__
Definition: z3py.py:313
def __str__ (   self)

Definition at line 310 of file z3py.py.

311  def __str__(self):
312  return obj_to_string(self)
def __str__
Definition: z3py.py:310
def as_ast (   self)
Return a pointer to the corresponding C Z3_ast object.

Definition at line 344 of file z3py.py.

Referenced by AstRef.__del__(), ArrayRef.__getitem__(), ArithRef.__neg__(), AlgebraicNumRef.approx(), ExprRef.arg(), AlgebraicNumRef.as_decimal(), FiniteDomainRef.as_string(), FiniteDomainNumRef.as_string(), ExprRef.decl(), ArrayRef.default(), AstRef.eq(), AstRef.get_id(), SortRef.get_id(), FuncDeclRef.get_id(), ExprRef.get_id(), AstRef.hash(), ExprRef.num_args(), AstRef.sexpr(), ExprRef.sort(), BoolRef.sort(), ArithRef.sort(), ArrayRef.sort(), FiniteDomainRef.sort(), and AstRef.translate().

345  def as_ast(self):
346  """Return a pointer to the corresponding C Z3_ast object."""
347  return self.ast
def as_ast
Definition: z3py.py:344
def ctx_ref (   self)
Return a reference to the C context where this AST node is stored.

Definition at line 352 of file z3py.py.

Referenced by FuncDeclRef.__call__(), ArithRef.__div__(), SortRef.__eq__(), ExprRef.__eq__(), ArithRef.__ge__(), ArrayRef.__getitem__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), ArithRef.__mod__(), SortRef.__ne__(), ExprRef.__ne__(), ArithRef.__neg__(), ArithRef.__pow__(), ArithRef.__rdiv__(), ArithRef.__rmod__(), ArithRef.__rpow__(), AlgebraicNumRef.approx(), ExprRef.arg(), FuncDeclRef.arity(), SortRef.as_ast(), FuncDeclRef.as_ast(), AlgebraicNumRef.as_decimal(), FiniteDomainRef.as_string(), FiniteDomainNumRef.as_string(), ExprRef.decl(), ArrayRef.default(), FuncDeclRef.domain(), ArraySortRef.domain(), AstRef.eq(), AstRef.get_id(), SortRef.get_id(), FuncDeclRef.get_id(), ExprRef.get_id(), AstRef.hash(), FuncDeclRef.kind(), SortRef.name(), FuncDeclRef.name(), ExprRef.num_args(), FuncDeclRef.params(), FuncDeclRef.range(), ArraySortRef.range(), AstRef.sexpr(), FiniteDomainSortRef.size(), BoolRef.sort(), ArithRef.sort(), ArrayRef.sort(), and FiniteDomainRef.sort().

353  def ctx_ref(self):
354  """Return a reference to the C context where this AST node is stored."""
355  return self.ctx.ref()
def ctx_ref
Definition: z3py.py:352
def eq (   self,
  other 
)
Return `True` if `self` and `other` are structurally identical.

>>> x = Int('x')
>>> n1 = x + 1
>>> n2 = 1 + x
>>> n1.eq(n2)
False
>>> n1 = simplify(n1)
>>> n2 = simplify(n2)
>>> n1.eq(n2)
True

Definition at line 356 of file z3py.py.

Referenced by AstRef.__bool__(), AstRef.__eq__(), SortRef.cast(), and BoolSortRef.cast().

357  def eq(self, other):
358  """Return `True` if `self` and `other` are structurally identical.
359 
360  >>> x = Int('x')
361  >>> n1 = x + 1
362  >>> n2 = 1 + x
363  >>> n1.eq(n2)
364  False
365  >>> n1 = simplify(n1)
366  >>> n2 = simplify(n2)
367  >>> n1.eq(n2)
368  True
369  """
370  if z3_debug():
371  _z3_assert(is_ast(other), "Z3 AST expected")
372  return Z3_is_eq_ast(self.ctx_ref(), self.as_ast(), other.as_ast())
def is_ast
Definition: z3py.py:402
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
def eq
Definition: z3py.py:356
def as_ast
Definition: z3py.py:344
def z3_debug
Definition: z3py.py:58
def ctx_ref
Definition: z3py.py:352
def get_id (   self)
Return unique identifier for object. It can be used for hash-tables and maps.

Definition at line 348 of file z3py.py.

349  def get_id(self):
350  """Return unique identifier for object. It can be used for hash-tables and maps."""
351  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
def get_id
Definition: z3py.py:348
unsigned Z3_API Z3_get_ast_id(Z3_context c, Z3_ast t)
Return a unique identifier for t. The identifier is unique up to structural equality. Thus, two ast nodes created by the same context and having the same children and same function symbols have the same identifiers. Ast nodes created in the same context, but having different children or different functions have different identifiers. Variables and quantifiers are also assigned different identifiers according to their structure.
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
def hash (   self)
Return a hashcode for the `self`.

>>> n1 = simplify(Int('x') + 1)
>>> n2 = simplify(2 + Int('x') - 1)
>>> n1.hash() == n2.hash()
True

Definition at line 392 of file z3py.py.

Referenced by AstRef.__hash__().

393  def hash(self):
394  """Return a hashcode for the `self`.
395 
396  >>> n1 = simplify(Int('x') + 1)
397  >>> n2 = simplify(2 + Int('x') - 1)
398  >>> n1.hash() == n2.hash()
399  True
400  """
401  return Z3_get_ast_hash(self.ctx_ref(), self.as_ast())
unsigned Z3_API Z3_get_ast_hash(Z3_context c, Z3_ast a)
Return a hash code for the given AST. The hash code is structural. You can use Z3_get_ast_id intercha...
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
def hash
Definition: z3py.py:392
def sexpr (   self)
Return a string representing the AST node in s-expression notation.

>>> x = Int('x')
>>> ((x + 1)*x).sexpr()
'(* (+ x 1) x)'

Definition at line 335 of file z3py.py.

Referenced by ArithRef.__div__(), BitVecRef.__div__(), BitVecRef.__ge__(), ArrayRef.__getitem__(), BitVecRef.__gt__(), BitVecRef.__le__(), BitVecRef.__lshift__(), BitVecRef.__lt__(), BitVecRef.__mod__(), ArithRef.__rdiv__(), BitVecRef.__rdiv__(), Fixedpoint.__repr__(), Optimize.__repr__(), BitVecRef.__rlshift__(), BitVecRef.__rmod__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), BitVecSortRef.cast(), and FPSortRef.cast().

336  def sexpr(self):
337  """Return a string representing the AST node in s-expression notation.
338 
339  >>> x = Int('x')
340  >>> ((x + 1)*x).sexpr()
341  '(* (+ x 1) x)'
342  """
343  return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
def sexpr
Definition: z3py.py:335
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.
def as_ast
Definition: z3py.py:344
def ctx_ref
Definition: z3py.py:352
def translate (   self,
  target 
)
Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.

>>> c1 = Context()
>>> c2 = Context()
>>> x  = Int('x', c1)
>>> y  = Int('y', c2)
>>> # Nodes in different contexts can't be mixed.
>>> # However, we can translate nodes from one context to another.
>>> x.translate(c2) + y
x + y

Definition at line 373 of file z3py.py.

Referenced by AstRef.__copy__().

374  def translate(self, target):
375  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
376 
377  >>> c1 = Context()
378  >>> c2 = Context()
379  >>> x = Int('x', c1)
380  >>> y = Int('y', c2)
381  >>> # Nodes in different contexts can't be mixed.
382  >>> # However, we can translate nodes from one context to another.
383  >>> x.translate(c2) + y
384  x + y
385  """
386  if z3_debug():
387  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
388  return _to_ast_ref(Z3_translate(self.ctx.ref(), self.as_ast(), target.ref()), target)
def as_ast
Definition: z3py.py:344
def z3_debug
Definition: z3py.py:58
Z3_ast Z3_API Z3_translate(Z3_context source, Z3_ast a, Z3_context target)
Translate/Copy the AST a from context source to context target. AST a must have been created using co...
def translate
Definition: z3py.py:373

Field Documentation

ast

Definition at line 299 of file z3py.py.

Referenced by FuncDeclRef.__call__(), AstRef.__deepcopy__(), SortRef.__eq__(), SortRef.__ne__(), FuncDeclRef.arity(), AstRef.as_ast(), SortRef.as_ast(), FuncDeclRef.as_ast(), ExprRef.as_ast(), FuncDeclRef.as_func_decl(), FuncDeclRef.domain(), ArraySortRef.domain(), SortRef.kind(), FuncDeclRef.kind(), SortRef.name(), FuncDeclRef.name(), FuncDeclRef.params(), FuncDeclRef.range(), ArraySortRef.range(), and FiniteDomainSortRef.size().

ctx

Definition at line 300 of file z3py.py.

Referenced by ArithRef.__add__(), FuncDeclRef.__call__(), AstRef.__copy__(), AstRef.__deepcopy__(), AstMap.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), ArithRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), Probe.__ge__(), ArrayRef.__getitem__(), AstMap.__getitem__(), ApplyResult.__getitem__(), ArithRef.__gt__(), Probe.__gt__(), ArithRef.__le__(), Probe.__le__(), ArithRef.__lt__(), Probe.__lt__(), ArithRef.__mod__(), ArithRef.__mul__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), ArithRef.__pow__(), ArithRef.__radd__(), ArithRef.__rdiv__(), ArithRef.__rmod__(), ArithRef.__rmul__(), ArithRef.__rpow__(), ArithRef.__rsub__(), ArithRef.__sub__(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), AlgebraicNumRef.approx(), ExprRef.arg(), ApplyResult.as_expr(), Optimize.assert_and_track(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), BoolSortRef.cast(), ExprRef.decl(), ArrayRef.default(), FuncDeclRef.domain(), ArraySortRef.domain(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), AstMap.keys(), SortRef.kind(), Optimize.model(), SortRef.name(), FuncDeclRef.name(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), FuncDeclRef.params(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), FuncDeclRef.range(), ArraySortRef.range(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), ArithRef.sort(), ArrayRef.sort(), FiniteDomainRef.sort(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Optimize.unsat_core(), and Fixedpoint.update_rule().