Inheritance diagram for AstRef:

Public Member Functions
def	__init__

def	__del__ (self)

def	__deepcopy__

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

Constructor & Destructor Documentation

def __init__	(	self,
		ast,
		ctx = `None`
	)

Definition at line 344 of file z3py.py.

     def __init__(self, ast, ctx=None):
         self.ast = ast
         self.ctx = _get_ctx(ctx)
         Z3_inc_ref(self.ctx.ref(), self.as_ast())
 

def __del__ ( self )

Definition at line 349 of file z3py.py.

     def __del__(self):
         if self.ctx.ref() is not None and self.ast is not None:
             Z3_dec_ref(self.ctx.ref(), self.as_ast())
             self.ast = None
 

Member Function Documentation

def __bool__ ( self )

Definition at line 372 of file z3py.py.

Referenced by AstRef.__nonzero__().

     def __bool__(self):
         if is_true(self):
             return True
         elif is_false(self):
             return False
         elif is_eq(self) and self.num_args() == 2:
             return self.arg(0).eq(self.arg(1))
         else:
             raise Z3Exception("Symbolic expressions cannot be cast to concrete Boolean values.")
 

def __copy__ ( self )

Definition at line 436 of file z3py.py.

     def __copy__(self):
         return self.translate(self.ctx)
 

def __deepcopy__	(	self,
		memo = `{}`
	)

Definition at line 354 of file z3py.py.

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

def __eq__	(	self,
		other
	)

Definition at line 363 of file z3py.py.

Referenced by Probe.__ne__().

     def __eq__(self, other):
         return self.eq(other)
 

def __hash__ ( self )

Definition at line 366 of file z3py.py.

     def __hash__(self):
         return self.hash()
 

def __nonzero__ ( self )

Definition at line 369 of file z3py.py.

     def __nonzero__(self):
         return self.__bool__()
 

def __repr__ ( self )

Definition at line 360 of file z3py.py.

     def __repr__(self):
         return obj_to_string(self)
 

def __str__ ( self )

Definition at line 357 of file z3py.py.

     def __str__(self):
         return obj_to_string(self)
 

def as_ast ( self )

Return a pointer to the corresponding C Z3_ast object.

Definition at line 391 of file z3py.py.

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

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

def ctx_ref ( self )

Return a reference to the C context where this AST node is stored.

Definition at line 399 of file z3py.py.

Referenced by FuncDeclRef.__call__(), ArithRef.__div__(), SortRef.__eq__(), ExprRef.__eq__(), ArithRef.__ge__(), ArrayRef.__getitem__(), ArithRef.__gt__(), ArithRef.__le__(), ArithRef.__lt__(), ArithRef.__mod__(), SortRef.__ne__(), ExprRef.__ne__(), ArithRef.__neg__(), ArithRef.__pow__(), ArithRef.__rdiv__(), ArithRef.__rmod__(), ArithRef.__rpow__(), AlgebraicNumRef.approx(), ExprRef.arg(), FuncDeclRef.arity(), SortRef.as_ast(), FuncDeclRef.as_ast(), AlgebraicNumRef.as_decimal(), FiniteDomainRef.as_string(), FiniteDomainNumRef.as_string(), ExprRef.decl(), ArrayRef.default(), FuncDeclRef.domain(), ArraySortRef.domain(), AstRef.eq(), AstRef.get_id(), SortRef.get_id(), FuncDeclRef.get_id(), ExprRef.get_id(), AstRef.hash(), AlgebraicNumRef.index(), FuncDeclRef.kind(), SortRef.name(), FuncDeclRef.name(), ExprRef.num_args(), FuncDeclRef.params(), AlgebraicNumRef.poly(), FuncDeclRef.range(), ArraySortRef.range(), AstRef.sexpr(), FiniteDomainSortRef.size(), BoolRef.sort(), ArithRef.sort(), ArrayRef.sort(), and FiniteDomainRef.sort().

     def ctx_ref(self):
         """Return a reference to the C context where this AST node is stored."""
         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 403 of file z3py.py.

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

     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
         """
         if z3_debug():
             _z3_assert(is_ast(other), "Z3 AST expected")
         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.

Definition at line 395 of file z3py.py.

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

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

Referenced by AstRef.__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
         """
         return Z3_get_ast_hash(self.ctx_ref(), self.as_ast())
 
 

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 382 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().

     def sexpr(self):
         """Return a string representing the AST node in s-expression notation.
 
         >>> x = Int('x')
         >>> ((x + 1)*x).sexpr()
         '(* (+ x 1) x)'
         """
         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 420 of file z3py.py.

Referenced by AstRef.__copy__().

     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
         """
         if z3_debug():
             _z3_assert(isinstance(target, Context), "argument must be a Z3 context")
         return _to_ast_ref(Z3_translate(self.ctx.ref(), self.as_ast(), target.ref()), target)
 

Field Documentation

ctx

Definition at line 346 of file z3py.py.

Referenced by ArithRef.__add__(), FuncDeclRef.__call__(), AstRef.__copy__(), AstRef.__deepcopy__(), AstMap.__deepcopy__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), 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(), Optimize.assert_and_track(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), BoolSortRef.cast(), ExprRef.decl(), ArrayRef.default(), FuncDeclRef.domain(), ArraySortRef.domain(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), AstMap.keys(), SortRef.kind(), 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(), AlgebraicNumRef.poly(), Fixedpoint.query(), FuncDeclRef.range(), ArraySortRef.range(), Fixedpoint.set(), Optimize.set(), Optimize.set_on_model(), Tactic.solver(), ExprRef.sort(), BoolRef.sort(), ArithRef.sort(), ArrayRef.sort(), FiniteDomainRef.sort(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Optimize.unsat_core(), and Fixedpoint.update_rule().

Public Member Functions

Data Fields

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Field Documentation