From 2885ca77148f27fec5cd2710ae1f5d54f0e1f7c5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 19 Feb 2017 11:35:31 -0800
Subject: [PATCH] tune cardinalities

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/card_extension.cpp  | 51 ++++++++++++++++++++++++++++++++++---
 src/sat/sat_solver.cpp      | 22 ++++++++++++++++
 src/sat/sat_solver.h        |  1 +
 src/sat/tactic/goal2sat.cpp |  4 +++
 src/util/uint_set.h         |  7 ++++-
 5 files changed, 81 insertions(+), 4 deletions(-)

diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp
index 8fd0d89a8..b69b0aae5 100644
--- a/src/sat/card_extension.cpp
+++ b/src/sat/card_extension.cpp
@@ -273,8 +273,6 @@ namespace sat {
         reset_coeffs();
         m_num_marks = 0;
         m_bound = 0;
-        m_lemma.reset();        
-        // m_lemma.push_back(null_literal);
         literal consequent = s().m_not_l;
         justification js = s().m_conflict;
         m_conflict_lvl = s().get_max_lvl(consequent, js);
@@ -415,6 +413,51 @@ namespace sat {
             bool_var v = m_active_vars[i];
             slack += get_abs_coeff(v);
         }
+
+        m_lemma.reset();        
+
+#if 1
+        m_lemma.push_back(null_literal);
+        for (unsigned i = 0; 0 <= slack && i < m_active_vars.size(); ++i) { 
+            bool_var v = m_active_vars[i];
+            int coeff = get_coeff(v);
+            lbool val = m_solver->value(v);
+            bool is_true = val == l_true;
+            bool append = coeff != 0 && val != l_undef && (coeff < 0 == is_true);
+
+            if (append) {
+                literal lit(v, !is_true);
+                if (lvl(lit) == m_conflict_lvl) {
+                    if (m_lemma[0] == null_literal) {
+                        slack -= abs(coeff);
+                        m_lemma[0] = ~lit;
+                    }
+                }
+                else {
+                    slack -= abs(coeff);
+                    m_lemma.push_back(~lit);
+                }
+            }
+        }
+
+        if (slack >= 0) {
+            IF_VERBOSE(2, verbose_stream() << "(sat.card bail slack objective not met " << slack << ")\n";);
+            goto bail_out;
+        }
+
+        if (m_lemma[0] == null_literal) {
+            m_lemma[0] = m_lemma.back();
+            m_lemma.pop_back();
+            unsigned level = lvl(m_lemma[0]);
+            for (unsigned i = 1; i < m_lemma.size(); ++i) {
+                if (lvl(m_lemma[i]) > level) {
+                    level = lvl(m_lemma[i]);
+                    std::swap(m_lemma[0], m_lemma[i]);
+                }
+            }
+            IF_VERBOSE(2, verbose_stream() << "(sat.card set level to " << level << " < " << m_conflict_lvl << ")\n";);
+        }        
+#else
         ++idx;
         while (0 <= slack) {            
             literal lit = lits[idx];
@@ -437,13 +480,15 @@ namespace sat {
             SASSERT(idx > 0 || slack < 0);
             --idx;
         }
-
         if (m_lemma.size() >= 2 && lvl(m_lemma[1]) == m_conflict_lvl) {
             // TRACE("sat", tout << "Bail out on no progress " << lit << "\n";);
             IF_VERBOSE(2, verbose_stream() << "(sat.card bail non-asserting resolvent)\n";);
             goto bail_out;
         }
 
+#endif
+
+
         SASSERT(slack < 0);
 
         SASSERT(validate_conflict(m_lemma, m_A));
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 476295f7a..740eea371 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -176,6 +176,28 @@ namespace sat {
         return v;
     }
 
+    void solver::set_external(bool_var v) {
+        if (m_external[v]) return;
+        m_external[v] = true;
+
+        if (!m_ext) return;
+        
+        lbool val = value(v);
+
+        switch (val) {
+        case l_true: {
+            m_ext->asserted(literal(v, false));
+            break;
+        }
+        case l_false: {
+            m_ext->asserted(literal(v, true));
+            break;
+        }
+        default:
+            break;
+        }
+    }
+
     void solver::mk_clause(unsigned num_lits, literal * lits) {
         m_model_is_current = false;
         DEBUG_CODE({
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 37e5f1bb6..9393a8e10 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -227,6 +227,7 @@ namespace sat {
         unsigned num_clauses() const;
         unsigned num_restarts() const { return m_restarts; }
         bool is_external(bool_var v) const { return m_external[v] != 0; }
+        void set_external(bool_var v);
         bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
         unsigned scope_lvl() const { return m_scope_lvl; }
         unsigned search_lvl() const { return m_search_lvl; }
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 1fcaa78b1..87d69b35e 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -378,11 +378,15 @@ struct goal2sat::imp {
         for (unsigned i = 0; i < num_args; ++i) {
             sat::literal lit(m_result_stack[sz - num_args + i]);
             if (!m_solver.is_external(lit.var())) {
+#if 1
+                m_solver.set_external(lit.var());
+#else
                 sat::bool_var w = m_solver.mk_var(true);
                 sat::literal lit2(w, false);
                 mk_clause(lit, ~lit2);
                 mk_clause(~lit, lit2);
                 lit = lit2;
+#endif
             }
             lits.push_back(lit);
         }
diff --git a/src/util/uint_set.h b/src/util/uint_set.h
index 7ff497709..d0cc8a32a 100644
--- a/src/util/uint_set.h
+++ b/src/util/uint_set.h
@@ -304,7 +304,12 @@ public:
     unsigned size() const { return m_set.size(); }
     iterator begin() const { return m_set.begin(); }
     iterator end() const { return m_set.end(); }
-    void reset() { m_set.reset(); m_in_set.reset(); }
+    // void reset() { m_set.reset(); m_in_set.reset(); }
+    void reset() { 
+        unsigned sz = m_set.size();
+        for (unsigned i = 0; i < sz; ++i) m_in_set[m_set[i]] = false;
+        m_set.reset(); 
+    }
     void finalize() { m_set.finalize(); m_in_set.finalize(); }
     tracked_uint_set& operator&=(tracked_uint_set const& other) {
         unsigned j = 0;