Z3
Public Member Functions | Data Fields
Simplifier Class Reference

Public Member Functions

def __init__
 
def __deepcopy__
 
def __del__ (self)
 
def using_params (self, args, keys)
 
def add (self, solver)
 
def help (self)
 
def param_descrs (self)
 

Data Fields

 ctx
 
 simplifier
 

Detailed Description

Simplifiers act as pre-processing utilities for solvers.
Build a custom simplifier and add it to a solver

Definition at line 8174 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  simplifier,
  ctx = None 
)

Definition at line 8178 of file z3py.py.

8178  def __init__(self, simplifier, ctx=None):
8179  self.ctx = _get_ctx(ctx)
8180  self.simplifier = None
8181  if isinstance(simplifier, SimplifierObj):
8182  self.simplifier = simplifier
8183  elif isinstance(simplifier, list):
8184  simps = [Simplifier(s, ctx) for s in simplifier]
8185  self.simplifier = simps[0].simplifier
8186  for i in range(1, len(simps)):
8187  self.simplifier = Z3_simplifier_and_then(self.ctx.ref(), self.simplifier, simps[i].simplifier)
8188  Z3_simplifier_inc_ref(self.ctx.ref(), self.simplifier)
8189  return
8190  else:
8191  if z3_debug():
8192  _z3_assert(isinstance(simplifier, str), "simplifier name expected")
8193  try:
8194  self.simplifier = Z3_mk_simplifier(self.ctx.ref(), str(simplifier))
8195  except Z3Exception:
8196  raise Z3Exception("unknown simplifier '%s'" % simplifier)
8197  Z3_simplifier_inc_ref(self.ctx.ref(), self.simplifier)
8198 
expr range(expr const &lo, expr const &hi)
Definition: z3++.h:4085
Z3_simplifier Z3_API Z3_simplifier_and_then(Z3_context c, Z3_simplifier t1, Z3_simplifier t2)
Return a simplifier that applies t1 to a given goal and t2 to every subgoal produced by t1...
def z3_debug()
Definition: z3py.py:62
void Z3_API Z3_simplifier_inc_ref(Z3_context c, Z3_simplifier t)
Increment the reference counter of the given simplifier.
def __init__
Definition: z3py.py:8178
Z3_simplifier Z3_API Z3_mk_simplifier(Z3_context c, Z3_string name)
Return a simplifier associated with the given name. The complete list of simplifiers may be obtained ...
def __del__ (   self)

Definition at line 8202 of file z3py.py.

8202  def __del__(self):
8203  if self.simplifier is not None and self.ctx.ref() is not None and Z3_simplifier_dec_ref is not None:
8204  Z3_simplifier_dec_ref(self.ctx.ref(), self.simplifier)
8205 
void Z3_API Z3_simplifier_dec_ref(Z3_context c, Z3_simplifier g)
Decrement the reference counter of the given simplifier.
def __del__(self)
Definition: z3py.py:8202

Member Function Documentation

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 8199 of file z3py.py.

8199  def __deepcopy__(self, memo={}):
8200  return Simplifier(self.simplifier, self.ctx)
8201 
def __deepcopy__
Definition: z3py.py:8199
def add (   self,
  solver 
)
Return a solver that applies the simplification pre-processing specified by the simplifier

Definition at line 8211 of file z3py.py.

8211  def add(self, solver):
8212  """Return a solver that applies the simplification pre-processing specified by the simplifier"""
8213  return Solver(Z3_solver_add_simplifier(self.ctx.ref(), solver.solver, self.simplifier), self.ctx)
8214 
def add(self, solver)
Definition: z3py.py:8211
Z3_solver Z3_API Z3_solver_add_simplifier(Z3_context c, Z3_solver solver, Z3_simplifier simplifier)
Attach simplifier to a solver. The solver will use the simplifier for incremental pre-processing...
def help (   self)
Display a string containing a description of the available options for the `self` simplifier.

Definition at line 8215 of file z3py.py.

8215  def help(self):
8216  """Display a string containing a description of the available options for the `self` simplifier."""
8217  print(Z3_simplifier_get_help(self.ctx.ref(), self.simplifier))
8218 
Z3_string Z3_API Z3_simplifier_get_help(Z3_context c, Z3_simplifier t)
Return a string containing a description of parameters accepted by the given simplifier.
def help(self)
Definition: z3py.py:8215
def param_descrs (   self)
Return the parameter description set.

Definition at line 8219 of file z3py.py.

8219  def param_descrs(self):
8220  """Return the parameter description set."""
8221  return ParamDescrsRef(Z3_simplifier_get_param_descrs(self.ctx.ref(), self.simplifier), self.ctx)
8222 
8223 
def param_descrs(self)
Definition: z3py.py:8219
Z3_param_descrs Z3_API Z3_simplifier_get_param_descrs(Z3_context c, Z3_simplifier t)
Return the parameter description set for the given simplifier object.
def using_params (   self,
  args,
  keys 
)
Return a simplifier that uses the given configuration options

Definition at line 8206 of file z3py.py.

8206  def using_params(self, *args, **keys):
8207  """Return a simplifier that uses the given configuration options"""
8208  p = args2params(args, keys, self.ctx)
8209  return Simplifier(Z3_simplifier_using_params(self.ctx.ref(), self.simplifier, p.params), self.ctx)
8210 
def args2params
Definition: z3py.py:5458
Z3_simplifier Z3_API Z3_simplifier_using_params(Z3_context c, Z3_simplifier t, Z3_params p)
Return a simplifier that applies t using the given set of parameters.
def using_params(self, args, keys)
Definition: z3py.py:8206

Field Documentation

ctx
simplifier