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

Public Member Functions

def __init__
 
def __del__ (self)
 
def __deepcopy__
 
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 __copy__ (self)
 
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 342 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  ast,
  ctx = None 
)

Definition at line 345 of file z3py.py.

345  def __init__(self, ast, ctx=None):
346  self.ast = ast
347  self.ctx = _get_ctx(ctx)
348  Z3_inc_ref(self.ctx.ref(), self.as_ast())
349 
def as_ast(self)
Definition: z3py.py:392
def __init__
Definition: z3py.py:345
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 350 of file z3py.py.

350  def __del__(self):
351  if self.ctx.ref() is not None and self.ast is not None and Z3_dec_ref is not None:
352  Z3_dec_ref(self.ctx.ref(), self.as_ast())
353  self.ast = None
354 
def as_ast(self)
Definition: z3py.py:392
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 __del__(self)
Definition: z3py.py:350

Member Function Documentation

def __bool__ (   self)

Definition at line 373 of file z3py.py.

Referenced by AstRef.__nonzero__().

373  def __bool__(self):
374  if is_true(self):
375  return True
376  elif is_false(self):
377  return False
378  elif is_eq(self) and self.num_args() == 2:
379  return self.arg(0).eq(self.arg(1))
380  else:
381  raise Z3Exception("Symbolic expressions cannot be cast to concrete Boolean values.")
382 
def is_eq(a)
Definition: z3py.py:1665
def __bool__(self)
Definition: z3py.py:373
def is_true(a)
Definition: z3py.py:1585
def eq(self, other)
Definition: z3py.py:404
def is_false(a)
Definition: z3py.py:1603
def __copy__ (   self)

Definition at line 437 of file z3py.py.

437  def __copy__(self):
438  return self.translate(self.ctx)
439 
def translate(self, target)
Definition: z3py.py:421
def __copy__(self)
Definition: z3py.py:437
def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 355 of file z3py.py.

355  def __deepcopy__(self, memo={}):
356  return _to_ast_ref(self.ast, self.ctx)
357 
def __deepcopy__
Definition: z3py.py:355
def __eq__ (   self,
  other 
)

Definition at line 364 of file z3py.py.

Referenced by Probe.__ne__().

364  def __eq__(self, other):
365  return self.eq(other)
366 
def __eq__(self, other)
Definition: z3py.py:364
def eq(self, other)
Definition: z3py.py:404
def __hash__ (   self)

Definition at line 367 of file z3py.py.

367  def __hash__(self):
368  return self.hash()
369 
def hash(self)
Definition: z3py.py:440
def __hash__(self)
Definition: z3py.py:367
def __nonzero__ (   self)

Definition at line 370 of file z3py.py.

370  def __nonzero__(self):
371  return self.__bool__()
372 
def __nonzero__(self)
Definition: z3py.py:370
def __bool__(self)
Definition: z3py.py:373
def __repr__ (   self)

Definition at line 361 of file z3py.py.

361  def __repr__(self):
362  return obj_to_string(self)
363 
def __repr__(self)
Definition: z3py.py:361
def __str__ (   self)

Definition at line 358 of file z3py.py.

358  def __str__(self):
359  return obj_to_string(self)
360 
def __str__(self)
Definition: z3py.py:358
def as_ast (   self)
def ctx_ref (   self)
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 404 of file z3py.py.

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

404  def eq(self, other):
405  """Return `True` if `self` and `other` are structurally identical.
406 
407  >>> x = Int('x')
408  >>> n1 = x + 1
409  >>> n2 = 1 + x
410  >>> n1.eq(n2)
411  False
412  >>> n1 = simplify(n1)
413  >>> n2 = simplify(n2)
414  >>> n1.eq(n2)
415  True
416  """
417  if z3_debug():
418  _z3_assert(is_ast(other), "Z3 AST expected")
419  return Z3_is_eq_ast(self.ctx_ref(), self.as_ast(), other.as_ast())
420 
def as_ast(self)
Definition: z3py.py:392
bool Z3_API Z3_is_eq_ast(Z3_context c, Z3_ast t1, Z3_ast t2)
Compare terms.
def eq(self, other)
Definition: z3py.py:404
def z3_debug()
Definition: z3py.py:62
def ctx_ref(self)
Definition: z3py.py:400
def is_ast(a)
Definition: z3py.py:451
def get_id (   self)
Return unique identifier for object. It can be used for hash-tables and maps.

