remove dead (and incorrect) code

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

src/sat/sat_solver.cpp

@@ -3151,7 +3151,7 @@ namespace sat {
 
     lbool solver::get_consequences(literal_vector const& asms, literal_vector const& lits, vector<literal_vector>& conseq) {
         m_antecedents.reset();
-        literal_set unfixed(lits), assumptions(asms);
+        literal_set vars(lits), assumptions(asms);
 
         pop_to_base_level();
         if (inconsistent()) return l_false;
@@ -3162,11 +3162,12 @@ namespace sat {
         propagate(false);
         if (check_inconsistent()) return l_false;
        
-        unsigned num_units = 0;
+        unsigned num_units = 0, num_iterations = 0;
-        extract_fixed_consequences(num_units, assumptions, unfixed, conseq);
+        extract_fixed_consequences(num_units, assumptions, vars, conseq);
-        while (!unfixed.empty()) {
+        while (!vars.empty()) {
+            ++num_iterations;
             checkpoint();
-            literal_set::iterator it = unfixed.begin(), end = unfixed.end();
+            literal_set::iterator it = vars.begin(), end = vars.end();
             for (; it != end; ++it) {
                 literal lit = *it;
                 if (value(lit) != l_undef) {
@@ -3197,9 +3198,16 @@ namespace sat {
                 m_inconsistent = false;
             }
             if (is_sat == l_true) {
-                delete_unfixed(unfixed);
+                delete_unfixed(vars);
             }
-            extract_fixed_consequences(num_units, assumptions, unfixed, conseq);            
+            extract_fixed_consequences(num_units, assumptions, vars, conseq);            
+            IF_VERBOSE(1, verbose_stream() << "(get-consequences"
+                       << " iterations: " << num_iterations
+                       << " variables: " << vars.size()
+                       << " fixed: " << conseq.size()
+                       << " unfixed: " << lits.size() - conseq.size() - vars.size()
+                       << ")\n";);
+
         }
         return l_true;
     }

src/solver/mus.cpp

@@ -239,6 +239,17 @@ struct mus::imp {
         return l_false;
     }
 
+    void get_core(expr_set& core) {
+        core.reset();
+        ptr_vector<expr> core_exprs;
+        m_solver.get_unsat_core(core_exprs);
+        for (unsigned i = 0; i < core_exprs.size(); ++i) {
+            if (m_expr2lit.contains(core_exprs[i])) {
+                core.insert(core_exprs[i]);
+            }
+        }
+    }
+
     bool have_intersection(expr_set const& A, expr_set const& B) {
         if (A.size() < B.size()) {
             expr_set::iterator it = A.begin(), end = A.end();
@@ -345,110 +356,6 @@ struct mus::imp {
         return m_weight;
     }
 
-
-    lbool qx(expr_ref_vector& mus) {
-        expr_set core, support;
-        for (unsigned i = 0; i < m_lit2expr.size(); ++i) {
-            core.insert(m_lit2expr[i].get());
-        }
-        lbool is_sat = qx(core, support, false);
-        if (is_sat == l_true) {
-            expr_set::iterator it = core.begin(), end = core.end();
-            mus.reset();
-            for (; it != end; ++it) {
-                mus.push_back(*it);
-            }
-        }
-        return is_sat;
-    }
-
-    lbool qx(expr_set& assignment, expr_set& support, bool has_support) {
-        lbool is_sat = l_true;
-#if 0
-        if (s.m_config.m_minimize_core_partial && s.m_stats.m_restart - m_restart > m_max_restarts) {
-            IF_VERBOSE(1, verbose_stream() << "(sat restart budget exceeded)\n";);
-            return l_true;
-        }
-#endif
-        if (has_support) {
-            expr_ref_vector asms(m);
-            scoped_append _sa1(*this, asms, support);
-            scoped_append _sa2(*this, asms, m_assumptions);
-            is_sat = m_solver.check_sat(asms);
-            switch (is_sat) {
-            case l_false: {
-                expr_set core; 
-                get_core(core);
-                support &= core;
-                assignment.reset();
-                return l_true;
-            }
-            case l_undef:
-                return l_undef;
-            case l_true:
-                update_model();
-                break;
-            default:
-                break;
-            }
-        }
-        if (assignment.size() == 1) {
-            return l_true;
-        }
-        expr_set assign2;
-        split(assignment, assign2);
-        support |= assignment;
-        is_sat = qx(assign2, support, !assignment.empty());        
-        unsplit(support, assignment);
-        if (is_sat != l_true) return is_sat;
-        support |= assign2;
-        is_sat = qx(assignment, support, !assign2.empty());
-        assignment |= assign2;
-        unsplit(support, assign2);
-        return is_sat;
-    }
-
-    void get_core(expr_set& core) {
-        core.reset();
-        ptr_vector<expr> core_exprs;
-        m_solver.get_unsat_core(core_exprs);
-        for (unsigned i = 0; i < core_exprs.size(); ++i) {
-            if (m_expr2lit.contains(core_exprs[i])) {
-                core.insert(core_exprs[i]);
-            }
-        }
-    }
-
-    void unsplit(expr_set& A, expr_set& B) {
-        expr_set A1, B1;
-        expr_set::iterator it = A.begin(), end = A.end();
-        for (; it != end; ++it) {
-            if (B.contains(*it)) {
-                B1.insert(*it);
-            }
-            else {
-                A1.insert(*it);
-            }
-        }
-        A = A1;
-        B = B1;
-    }
-
-    void split(expr_set& lits1, expr_set& lits2) {
-        unsigned half = lits1.size()/2;
-        expr_set lits3;
-        expr_set::iterator it = lits1.begin(), end = lits1.end();
-        for (unsigned i = 0; it != end; ++it, ++i) {
-            if (i < half) {
-                lits3.insert(*it);
-            }
-            else {
-                lits2.insert(*it);
-            }
-        }
-        lits1 = lits3;
-    }
-
 };
 
 mus::mus(solver& s) {