#8552

make it recompile constraints with duplicates

src/sat/smt/pb_pb.h

@@ -34,6 +34,7 @@ namespace pb {
         literal lit() const { return m_lit; }
         wliteral operator[](unsigned i) const { return m_wlits[i]; }
         wliteral& operator[](unsigned i) { return m_wlits[i]; }
+        wliteral *data() { return m_wlits; }
         wliteral const* begin() const { return m_wlits; }
         wliteral const* end() const { return begin() + m_size; }
 

src/sat/smt/pb_solver.cpp

@@ -397,19 +397,17 @@ namespace pb {
         return l_undef;
     }
 
-    void solver::recompile(pbc& p) {
+    std::pair<unsigned, unsigned> solver::normalize(wliteral* begin, wliteral* end, unsigned k) {
-        // IF_VERBOSE(2, verbose_stream() << "re: " << p << "\n";);
         SASSERT(p.num_watch() == 0);
-        m_weights.resize(2*s().num_vars(), 0);
+        m_weights.resize(2 * s().num_vars(), 0);
-        for (auto [w, lit] : p) {
+        for (auto it = begin; it != end; ++it) {
+            auto [w, lit] = *it;        
             m_weights[lit.index()] += w;
         }        
-        unsigned k = p.k();
+        auto j = begin;
-        unsigned sz = p.size();
+        unsigned sz = 0;
-        bool all_units = true;
+        for (auto it = begin; it != end; ++it) {
-        unsigned j = 0;
+            auto [w, l] = *it;
-        for (unsigned i = 0; i < sz && 0 < k; ++i) {
-            auto [w, l] = p[i];
             unsigned w1 = m_weights[l.index()];
             unsigned w2 = m_weights[(~l).index()];
             if (w1 == 0 || w1 < w2) {
@@ -429,18 +427,28 @@ namespace pb {
                     continue;
                 }
                 else {
-                    p[j] = wliteral(w1, l);            
+                    *j = wliteral(w1, l);
-                    all_units &= w1 == 1;
                     ++j;
+                    ++sz;
                 }
             }
         }
-        sz = j;
         // clear weights
-        for (auto [w, lit] : p) {
+        while (begin != end) {
-            m_weights[lit.index()] = 0;
+            auto [w, l] = *begin;
-            m_weights[(~lit).index()] = 0;
+            m_weights[l.index()] = 0;
+            m_weights[(~l).index()] = 0;
+            ++begin;
         }
+        return {sz, k};
+    }
+
+    void solver::recompile(pbc& p) {
+        // IF_VERBOSE(2, verbose_stream() << "re: " << p << "\n";);
+
+        auto [sz, k] = normalize(p.data(), p.data() + p.size(), p.k());
+        p.set_size(sz);
+        auto all_units = all_of(p, [](wliteral const& wl) { return wl.first == 1; });
 
         if (k == 0) {
             if (p.lit() != sat::null_literal) {
@@ -464,7 +472,6 @@ namespace pb {
             return;
         }
         else {            
-            p.set_size(sz);
             p.update_max_sum();
             if (p.max_sum() < k) {
                 if (p.lit() == sat::null_literal) {
@@ -1463,7 +1470,10 @@ namespace pb {
         for (auto const&[w, l] : wlits) {
             auto v = l.var();
             if (is_visited(v)) {
-                throw default_exception("malformed constraint: variable appears more than once - is pre-processing disabled?");
+                svector<wliteral> wlits2(wlits);
+                auto [sz, k2] = normalize(wlits2.data(), wlits2.data() + wlits2.size(), k);
+                wlits2.shrink(sz);
+                return add_pb_ge(lit, wlits2, k2, learned);
             }
             mark_visited(v);
         }

src/sat/smt/pb_solver.h

@@ -235,6 +235,7 @@ namespace pb {
         void simplify(constraint& p);
         void simplify2(pbc& p);
         bool is_cardinality(pbc const& p);
+        std::pair<unsigned, unsigned> normalize(wliteral *begin, wliteral *end, unsigned k);
         void flush_roots(pbc& p);
         void recompile(pbc& p);
         bool clausify(pbc& p);