From ac3bbed311548e28ecf90b2df7adfa1e5ec34a25 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Thu, 17 May 2018 12:17:39 -0700
Subject: [PATCH] Remove dead code in spacer_manager

  - removed bg_assertions. Incompatible with mbp in spacer
  - removed unique number. Unused
  - removed mk_and() and switched to ast_util:mk_and() instead
       spacer_manager::mk_and() uses bool_rewriter to simplify the
       conjunction
---
 src/muz/spacer/spacer_context.cpp      |  41 ++---
 src/muz/spacer/spacer_context.h        |   2 -
 src/muz/spacer/spacer_dl_interface.cpp |  15 +-
 src/muz/spacer/spacer_generalizers.cpp |   2 +-
 src/muz/spacer/spacer_manager.cpp      | 126 +------------
 src/muz/spacer/spacer_manager.h        | 242 ++++---------------------
 src/muz/spacer/spacer_prop_solver.cpp  |   7 +-
 src/muz/spacer/spacer_prop_solver.h    |   4 +-
 8 files changed, 73 insertions(+), 366 deletions(-)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 5de817435..7d8ffc0aa 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -312,11 +312,10 @@ expr_ref pred_transformer::get_formulas(unsigned level, bool add_axioms)
 {
     expr_ref_vector res(m);
     if (add_axioms) {
-        res.push_back(pm.get_background());
         res.push_back((level == 0)?initial_state():transition());
     }
     m_frames.get_frame_geq_lemmas (level, res);
-    return pm.mk_and(res);
+    return mk_and(res);
 }
 
 bool pred_transformer::propagate_to_next_level (unsigned src_level)
@@ -539,7 +538,7 @@ expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level)
 
     expr_ref_vector lemmas (m);
     m_frames.get_frame_lemmas (level == -1 ? infty_level() : level, lemmas);
-    if (!lemmas.empty()) { result = pm.mk_and(lemmas); }
+    if (!lemmas.empty()) { result = mk_and(lemmas); }
 
     // replace local constants by bound variables.
     expr_substitution sub(m);
@@ -611,7 +610,7 @@ expr_ref pred_transformer::get_origin_summary (model_evaluator_util &mev,
     expr_ref_vector literals (m);
     compute_implicant_literals (mev, summary, literals);
 
-    return get_manager ().mk_and (literals);
+    return mk_and(literals);
 }
 
 
@@ -857,10 +856,10 @@ bool pred_transformer::is_invariant(unsigned level, lemma* lem,
 bool pred_transformer::check_inductive(unsigned level, expr_ref_vector& state,
                                        unsigned& uses_level, unsigned weakness)
 {
-    manager& pm = get_manager();
     expr_ref_vector conj(m), core(m);
     expr_ref states(m);
-    states = m.mk_not(pm.mk_and(state));
+    states = mk_and(state);
+    states = m.mk_not(states);
     mk_assumptions(head(), states, conj);
     prop_solver::scoped_level _sl(m_solver, level);
     prop_solver::scoped_subset_core _sc (m_solver, true);
@@ -972,7 +971,7 @@ void pred_transformer::init_rules(decl2rel const& pts, expr_ref& init, expr_ref&
         transitions.push_back (m.mk_or (pred, m_extend_lit->get_arg (0)));
         if (!is_init [0]) { init_conds.push_back(m.mk_not(pred)); }
 
-        transition = pm.mk_and(transitions);
+        transition = mk_and(transitions);
         break;
     }
     default:
@@ -992,11 +991,11 @@ void pred_transformer::init_rules(decl2rel const& pts, expr_ref& init, expr_ref&
             }
         }
         transitions.push_back(m.mk_or(disj.size(), disj.c_ptr()));
-        transition = pm.mk_and(transitions);
+        transition = mk_and(transitions);
         break;
     }
     // mk init condition
-    init = pm.mk_and (init_conds);
+    init = mk_and (init_conds);
     if (init_conds.empty ()) { // no rule has uninterpreted tail
         m_all_init = true;
     }
