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

Constructor & Destructor Documentation

◆ __init__()

__init__ ( self,
simplifier,
ctx = None )

Definition at line 8360 of file z3py.py.

8360 def __init__(self, simplifier, ctx=None):
8361 self.ctx = _get_ctx(ctx)
8362 self.simplifier = None
8363 if isinstance(simplifier, SimplifierObj):
8364 self.simplifier = simplifier
8365 elif isinstance(simplifier, list):
8366 simps = [Simplifier(s, ctx) for s in simplifier]
8367 self.simplifier = simps[0].simplifier
8368 for i in range(1, len(simps)):
8369 self.simplifier = Z3_simplifier_and_then(self.ctx.ref(), self.simplifier, simps[i].simplifier)
8370 Z3_simplifier_inc_ref(self.ctx.ref(), self.simplifier)
8371 return
8372 else:
8373 if z3_debug():
8374 _z3_assert(isinstance(simplifier, str), "simplifier name expected")
8375 try:
8376 self.simplifier = Z3_mk_simplifier(self.ctx.ref(), str(simplifier))
8377 except Z3Exception:
8378 raise Z3Exception("unknown simplifier '%s'" % simplifier)
8379 Z3_simplifier_inc_ref(self.ctx.ref(), self.simplifier)
8380
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 8384 of file z3py.py.

8384 def __del__(self):
8385 if self.simplifier is not None and self.ctx.ref() is not None and Z3_simplifier_dec_ref is not None:
8386 Z3_simplifier_dec_ref(self.ctx.ref(), self.simplifier)
8387
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 8381 of file z3py.py.

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

◆ add()

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

Definition at line 8393 of file z3py.py.

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

◆ help()

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

Definition at line 8397 of file z3py.py.

8397 def help(self):
8398 """Display a string containing a description of the available options for the `self` simplifier."""
8399 print(Z3_simplifier_get_help(self.ctx.ref(), self.simplifier))
8400
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 8401 of file z3py.py.

8401 def param_descrs(self):
8402 """Return the parameter description set."""
8403 return ParamDescrsRef(Z3_simplifier_get_param_descrs(self.ctx.ref(), self.simplifier), self.ctx)
8404
8405
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 8388 of file z3py.py.

8388 def using_params(self, *args, **keys):
8389 """Return a simplifier that uses the given configuration options"""
8390 p = args2params(args, keys, self.ctx)
8391 return Simplifier(Z3_simplifier_using_params(self.ctx.ref(), self.simplifier, p.params), self.ctx)
8392
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 8361 of file z3py.py.

◆ simplifier

simplifier = None

Definition at line 8362 of file z3py.py.