Definition at line 396 of file z3py.py.

396  def get_id(self):
397  """Return unique identifier for object. It can be used for hash-tables and maps."""
398  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
399 
def as_ast(self)
Definition: z3py.py:392
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 get_id(self)
Definition: z3py.py:396
def ctx_ref(self)
Definition: z3py.py:400
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 440 of file z3py.py.

Referenced by AstRef.__hash__().

440  def hash(self):
441  """Return a hashcode for the `self`.
442 
443  >>> n1 = simplify(Int('x') + 1)
444  >>> n2 = simplify(2 + Int('x') - 1)
445  >>> n1.hash() == n2.hash()
446  True
447  """
448  return Z3_get_ast_hash(self.ctx_ref(), self.as_ast())
449 
450 
def as_ast(self)
Definition: z3py.py:392
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 but two different AST objects can m...
def hash(self)
Definition: z3py.py:440
def ctx_ref(self)
Definition: z3py.py:400
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 383 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().

383  def sexpr(self):
384  """Return a string representing the AST node in s-expression notation.
385 
386  >>> x = Int('x')
387  >>> ((x + 1)*x).sexpr()
388  '(* (+ x 1) x)'
389  """
390  return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
391 
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(self)
Definition: z3py.py:392
def sexpr(self)
Definition: z3py.py:383
def ctx_ref(self)
Definition: z3py.py:400
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 421 of file z3py.py.

Referenced by AstRef.__copy__().

421  def translate(self, target):
422  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
423 
424  >>> c1 = Context()
425  >>> c2 = Context()
426  >>> x = Int('x', c1)
427  >>> y = Int('y', c2)
428  >>> # Nodes in different contexts can't be mixed.
429  >>> # However, we can translate nodes from one context to another.
430  >>> x.translate(c2) + y
431  x + y
432  """
433  if z3_debug():
434  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
435  return _to_ast_ref(Z3_translate(self.ctx.ref(), self.as_ast(), target.ref()), target)
436 
def as_ast(self)
Definition: z3py.py:392
def translate(self, target)
Definition: z3py.py:421
def z3_debug()
Definition: z3py.py:62
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
ctx

Definition at line 347 of file z3py.py.

Referenced by ArithRef.__add__(), FuncDeclRef.__call__(), AstRef.__copy__(), AstRef.__deepcopy__(), AstMap.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Simplifier.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), ArithRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), Probe.__ge__(), AstMap.__getitem__(), ApplyResult.__getitem__(), ArithRef.__gt__(), Probe.__gt__(), ArithRef.__le__(), Probe.__le__(), ArithRef.__lt__(), Probe.__lt__(), ArithRef.__mod__(), BoolRef.__mul__(), ArithRef.__mul__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), ArithRef.__pow__(), ArithRef.__radd__(), ArithRef.__rdiv__(), ArithRef.__rmod__(), ArithRef.__rmul__(), ArithRef.__rpow__(), ArithRef.__rsub__(), ArithRef.__sub__(), Simplifier.add(), 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(), ArraySortRef.domain_n(), ParserContext.from_string(), 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(), Simplifier.param_descrs(), Tactic.param_descrs(), FuncDeclRef.params(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), AlgebraicNumRef.poly(), Fixedpoint.query(), FuncDeclRef.range(), ArraySortRef.range(), Fixedpoint.set(), Optimize.set(), Optimize.set_on_model(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), ArithRef.sort(), ArrayRef.sort(), FiniteDomainRef.sort(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Optimize.unsat_core(), Fixedpoint.update_rule(), and Simplifier.using_params().