Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules Pages
Public Member Functions | Data Fields
ScopedConstructorList Class Reference

Public Member Functions

def __init__
 
def __del__
 

Data Fields

 c
 
 ctx
 

Detailed Description

Auxiliary object used to create Z3 datatypes.

Definition at line 4201 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  c,
  ctx 
)

Definition at line 4203 of file z3py.py.

4204  def __init__(self, c, ctx):
4205  self.c = c
self.ctx = ctx
def __del__ (   self)

Definition at line 4206 of file z3py.py.

4207  def __del__(self):
4208  Z3_del_constructor_list(self.ctx.ref(), self.c)
void Z3_API Z3_del_constructor_list(__in Z3_context c, __in Z3_constructor_list clist)
Reclaim memory allocated for constructor list.

Field Documentation

c

Definition at line 4204 of file z3py.py.

Referenced by ScopedConstructorList.__del__().

ctx

Definition at line 4205 of file z3py.py.

Referenced by Probe.__eq__(), Probe.__ge__(), AstVector.__getitem__(), AstMap.__getitem__(), ModelRef.__getitem__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_rule(), Tactic.apply(), FuncEntry.arg_value(), Goal.as_expr(), ApplyResult.as_expr(), Goal.assert_exprs(), Fixedpoint.assert_exprs(), ApplyResult.convert_model(), ModelRef.decls(), FuncInterp.else_value(), FuncInterp.entry(), ModelRef.eval(), Goal.get(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), ModelRef.get_interp(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), Fixedpoint.get_rules(), ModelRef.get_sort(), ModelRef.get_universe(), AstMap.keys(), Fixedpoint.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), ParamsRef.set(), Fixedpoint.set(), Tactic.solver(), Fixedpoint.statistics(), Solver.to_smt2(), Fixedpoint.update_rule(), and FuncEntry.value().