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

Parameter Sets. More...

Public Member Functions

def __init__
 
def __del__
 
def set
 
def __repr__
 
def validate
 

Data Fields

 ctx
 
 params
 

Detailed Description

Parameter Sets. 

Set of parameters used to configure Solvers, Tactics and Simplifiers in Z3.

Consider using the function `args2params` to create instances of this object.

Definition at line 4346 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  ctx = None 
)

Definition at line 4351 of file z3py.py.

4351 
4352  def __init__(self, ctx=None):
4353  self.ctx = _get_ctx(ctx)
4354  self.params = Z3_mk_params(self.ctx.ref())
4355  Z3_params_inc_ref(self.ctx.ref(), self.params)
def __del__ (   self)

Definition at line 4356 of file z3py.py.

4356 
4357  def __del__(self):
4358  Z3_params_dec_ref(self.ctx.ref(), self.params)

Member Function Documentation

def __repr__ (   self)

Definition at line 4376 of file z3py.py.

4376 
4377  def __repr__(self):
4378  return Z3_params_to_string(self.ctx.ref(), self.params)
def set (   self,
  name,
  val 
) 
Set parameter name with value val.

Definition at line 4359 of file z3py.py.

4359 
4360  def set(self, name, val):
4361  """Set parameter name with value val."""
4362  if __debug__:
4363  _z3_assert(isinstance(name, str), "parameter name must be a string")
4364  name_sym = to_symbol(name, self.ctx)
4365  if isinstance(val, bool):
4366  Z3_params_set_bool(self.ctx.ref(), self.params, name_sym, val)
4367  elif isinstance(val, int):
4368  Z3_params_set_uint(self.ctx.ref(), self.params, name_sym, val)
4369  elif isinstance(val, float):
4370  Z3_params_set_double(self.ctx.ref(), self.params, name_sym, val)
4371  elif isinstance(val, str):
4372  Z3_params_set_symbol(self.ctx.ref(), self.params, name_sym, to_symbol(val, self.ctx))
4373  else:
4374  if __debug__:
4375  _z3_assert(False, "invalid parameter value")
def validate (   self,
  ds 
)

Definition at line 4379 of file z3py.py.

4379 
4380  def validate(self, ds):
4381  _z3_assert(isinstance(ds, ParamDescrsRef), "parameter description set expected")
4382  Z3_params_validate(self.ctx.ref(), self.params, ds.descr)

Field Documentation

ctx

Definition at line 4352 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(), Fixedpoint.get_rules(), Tactic.param_descrs(), Fixedpoint.parse_file(), Fixedpoint.parse_string(), ParamsRef.set(), Tactic.solver(), and Fixedpoint.statistics().

params

Definition at line 4353 of file z3py.py.

Referenced by ParamsRef.__del__(), ParamsRef.__repr__(), ParamsRef.set(), and ParamsRef.validate().

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