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)):
8371 return
8372 else:
8373 if z3_debug():
8374 _z3_assert(isinstance(simplifier, str), "simplifier name expected")
8375 try:
8377 except Z3Exception:
8378 raise Z3Exception("unknown simplifier '%s'" % 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 ...