From 4d8d705b3f72cb0b78c4c4e8779203e5c6e16a7a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Feb 2017 08:02:24 -0800 Subject: [PATCH] bypass combined solver when logic is set to QF_BV or QF_FD Signed-off-by: Nikolaj Bjorner --- src/tactic/portfolio/smt_strategic_solver.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index d2414ec72..16e59302b 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -98,13 +98,19 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const return mk_default_tactic(m, p); } -static solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) { +static solver* mk_special_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) { bv_rewriter rw(m); if (logic == "QF_BV" && rw.hi_div0()) return mk_inc_sat_solver(m, p); if (logic == "QF_FD") return mk_fd_solver(m, p); - return mk_smt_solver(m, p, logic); + return 0; +} + +static solver* mk_solver_for_logic(ast_manager & m, params_ref const & p, symbol const& logic) { + solver* s = mk_special_solver_for_logic(m, p, logic); + if (!s) s = mk_smt_solver(m, p, logic); + return s; } class smt_strategic_solver_factory : public solver_factory { @@ -119,6 +125,8 @@ public: l = m_logic; else l = logic; + solver* s = mk_special_solver_for_logic(m, p, l); + if (s) return s; tactic * t = mk_tactic_for_logic(m, p, l); return mk_combined_solver(mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, l), mk_solver_for_logic(m, p, l),