| 180 | |
| 181 | |
| 182 | struct NamedTactic final : public Tactic { |
| 183 | const char *name = nullptr; |
| 184 | |
| 185 | NamedTactic(const char *name) : Tactic(Z3_mk_tactic(ctx(), name)) { |
| 186 | this->name = name; |
| 187 | } |
| 188 | |
| 189 | TacticResult exec(const Goal &goal) const override { |
| 190 | dbg() << "\nApplying " << name << endl; |
| 191 | Tactic to(Z3_tactic_or_else(ctx(), |
| 192 | Tactic(Z3_tactic_try_for(ctx(), t, 10000)).t, |
| 193 | Tactic(Z3_tactic_skip(ctx())).t)); |
| 194 | return Z3_tactic_apply(ctx(), to.t, goal.goal); |
| 195 | } |
| 196 | }; |
| 197 | |
| 198 | |
| 199 | struct IfTactic final : public Tactic { |