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

Public Member Functions

def __init__
 
def __del__
 
def size
 
def __len__
 
def get_name
 
def get_kind
 
def __getitem__
 
def __repr__
 

Data Fields

 ctx
 
 descr
 

Detailed Description

Set of parameter descriptions for Solvers, Tactics and Simplifiers in Z3.

Definition at line 4405 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  descr,
  ctx = None 
)

Definition at line 4408 of file z3py.py.

4408 
4409  def __init__(self, descr, ctx=None):
4410  _z3_assert(isinstance(descr, ParamDescrs), "parameter description object expected")
4411  self.ctx = _get_ctx(ctx)
4412  self.descr = descr
4413  Z3_param_descrs_inc_ref(self.ctx.ref(), self.descr)
def __del__ (   self)

Definition at line 4414 of file z3py.py.

4414 
4415  def __del__(self):
4416  Z3_param_descrs_dec_ref(self.ctx.ref(), self.descr)

Member Function Documentation

def __getitem__ (   self,
  arg 
)

Definition at line 4437 of file z3py.py.

4437 
4438  def __getitem__(self, arg):
4439  if isinstance(arg, int) or isinstance(arg, long):
4440  return self.get_name(arg)
4441  else:
4442  return self.get_kind(arg)
def __len__ (   self) 
Return the size of in the parameter description `self`.

Definition at line 4422 of file z3py.py.

4422 
4423  def __len__(self):
4424  """Return the size of in the parameter description `self`.
4425  """
4426  return self.size()
def __repr__ (   self)

Definition at line 4443 of file z3py.py.

4443 
4444  def __repr__(self):
4445  return Z3_param_descrs_to_string(self.ctx.ref(), self.descr)
def get_kind (   self,
  n 
) 
Return the kind of the parameter named `n`.

Definition at line 4432 of file z3py.py.

Referenced by ParamDescrsRef.__getitem__().

4432 
4433  def get_kind(self, n):
4434  """Return the kind of the parameter named `n`.
4435  """
4436  return Z3_param_descrs_get_kind(self.ctx.ref(), self.descr, to_symbol(n, self.ctx))
def get_name (   self,
  i 
) 
Return the i-th parameter name in the parameter description `self`.

Definition at line 4427 of file z3py.py.

Referenced by ParamDescrsRef.__getitem__().

4427 
4428  def get_name(self, i):
4429  """Return the i-th parameter name in the parameter description `self`.
4430  """
4431  return _symbol2py(self.ctx, Z3_param_descrs_get_name(self.ctx.ref(), self.descr, i))
def size (   self) 
Return the size of in the parameter description `self`.

Definition at line 4417 of file z3py.py.

Referenced by ParamDescrsRef.__len__().

4417 
4418  def size(self):
4419  """Return the size of in the parameter description `self`.
4420  """
4421  return int(Z3_param_descrs_size(self.ctx.ref(), self.descr))

Field Documentation

ctx

Definition at line 4410 of file z3py.py.

Referenced by Probe.__eq__(), Probe.__ge__(), ApplyResult.__getitem__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Tactic.apply(), ApplyResult.as_expr(), ApplyResult.convert_model(), Fixedpoint.get_assertions(), Fixedpoint.get_cover_delta(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), Fixedpoint.get_rules(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), Tactic.solver(), and Fixedpoint.statistics().

descr

Definition at line 4411 of file z3py.py.

Referenced by ParamDescrsRef.__del__(), ParamDescrsRef.__repr__(), ParamDescrsRef.get_kind(), ParamDescrsRef.get_name(), and ParamDescrsRef.size().

Generated on Thu Nov 22 2012 18:37:32 for Z3 by   doxygen 1.8.2