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

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  ast,
  ctx = None 
)

Definition at line 288 of file z3py.py.

288  def __init__(self, ast, ctx=None):
289  self.ast = ast
290  self.ctx = _get_ctx(ctx)
291  Z3_inc_ref(self.ctx.ref(), self.as_ast())
292 
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 293 of file z3py.py.

293  def __del__(self):
294  if self.ctx.ref() is not None:
295  Z3_dec_ref(self.ctx.ref(), self.as_ast())
296 
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 315 of file z3py.py.

Referenced by AstRef.__nonzero__().

315  def __bool__(self):
316  if is_true(self):
317  return True
318  elif is_false(self):
319  return False
320  elif is_eq(self) and self.num_args() == 2:
321  return self.arg(0).eq(self.arg(1))
322  else:
323  raise Z3Exception("Symbolic expressions cannot be cast to concrete Boolean values.")
324 
def is_eq(a)
Definition: z3py.py:1429
def eq(a, b)
Definition: z3py.py:412
def is_true(a)
Definition: z3py.py:1366
def is_false(a)
Definition: z3py.py:1383

◆ __copy__()

def __copy__ (   self)

Definition at line 379 of file z3py.py.

379  def __copy__(self):
380  return self.translate(self.ctx)
381 

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 297 of file z3py.py.

297  def __deepcopy__(self, memo={}):
298  return _to_ast_ref(self.ast, self.ctx)
299 

◆ __eq__()

def __eq__ (   self,
  other 
)

Definition at line 306 of file z3py.py.

Referenced by Probe.__ne__().

306  def __eq__(self, other):
307  return self.eq(other)
308 

◆ __hash__()

def __hash__ (   self)

Definition at line 309 of file z3py.py.

309  def __hash__(self):
310  return self.hash()
311 

◆ __nonzero__()

def __nonzero__ (   self)

Definition at line 312 of file z3py.py.

312  def __nonzero__(self):
313  return self.__bool__()
314 

◆ __repr__()

def __repr__ (   self)

Definition at line 303 of file z3py.py.

303  def __repr__(self):
304  return obj_to_string(self)
305 

◆ __str__()

def __str__ (   self)

Definition at line 300 of file z3py.py.

300  def __str__(self):
301  return obj_to_string(self)
302 

◆ as_ast()

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

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

334  def as_ast(self):
335  """Return a pointer to the corresponding C Z3_ast object."""
336  return self.ast
337 

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

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

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

◆ get_id()

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

Definition at line 338 of file z3py.py.

338  def get_id(self):
339  """Return unique identifier for object. It can be used for hash-tables and maps."""
340  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
341 
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 382 of file z3py.py.

Referenced by AstRef.__hash__().

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

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

Referenced by AstRef.__copy__().

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