8356 def __init__(self, simplifier, ctx=None):
8357 self.ctx = _get_ctx(ctx)
8358 self.simplifier = None
8359 if isinstance(simplifier, SimplifierObj):
8360 self.simplifier = simplifier
8361 elif isinstance(simplifier, list):
8362 simps = [Simplifier(s, ctx) for s in simplifier]
8363 self.simplifier = simps[0].simplifier
8364 for i in range(1, len(simps)):
8367 return
8368 else:
8369 if z3_debug():
8370 _z3_assert(isinstance(simplifier, str), "simplifier name expected")
8371 try:
8373 except Z3Exception:
8374 raise Z3Exception("unknown simplifier '%s'" % simplifier)
8376
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 ...