@@ -1146,7 +1145,6 @@ void pred_transformer::init_atom(
 
 void pred_transformer::add_premises(decl2rel const& pts, unsigned lvl, expr_ref_vector& r)
 {
-    r.push_back(pm.get_background());
     r.push_back((lvl == 0)?initial_state():transition());
     for (unsigned i = 0; i < rules().size(); ++i) {
         add_premises(pts, lvl, *rules()[i], r);
@@ -1736,7 +1734,7 @@ pob *derivation::create_next_child (model_evaluator_util &mev)
 
     // -- update m_trans with the pre-image of m_trans over the must summaries
     summaries.push_back (m_trans);
-    m_trans = get_manager ().mk_and (summaries);
+    m_trans = mk_and (summaries);
     summaries.reset ();
 
     if (!vars.empty()) {
@@ -1765,7 +1763,7 @@ pob *derivation::create_next_child (model_evaluator_util &mev)
     summaries.push_back (m_trans);
 
     expr_ref post(m);
-    post = get_manager ().mk_and (summaries);
+    post = mk_and (summaries);
     summaries.reset ();
     if (!vars.empty()) {
         timeit _timer2 (is_trace_enabled("spacer_timeit"),
@@ -1827,7 +1825,7 @@ pob *derivation::create_next_child ()
 
     // if not true, bail out, the must summary of m_active is not strong enough
     // this is possible if m_post was weakened for some reason
-    if (!pt.is_must_reachable(pm.mk_and(summaries), &model)) { return nullptr; }
+    if (!pt.is_must_reachable(mk_and(summaries), &model)) { return nullptr; }
 
     model_evaluator_util mev (m);
     mev.set_model (*model);
@@ -1840,7 +1838,7 @@ pob *derivation::create_next_child ()
     u.push_back (rf->get ());
     compute_implicant_literals (mev, u, lits);
     expr_ref v(m);
-    v = pm.mk_and (lits);
+    v = mk_and (lits);
 
     // XXX The summary is not used by anyone after this point
     m_premises[m_active].set_summary (v, true, &(rf->aux_vars ()));
@@ -1860,7 +1858,7 @@ pob *derivation::create_next_child ()
         summaries.reset ();
         summaries.push_back (v);
         summaries.push_back (active_trans);
-        m_trans = pm.mk_and (summaries);
+        m_trans = mk_and (summaries);
 
         // variables to eliminate
         vars.append (rf->aux_vars ().size (), rf->aux_vars ().c_ptr ());
@@ -3184,8 +3182,7 @@ lbool context::expand_node(pob& n)
             n.bump_weakness();
             return expand_node(n);
         }
-        TRACE("spacer", tout << "unknown state: "
-              << mk_pp(m_pm.mk_and(cube), m) << "\n";);
+        TRACE("spacer", tout << "unknown state: " << mk_and(cube) << "\n";);
         throw unknown_exception();
     }
     UNREACHABLE();
@@ -3305,14 +3302,14 @@ reach_fact *context::mk_reach_fact (pob& n, model_evaluator_util &mev,
     bool elim_aux = get_params ().spacer_elim_aux ();
     if (elim_aux) { vars.append(aux_vars.size(), aux_vars.c_ptr()); }
 
-    res = m_pm.mk_and (path_cons);
+    res = mk_and (path_cons);
 
     // -- pick an implicant from the path condition
     if (get_params().spacer_reach_dnf()) {
         expr_ref_vector u(m), lits(m);
         u.push_back (res);
         compute_implicant_literals (mev, u, lits);
-        res = m_pm.mk_and (lits);
+        res = mk_and (lits);
     }
 
 
@@ -3405,7 +3402,7 @@ bool context::create_children(pob& n, datalog::rule const& r,
 
     n.get_skolems(vars);
 
-    expr_ref phi1 = m_pm.mk_and (Phi);
+    expr_ref phi1 = mk_and (Phi);
     qe_project (m, vars, phi1, mev.get_model (), true,
                 m_use_native_mbp, !m_ground_cti);
     //qe::reduce_array_selects (*mev.get_model (), phi1);
@@ -3413,7 +3410,7 @@ bool context::create_children(pob& n, datalog::rule const& r,
 
     TRACE ("spacer",
            tout << "Implicant\n";
-           tout << mk_pp (m_pm.mk_and (Phi), m) << "\n";
+           tout << mk_and (Phi) << "\n";
            tout << "Projected Implicant\n" << mk_pp (phi1, m) << "\n";
         );
 
@@ -3615,7 +3612,7 @@ expr_ref context::get_constraints (unsigned level)
     }
 
     if (constraints.empty()) { return expr_ref(m.mk_true(), m); }
-    return m_pm.mk_and (constraints);
+    return mk_and (constraints);
 }
 
 void context::add_constraint (expr *c, unsigned level)
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 596e5e047..9d3456f2b 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -895,8 +895,6 @@ public:
 
     void update_rules(datalog::rule_set& rules);
 
-    void set_axioms(expr* axioms) { m_pm.set_background(axioms); }
-
     unsigned get_num_levels(func_decl* p);
 
     expr_ref get_cover_delta(int level, func_decl* p_orig, func_decl* p);
diff --git a/src/muz/spacer/spacer_dl_interface.cpp b/src/muz/spacer/spacer_dl_interface.cpp
index b121cf50a..cadbcfb0e 100644
--- a/src/muz/spacer/spacer_dl_interface.cpp
+++ b/src/muz/spacer/spacer_dl_interface.cpp
@@ -93,19 +93,14 @@ lbool dl_interface::query(expr * query)
     datalog::rule_set        old_rules(rules0);
     func_decl_ref            query_pred(m);
     rm.mk_query(query, m_ctx.get_rules());
-    expr_ref bg_assertion = m_ctx.get_background_assertion();
 
     check_reset();
 
     TRACE("spacer",
-    if (!m.is_true(bg_assertion)) {
-    tout << "axioms:\n";
-    tout << mk_pp(bg_assertion, m) << "\n";
-    }
-    tout << "query: " << mk_pp(query, m) << "\n";
-         tout << "rules:\n";
-         m_ctx.display_rules(tout);
-         );
+          tout << "query: " << mk_pp(query, m) << "\n";
+          tout << "rules:\n";
+          m_ctx.display_rules(tout);
+        );
 
 
     apply_default_transformation(m_ctx);
@@ -161,7 +156,6 @@ lbool dl_interface::query(expr * query)
     m_context->set_proof_converter(m_ctx.get_proof_converter());
     m_context->set_model_converter(m_ctx.get_model_converter());
     m_context->set_query(query_pred);
-    m_context->set_axioms(bg_assertion);
     m_context->update_rules(m_spacer_rules);
 
     if (m_spacer_rules.get_rules().empty()) {
@@ -255,7 +249,6 @@ lbool dl_interface::query_from_lvl(expr * query, unsigned lvl)
     m_context->set_proof_converter(m_ctx.get_proof_converter());
     m_context->set_model_converter(m_ctx.get_model_converter());
     m_context->set_query(query_pred);
-    m_context->set_axioms(bg_assertion);
     m_context->update_rules(m_spacer_rules);
 
     if (m_spacer_rules.get_rules().empty()) {
diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp
index 3f6e28be6..34f1eb730 100644
--- a/src/muz/spacer/spacer_generalizers.cpp
+++ b/src/muz/spacer/spacer_generalizers.cpp
@@ -289,7 +289,7 @@ void lemma_array_eq_generalizer::operator() (lemma_ref &lemma)
     // }
 
     TRACE("core_array_eq", tout << "new possible core "
-          << mk_pp(pm.mk_and(lits), m) << "\n";);
+          << mk_and(lits) << "\n";);
 
 
     pred_transformer &pt = lemma->get_pob()->pt();
diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp
index c46c31924..04d3c09d4 100644
--- a/src/muz/spacer/spacer_manager.cpp
+++ b/src/muz/spacer/spacer_manager.cpp
@@ -168,8 +168,8 @@ void inductive_property::display(datalog::rule_manager& rm, ptr_vector<datalog::
     }
 }
 
-std::vector<std::string> manager::get_state_suffixes()
-{
+
+static std::vector<std::string> state_suffixes() {
     std::vector<std::string> res;
     res.push_back("_n");
     return res;
@@ -177,15 +177,11 @@ std::vector<std::string> manager::get_state_suffixes()
 
 manager::manager(unsigned max_num_contexts, ast_manager& manager) :
     m(manager),
-    m_brwr(m),
-    m_mux(m, get_state_suffixes()),
-    m_background(m.mk_true(), m),
+    m_mux(m, state_suffixes()),
     m_contexts(m, max_num_contexts),
     m_contexts2(m, max_num_contexts),
-    m_contexts3(m, max_num_contexts),
-    m_next_unique_num(0)
-{
-}
+    m_contexts3(m, max_num_contexts)
+{}
 
 
 void manager::add_new_state(func_decl * s)
@@ -195,7 +191,6 @@ void manager::add_new_state(func_decl * s)
 
     SASSERT(o_index(0) == 1); //we assume this in the number of retrieved symbols
     m_mux.create_tuple(s, s->get_arity(), s->get_domain(), s->get_range(), 2, vect);
-    m_o0_preds.push_back(vect[o_index(0)]);
 }
 
 func_decl * manager::get_o_pred(func_decl* s, unsigned idx)
@@ -218,117 +213,6 @@ func_decl * manager::get_n_pred(func_decl* s)
     return res;
 }
 
-void manager::mk_model_into_cube(const expr_ref_vector & mdl, expr_ref & res)
-{
-    m_brwr.mk_and(mdl.size(), mdl.c_ptr(), res);
-}
-
-void manager::mk_core_into_cube(const expr_ref_vector & core, expr_ref & res)
-{
-    m_brwr.mk_and(core.size(), core.c_ptr(), res);
-}
-
-void manager::mk_cube_into_lemma(expr * cube, expr_ref & res)
-{
-    m_brwr.mk_not(cube, res);
-}
-
-void manager::mk_lemma_into_cube(expr * lemma, expr_ref & res)
-{
-    m_brwr.mk_not(lemma, res);
-}
-
-expr_ref manager::mk_and(unsigned sz, expr* const* exprs)
-{
-    expr_ref result(m);
-    m_brwr.mk_and(sz, exprs, result);
-    return result;
-}
-
-expr_ref manager::mk_or(unsigned sz, expr* const* exprs)
-{
-    expr_ref result(m);
-    m_brwr.mk_or(sz, exprs, result);
-    return result;
-}
-
-expr_ref manager::mk_not_and(expr_ref_vector const& conjs)
-{
-    expr_ref result(m), e(m);
-    expr_ref_vector es(conjs);
-    flatten_and(es);
-    for (unsigned i = 0; i < es.size(); ++i) {
-        m_brwr.mk_not(es[i].get(), e);
-        es[i] = e;
-    }
-    m_brwr.mk_or(es.size(), es.c_ptr(), result);
-    return result;
-}
-
-void manager::get_or(expr* e, expr_ref_vector& result)
-{
-    result.push_back(e);
-    for (unsigned i = 0; i < result.size();) {
-        e = result[i].get();
-        if (m.is_or(e)) {
-            result.append(to_app(e)->get_num_args(), to_app(e)->get_args());
-            result[i] = result.back();
-            result.pop_back();
-        } else {
-            ++i;
-        }
-    }
-}
-
-bool manager::try_get_state_and_value_from_atom(expr * atom0, app *& state, app_ref& value)
-{
-    if (!is_app(atom0)) {
-        return false;
-    }
-    app * atom = to_app(atom0);
-    expr * arg1;
-    expr * arg2;
-    app * candidate_state;
-    app_ref candidate_value(m);
-    if (m.is_not(atom, arg1)) {
-        if (!is_app(arg1)) {
-            return false;
-        }
-        candidate_state = to_app(arg1);
-        candidate_value = m.mk_false();
-    } else if (m.is_eq(atom, arg1, arg2)) {
-        if (!is_app(arg1) || !is_app(arg2)) {
-            return false;
-        }
-        if (!m_mux.is_muxed(to_app(arg1)->get_decl())) {
-            std::swap(arg1, arg2);
-        }
-        candidate_state = to_app(arg1);
-        candidate_value = to_app(arg2);
-    } else {
-        candidate_state = atom;
-        candidate_value = m.mk_true();
-    }
-    if (!m_mux.is_muxed(candidate_state->get_decl())) {
-        return false;
-    }
-    state = candidate_state;
-    value = candidate_value;
-    return true;
-}
-
-bool manager::try_get_state_decl_from_atom(expr * atom, func_decl *& state)
-{
-    app_ref dummy_value_holder(m);
-    app * s;
-    if (try_get_state_and_value_from_atom(atom, s, dummy_value_holder)) {
-        state = s->get_decl();
-        return true;
-    } else {
-        return false;
-    }
-}
-
 /**
  * Create a new skolem constant
  */
diff --git a/src/muz/spacer/spacer_manager.h b/src/muz/spacer/spacer_manager.h
index 32cf61d57..58b5aca07 100644
--- a/src/muz/spacer/spacer_manager.h
+++ b/src/muz/spacer/spacer_manager.h
@@ -37,9 +37,7 @@ Revision History:
 #include "muz/spacer/spacer_smt_context_manager.h"
 #include "muz/base/dl_rule.h"
 
-namespace smt {
-class context;
-}
+namespace smt {class context;}
 
 namespace spacer {
 
@@ -67,32 +65,24 @@ public:
         m_relation_info(relations) {}
 
     std::string to_string() const;
-
     expr_ref to_expr() const;
-
     void to_model(model_ref& md) const;
-
-    void display(datalog::rule_manager& rm, ptr_vector<datalog::rule> const& rules, std::ostream& out) const;
+    void display(datalog::rule_manager& rm,
+                 ptr_vector<datalog::rule> const& rules,
+                 std::ostream& out) const;
 };
 
 class manager {
     ast_manager&      m;
 
-    mutable bool_rewriter m_brwr;
-
+    // manager of multiplexed names
     sym_mux               m_mux;
-    expr_ref              m_background;
-    decl_vector           m_o0_preds;
+
+    // three solver pools for different queries
     spacer::smt_context_manager   m_contexts;
     spacer::smt_context_manager   m_contexts2;
     spacer::smt_context_manager   m_contexts3;
 
-    /** whenever we need an unique number, we get this one and increase */
-    unsigned m_next_unique_num;
-
-
-    static std::vector<std::string> get_state_suffixes();
-
     unsigned n_index() const { return 0; }
     unsigned o_index(unsigned i) const { return i + 1; }
 
@@ -102,218 +92,68 @@ public:
     manager(unsigned max_num_contexts, ast_manager & manager);
 
     ast_manager& get_manager() const { return m; }
-    bool_rewriter& get_brwr() const { return m_brwr; }
 
-    expr_ref mk_and(unsigned sz, expr* const* exprs);
-    expr_ref mk_and(expr_ref_vector const& exprs)
-    {
-        return mk_and(exprs.size(), exprs.c_ptr());
-    }
-    expr_ref mk_and(expr* a, expr* b)
-    {
-        expr* args[2] = { a, b };
-        return mk_and(2, args);
-    }
-    expr_ref mk_or(unsigned sz, expr* const* exprs);
-    expr_ref mk_or(expr_ref_vector const& exprs)
-    {
-        return mk_or(exprs.size(), exprs.c_ptr());
-    }
-
-    expr_ref mk_not_and(expr_ref_vector const& exprs);
-
-    void get_or(expr* e, expr_ref_vector& result);
+    // management of mux names
 
     //"o" predicates stand for the old states and "n" for the new states
     func_decl * get_o_pred(func_decl * s, unsigned idx);
     func_decl * get_n_pred(func_decl * s);
 
-    /**
-       Marks symbol as non-model which means it will not appear in models collected by
-       get_state_cube_from_model function.
-       This is to take care of auxiliary symbols introduced by the disjunction relations
-       to relativize lemmas coming from disjuncts.
-    */
-    void mark_as_non_model(func_decl * p)
-    {
-        m_mux.mark_as_non_model(p);
-    }
-
-
-    func_decl * const * begin_o0_preds() const { return m_o0_preds.begin(); }
-    func_decl * const * end_o0_preds() const { return m_o0_preds.end(); }
-
-    bool is_state_pred(func_decl * p) const { return m_mux.is_muxed(p); }
-    func_decl * to_o0(func_decl * p) { return m_mux.conv(m_mux.get_primary(p), 0, o_index(0)); }
-
-    bool is_o(func_decl * p, unsigned idx) const
-    {
-        return m_mux.has_index(p, o_index(idx));
-    }
-    void get_o_index(func_decl* p, unsigned& idx) const
-    {
+    void get_o_index(func_decl* p, unsigned& idx) const {
         m_mux.try_get_index(p, idx);
         SASSERT(idx != n_index());
         idx--;  // m_mux has indices starting at 1
     }
-    bool is_o(expr* e, unsigned idx) const
-    {
-        return is_app(e) && is_o(to_app(e)->get_decl(), idx);
-    }
-    bool is_o(func_decl * p) const
-    {
+
+    bool is_o(func_decl * p, unsigned idx) const
+    {return m_mux.has_index(p, o_index(idx));}
+    bool is_o(func_decl * p) const {
         unsigned idx;
         return m_mux.try_get_index(p, idx) && idx != n_index();
     }
     bool is_o(expr* e) const
-    {
-        return is_app(e) && is_o(to_app(e)->get_decl());
-    }
+    {return is_app(e) && is_o(to_app(e)->get_decl());}
+    bool is_o(expr* e, unsigned idx) const
+    {return is_app(e) && is_o(to_app(e)->get_decl(), idx);}
     bool is_n(func_decl * p) const
-    {
-        return m_mux.has_index(p, n_index());
-    }
+    {return m_mux.has_index(p, n_index());}
     bool is_n(expr* e) const
-    {
-        return is_app(e) && is_n(to_app(e)->get_decl());
-    }
-
-    /** true if p should not appead in models propagates into child relations */
-    bool is_non_model_sym(func_decl * p) const
-    { return m_mux.is_non_model_sym(p); }
+    {return is_app(e) && is_n(to_app(e)->get_decl());}
 
 
     /** true if f doesn't contain any n predicates */
     bool is_o_formula(expr * f) const
-    {
-        return !m_mux.contains(f, n_index());
-    }
-
+    {return !m_mux.contains(f, n_index());}
     /** true if f contains only o state preds of index o_idx */
     bool is_o_formula(expr * f, unsigned o_idx) const
-    {
-        return m_mux.is_homogenous_formula(f, o_index(o_idx));
-    }
+    {return m_mux.is_homogenous_formula(f, o_index(o_idx));}
     /** true if f doesn't contain any o predicates */
     bool is_n_formula(expr * f) const
-    {
-        return m_mux.is_homogenous_formula(f, n_index());
-    }
+    {return m_mux.is_homogenous_formula(f, n_index());}
 
     func_decl * o2n(func_decl * p, unsigned o_idx) const
-    {
-        return m_mux.conv(p, o_index(o_idx), n_index());
-    }
+    {return m_mux.conv(p, o_index(o_idx), n_index());}
     func_decl * o2o(func_decl * p, unsigned src_idx, unsigned tgt_idx) const
-    {
-        return m_mux.conv(p, o_index(src_idx), o_index(tgt_idx));
-    }
+    {return m_mux.conv(p, o_index(src_idx), o_index(tgt_idx));}
     func_decl * n2o(func_decl * p, unsigned o_idx) const
-    {
-        return m_mux.conv(p, n_index(), o_index(o_idx));
-    }
+    {return m_mux.conv(p, n_index(), o_index(o_idx));}
 
     void formula_o2n(expr * f, expr_ref & result, unsigned o_idx, bool homogenous = true) const
-    { m_mux.conv_formula(f, o_index(o_idx), n_index(), result, homogenous); }
+    {m_mux.conv_formula(f, o_index(o_idx), n_index(), result, homogenous);}
 
     void formula_n2o(expr * f, expr_ref & result, unsigned o_idx, bool homogenous = true) const
-    { m_mux.conv_formula(f, n_index(), o_index(o_idx), result, homogenous); }
+    {m_mux.conv_formula(f, n_index(), o_index(o_idx), result, homogenous);}
 
     void formula_n2o(unsigned o_idx, bool homogenous, expr_ref & result) const
-    { m_mux.conv_formula(result.get(), n_index(), o_index(o_idx), result, homogenous); }
+    {m_mux.conv_formula(result.get(), n_index(), o_index(o_idx), result, homogenous);}
 
-    void formula_o2o(expr * src, expr_ref & tgt, unsigned src_idx, unsigned tgt_idx, bool homogenous = true) const
-    { m_mux.conv_formula(src, o_index(src_idx), o_index(tgt_idx), tgt, homogenous); }
-
-    /**
-       Return true if all state symbols which e contains are of one kind (either "n" or one of "o").
-    */
-    bool is_homogenous_formula(expr * e) const
-    {
-        return m_mux.is_homogenous_formula(e);
-    }
-
-    /**
-        Collect indices used in expression.
-    */
-    void collect_indices(expr* e, unsigned_vector& indices) const
-    {
-        m_mux.collect_indices(e, indices);
-    }
-
-    /**
-        Collect used variables of each index.
-    */
-    void collect_variables(expr* e, vector<ptr_vector<app> >& vars) const
-    {
-        m_mux.collect_variables(e, vars);
-    }
-
-    /**
-       Return true iff both s1 and s2 are either "n" or "o" of the same index.
-       If one (or both) of them are not state symbol, return false.
-    */
-    bool have_different_state_kinds(func_decl * s1, func_decl * s2) const
-    {
-        unsigned i1, i2;
-        return m_mux.try_get_index(s1, i1) && m_mux.try_get_index(s2, i2) && i1 != i2;
-    }
-
-    /**
-       Increase indexes of state symbols in formula by dist.
-       The 'N' index becomes 'O' index with number dist-1.
-    */
-    void formula_shift(expr * src, expr_ref & tgt, unsigned dist) const
-    {
-        SASSERT(n_index() == 0);
-        SASSERT(o_index(0) == 1);
-        m_mux.shift_formula(src, dist, tgt);
-    }
-
-    void mk_model_into_cube(const expr_ref_vector & mdl, expr_ref & res);
-    void mk_core_into_cube(const expr_ref_vector & core, expr_ref & res);
-    void mk_cube_into_lemma(expr * cube, expr_ref & res);
-    void mk_lemma_into_cube(expr * lemma, expr_ref & res);
-
-    /**
-       Remove from vec all atoms that do not have an "o" state.
-       The order of elements in vec may change.
-       An assumption is that atoms having "o" state of given index
-       do not have "o" states of other indexes or "n" states.
-    */
-    void filter_o_atoms(expr_ref_vector& vec, unsigned o_idx) const
-    { m_mux.filter_idx(vec, o_index(o_idx)); }
-    void filter_n_atoms(expr_ref_vector& vec) const
-    { m_mux.filter_idx(vec, n_index()); }
-
-    /**
-       Partition literals into o_lits and others.
-    */
-    void partition_o_atoms(expr_ref_vector const& lits,
-                           expr_ref_vector& o_lits,
-                           expr_ref_vector& other,
-                           unsigned o_idx) const
-    {
-        m_mux.partition_o_idx(lits, o_lits, other, o_index(o_idx));
-    }
-
-    void filter_out_non_model_atoms(expr_ref_vector& vec) const
-    { m_mux.filter_non_model_lits(vec); }
-
-    bool try_get_state_and_value_from_atom(expr * atom, app *& state, app_ref& value);
-    bool try_get_state_decl_from_atom(expr * atom, func_decl *& state);
+    void formula_o2o(expr * src, expr_ref & tgt, unsigned src_idx,
+                     unsigned tgt_idx, bool homogenous = true) const
+    {m_mux.conv_formula(src, o_index(src_idx), o_index(tgt_idx), tgt, homogenous);}
 
 
-    std::string pp_model(const model_core & mdl) const
-    {  return m_mux.pp_model(mdl); }
-
-
-    void set_background(expr* b) { m_background = b; }
-
-    expr* get_background() const { return m_background; }
-
-    unsigned get_unique_num() { return m_next_unique_num++; }
-
+    // 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(); }
     solver* mk_fresh2() {return m_contexts2.mk_fresh();}
@@ -323,32 +163,30 @@ public:
 
 
 
-    void collect_statistics(statistics& st) const
-    {
+    void collect_statistics(statistics& st) const {
         m_contexts.collect_statistics(st);
         m_contexts2.collect_statistics(st);
         m_contexts3.collect_statistics(st);
     }
 
-    void reset_statistics()
-    {
+    void reset_statistics() {
         m_contexts.reset_statistics();
         m_contexts2.reset_statistics();
         m_contexts3.reset_statistics();
     }
 };
 
+/** Skolem constants for quantified spacer */
 app* mk_zk_const (ast_manager &m, unsigned idx, sort *s);
 int find_zk_const(expr* e, app_ref_vector &out);
-inline int find_zk_const(expr_ref_vector const &v, app_ref_vector &out) {
-    return find_zk_const (mk_and(v), out);
-}
+inline int find_zk_const(expr_ref_vector const &v, app_ref_vector &out)
+{return find_zk_const (mk_and(v), out);}
+
 bool has_zk_const(expr* e);
 bool is_zk_const (const app *a, int &n);
 
-struct sk_lt_proc {
-    bool operator()(const app* a1, const app* a2);
-};
+struct sk_lt_proc {bool operator()(const app* a1, const app* a2);};
+
 }
 
 #endif
diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp
index f2fcf5be7..1dd4515a7 100644
--- a/src/muz/spacer/spacer_prop_solver.cpp
+++ b/src/muz/spacer/spacer_prop_solver.cpp
@@ -40,9 +40,9 @@ Revision History:
 
 namespace spacer {
 
-prop_solver::prop_solver(manager& pm, fixedpoint_params const& p, symbol const& name) :
+prop_solver::prop_solver(spacer::manager& pm,
+                         fixedpoint_params const& p, symbol const& name) :
     m(pm.get_manager()),
-    m_pm(pm),
     m_name(name),
     m_ctx(nullptr),
     m_pos_level_atoms(m),
@@ -73,9 +73,6 @@ prop_solver::prop_solver(manager& pm, fixedpoint_params const& p, symbol const&
                           p.spacer_iuc_print_farkas_stats(),
                           p.spacer_iuc_old_hyp_reducer(),
                           p.spacer_iuc_split_farkas_literals());
-
-    for (unsigned i = 0; i < 2; ++i)
-    { m_contexts[i]->assert_expr(m_pm.get_background()); }
 }
 
 void prop_solver::add_level()
diff --git a/src/muz/spacer/spacer_prop_solver.h b/src/muz/spacer/spacer_prop_solver.h
index 12d01ac40..d10ebcfcd 100644
--- a/src/muz/spacer/spacer_prop_solver.h
+++ b/src/muz/spacer/spacer_prop_solver.h
@@ -41,7 +41,6 @@ class prop_solver {
 
 private:
     ast_manager&        m;
-    manager&            m_pm;
     symbol              m_name;
     smt_params*         m_fparams[2];
     solver*             m_solvers[2];
@@ -75,7 +74,8 @@ private:
 
 
 public:
-    prop_solver(spacer::manager& pm, fixedpoint_params const& p, symbol const& name);
+    prop_solver(spacer::manager &manager,
+                fixedpoint_params const& p, symbol const& name);
 
 
     void set_core(expr_ref_vector* core) { m_core = core; }