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

Definition at line 273 of file z3py.py.

Referenced by FuncDeclRef::__call__(), SortRef::__eq__(), SortRef::__ne__(), FuncDeclRef::arity(), AstRef::as_ast(), SortRef::as_ast(), FuncDeclRef::as_ast(), ExprRef::as_ast(), FuncDeclRef::as_func_decl(), FuncDeclRef::domain(), SortRef::kind(), FuncDeclRef::kind(), SortRef::name(), FuncDeclRef::name(), and FuncDeclRef::range().

ctx

Reimplemented in BitVecSortRef, and ArithSortRef.

Definition at line 273 of file z3py.py.

Referenced by FuncDeclRef.__call__(), ExprRef.__eq__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), ExprRef.__ne__(), Probe.__ne__(), Fixedpoint.add_rule(), Tactic.apply(), ExprRef.arg(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), BoolSortRef.cast(), ApplyResult.convert_model(), ExprRef.decl(), FuncDeclRef.domain(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_rules(), SortRef.kind(), SortRef.name(), FuncDeclRef.name(), Fixedpoint.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), FuncDeclRef.range(), Fixedpoint.set(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), Fixedpoint.statistics(), Solver.to_smt2(), and Fixedpoint.update_rule().

Public Member Functions

Data Fields

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Field Documentation