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

Public Member Functions

def __init__ (self, ast, ctx=None)
 
def __del__ (self)
 
def __str__ (self)
 
def __repr__ (self)
 
def __eq__ (self, other)
 
def __hash__ (self)
 
def __nonzero__ (self)
 
def __bool__ (self)
 
def sexpr (self)
 
def as_ast (self)
 
def get_id (self)
 
def ctx_ref (self)
 
def eq (self, other)
 
def translate (self, target)
 
def hash (self)
 
- Public Member Functions inherited from Z3PPObject
def use_pp (self)
 

Data Fields

 ast
 
 ctx
 

Detailed Description

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

Definition at line 280 of file z3py.py.

Constructor & Destructor Documentation

§ __init__()

def __init__ (   self,
  ast,
  ctx = None 
)

Definition at line 282 of file z3py.py.

282  def __init__(self, ast, ctx=None):
283  self.ast = ast
284  self.ctx = _get_ctx(ctx)
285  Z3_inc_ref(self.ctx.ref(), self.as_ast())
286 
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_...

§ __del__()

def __del__ (   self)

Definition at line 287 of file z3py.py.

287  def __del__(self):
288  if self.ctx.ref() is not None:
289  Z3_dec_ref(self.ctx.ref(), self.as_ast())
290 
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_...

Member Function Documentation

§ __bool__()

def __bool__ (   self)

Definition at line 306 of file z3py.py.

Referenced by AstRef.__nonzero__().

306  def __bool__(self):
307  if is_true(self):
308  return True
309  elif is_false(self):
310  return False
311  elif is_eq(self) and self.num_args() == 2:
312  return self.arg(0).eq(self.arg(1))
313  else:
314  raise Z3Exception("Symbolic expressions cannot be cast to concrete Boolean values.")
315 
def is_eq(a)
Definition: z3py.py:1387
def eq(a, b)
Definition: z3py.py:400
def is_true(a)
Definition: z3py.py:1324
def is_false(a)
Definition: z3py.py:1341

§ __eq__()

def __eq__ (   self,
  other 
)

Definition at line 297 of file z3py.py.

Referenced by Probe.__ne__().

297  def __eq__(self, other):
298  return self.eq(other)
299 

§ __hash__()

def __hash__ (   self)

Definition at line 300 of file z3py.py.

300  def __hash__(self):
301  return self.hash()
302 

§ __nonzero__()

def __nonzero__ (   self)

Definition at line 303 of file z3py.py.

303  def __nonzero__(self):
304  return self.__bool__()
305 

§ __repr__()

def __repr__ (   self)

Definition at line 294 of file z3py.py.

294  def __repr__(self):
295  return obj_to_string(self)
296 

§ __str__()

def __str__ (   self)

Definition at line 291 of file z3py.py.

291  def __str__(self):
292  return obj_to_string(self)
293 

§ as_ast()

def as_ast (   self)
Return a pointer to the corresponding C Z3_ast object.

Definition at line 325 of file z3py.py.

Referenced by AstRef.__del__(), ExprRef.arg(), FiniteDomainRef.as_string(), FiniteDomainNumRef.as_string(), ExprRef.decl(), 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(), FiniteDomainRef.sort(), and AstRef.translate().

325  def as_ast(self):
326  """Return a pointer to the corresponding C Z3_ast object."""
327  return self.ast
328 

§ ctx_ref()

def ctx_ref (   self)

§ eq()

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

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

337  def eq(self, other):
338  """Return `True` if `self` and `other` are structurally identical.
339 
340  >>> x = Int('x')
341  >>> n1 = x + 1
342  >>> n2 = 1 + x
343  >>> n1.eq(n2)
344  False
345  >>> n1 = simplify(n1)
346  >>> n2 = simplify(n2)
347  >>> n1.eq(n2)
348  True
349  """
350  if __debug__:
351  _z3_assert(is_ast(other), "Z3 AST expected")
352  return Z3_is_eq_ast(self.ctx_ref(), self.as_ast(), other.as_ast())
353 
def eq(a, b)
Definition: z3py.py:400
def is_ast(a)
Definition: z3py.py:380

§ get_id()

def get_id (   self)
Return unique identifier for object. It can be used for hash-tables and maps.

Definition at line 329 of file z3py.py.

329  def get_id(self):
330  """Return unique identifier for object. It can be used for hash-tables and maps."""
331  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
332 

§ hash()

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

Referenced by AstRef.__hash__().

370  def hash(self):
371  """Return a hashcode for the `self`.
372 
373  >>> n1 = simplify(Int('x') + 1)
374  >>> n2 = simplify(2 + Int('x') - 1)
375  >>> n1.hash() == n2.hash()
376  True
377  """
378  return Z3_get_ast_hash(self.ctx_ref(), self.as_ast())
379 

§ sexpr()

def sexpr (   self)
Return an string representing the AST node in s-expression notation.

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

Definition at line 316 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().

316  def sexpr(self):
317  """Return an string representing the AST node in s-expression notation.
318 
319  >>> x = Int('x')
320  >>> ((x + 1)*x).sexpr()
321  '(* (+ x 1) x)'
322  """
323  return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
324 
Z3_string Z3_API Z3_ast_to_string(Z3_context c, Z3_ast a)
Convert the given AST node into a string.

§ translate()

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

354  def translate(self, target):
355  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
356 
357  >>> c1 = Context()
358  >>> c2 = Context()
359  >>> x = Int('x', c1)
360  >>> y = Int('y', c2)
361  >>> # Nodes in different contexts can't be mixed.
362  >>> # However, we can translate nodes from one context to another.
363  >>> x.translate(c2) + y
364  x + y
365  """
366  if __debug__:
367  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
368  return _to_ast_ref(Z3_translate(self.ctx.ref(), self.as_ast(), target.ref()), target)
369 
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...

Field Documentation

§ ast

ast

§ ctx

ctx

Definition at line 284 of file z3py.py.

Referenced by FuncDeclRef.__call__(), Probe.__call__(), AstRef.__del__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), ExprRef.__eq__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), ApplyResult.__len__(), Probe.__lt__(), ExprRef.__ne__(), Probe.__ne__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ExprRef.arg(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), BoolSortRef.cast(), Optimize.check(), ApplyResult.convert_model(), AstRef.ctx_ref(), ExprRef.decl(), FuncDeclRef.domain(), Optimize.from_file(), Optimize.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_num_levels(), Fixedpoint.get_rules(), Fixedpoint.help(), Optimize.help(), Tactic.help(), SortRef.kind(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), SortRef.name(), FuncDeclRef.name(), 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(), FuncDeclRef.range(), 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(), ExprRef.sort(), BoolRef.sort(), FiniteDomainRef.sort(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), AstRef.translate(), and Fixedpoint.update_rule().