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 __deepcopy__ (self, memo={})
 
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 275 of file z3py.py.

Constructor & Destructor Documentation

§ __init__()

def __init__ (   self,
  ast,
  ctx = None 
)

Definition at line 277 of file z3py.py.

277  def __init__(self, ast, ctx=None):
278  self.ast = ast
279  self.ctx = _get_ctx(ctx)
280  Z3_inc_ref(self.ctx.ref(), self.as_ast())
281 
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 282 of file z3py.py.

282  def __del__(self):
283  if self.ctx.ref() is not None:
284  Z3_dec_ref(self.ctx.ref(), self.as_ast())
285 
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 304 of file z3py.py.

Referenced by AstRef.__nonzero__().

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

§ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 286 of file z3py.py.

286  def __deepcopy__(self, memo={}):
287  return _to_ast_ref(self.ast, self.ctx)
288 

§ __eq__()

def __eq__ (   self,
  other 
)

Definition at line 295 of file z3py.py.

Referenced by Probe.__ne__().

295  def __eq__(self, other):
296  return self.eq(other)
297 

§ __hash__()

def __hash__ (   self)

Definition at line 298 of file z3py.py.

298  def __hash__(self):
299  return self.hash()
300 

§ __nonzero__()

def __nonzero__ (   self)

Definition at line 301 of file z3py.py.

301  def __nonzero__(self):
302  return self.__bool__()
303 

§ __repr__()

def __repr__ (   self)

Definition at line 292 of file z3py.py.

292  def __repr__(self):
293  return obj_to_string(self)
294 

§ __str__()

def __str__ (   self)

Definition at line 289 of file z3py.py.

289  def __str__(self):
290  return obj_to_string(self)
291 

§ as_ast()

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

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

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

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

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

335  def eq(self, other):
336  """Return `True` if `self` and `other` are structurally identical.
337 
338  >>> x = Int('x')
339  >>> n1 = x + 1
340  >>> n2 = 1 + x
341  >>> n1.eq(n2)
342  False
343  >>> n1 = simplify(n1)
344  >>> n2 = simplify(n2)
345  >>> n1.eq(n2)
346  True
347  """
348  if __debug__:
349  _z3_assert(is_ast(other), "Z3 AST expected")
350  return Z3_is_eq_ast(self.ctx_ref(), self.as_ast(), other.as_ast())
351 
Z3_bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
def eq(a, b)
Definition: z3py.py:398
def is_ast(a)
Definition: z3py.py:378

§ get_id()

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

Definition at line 327 of file z3py.py.

327  def get_id(self):
328  """Return unique identifier for object. It can be used for hash-tables and maps."""
329  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
330 
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.

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

Referenced by AstRef.__hash__().

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

§ sexpr()

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 314 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().

314  def sexpr(self):
315  """Return a string representing the AST node in s-expression notation.
316 
317  >>> x = Int('x')
318  >>> ((x + 1)*x).sexpr()
319  '(* (+ x 1) x)'
320  """
321  return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
322 
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 352 of file z3py.py.

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

Referenced by FuncDeclRef.__call__(), Probe.__call__(), AstRef.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), 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_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(), SortRef.kind(), Optimize.maximize(), Optimize.minimize(), 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.pop(), Optimize.pop(), Fixedpoint.push(), Optimize.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), 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().