1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3
4 Module Name:
5
6 combined_solver.cpp
7
8 Abstract:
9
10 Implements the solver API by combining two solvers.
11
12 This is a replacement for the strategic_solver class.
13
14 Author:
15
16 Leonardo (leonardo) 2012-12-11
17
18 Notes:
19
20 --*/
21 #include "util/scoped_timer.h"
22 #include "util/common_msgs.h"
23 #include "ast/ast_pp.h"
24 #include "solver/solver.h"
25 #include "solver/combined_solver_params.hpp"
26 #include <atomic>
27 #define PS_VB_LVL 15
28
29 /**
30 \brief Implementation of the solver API that combines two given solvers.
31
32 The combined solver has two modes:
33 - non-incremental
34 - incremental
35 In non-incremental mode, the first solver is used.
36 In incremental mode, the second one is used.
37
38 A timeout for the second solver can be specified.
39 If the timeout is reached, then the first solver is executed.
40
41 The object switches to incremental when:
42 - push is used
43 - assertions are performed after a check_sat
44 - parameter ignore_solver1==false
45 */
46 class combined_solver : public solver {
47 public:
48 // Behavior when the incremental solver returns unknown.
49 enum inc_unknown_behavior {
50 IUB_RETURN_UNDEF, // just return unknown
51 IUB_USE_TACTIC_IF_QF, // invoke tactic if problem is quantifier free
52 IUB_USE_TACTIC // invoke tactic
53 };
54
55 private:
56 bool m_inc_mode;
57 bool m_check_sat_executed;
58 bool m_use_solver1_results;
59 ref<solver> m_solver1;
60 ref<solver> m_solver2;
61 // We delay sending assertions to solver 2
62 // This is relevant for big benchmarks that are meant to be solved
63 // by a non-incremental solver. );
64
65 bool m_ignore_solver1;
66 inc_unknown_behavior m_inc_unknown_behavior;
67 unsigned m_inc_timeout;
68
switch_inc_mode()69 void switch_inc_mode() {
70 m_inc_mode = true;
71 }
72
73 struct aux_timeout_eh : public event_handler {
74 solver * m_solver;
75 std::atomic<bool> m_canceled;
aux_timeout_ehcombined_solver::aux_timeout_eh76 aux_timeout_eh(solver * s):m_solver(s), m_canceled(false) {}
~aux_timeout_ehcombined_solver::aux_timeout_eh77 ~aux_timeout_eh() override {
78 if (m_canceled) {
79 m_solver->get_manager().limit().dec_cancel();
80 }
81 }
operator ()combined_solver::aux_timeout_eh82 void operator()(event_handler_caller_t caller_id) override {
83 m_canceled = true;
84 m_solver->get_manager().limit().inc_cancel();
85 }
86 };
87
updt_local_params(params_ref const & _p)88 void updt_local_params(params_ref const & _p) {
89 combined_solver_params p(_p);
90 m_inc_timeout = p.solver2_timeout();
91 m_ignore_solver1 = p.ignore_solver1();
92 m_inc_unknown_behavior = static_cast<inc_unknown_behavior>(p.solver2_unknown());
93 }
94
get_manager() const95 ast_manager& get_manager() const override { return m_solver1->get_manager(); }
96
has_quantifiers() const97 bool has_quantifiers() const {
98 unsigned sz = get_num_assertions();
99 for (unsigned i = 0; i < sz; i++) {
100 if (::has_quantifiers(get_assertion(i)))
101 return true;
102 }
103 return false;
104 }
105
use_solver1_when_undef() const106 bool use_solver1_when_undef() const {
107 switch (m_inc_unknown_behavior) {
108 case IUB_RETURN_UNDEF: return false;
109 case IUB_USE_TACTIC_IF_QF: return !has_quantifiers();
110 case IUB_USE_TACTIC: return true;
111 default:
112 UNREACHABLE();
113 return false;
114 }
115 }
116
117 public:
combined_solver(solver * s1,solver * s2,params_ref const & p)118 combined_solver(solver * s1, solver * s2, params_ref const & p) {
119 m_solver1 = s1;
120 m_solver2 = s2;
121 updt_local_params(p);
122 m_inc_mode = false;
123 m_check_sat_executed = false;
124 m_use_solver1_results = true;
125 }
126
translate(ast_manager & m,params_ref const & p)127 solver* translate(ast_manager& m, params_ref const& p) override {
128 TRACE("solver", tout << "translate\n";);
129 solver* s1 = m_solver1->translate(m, p);
130 solver* s2 = m_solver2->translate(m, p);
131 combined_solver* r = alloc(combined_solver, s1, s2, p);
132 r->m_inc_mode = m_inc_mode;
133 r->m_check_sat_executed = m_check_sat_executed;
134 r->m_use_solver1_results = m_use_solver1_results;
135 return r;
136 }
137
set_phase(expr * e)138 void set_phase(expr* e) override { m_solver1->set_phase(e); m_solver2->set_phase(e); }
get_phase()139 solver::phase* get_phase() override { auto* p = m_solver1->get_phase(); if (!p) p = m_solver2->get_phase(); return p; }
set_phase(solver::phase * p)140 void set_phase(solver::phase* p) override { m_solver1->set_phase(p); m_solver2->set_phase(p); }
move_to_front(expr * e)141 void move_to_front(expr* e) override { m_solver1->move_to_front(e); m_solver2->move_to_front(e); }
142
updt_params(params_ref const & p)143 void updt_params(params_ref const & p) override {
144 solver::updt_params(p);
145 m_solver1->updt_params(p);
146 m_solver2->updt_params(p);
147 updt_local_params(p);
148 }
149
collect_param_descrs(param_descrs & r)150 void collect_param_descrs(param_descrs & r) override {
151 m_solver1->collect_param_descrs(r);
152 m_solver2->collect_param_descrs(r);
153 combined_solver_params::collect_param_descrs(r);
154 }
155
set_produce_models(bool f)156 void set_produce_models(bool f) override {
157 m_solver1->set_produce_models(f);
158 m_solver2->set_produce_models(f);
159 }
160
assert_expr_core(expr * t)161 void assert_expr_core(expr * t) override {
162 if (m_check_sat_executed)
163 switch_inc_mode();
164 m_solver1->assert_expr(t);
165 m_solver2->assert_expr(t);
166 }
167
assert_expr_core2(expr * t,expr * a)168 void assert_expr_core2(expr * t, expr * a) override {
169 if (m_check_sat_executed)
170 switch_inc_mode();
171 m_solver1->assert_expr(t, a);
172 m_solver2->assert_expr(t, a);
173 }
174
push()175 void push() override {
176 switch_inc_mode();
177 m_solver1->push();
178 m_solver2->push();
179 TRACE("pop", tout << "push\n";);
180 }
181
pop(unsigned n)182 void pop(unsigned n) override {
183 TRACE("pop", tout << n << "\n";);
184 switch_inc_mode();
185 m_solver1->pop(n);
186 m_solver2->pop(n);
187 }
188
get_scope_level() const189 unsigned get_scope_level() const override {
190 return m_solver1->get_scope_level();
191 }
192
get_consequences(expr_ref_vector const & asms,expr_ref_vector const & vars,expr_ref_vector & consequences)193 lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) override {
194 switch_inc_mode();
195 m_use_solver1_results = false;
196 try {
197 return m_solver2->get_consequences(asms, vars, consequences);
198 }
199 catch (z3_exception& ex) {
200 if (!get_manager().inc()) {
201 throw;
202 }
203 else {
204 set_reason_unknown(ex.msg());
205 }
206 }
207 return l_undef;
208 }
209
check_sat_core(unsigned num_assumptions,expr * const * assumptions)210 lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) override {
211 m_check_sat_executed = true;
212 m_use_solver1_results = false;
213
214 if (get_num_assumptions() != 0 ||
215 num_assumptions > 0 || // assumptions were provided
216 m_ignore_solver1) {
217 // must use incremental solver
218 switch_inc_mode();
219 return m_solver2->check_sat_core(num_assumptions, assumptions);
220 }
221
222 if (m_inc_mode) {
223 if (m_inc_timeout == UINT_MAX) {
224 IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (without a timeout)\")\n";);
225 lbool r = m_solver2->check_sat_core(num_assumptions, assumptions);
226 if (r != l_undef || !use_solver1_when_undef() || !get_manager().inc()) {
227 return r;
228 }
229 }
230 else {
231 IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 2 (with timeout)\")\n";);
232 aux_timeout_eh eh(m_solver2.get());
233 lbool r = l_undef;
234 try {
235 scoped_timer timer(m_inc_timeout, &eh);
236 r = m_solver2->check_sat_core(num_assumptions, assumptions);
237 }
238 catch (z3_exception&) {
239 if (!eh.m_canceled) {
240 throw;
241 }
242 }
243 if ((r != l_undef || !use_solver1_when_undef()) && !eh.m_canceled) {
244 return r;
245 }
246 }
247 IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"solver 2 failed, trying solver1\")\n";);
248 }
249
250 IF_VERBOSE(PS_VB_LVL, verbose_stream() << "(combined-solver \"using solver 1\")\n";);
251 m_use_solver1_results = true;
252 return m_solver1->check_sat_core(num_assumptions, assumptions);
253 }
254
set_progress_callback(progress_callback * callback)255 void set_progress_callback(progress_callback * callback) override {
256 m_solver1->set_progress_callback(callback);
257 m_solver2->set_progress_callback(callback);
258 }
259
get_num_assertions() const260 unsigned get_num_assertions() const override {
261 return m_solver1->get_num_assertions();
262 }
263
get_assertion(unsigned idx) const264 expr * get_assertion(unsigned idx) const override {
265 return m_solver1->get_assertion(idx);
266 }
267
get_num_assumptions() const268 unsigned get_num_assumptions() const override {
269 return m_solver1->get_num_assumptions() + m_solver2->get_num_assumptions();
270 }
271
cube(expr_ref_vector & vars,unsigned backtrack_level)272 expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override {
273 switch_inc_mode();
274 return m_solver2->cube(vars, backtrack_level);
275 }
276
get_assumption(unsigned idx) const277 expr * get_assumption(unsigned idx) const override {
278 unsigned c1 = m_solver1->get_num_assumptions();
279 if (idx < c1) return m_solver1->get_assumption(idx);
280 return m_solver2->get_assumption(idx - c1);
281 }
282
display(std::ostream & out,unsigned n,expr * const * es) const283 std::ostream& display(std::ostream & out, unsigned n, expr* const* es) const override {
284 return m_solver1->display(out, n, es);
285 }
286
collect_statistics(statistics & st) const287 void collect_statistics(statistics & st) const override {
288 m_solver2->collect_statistics(st);
289 if (m_use_solver1_results)
290 m_solver1->collect_statistics(st);
291 }
292
get_unsat_core(expr_ref_vector & r)293 void get_unsat_core(expr_ref_vector & r) override {
294 if (m_use_solver1_results)
295 m_solver1->get_unsat_core(r);
296 else
297 m_solver2->get_unsat_core(r);
298 }
299
get_model_core(model_ref & m)300 void get_model_core(model_ref & m) override {
301 if (m_use_solver1_results)
302 m_solver1->get_model(m);
303 else
304 m_solver2->get_model(m);
305 }
306
get_levels(ptr_vector<expr> const & vars,unsigned_vector & depth)307 void get_levels(ptr_vector<expr> const& vars, unsigned_vector& depth) override {
308 if (m_use_solver1_results)
309 m_solver1->get_levels(vars, depth);
310 else
311 m_solver2->get_levels(vars, depth);
312 }
313
get_trail()314 expr_ref_vector get_trail() override {
315 if (m_use_solver1_results)
316 return m_solver1->get_trail();
317 else
318 return m_solver2->get_trail();
319 }
320
get_proof()321 proof * get_proof() override {
322 if (m_use_solver1_results)
323 return m_solver1->get_proof();
324 else
325 return m_solver2->get_proof();
326 }
327
reason_unknown() const328 std::string reason_unknown() const override {
329 if (m_use_solver1_results)
330 return m_solver1->reason_unknown();
331 else
332 return m_solver2->reason_unknown();
333 }
334
set_reason_unknown(char const * msg)335 void set_reason_unknown(char const* msg) override {
336 m_solver1->set_reason_unknown(msg);
337 m_solver2->set_reason_unknown(msg);
338 }
339
get_labels(svector<symbol> & r)340 void get_labels(svector<symbol> & r) override {
341 if (m_use_solver1_results)
342 return m_solver1->get_labels(r);
343 else
344 return m_solver2->get_labels(r);
345 }
346
347 };
348
349
mk_combined_solver(solver * s1,solver * s2,params_ref const & p)350 solver * mk_combined_solver(solver * s1, solver * s2, params_ref const & p) {
351 return alloc(combined_solver, s1, s2, p);
352 }
353
354 class combined_solver_factory : public solver_factory {
355 scoped_ptr<solver_factory> m_f1;
356 scoped_ptr<solver_factory> m_f2;
357 public:
combined_solver_factory(solver_factory * f1,solver_factory * f2)358 combined_solver_factory(solver_factory * f1, solver_factory * f2):m_f1(f1), m_f2(f2) {}
~combined_solver_factory()359 ~combined_solver_factory() override {}
360
operator ()(ast_manager & m,params_ref const & p,bool proofs_enabled,bool models_enabled,bool unsat_core_enabled,symbol const & logic)361 solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) override {
362 return mk_combined_solver((*m_f1)(m, p, proofs_enabled, models_enabled, unsat_core_enabled, logic),
363 (*m_f2)(m, p, proofs_enabled, models_enabled, unsat_core_enabled, logic),
364 p);
365 }
366 };
367
mk_combined_solver_factory(solver_factory * f1,solver_factory * f2)368 solver_factory * mk_combined_solver_factory(solver_factory * f1, solver_factory * f2) {
369 return alloc(combined_solver_factory, f1, f2);
370 }
371