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

Constructor & Destructor Documentation

__init__()

__init__	(		self,
			simplifier,
			ctx = None )

Definition at line 9086 of file z3py.py.

    def __init__(self, simplifier, ctx=None):
        self.ctx = _get_ctx(ctx)
        self.simplifier = None
        if isinstance(simplifier, SimplifierObj):
            self.simplifier = simplifier
        elif isinstance(simplifier, list):
            simps = [Simplifier(s, ctx) for s in simplifier]
            self.simplifier = simps[0].simplifier
            for i in range(1, len(simps)):
                self.simplifier = Z3_simplifier_and_then(self.ctx.ref(), self.simplifier, simps[i].simplifier)
            Z3_simplifier_inc_ref(self.ctx.ref(), self.simplifier)
            return
        else:
            if z3_debug():
                _z3_assert(isinstance(simplifier, str), "simplifier name expected")
            try:
                self.simplifier = Z3_mk_simplifier(self.ctx.ref(), str(simplifier))
            except Z3Exception:
                raise Z3Exception("unknown simplifier '%s'" % simplifier)
        Z3_simplifier_inc_ref(self.ctx.ref(), self.simplifier)
 

__del__()

__del__

(

self

)

Definition at line 9110 of file z3py.py.

    def __del__(self):
        if self.simplifier is not None and self.ctx.ref() is not None and Z3_simplifier_dec_ref is not None:
            Z3_simplifier_dec_ref(self.ctx.ref(), self.simplifier)
 

Member Function Documentation

__deepcopy__()

__deepcopy__	(		self,
			memo = {} )

Definition at line 9107 of file z3py.py.

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

add()

add	(		self,
			solver )

Return a solver that applies the simplification pre-processing specified by the simplifier

Definition at line 9119 of file z3py.py.

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

help()

help

(

self

)

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

Definition at line 9123 of file z3py.py.

    def help(self):
        """Display a string containing a description of the available options for the `self` simplifier."""
        print(Z3_simplifier_get_help(self.ctx.ref(), self.simplifier))
 

param_descrs()

param_descrs

(

self

)

Return the parameter description set.

Definition at line 9127 of file z3py.py.

    def param_descrs(self):
        """Return the parameter description set."""
        return ParamDescrsRef(Z3_simplifier_get_param_descrs(self.ctx.ref(), self.simplifier), self.ctx)
        
    

using_params()

using_params	(		self,
		*	args,
		**	keys )

Return a simplifier that uses the given configuration options

Definition at line 9114 of file z3py.py.

    def using_params(self, *args, **keys):
        """Return a simplifier that uses the given configuration options"""
        p = args2params(args, keys, self.ctx)
        return Simplifier(Z3_simplifier_using_params(self.ctx.ref(), self.simplifier, p.params), self.ctx)
 

Field Documentation

ctx

ctx = _get_ctx(ctx)

Definition at line 9087 of file z3py.py.

simplifier

simplifier = None

Definition at line 9088 of file z3py.py.