Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Data Fields
AstRef Class Reference
+ Inheritance diagram for AstRef:

Public Member Functions

def __init__
def __del__
def __str__
def __repr__
def sexpr
def as_ast
def get_id
def ctx_ref
def eq
def translate
def hash

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.

00273 
00274     def __init__(self, ast, ctx=None):
00275         self.ast  = ast
00276         self.ctx  = _get_ctx(ctx)
00277         Z3_inc_ref(self.ctx.ref(), self.as_ast())

def __del__ (   self)

Definition at line 278 of file z3py.py.

00278 
00279     def __del__(self):
00280         Z3_dec_ref(self.ctx.ref(), self.as_ast())


Member Function Documentation

def __repr__ (   self)

Definition at line 284 of file z3py.py.

00284 
00285     def __repr__(self):
00286         return obj_to_string(self)

def __str__ (   self)

Definition at line 281 of file z3py.py.

00281 
00282     def __str__(self):
00283         return obj_to_string(self)

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

Reimplemented in QuantifierRef, PatternRef, ExprRef, FuncDeclRef, and SortRef.

Definition at line 296 of file z3py.py.

Referenced by AstRef.__del__(), ExprRef.arg(), 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(), and AstRef.translate().

00296 
00297     def as_ast(self):
00298         """Return a pointer to the corresponding C Z3_ast object."""
00299         return self.ast

def ctx_ref (   self)
Return a reference to the C context where this AST node is stored.

Definition at line 305 of file z3py.py.

Referenced by FuncDeclRef.__call__(), SortRef.__eq__(), ExprRef.__eq__(), SortRef.__ne__(), ExprRef.__ne__(), ExprRef.arg(), FuncDeclRef.arity(), SortRef.as_ast(), FuncDeclRef.as_ast(), ExprRef.decl(), FuncDeclRef.domain(), AstRef.eq(), AstRef.get_id(), SortRef.get_id(), FuncDeclRef.get_id(), ExprRef.get_id(), AstRef.hash(), FuncDeclRef.kind(), SortRef.name(), FuncDeclRef.name(), ExprRef.num_args(), FuncDeclRef.range(), AstRef.sexpr(), and BoolRef.sort().

00305 
00306     def ctx_ref(self):
00307         """Return a reference to the C context where this AST node is stored."""
00308         return self.ctx.ref()
        
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 309 of file z3py.py.

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

00309 
00310     def eq(self, other):
00311         """Return `True` if `self` and `other` are structurally identical.
00312         
00313         >>> x = Int('x')
00314         >>> n1 = x + 1
00315         >>> n2 = 1 + x
00316         >>> n1.eq(n2)
00317         False
00318         >>> n1 = simplify(n1)
00319         >>> n2 = simplify(n2)
00320         >>> n1.eq(n2)
00321         True
00322         """
00323         if __debug__:
00324             _z3_assert(is_ast(other), "Z3 AST expected")
00325         return Z3_is_eq_ast(self.ctx_ref(), self.as_ast(), other.as_ast())
    
def get_id (   self)
Return unique identifier for object. It can be used for hash-tables and maps.

Reimplemented in QuantifierRef, PatternRef, ExprRef, FuncDeclRef, and SortRef.

Definition at line 300 of file z3py.py.

00300 
00301     def get_id(self):
00302         """Return unique identifier for object. It can be used for hash-tables and maps."""
00303         return Z3_get_ast_id(self.ctx_ref(), self.as_ast())
00304 

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

00342 
00343     def hash(self):
00344         """Return a hashcode for the `self`.
00345         
00346         >>> n1 = simplify(Int('x') + 1)
00347         >>> n2 = simplify(2 + Int('x') - 1)
00348         >>> n1.hash() == n2.hash()
00349         True
00350         """
00351         return Z3_get_ast_hash(self.ctx_ref(), self.as_ast())

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__(), BitVecRef.__rlshift__(), BitVecRef.__rmod__(), BitVecRef.__rrshift__(), BitVecRef.__rshift__(), and BitVecSortRef.cast().

00287 
00288     def sexpr(self):
00289         """Return an string representing the AST node in s-expression notation.
00290         
00291         >>> x = Int('x')
00292         >>> ((x + 1)*x).sexpr()
00293         '(* (+ x 1) x)'
00294         """
00295         return Z3_ast_to_string(self.ctx_ref(), self.as_ast())

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

00326 
00327     def translate(self, target):
00328         """Translate `self` to the context `target`. That is, return a copy of `self` in the context `target`. 
00329         
00330         >>> c1 = Context()
00331         >>> c2 = Context()
00332         >>> x  = Int('x', c1)
00333         >>> y  = Int('y', c2)
00334         >>> # Nodes in different contexts can't be mixed.
00335         >>> # However, we can translate nodes from one context to another.
00336         >>> x.translate(c2) + y
00337         x + y
00338         """
00339         if __debug__:
00340             _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
00341         return _to_ast_ref(Z3_translate(self.ctx.ref(), self.as_ast(), target.ref()), target)


Field Documentation

ast
ctx
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines