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

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  ast,
  ctx = None 
)

Definition at line 292 of file z3py.py.

292  def __init__(self, ast, ctx=None):
293  self.ast = ast
294  self.ctx = _get_ctx(ctx)
295  Z3_inc_ref(self.ctx.ref(), self.as_ast())
296 
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 297 of file z3py.py.

297  def __del__(self):
298  if self.ctx.ref() is not None:
299  Z3_dec_ref(self.ctx.ref(), self.as_ast())
300 
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 319 of file z3py.py.

Referenced by AstRef.__nonzero__().

319  def __bool__(self):
320  if is_true(self):
321  return True
322  elif is_false(self):
323  return False
324  elif is_eq(self) and self.num_args() == 2:
325  return self.arg(0).eq(self.arg(1))
326  else:
327  raise Z3Exception("Symbolic expressions cannot be cast to concrete Boolean values.")
328 
def is_eq(a)
Definition: z3py.py:1492
def eq(a, b)
Definition: z3py.py:416
def is_true(a)
Definition: z3py.py:1418
def is_false(a)
Definition: z3py.py:1435

◆ __copy__()

def __copy__ (   self)

Definition at line 383 of file z3py.py.

383  def __copy__(self):
384  return self.translate(self.ctx)
385 

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 301 of file z3py.py.

301  def __deepcopy__(self, memo={}):
302  return _to_ast_ref(self.ast, self.ctx)
303 

◆ __eq__()

def __eq__ (   self,
  other 
)

Definition at line 310 of file z3py.py.

Referenced by Probe.__ne__().

310  def __eq__(self, other):
311  return self.eq(other)
312 

◆ __hash__()

def __hash__ (   self)

Definition at line 313 of file z3py.py.

313  def __hash__(self):
314  return self.hash()
315 

◆ __nonzero__()

def __nonzero__ (   self)

Definition at line 316 of file z3py.py.

316  def __nonzero__(self):
317  return self.__bool__()
318 

◆ __repr__()

def __repr__ (   self)

Definition at line 307 of file z3py.py.

307  def __repr__(self):
308  return obj_to_string(self)
309 

◆ __str__()

def __str__ (   self)

Definition at line 304 of file z3py.py.

304  def __str__(self):
305  return obj_to_string(self)
306 

◆ as_ast()

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

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

338  def as_ast(self):
339  """Return a pointer to the corresponding C Z3_ast object."""
340  return self.ast
341 

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

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

350  def eq(self, other):
351  """Return `True` if `self` and `other` are structurally identical.
352 
353  >>> x = Int('x')
354  >>> n1 = x + 1
355  >>> n2 = 1 + x
356  >>> n1.eq(n2)
357  False
358  >>> n1 = simplify(n1)
359  >>> n2 = simplify(n2)
360  >>> n1.eq(n2)
361  True
362  """
363  if __debug__:
364  _z3_assert(is_ast(other), "Z3 AST expected")
365  return Z3_is_eq_ast(self.ctx_ref(), self.as_ast(), other.as_ast())
366 
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:416
def is_ast(a)
Definition: z3py.py:396

◆ get_id()

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

Definition at line 342 of file z3py.py.

342  def get_id(self):
343  """Return unique identifier for object. It can be used for hash-tables and maps."""
344  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
345 
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 386 of file z3py.py.

Referenced by AstRef.__hash__().

386  def hash(self):
387  """Return a hashcode for the `self`.
388 
389  >>> n1 = simplify(Int('x') + 1)
390  >>> n2 = simplify(2 + Int('x') - 1)
391  >>> n1.hash() == n2.hash()
392  True
393  """
394  return Z3_get_ast_hash(self.ctx_ref(), self.as_ast())
395 
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 329 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().

329  def sexpr(self):
330  """Return a string representing the AST node in s-expression notation.
331 
332  >>> x = Int('x')
333  >>> ((x + 1)*x).sexpr()
334  '(* (+ x 1) x)'
335  """
336  return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
337 
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 367 of file z3py.py.

Referenced by AstRef.__copy__().

367  def translate(self, target):
368  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
369 
370  >>> c1 = Context()
371  >>> c2 = Context()
372  >>> x = Int('x', c1)
373  >>> y = Int('y', c2)
374  >>> # Nodes in different contexts can't be mixed.
375  >>> # However, we can translate nodes from one context to another.
376  >>> x.translate(c2) + y
377  x + y
378  """
379  if __debug__:
380  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
381  return _to_ast_ref(Z3_translate(self.ctx.ref(), self.as_ast(), target.ref()), target)
382 
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 294 of file z3py.py.

Referenced by FuncDeclRef.__call__(), Probe.__call__(), AstRef.__copy__(), 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(), 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(), Optimize.unsat_core(), and Fixedpoint.update_rule().