merge more from csp

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/sat/sat_elim_eqs.cpp

@@ -239,7 +239,7 @@ namespace sat {
             else {
                 model_converter::entry & e = mc.mk(model_converter::ELIM_VAR, v);
                 TRACE("save_elim", tout << "marking as deleted: " << v << " l: " << l << " r: " << r << "\n";);
-                m_solver.m_eliminated[v] = true;
+                m_solver.set_eliminated(v, true);
                 mc.insert(e, ~l, r);
                 mc.insert(e,  l, ~r);
             }

src/smt/smt_kernel.cpp

@@ -156,21 +156,6 @@ namespace smt {
             return m_kernel.get_trail();
         }
         
-        void set_activity(expr* lit, double act) {
-            SASSERT(m().is_bool(lit));
-            m().is_not(lit, lit);
-            if (!m_kernel.b_internalized(lit)) {
-                m_kernel.internalize(lit, false);
-            }
-            if (!m_kernel.b_internalized(lit)) {
-                return;
-            }
-            auto v = m_kernel.get_bool_var(lit);
-            double old_act = m_kernel.get_activity(v);
-            m_kernel.set_activity(v, act);
-            m_kernel.activity_changed(v, act > old_act);
-        }
-        
         failure last_failure() const {
             return m_kernel.get_last_search_failure();
         }
@@ -427,9 +412,5 @@ namespace smt {
         return m_imp->get_trail();
     }
 
-    void kernel::set_activity(expr* lit, double activity) {
-        m_imp->set_activity(lit, activity);
-    }
-
 
 };

src/smt/smt_kernel.h

@@ -229,11 +229,6 @@ namespace smt {
         */
         expr_ref_vector get_trail();
 
-        /**
-           \brief set activity of literal
-        */
-        void set_activity(expr* lit, double activity);
-
         /**
            \brief (For debubbing purposes) Prints the state of the kernel
         */