8365 def __init__(self, simplifier, ctx=None):
8366 self.ctx = _get_ctx(ctx)
8367 self.simplifier = None
8368 if isinstance(simplifier, SimplifierObj):
8369 self.simplifier = simplifier
8370 elif isinstance(simplifier, list):
8371 simps = [Simplifier(s, ctx) for s in simplifier]
8372 self.simplifier = simps[0].simplifier
8373 for i in range(1, len(simps)):
8376 return
8377 else:
8378 if z3_debug():
8379 _z3_assert(isinstance(simplifier, str), "simplifier name expected")
8380 try:
8382 except Z3Exception:
8383 raise Z3Exception("unknown simplifier '%s'" % simplifier)
8385
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 ...