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

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  ast,
  ctx = None 
)

Definition at line 298 of file z3py.py.

298  def __init__(self, ast, ctx=None):
299  self.ast = ast
300  self.ctx = _get_ctx(ctx)
301  Z3_inc_ref(self.ctx.ref(), self.as_ast())
302 
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 303 of file z3py.py.

303  def __del__(self):
304  if self.ctx.ref() is not None:
305  Z3_dec_ref(self.ctx.ref(), self.as_ast())
306 
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 325 of file z3py.py.

Referenced by AstRef.__nonzero__().

325  def __bool__(self):
326  if is_true(self):
327  return True
328  elif is_false(self):
329  return False
330  elif is_eq(self) and self.num_args() == 2:
331  return self.arg(0).eq(self.arg(1))
332  else:
333  raise Z3Exception("Symbolic expressions cannot be cast to concrete Boolean values.")
334 
def is_eq(a)
Definition: z3py.py:1503
def eq(a, b)
Definition: z3py.py:422
def is_true(a)
Definition: z3py.py:1429
def is_false(a)
Definition: z3py.py:1446

◆ __copy__()

def __copy__ (   self)

Definition at line 389 of file z3py.py.

389  def __copy__(self):
390  return self.translate(self.ctx)
391 

◆ __deepcopy__()

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 307 of file z3py.py.

307  def __deepcopy__(self, memo={}):
308  return _to_ast_ref(self.ast, self.ctx)
309 

◆ __eq__()

def __eq__ (   self,
  other 
)

Definition at line 316 of file z3py.py.

Referenced by Probe.__ne__().

316  def __eq__(self, other):
317  return self.eq(other)
318 

◆ __hash__()

def __hash__ (   self)

Definition at line 319 of file z3py.py.

319  def __hash__(self):
320  return self.hash()
321 

◆ __nonzero__()

def __nonzero__ (   self)

Definition at line 322 of file z3py.py.

322  def __nonzero__(self):
323  return self.__bool__()
324 

◆ __repr__()

def __repr__ (   self)

Definition at line 313 of file z3py.py.

313  def __repr__(self):
314  return obj_to_string(self)
315 

◆ __str__()

def __str__ (   self)

Definition at line 310 of file z3py.py.

310  def __str__(self):
311  return obj_to_string(self)
312 

◆ as_ast()

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

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

344  def as_ast(self):
345  """Return a pointer to the corresponding C Z3_ast object."""
346  return self.ast
347 

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

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

356  def eq(self, other):
357  """Return `True` if `self` and `other` are structurally identical.
358 
359  >>> x = Int('x')
360  >>> n1 = x + 1
361  >>> n2 = 1 + x
362  >>> n1.eq(n2)
363  False
364  >>> n1 = simplify(n1)
365  >>> n2 = simplify(n2)
366  >>> n1.eq(n2)
367  True
368  """
369  if z3_debug():
370  _z3_assert(is_ast(other), "Z3 AST expected")
371  return Z3_is_eq_ast(self.ctx_ref(), self.as_ast(), other.as_ast())
372 
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:422
def z3_debug()
Definition: z3py.py:58
def is_ast(a)
Definition: z3py.py:402

◆ get_id()

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

Definition at line 348 of file z3py.py.

348  def get_id(self):
349  """Return unique identifier for object. It can be used for hash-tables and maps."""
350  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
351 
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 392 of file z3py.py.

Referenced by AstRef.__hash__().

392  def hash(self):
393  """Return a hashcode for the `self`.
394 
395  >>> n1 = simplify(Int('x') + 1)
396  >>> n2 = simplify(2 + Int('x') - 1)
397  >>> n1.hash() == n2.hash()
398  True
399  """
400  return Z3_get_ast_hash(self.ctx_ref(), self.as_ast())
401 
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 335 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().

335  def sexpr(self):
336  """Return a string representing the AST node in s-expression notation.
337 
338  >>> x = Int('x')
339  >>> ((x + 1)*x).sexpr()
340  '(* (+ x 1) x)'
341  """
342  return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
343 
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 373 of file z3py.py.

Referenced by AstRef.__copy__().

373  def translate(self, target):
374  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
375 
376  >>> c1 = Context()
377  >>> c2 = Context()
378  >>> x = Int('x', c1)
379  >>> y = Int('y', c2)
380  >>> # Nodes in different contexts can't be mixed.
381  >>> # However, we can translate nodes from one context to another.
382  >>> x.translate(c2) + y
383  x + y
384  """
385  if z3_debug():
386  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
387  return _to_ast_ref(Z3_translate(self.ctx.ref(), self.as_ast(), target.ref()), target)
388 
def z3_debug()
Definition: z3py.py:58
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 300 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(), Optimize.assert_and_track(), 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(), Optimize.pop(), 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().