Z3
 
Loading...
Searching...
No Matches
Simplifier Class Reference

Public Member Functions

 __init__ (self, simplifier, ctx=None)
 
 __deepcopy__ (self, memo={})
 
 __del__ (self)
 
 using_params (self, *args, **keys)
 
 add (self, solver)
 
 help (self)
 
 param_descrs (self)
 

Data Fields

 ctx = _get_ctx(ctx)
 
 simplifier = None
 

Detailed Description

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

Definition at line 8306 of file z3py.py.

Constructor & Destructor Documentation

◆ __init__()

__init__ ( self,
simplifier,
ctx = None )

Definition at line 8310 of file z3py.py.

8310 def __init__(self, simplifier, ctx=None):
8311 self.ctx = _get_ctx(ctx)
8312 self.simplifier = None
8313 if isinstance(simplifier, SimplifierObj):
8314 self.simplifier = simplifier
8315 elif isinstance(simplifier, list):
8316 simps = [Simplifier(s, ctx) for s in simplifier]
8317 self.simplifier = simps[0].simplifier
8318 for i in range(1, len(simps)):
8319 self.simplifier = Z3_simplifier_and_then(self.ctx.ref(), self.simplifier, simps[i].simplifier)
8320 Z3_simplifier_inc_ref(self.ctx.ref(), self.simplifier)
8321 return
8322 else:
8323 if z3_debug():
8324 _z3_assert(isinstance(simplifier, str), "simplifier name expected")
8325 try:
8326 self.simplifier = Z3_mk_simplifier(self.ctx.ref(), str(simplifier))
8327 except Z3Exception:
8328 raise Z3Exception("unknown simplifier '%s'" % simplifier)
8329 Z3_simplifier_inc_ref(self.ctx.ref(), self.simplifier)
8330
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.
void Z3_API Z3_simplifier_inc_ref(Z3_context c, Z3_simplifier t)
Increment the reference counter of the given simplifier.
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 ...

◆ __del__()

__del__ ( self)

Definition at line 8334 of file z3py.py.

8334 def __del__(self):
8335 if self.simplifier is not None and self.ctx.ref() is not None and Z3_simplifier_dec_ref is not None:
8336 Z3_simplifier_dec_ref(self.ctx.ref(), self.simplifier)
8337
void Z3_API Z3_simplifier_dec_ref(Z3_context c, Z3_simplifier g)
Decrement the reference counter of the given simplifier.

Member Function Documentation

◆ __deepcopy__()

__deepcopy__ ( self,
memo = {} )

Definition at line 8331 of file z3py.py.

8331 def __deepcopy__(self, memo={}):
8332 return Simplifier(self.simplifier, self.ctx)
8333

◆ add()

add ( self,
solver )
Return a solver that applies the simplification pre-processing specified by the simplifier

Definition at line 8343 of file z3py.py.

8343 def add(self, solver):
8344 """Return a solver that applies the simplification pre-processing specified by the simplifier"""
8345 return Solver(Z3_solver_add_simplifier(self.ctx.ref(), solver.solver, self.simplifier), self.ctx)
8346

◆ help()

help ( self)
Display a string containing a description of the available options for the `self` simplifier.

Definition at line 8347 of file z3py.py.

8347 def help(self):
8348 """Display a string containing a description of the available options for the `self` simplifier."""
8349 print(Z3_simplifier_get_help(self.ctx.ref(), self.simplifier))
8350
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.

◆ param_descrs()

param_descrs ( self)
Return the parameter description set.

Definition at line 8351 of file z3py.py.

8351 def param_descrs(self):
8352 """Return the parameter description set."""
8353 return ParamDescrsRef(Z3_simplifier_get_param_descrs(self.ctx.ref(), self.simplifier), self.ctx)
8354
8355
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.

◆ using_params()

using_params ( self,
* args,
** keys )
Return a simplifier that uses the given configuration options

Definition at line 8338 of file z3py.py.

8338 def using_params(self, *args, **keys):
8339 """Return a simplifier that uses the given configuration options"""
8340 p = args2params(args, keys, self.ctx)
8341 return Simplifier(Z3_simplifier_using_params(self.ctx.ref(), self.simplifier, p.params), self.ctx)
8342
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.

Field Documentation

◆ ctx

ctx = _get_ctx(ctx)

Definition at line 8311 of file z3py.py.

◆ simplifier

simplifier = None

Definition at line 8312 of file z3py.py.