expose strategic solver factory prototype at level of solver module

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

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<solver_factory> 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<frame> 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);
 }
 

src/solver/solver.h

@@ -32,6 +32,8 @@ class solver_factory {
     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.

src/tactic/portfolio/smt_strategic_solver.h

@@ -22,6 +22,6 @@ Module Name:
 
 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