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 __str__ (self)
 
def __repr__ (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 271 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  ast,
  ctx = None 
)

Definition at line 273 of file z3py.py.

273  def __init__(self, ast, ctx=None):
274  self.ast = ast
275  self.ctx = _get_ctx(ctx)
276  Z3_inc_ref(self.ctx.ref(), self.as_ast())
277 
def as_ast(self)
Definition: z3py.py:296
def __init__(self, ast, ctx=None)
Definition: z3py.py:273
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 278 of file z3py.py.

278  def __del__(self):
279  Z3_dec_ref(self.ctx.ref(), self.as_ast())
280 
def as_ast(self)
Definition: z3py.py: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_...
def __del__(self)
Definition: z3py.py:278

Member Function Documentation

def __repr__ (   self)

Definition at line 284 of file z3py.py.

284  def __repr__(self):
285  return obj_to_string(self)
286 
def __repr__(self)
Definition: z3py.py:284
def __str__ (   self)

Definition at line 281 of file z3py.py.

281  def __str__(self):
282  return obj_to_string(self)
283 
def __str__(self)
Definition: z3py.py:281
def as_ast (   self)
Return a pointer to the corresponding C Z3_ast object.

Definition at line 296 of file z3py.py.

Referenced by AstRef.__del__(), ArrayRef.__getitem__(), ArithRef.__neg__(), AlgebraicNumRef.approx(), ExprRef.arg(), AlgebraicNumRef.as_decimal(), ExprRef.decl(), AstRef.eq(), AstRef.get_id(), SortRef.get_id(), FuncDeclRef.get_id(), ExprRef.get_id(), AstRef.hash(), ArrayRef.mk_default(), ExprRef.num_args(), AstRef.sexpr(), ExprRef.sort(), BoolRef.sort(), ArithRef.sort(), ArrayRef.sort(), and AstRef.translate().

296  def as_ast(self):
297  """Return a pointer to the corresponding C Z3_ast object."""
298  return self.ast
299 
def as_ast(self)
Definition: z3py.py:296
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 308 of file z3py.py.

Referenced by SortRef.cast(), and BoolSortRef.cast().

308  def eq(self, other):
309  """Return `True` if `self` and `other` are structurally identical.
310 
311  >>> x = Int('x')
312  >>> n1 = x + 1
313  >>> n2 = 1 + x
314  >>> n1.eq(n2)
315  False
316  >>> n1 = simplify(n1)
317  >>> n2 = simplify(n2)
318  >>> n1.eq(n2)
319  True
320  """
321  if __debug__:
322  _z3_assert(is_ast(other), "Z3 AST expected")
323  return Z3_is_eq_ast(self.ctx_ref(), self.as_ast(), other.as_ast())
324 
def as_ast(self)
Definition: z3py.py:296
Z3_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:308
def ctx_ref(self)
Definition: z3py.py:304
def is_ast(a)
Definition: z3py.py:351
def get_id (   self)
Return unique identifier for object. It can be used for hash-tables and maps.

Definition at line 300 of file z3py.py.

300  def get_id(self):
301  """Return unique identifier for object. It can be used for hash-tables and maps."""
302  return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
303 
def as_ast(self)
Definition: z3py.py:296
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:300
def ctx_ref(self)
Definition: z3py.py:304
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 341 of file z3py.py.

341  def hash(self):
342  """Return a hashcode for the `self`.
343 
344  >>> n1 = simplify(Int('x') + 1)
345  >>> n2 = simplify(2 + Int('x') - 1)
346  >>> n1.hash() == n2.hash()
347  True
348  """
349  return Z3_get_ast_hash(self.ctx_ref(), self.as_ast())
350 
def as_ast(self)
Definition: z3py.py:296
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...
def hash(self)
Definition: z3py.py:341
def ctx_ref(self)
Definition: z3py.py:304
def sexpr (   self)
Return an string representing the AST node in s-expression notation.

>>> x = Int('x')
>>> ((x + 1)*x).sexpr()
'(* (+ x 1) x)'

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

287  def sexpr(self):
288  """Return an string representing the AST node in s-expression notation.
289 
290  >>> x = Int('x')
291  >>> ((x + 1)*x).sexpr()
292  '(* (+ x 1) x)'
293  """
294  return Z3_ast_to_string(self.ctx_ref(), self.as_ast())
295 
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:296
def sexpr(self)
Definition: z3py.py:287
def ctx_ref(self)
Definition: z3py.py:304
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 325 of file z3py.py.

325  def translate(self, target):
326  """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`.
327 
328  >>> c1 = Context()
329  >>> c2 = Context()
330  >>> x = Int('x', c1)
331  >>> y = Int('y', c2)
332  >>> # Nodes in different contexts can't be mixed.
333  >>> # However, we can translate nodes from one context to another.
334  >>> x.translate(c2) + y
335  x + y
336  """
337  if __debug__:
338  _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
339  return _to_ast_ref(Z3_translate(self.ctx.ref(), self.as_ast(), target.ref()), target)
340 
def as_ast(self)
Definition: z3py.py:296
def translate(self, target)
Definition: z3py.py:325
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 275 of file z3py.py.

Referenced by ArithRef.__add__(), FuncDeclRef.__call__(), ArithRef.__div__(), ExprRef.__eq__(), Probe.__eq__(), ArithRef.__ge__(), Probe.__ge__(), ArrayRef.__getitem__(), AstMap.__getitem__(), ApplyResult.__getitem__(), ArithRef.__gt__(), Probe.__gt__(), ArithRef.__le__(), Probe.__le__(), ArithRef.__lt__(), Probe.__lt__(), ArithRef.__mod__(), ArithRef.__mul__(), ExprRef.__ne__(), Probe.__ne__(), ArithRef.__neg__(), ArithRef.__pow__(), ArithRef.__radd__(), ArithRef.__rdiv__(), ArithRef.__rmod__(), ArithRef.__rmul__(), ArithRef.__rpow__(), ArithRef.__rsub__(), ArithRef.__sub__(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), AlgebraicNumRef.approx(), ExprRef.arg(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), BoolSortRef.cast(), ApplyResult.convert_model(), ExprRef.decl(), FuncDeclRef.domain(), ArraySortRef.domain(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), AstMap.keys(), SortRef.kind(), ArrayRef.mk_default(), Optimize.model(), SortRef.name(), FuncDeclRef.name(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.query(), FuncDeclRef.range(), ArraySortRef.range(), Fixedpoint.set(), Optimize.set(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), ArithRef.sort(), ArrayRef.sort(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), and Fixedpoint.update_rule().