8464 def apply(self, goal, *arguments, **keywords):
8465 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options.
8466
8467 >>> x, y = Ints('x y')
8468 >>> t = Tactic('solve-eqs')
8469 >>> t.apply(And(x == 0, y >= x + 1))
8470 [[y >= 1]]
8471 """
8472 if z3_debug():
8473 _z3_assert(isinstance(goal, (Goal, BoolRef)), "Z3 Goal or Boolean expressions expected")
8474 goal = _to_goal(goal)
8475 if len(arguments) > 0 or len(keywords) > 0:
8476 p = args2params(arguments, keywords, self.ctx)
8477 return ApplyResult(
Z3_tactic_apply_ex(self.ctx.ref(), self.tactic, goal.goal, p.params), self.ctx)
8478 else:
8479 return ApplyResult(
Z3_tactic_apply(self.ctx.ref(), self.tactic, goal.goal), self.ctx)
8480
Z3_apply_result Z3_API Z3_tactic_apply_ex(Z3_context c, Z3_tactic t, Z3_goal g, Z3_params p)
Apply tactic t to the goal g using the parameter set p.
Z3_apply_result Z3_API Z3_tactic_apply(Z3_context c, Z3_tactic t, Z3_goal g)
Apply tactic t to the goal g.