8409 def apply(self, goal, *arguments, **keywords):
8410 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options.
8411
8412 >>> x, y = Ints('x y')
8413 >>> t = Tactic('solve-eqs')
8414 >>> t.apply(And(x == 0, y >= x + 1))
8415 [[y >= 1]]
8416 """
8417 if z3_debug():
8418 _z3_assert(isinstance(goal, (Goal, BoolRef)), "Z3 Goal or Boolean expressions expected")
8419 goal = _to_goal(goal)
8420 if len(arguments) > 0 or len(keywords) > 0:
8421 p = args2params(arguments, keywords, self.ctx)
8422 return ApplyResult(
Z3_tactic_apply_ex(self.ctx.ref(), self.tactic, goal.goal, p.params), self.ctx)
8423 else:
8424 return ApplyResult(
Z3_tactic_apply(self.ctx.ref(), self.tactic, goal.goal), self.ctx)
8425
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.