8455 def apply(self, goal, *arguments, **keywords):
8456 """Apply tactic `self` to the given goal or Z3 Boolean expression using the given options.
8457
8458 >>> x, y = Ints('x y')
8459 >>> t = Tactic('solve-eqs')
8460 >>> t.apply(And(x == 0, y >= x + 1))
8461 [[y >= 1]]
8462 """
8463 if z3_debug():
8464 _z3_assert(isinstance(goal, (Goal, BoolRef)), "Z3 Goal or Boolean expressions expected")
8465 goal = _to_goal(goal)
8466 if len(arguments) > 0 or len(keywords) > 0:
8467 p = args2params(arguments, keywords, self.ctx)
8468 return ApplyResult(
Z3_tactic_apply_ex(self.ctx.ref(), self.tactic, goal.goal, p.params), self.ctx)
8469 else:
8470 return ApplyResult(
Z3_tactic_apply(self.ctx.ref(), self.tactic, goal.goal), self.ctx)
8471
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.