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

Constructor & Destructor Documentation

def __init__	(		self,
			simplifier,
			ctx = None
	)

Definition at line 8360 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)

def __del__

(

self

)

Definition at line 8384 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

def __deepcopy__	(		self,
			memo = {}
	)

Definition at line 8381 of file z3py.py.

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

def add	(		self,
			solver
	)

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

Definition at line 8393 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)

def help

(

self

)

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

Definition at line 8397 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))

def param_descrs

(

self

)

Return the parameter description set.

Definition at line 8401 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)
        
    

def using_params	(		self,
			args,
			keys
	)

Return a simplifier that uses the given configuration options

Definition at line 8388 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

Definition at line 8361 of file z3py.py.

Referenced by Simplifier.__deepcopy__(), Tactic.__deepcopy__(), Probe.__deepcopy__(), Probe.__eq__(), Probe.__ge__(), Probe.__gt__(), Probe.__le__(), Probe.__lt__(), Probe.__ne__(), Simplifier.add(), Tactic.apply(), ParserContext.from_string(), Simplifier.param_descrs(), Tactic.param_descrs(), Tactic.solver(), and Simplifier.using_params().

simplifier

Definition at line 8362 of file z3py.py.

Referenced by Simplifier.__deepcopy__(), Simplifier.__del__(), Simplifier.add(), Simplifier.help(), Simplifier.param_descrs(), and Simplifier.using_params().