Z3
Public Member Functions | Data Fields
ScopedConstructorList Class Reference

Public Member Functions

def __init__ (self, c, ctx)
 
def __del__ (self)
 

Data Fields

 c
 
 ctx
 

Detailed Description

Auxiliary object used to create Z3 datatypes.

Definition at line 4492 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

def __init__ (   self,
  c,
  ctx 
)

Definition at line 4494 of file z3py.py.

4494  def __init__(self, c, ctx):
4495  self.c = c
4496  self.ctx = ctx

◆ __del__()

def __del__ (   self)

Definition at line 4497 of file z3py.py.

4497  def __del__(self):
4498  if self.ctx.ref() is not None:
4499  Z3_del_constructor_list(self.ctx.ref(), self.c)
4500 
void Z3_API Z3_del_constructor_list(Z3_context c, Z3_constructor_list clist)
Reclaim memory allocated for constructor list.

Field Documentation

◆ c

c

Definition at line 4495 of file z3py.py.

◆ ctx

ctx

Definition at line 4496 of file z3py.py.

Referenced by Probe.__call__(), Fixedpoint.__deepcopy__(), Optimize.__deepcopy__(), ApplyResult.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Fixedpoint.__del__(), Optimize.__del__(), ApplyResult.__del__(), Tactic.__del__(), Probe.__del__(), Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), ApplyResult.__len__(), Probe.__lt__(), Probe.__ne__(), Fixedpoint.add_cover(), Fixedpoint.add_rule(), Optimize.add_soft(), Tactic.apply(), ApplyResult.as_expr(), Fixedpoint.assert_exprs(), Optimize.assert_exprs(), Optimize.assertions(), Optimize.check(), ApplyResult.convert_model(), Optimize.from_file(), Optimize.from_string(), Fixedpoint.get_answer(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), Fixedpoint.get_ground_sat_answer(), Fixedpoint.get_num_levels(), Fixedpoint.get_rule_names_along_trace(), Fixedpoint.get_rules(), Fixedpoint.get_rules_along_trace(), Fixedpoint.help(), Optimize.help(), Tactic.help(), Optimize.maximize(), Optimize.minimize(), Optimize.model(), Optimize.objectives(), Fixedpoint.param_descrs(), Optimize.param_descrs(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Fixedpoint.pop(), Optimize.pop(), Fixedpoint.push(), Optimize.push(), Fixedpoint.query(), Fixedpoint.query_from_lvl(), Fixedpoint.reason_unknown(), Optimize.reason_unknown(), Fixedpoint.register_relation(), Fixedpoint.set(), Optimize.set(), Fixedpoint.set_predicate_representation(), Fixedpoint.sexpr(), Optimize.sexpr(), ApplyResult.sexpr(), Tactic.solver(), Fixedpoint.statistics(), Optimize.statistics(), Solver.to_smt2(), Fixedpoint.to_string(), and Fixedpoint.update_rule().