Switch to using solver instead of smt::kernel all around

src/muz/spacer/spacer_context.cpp

@@ -2289,33 +2289,56 @@ void context::reset_lemma_generalizers()
 // initialize global SMT parameters shared by all solvers
 void context::init_global_smt_params() {
     m.toggle_proof_mode(PGM_ENABLED);
-    smt_params &fparams = m_pm.fparams ();
+    params_ref p;
     if (!m_params.spacer_eq_prop ()) {
-        fparams.m_arith_bound_prop = BP_NONE;
+        // arith_propagation_mode
-        fparams.m_arith_auto_config_simplex = true;
+        p.set_uint("arith.propagation_mode", 0);
-        fparams.m_arith_propagate_eqs = false;
+        // fparams.m_arith_bound_prop = BP_NONE;
-        fparams.m_arith_eager_eq_axioms = false;
+        // NOT AVAILABLE
+        // fparams.m_arith_auto_config_simplex = true;
+        // arith_propagate_eqs
+        // fparams.m_arith_propagate_eqs = false;
+        p.set_bool("arith.propagate_eqs", false);
+        // NOT AVAILABLE
+        // fparams.m_arith_eager_eq_axioms = false;
     }
-    fparams.m_random_seed = m_params.spacer_random_seed ();
+    // fparams.m_random_seed = m_params.spacer_random_seed ();
+    p.set_uint("random_seed", m_params.spacer_random_seed());
 
-    fparams.m_dump_benchmarks = m_params.spacer_vs_dump_benchmarks();
+    // fparams.m_dump_benchmarks = m_params.spacer_vs_dump_benchmarks();
-    fparams.m_dump_min_time = m_params.spacer_vs_dump_min_time();
+    // fparams.m_dump_min_time = m_params.spacer_vs_dump_min_time();
-    fparams.m_dump_recheck = m_params.spacer_vs_recheck();
+    // fparams.m_dump_recheck = m_params.spacer_vs_recheck();
 
-    fparams.m_mbqi = m_params.spacer_mbqi();
+    // mbqi
+    // fparams.m_mbqi = m_params.spacer_mbqi();
+    p.set_bool("mbqi", m_params.spacer_mbqi());
 
     if (!m_params.spacer_ground_cti()) {
-        fparams.m_pi_use_database = true; // you don't need this
+        // fparams.m_pi_use_database = true; // you don't need this
-        fparams.m_phase_selection = PS_CACHING_CONSERVATIVE2;
+        // phase_selection
-        fparams.m_restart_strategy = RS_GEOMETRIC;
+        // fparams.m_phase_selection = PS_CACHING_CONSERVATIVE2;
-        fparams.m_restart_factor = 1.5;
+        p.set_uint("phase_selection", 4);
-        fparams.m_eliminate_bounds = true;
+        // restart_strategy
-        fparams.m_qi_quick_checker = MC_UNSAT; // 
+        // fparams.m_restart_strategy = RS_GEOMETRIC;
-        fparams.m_qi_eager_threshold = 10;
+        p.set_uint("restart_strategy", 0);
-        fparams.m_qi_lazy_threshold = 20;
+        // restart factor
-        fparams.m_ng_lift_ite = LI_FULL;    // ? probably useless 
+        // fparams.m_restart_factor = 1.5;
+        p.set_double("restart_factor", 1.5);
+        // probably not needed in our use case
+        // fparams.m_eliminate_bounds = true;
+        // NONE
+        // fparams.m_qi_quick_checker = MC_UNSAT; //
+        // qi_eager_threshold
+        // fparams.m_qi_eager_threshold = 10;
+        p.set_double("qi.eager_threshold", 10.0);
+        // qi_lazy_threshold
+        // fparams.m_qi_lazy_threshold = 20;
+        p.set_double("qi.lazy_threshold", 20.0);
+        // useless
+        // fparams.m_ng_lift_ite = LI_FULL;
     }
 
+    m_pm.updt_params(p);
 }
 void context::init_lemma_generalizers()
 {

src/muz/spacer/spacer_iuc_solver.h

@@ -107,6 +107,10 @@ public:
 
     solver* translate(ast_manager &m, params_ref const &p) override  { return m_solver.translate(m, p);}
     void updt_params(params_ref const &p) override   {m_solver.updt_params(p);}
+    void reset_params(params_ref const &p) override  {m_solver.reset_params(p);}
+    const params_ref &get_params() const override {return m_solver.get_params();}
+    void push_params() override {m_solver.push_params();}
+    void pop_params() override {m_solver.pop_params();}
     void collect_param_descrs(param_descrs &r) override  { m_solver.collect_param_descrs(r);}
     void set_produce_models(bool f) override  { m_solver.set_produce_models(f);}
     void assert_expr_core(expr *t) override  { m_solver.assert_expr(t);}

src/muz/spacer/spacer_manager.h

@@ -155,11 +155,13 @@ public:
     // three different solvers with three different sets of parameters
     // different solvers are used for different types of queries in spacer
     solver* mk_fresh() {return m_contexts.mk_fresh();}
-    smt_params& fparams() { return m_contexts.fparams(); }
+    void updt_params(const params_ref &p) {m_contexts.updt_params(p);}
+
     solver* mk_fresh2() {return m_contexts2.mk_fresh();}
-    smt_params &fparams2() { return m_contexts2.fparams(); }
+    void updt_params2(const params_ref &p) {m_contexts2.updt_params(p);}
+
     solver* mk_fresh3() {return m_contexts3.mk_fresh();}
-    smt_params &fparams3() {return m_contexts3.fparams();}
+    void updt_params3(const params_ref &p) {m_contexts3.updt_params(p);}
 
 
 

src/muz/spacer/spacer_prop_solver.cpp

@@ -56,10 +56,7 @@ prop_solver::prop_solver(spacer::manager& pm,
 {
 
     m_solvers[0] = pm.mk_fresh();
-    m_fparams[0] = &pm.fparams();
-
     m_solvers[1] = pm.mk_fresh2();
-    m_fparams[1] = &pm.fparams2();
 
     m_contexts[0] = alloc(spacer::iuc_solver, *(m_solvers[0]),
                           p.spacer_iuc(),
@@ -293,8 +290,12 @@ lbool prop_solver::internal_check_assumptions(
 {
     // XXX Turn model generation if m_model != 0
     SASSERT(m_ctx);
-    SASSERT(m_ctx_fparams);
+
-    flet<bool> _model(m_ctx_fparams->m_model, m_model != nullptr);
+    params_ref p;
+    if (m_model != nullptr) {
+        p.set_bool("produce_models", true);
+        m_ctx->updt_params(p);
+    }
 
     if (m_in_level) { assert_level_atoms(m_current_level); }
     lbool result = maxsmt(hard_atoms, soft_atoms);
@@ -333,6 +334,12 @@ lbool prop_solver::internal_check_assumptions(
         // manually undo proxies because maxsmt() call above manually adds proxies
         m_ctx->undo_proxies(*m_core);
     }
+
+    if (m_model != nullptr) {
+        p.set_bool("produce_models", false);
+        m_ctx->updt_params(p);
+    }
+
     return result;
 }
 
@@ -350,7 +357,6 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard,
     flatten_and(hard);
 
     m_ctx = m_contexts [solver_id == 0 ? 0 : 0 /* 1 */].get();
-    m_ctx_fparams = m_fparams [solver_id == 0 ? 0 : 0 /* 1 */];
 
     // can be disabled if use_push_bg == true
     // solver::scoped_push _s_(*m_ctx);

src/muz/spacer/spacer_prop_solver.h

@@ -42,11 +42,9 @@ class prop_solver {
 private:
     ast_manager&        m;
     symbol              m_name;
-    smt_params*         m_fparams[2];
     solver*             m_solvers[2];
     scoped_ptr<iuc_solver>  m_contexts[2];
     iuc_solver *            m_ctx;
-    smt_params *            m_ctx_fparams;
     decl_vector         m_level_preds;
     app_ref_vector      m_pos_level_atoms;  // atoms used to identify level
     app_ref_vector      m_neg_level_atoms;  //
@@ -138,25 +136,20 @@ public:
     };
 
     class scoped_weakness {
-
-        smt_params &m_params;
-        bool m_arith_ignore_int;
-        bool m_array_weak;
     public:
-        scoped_weakness(prop_solver &ps, unsigned solver_id, unsigned weakness) :
+        solver *sol;
-            m_params(*ps.m_fparams[solver_id == 0 ? 0 : 0 /*1*/]) {
+        scoped_weakness(prop_solver &ps, unsigned solver_id, unsigned weakness)
-            // save current values
+            : sol(nullptr) {
-            m_arith_ignore_int = m_params.m_arith_ignore_int;
+            sol = ps.m_solvers[solver_id == 0 ? 0 :  0 /* 1 */];
-            m_array_weak = m_params.m_array_weak;
+            if (!sol) return;
+            sol->push_params();
 
-            // set values based on weakness score
+            params_ref p;
-            m_params.m_arith_ignore_int = weakness < 1;
+            p.set_bool("arith.ignore_int", weakness < 1);
-            m_params.m_array_weak = weakness < 2;
+            p.set_bool("array.weak",  weakness < 2);
-        }
+            sol->updt_params(p);
-        ~scoped_weakness() {
-            m_params.m_arith_ignore_int = m_arith_ignore_int;
-            m_params.m_array_weak = m_array_weak;
         }
+        ~scoped_weakness() {if (sol) {sol->pop_params();}}
     };
 };
 }

src/muz/spacer/spacer_smt_context_manager.cpp

@@ -24,19 +24,17 @@ Revision History:
 
 #include "smt/smt_context.h"
 #include "smt/params/smt_params.h"
+#include "smt/smt_solver.h"
 
 #include "muz/spacer/spacer_util.h"
 #include "muz/spacer/spacer_smt_context_manager.h"
 namespace spacer {
 
-
-
-
 smt_context_manager::smt_context_manager(ast_manager &m,
         unsigned max_num_contexts,
         const params_ref &p) :
-    m_fparams(p),
     m(m),
+    m_params(p),
     m_max_num_contexts(max_num_contexts),
     m_num_contexts(0) { m_stats.reset();}
 
@@ -45,6 +43,13 @@ smt_context_manager::~smt_context_manager()
 {
     std::for_each(m_solvers.begin(), m_solvers.end(),
                   delete_proc<spacer::virtual_solver_factory>());
+    m_solvers.reset();
+    m_base_solvers.reset();
+}
+
+void smt_context_manager::updt_params(params_ref const &p) {
+    m_params.append(p);
+    for (auto *s : m_base_solvers) {s->updt_params(m_params);}
 }
 
 virtual_solver* smt_context_manager::mk_fresh()
@@ -53,10 +58,14 @@ virtual_solver* smt_context_manager::mk_fresh()
     virtual_solver_factory *solver_factory = nullptr;
 
     if (m_max_num_contexts == 0 || m_solvers.size() < m_max_num_contexts) {
-        m_solvers.push_back(alloc(spacer::virtual_solver_factory, m, m_fparams));
+        m_base_solvers.push_back(mk_smt_solver(m, m_params, symbol::null));
+        m_solvers.push_back(alloc(spacer::virtual_solver_factory,
+                                  *m_base_solvers.back()));
         solver_factory = m_solvers.back();
-    } else
+    }
-    { solver_factory = m_solvers[(m_num_contexts - 1) % m_max_num_contexts]; }
+    else {
+        solver_factory = m_solvers[(m_num_contexts - 1) % m_max_num_contexts];
+    }
 
     return solver_factory->mk_solver();
 }

src/muz/spacer/spacer_smt_context_manager.h

@@ -37,9 +37,10 @@ class smt_context_manager {
         void reset() { memset(this, 0, sizeof(*this)); }
     };
 
-    smt_params               m_fparams;
     ast_manager&             m;
+    params_ref               m_params;
     unsigned                 m_max_num_contexts;
+    sref_vector<solver> m_base_solvers;
     ptr_vector<virtual_solver_factory> m_solvers;
     unsigned                 m_num_contexts;
 
@@ -58,8 +59,8 @@ public:
     void collect_statistics(statistics& st) const;
     void reset_statistics();
 
-    void updt_params(params_ref const &p) { m_fparams.updt_params(p); }
+    void updt_params(params_ref const &p);
-    smt_params& fparams() {return m_fparams;}
+
 
 };
 

src/muz/spacer/spacer_virtual_solver.cpp

@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-   multi-solver view of a single smt::kernel
+   multi-solver view of a single solver
 
 Author:
 
@@ -28,13 +28,14 @@ Notes:
 
 #include "ast/scoped_proof.h"
 
+#include "smt/smt_kernel.h"
+
 namespace spacer {
-virtual_solver::virtual_solver(virtual_solver_factory &factory,
+virtual_solver::virtual_solver(virtual_solver_factory &factory, app* pred) :
-                               smt::kernel &context, app* pred) :
+    solver_na2as(factory.get_manager()),
-    solver_na2as(context.m()),
     m_factory(factory),
-    m(context.m()),
+    m(factory.get_manager()),
-    m_context(context),
+    m_context(factory.get_base_solver()),
     m_pred(pred, m),
     m_virtual(!m.is_true(pred)),
     m_assertions(m),
@@ -42,7 +43,7 @@ virtual_solver::virtual_solver(virtual_solver_factory &factory,
     m_flat(m),
     m_pushed(false),
     m_in_delay_scope(false),
-    m_dump_benchmarks(factory.fparams().m_dump_benchmarks),
+    m_dump_benchmarks(false /*factory.fparams().m_dump_benchmarks*/),
     m_dump_counter(0),
     m_proof(m)
 {
@@ -114,7 +115,7 @@ lbool virtual_solver::check_sat_core(unsigned num_assumptions,
         out << "(exit)\n";
         out.close();
     }
-    lbool res = m_context.check(num_assumptions, assumptions);
+    lbool res = m_context.check_sat(num_assumptions, assumptions);
     sw.stop();
     if (res == l_true) {
         m_factory.m_check_sat_watch.add(sw);
@@ -125,8 +126,8 @@ lbool virtual_solver::check_sat_core(unsigned num_assumptions,
     }
     set_status(res);
 
-    if (m_dump_benchmarks &&
+    if (false /*m_dump_benchmarks &&
-            sw.get_seconds() >= m_factory.fparams().m_dump_min_time) {
+                sw.get_seconds() >= m_factory.fparams().m_dump_min_time*/) {
         std::stringstream file_name;
         file_name << "virt_solver";
         if (m_virtual) { file_name << "_" << m_pred->get_decl()->get_name(); }
@@ -151,13 +152,13 @@ lbool virtual_solver::check_sat_core(unsigned num_assumptions,
         st.display_smt2(out);
 
 
-        if (m_factory.fparams().m_dump_recheck) {
+        if (false /* m_factory.fparams().m_dump_recheck */) {
             scoped_no_proof _no_proof_(m);
             smt_params p;
             stopwatch sw2;
             smt::kernel kernel(m, p);
-            for (unsigned i = 0, sz = m_context.size(); i < sz; ++i)
+            for (unsigned i = 0, sz = m_context.get_num_assertions(); i < sz; ++i)
-                { kernel.assert_expr(m_context.get_formula(i)); }
+                { kernel.assert_expr(m_context.get_assertion(i)); }
             sw2.start();
             kernel.check(num_assumptions, assumptions);
             sw2.stop();
@@ -208,10 +209,12 @@ void virtual_solver::pop_core(unsigned n) {
 
 void virtual_solver::get_unsat_core(ptr_vector<expr> &r)
 {
-    for (unsigned i = 0, sz = m_context.get_unsat_core_size(); i < sz; ++i) {
+    ptr_vector<expr> core;
-        expr *core = m_context.get_unsat_core_expr(i);
+    m_context.get_unsat_core(core);
-        if (is_aux_predicate(core)) { continue; }
+
-        r.push_back(core);
+    for (unsigned i = 0, sz = core.size(); i < sz; ++i) {
+        if (is_aux_predicate(core.get(i))) { continue; }
+        r.push_back(core.get(i));
     }
 }
 
@@ -244,40 +247,25 @@ void virtual_solver::internalize_assertions()
         m_context.assert_expr(f);
     }
 }
-void virtual_solver::refresh()
-{
-    SASSERT(!m_pushed);
-    m_head = 0;
-}
-
-void virtual_solver::reset()
-{
-    SASSERT(!m_pushed);
-    m_head = 0;
-    m_assertions.reset();
-    m_factory.refresh();
-}
 
 void virtual_solver::get_labels(svector<symbol> &r)
-{
+{m_context.get_labels(r);}
-    r.reset();
-    buffer<symbol> tmp;
-    m_context.get_relevant_labels(nullptr, tmp);
-    r.append(tmp.size(), tmp.c_ptr());
-}
 
 solver* virtual_solver::translate(ast_manager& m, params_ref const& p)
 {
     UNREACHABLE();
     return nullptr;
 }
-void virtual_solver::updt_params(params_ref const &p) { m_factory.updt_params(p); }
+void virtual_solver::updt_params(params_ref const &p) {m_context.updt_params(p);}
-void virtual_solver::collect_param_descrs(param_descrs &r) { m_factory.collect_param_descrs(r); }
+void virtual_solver::reset_params(params_ref const &p) {m_context.reset_params(p);}
-void virtual_solver::set_produce_models(bool f) { m_factory.set_produce_models(f); }
+const params_ref &virtual_solver::get_params() const {return m_context.get_params();}
-smt_params &virtual_solver::fparams() {return m_factory.fparams();}
+void virtual_solver::push_params(){m_context.push_params();}
+void virtual_solver::pop_params(){m_context.pop_params();}
+void virtual_solver::collect_param_descrs(param_descrs &r) { m_context.collect_param_descrs(r); }
+void virtual_solver::set_produce_models(bool f) { m_context.set_produce_models(f); }
 
 void virtual_solver::to_smt2_benchmark(std::ostream &out,
-                                       smt::kernel &context,
+                                       solver &context,
                                        unsigned num_assumptions,
                                        expr * const * assumptions,
                                        char const * name,
@@ -288,11 +276,8 @@ void virtual_solver::to_smt2_benchmark(std::ostream &out,
     ast_pp_util pp(m);
     expr_ref_vector asserts(m);
 
-
+    context.get_assertions(asserts);
-    for (unsigned i = 0, sz = context.size(); i < sz; ++i) {
+    pp.collect(asserts);
-        asserts.push_back(context.get_formula(i));
-        pp.collect(asserts.back());
-    }
     pp.collect(num_assumptions, assumptions);
     pp.display_decls(out);
     pp.display_asserts(out, asserts);
@@ -303,11 +288,8 @@ void virtual_solver::to_smt2_benchmark(std::ostream &out,
 }
 
 
-virtual_solver_factory::virtual_solver_factory(ast_manager &mgr, smt_params &fparams) :
+virtual_solver_factory::virtual_solver_factory(solver &base) :
-    m_fparams(fparams), m(mgr), m_context(m, m_fparams)
+    m(base.get_manager()), m_context(base) {m_stats.reset();}
-{
-    m_stats.reset();
-}
 
 virtual_solver* virtual_solver_factory::mk_solver()
 {
@@ -316,7 +298,7 @@ virtual_solver* virtual_solver_factory::mk_solver()
     app_ref pred(m);
     pred = m.mk_const(symbol(name.str().c_str()), m.mk_bool_sort());
     SASSERT(m_context.get_scope_level() == 0);
-    m_solvers.push_back(alloc(virtual_solver, *this, m_context, pred));
+    m_solvers.push_back(alloc(virtual_solver, *this, pred));
     return m_solvers.back();
 }
 
@@ -333,7 +315,6 @@ void virtual_solver_factory::collect_statistics(statistics &st) const
 }
 void virtual_solver_factory::reset_statistics()
 {
-    m_context.reset_statistics();
     m_stats.reset();
     m_check_sat_watch.reset();
     m_check_undef_watch.reset();
@@ -341,13 +322,6 @@ void virtual_solver_factory::reset_statistics()
     m_proof_watch.reset();
 }
 
-void virtual_solver_factory::refresh()
-{
-    m_context.reset();
-    for (unsigned i = 0, e = m_solvers.size(); i < e; ++i)
-    { m_solvers [i]->refresh(); }
-}
-
 virtual_solver_factory::~virtual_solver_factory()
 {
     for (unsigned i = 0, e = m_solvers.size(); i < e; ++i)

src/muz/spacer/spacer_virtual_solver.h

@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-   multi-solver view of a single smt::kernel
+   multi-solver view of a single solver
 
 Author:
 
@@ -21,7 +21,6 @@ Notes:
 #include"ast/ast.h"
 #include"util/params.h"
 #include"solver/solver_na2as.h"
-#include"smt/smt_kernel.h"
 #include"smt/params/smt_params.h"
 #include"util/stopwatch.h"
 namespace spacer {
@@ -33,7 +32,7 @@ class virtual_solver : public solver_na2as {
 private:
     virtual_solver_factory &m_factory;
     ast_manager &m;
-    smt::kernel &m_context;
+    solver &m_context;
     app_ref m_pred;
 
     bool m_virtual;
@@ -49,12 +48,12 @@ private:
 
     proof_ref m_proof;
 
-    virtual_solver(virtual_solver_factory &factory, smt::kernel &context, app* pred);
+    virtual_solver(virtual_solver_factory &factory, app* pred);
 
     bool is_aux_predicate(expr *p);
     void internalize_assertions();
     void to_smt2_benchmark(std::ostream &out,
-                           smt::kernel &context,
+                           solver &context,
                            unsigned num_assumptions,
                            expr * const * assumptions,
                            char const * name = "benchmarks",
@@ -62,8 +61,6 @@ private:
                            char const * status = "unknown",
                            char const * attributes = "");
 
-    void refresh();
-
 public:
     ~virtual_solver() override;
     unsigned get_num_assumptions() const override
@@ -84,21 +81,24 @@ public:
     void get_model_core(model_ref &m) override {m_context.get_model(m);}
     proof* get_proof() override;
     std::string reason_unknown() const override
-    {return m_context.last_failure_as_string();}
+    {return m_context.reason_unknown();}
     void set_reason_unknown(char const *msg) override
     {m_context.set_reason_unknown(msg);}
     ast_manager& get_manager() const override {return m;}
     void get_labels(svector<symbol> &r) override;
     void set_produce_models(bool f) override;
     smt_params &fparams();
-    void reset();
     expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); }
     void set_progress_callback(progress_callback *callback) override {UNREACHABLE();}
 
     solver *translate(ast_manager &m, params_ref const &p) override;
 
     void updt_params(params_ref const &p) override;
+    void reset_params(params_ref const& p) override;
+    params_ref const& get_params() const override;
     void collect_param_descrs(param_descrs &r) override;
+    void push_params() override;
+    void pop_params() override;
 
 
 protected:
@@ -107,13 +107,12 @@ protected:
     void pop_core(unsigned n) override;
 };
 
-/// multi-solver abstraction on top of a single smt::kernel
+/// multi-solver abstraction on top of a single solver
 class virtual_solver_factory {
     friend class virtual_solver;
 private:
-    smt_params  &m_fparams;
     ast_manager &m;
-    smt::kernel m_context;
+    solver &m_context;
     /// solvers managed by this factory
     ptr_vector<virtual_solver> m_solvers;
 
@@ -132,20 +131,17 @@ private:
     stopwatch m_proof_watch;
 
 
-    void refresh();
+    solver &get_base_solver() {return m_context;}
-
+    ast_manager &get_manager() {return m;}
-    smt_params &fparams() { return m_fparams; }
 
 public:
-    virtual_solver_factory(ast_manager &mgr, smt_params &fparams);
+    virtual_solver_factory(solver &base);
     virtual ~virtual_solver_factory();
     virtual_solver* mk_solver();
     void collect_statistics(statistics &st) const;
     void reset_statistics();
-    void updt_params(params_ref const &p) { m_fparams.updt_params(p); }
+    void updt_params(params_ref const &p) {m_context.updt_params(p);}
-    void collect_param_descrs(param_descrs &r) { /* empty */ }
+    void collect_param_descrs(param_descrs &r) {m_context.collect_param_descrs(r);}
-    void set_produce_models(bool f) { m_fparams.m_model = f; }
-    bool get_produce_models() { return m_fparams.m_model; }
 };
 
 }