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 8242 of file z3py.py.

Constructor & Destructor Documentation

def __init__ (   self,
  simplifier,
  ctx = None 
)

Definition at line 8246 of file z3py.py.

8246  def __init__(self, simplifier, ctx=None):
8247  self.ctx = _get_ctx(ctx)
8248  self.simplifier = None
8249  if isinstance(simplifier, SimplifierObj):
8250  self.simplifier = simplifier
8251  elif isinstance(simplifier, list):
8252  simps = [Simplifier(s, ctx) for s in simplifier]
8253  self.simplifier = simps[0].simplifier
8254  for i in range(1, len(simps)):
8255  self.simplifier = Z3_simplifier_and_then(self.ctx.ref(), self.simplifier, simps[i].simplifier)
8256  Z3_simplifier_inc_ref(self.ctx.ref(), self.simplifier)
8257  return
8258  else:
8259  if z3_debug():
8260  _z3_assert(isinstance(simplifier, str), "simplifier name expected")
8261  try:
8262  self.simplifier = Z3_mk_simplifier(self.ctx.ref(), str(simplifier))
8263  except Z3Exception:
8264  raise Z3Exception("unknown simplifier '%s'" % simplifier)
8265  Z3_simplifier_inc_ref(self.ctx.ref(), self.simplifier)
8266 
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:8246
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 8270 of file z3py.py.

8270  def __del__(self):
8271  if self.simplifier is not None and self.ctx.ref() is not None and Z3_simplifier_dec_ref is not None:
8272  Z3_simplifier_dec_ref(self.ctx.ref(), self.simplifier)
8273 
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:8270

Member Function Documentation

def __deepcopy__ (   self,
  memo = {} 
)

Definition at line 8267 of file z3py.py.

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

Definition at line 8279 of file z3py.py.

8279  def add(self, solver):
8280  """Return a solver that applies the simplification pre-processing specified by the simplifier"""
8281  return Solver(Z3_solver_add_simplifier(self.ctx.ref(), solver.solver, self.simplifier), self.ctx)
8282 
def add(self, solver)
Definition: z3py.py:8279
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 8283 of file z3py.py.

8283  def help(self):
8284  """Display a string containing a description of the available options for the `self` simplifier."""
8285  print(Z3_simplifier_get_help(self.ctx.ref(), self.simplifier))
8286 
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:8283
def param_descrs (   self)
Return the parameter description set.

Definition at line 8287 of file z3py.py.

8287  def param_descrs(self):
8288  """Return the parameter description set."""
8289  return ParamDescrsRef(Z3_simplifier_get_param_descrs(self.ctx.ref(), self.simplifier), self.ctx)
8290 
8291 
def param_descrs(self)
Definition: z3py.py:8287
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 8274 of file z3py.py.

8274  def using_params(self, *args, **keys):
8275  """Return a simplifier that uses the given configuration options"""
8276  p = args2params(args, keys, self.ctx)
8277  return Simplifier(Z3_simplifier_using_params(self.ctx.ref(), self.simplifier, p.params), self.ctx)
8278 
def args2params
Definition: z3py.py:5512
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:8274

Field Documentation

ctx
simplifier