| 148 | |
| 149 | |
| 150 | struct Tactic { |
| 151 | Z3_tactic t = nullptr; |
| 152 | |
| 153 | Tactic(Z3_tactic t = nullptr) : t(t) { |
| 154 | if (t) |
| 155 | Z3_tactic_inc_ref(ctx(), t); |
| 156 | } |
| 157 | |
| 158 | Tactic(Tactic &&other) noexcept { |
| 159 | swap(t, other.t); |
| 160 | } |
| 161 | |
| 162 | void destroy() { |
| 163 | if (t) |
| 164 | Z3_tactic_dec_ref(ctx(), t); |
| 165 | } |
| 166 | |
| 167 | virtual ~Tactic() { destroy(); } |
| 168 | |
| 169 | void set(Z3_tactic newt) { |
| 170 | Z3_tactic_inc_ref(ctx(), newt); |
| 171 | destroy(); |
| 172 | t = newt; |
| 173 | } |
| 174 | |
| 175 | virtual TacticResult exec(const Goal &goal) const { |
| 176 | UNREACHABLE(); |
| 177 | return {}; |
| 178 | }; |
| 179 | }; |
| 180 | |
| 181 | |
| 182 | struct NamedTactic final : public Tactic { |