From fc41a61b6e03c03760f8f87c4aef30ffed78c24f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 9 Aug 2019 15:52:12 -0700 Subject: [PATCH] expose strategic solver factory prototype at level of solver module Signed-off-by: Nikolaj Bjorner --- src/muz/spacer/spacer_sat_answer.cpp | 7 ++++++- src/solver/solver.h | 2 ++ src/tactic/portfolio/smt_strategic_solver.h | 2 +- 3 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/muz/spacer/spacer_sat_answer.cpp b/src/muz/spacer/spacer_sat_answer.cpp index 7b54260f5..7b0a6b09d 100644 --- a/src/muz/spacer/spacer_sat_answer.cpp +++ b/src/muz/spacer/spacer_sat_answer.cpp @@ -53,7 +53,11 @@ proof_ref ground_sat_answer_op::operator()(pred_transformer &query) { // -- turn on proof mode so that proof constructing API in ast_manager work correctly scoped_proof _pf(m); - m_solver = mk_smt_solver(m, params_ref::get_empty(), symbol::null); + scoped_ptr factory(mk_smt_strategic_solver_factory(symbol::null)); + m_solver = (*factory)(m, params_ref::get_empty(), + m.proofs_enabled() /*proofs*/, true /*models*/, false /*unsat_core*/, symbol::null /*logic*/); + + // m_solver = mk_smt_solver(m, params_ref::get_empty(), symbol::null); vector todo, new_todo; // -- find substitution for a query if query is not nullary @@ -100,6 +104,7 @@ proof_ref ground_sat_answer_op::operator()(pred_transformer &query) { todo.pop_back(); } } + m_solver.reset(); return proof_ref(m_cache.find(root_fact), m); } diff --git a/src/solver/solver.h b/src/solver/solver.h index 0c509b8c7..200a44ed8 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -32,6 +32,8 @@ public: virtual solver * operator()(ast_manager & m, params_ref const & p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const & logic) = 0; }; +solver_factory * mk_smt_strategic_solver_factory(symbol const & logic = symbol::null); + /** \brief Abstract interface for making solvers available in the Z3 API and front-ends such as SMT 2.0 and (legacy) SMT 1.0. diff --git a/src/tactic/portfolio/smt_strategic_solver.h b/src/tactic/portfolio/smt_strategic_solver.h index 77e9299e6..e805cc74c 100644 --- a/src/tactic/portfolio/smt_strategic_solver.h +++ b/src/tactic/portfolio/smt_strategic_solver.h @@ -22,6 +22,6 @@ Notes: class solver_factory; -solver_factory * mk_smt_strategic_solver_factory(symbol const & logic = symbol::null); +// solver_factory * mk_smt_strategic_solver_factory(symbol const & logic = symbol::null); #endif