bug fixes

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

src/ast/rewriter/pb2bv_rewriter.cpp

@@ -54,6 +54,8 @@ struct pb2bv_rewriter::imp {
         vector<rational> m_coeffs;
         bool m_keep_cardinality_constraints;
         bool m_keep_pb_constraints;
+        bool m_pb_num_system;
+        bool m_pb_totalizer;
         unsigned m_min_arity;
 
         template<lbool is_le>
@@ -114,23 +116,24 @@ struct pb2bv_rewriter::imp {
                 return expr_ref((is_le == l_false)?m.mk_true():m.mk_false(), m);
             }
 
-#if 0
+            if (m_pb_totalizer) {
-            expr_ref result(m);
+                expr_ref result(m);
-            switch (is_le) {
+                switch (is_le) {
-            case l_true:  if (mk_le_tot(sz, args, k, result)) return result; else break;
+                case l_true:  if (mk_le_tot(sz, args, k, result)) return result; else break;
-            case l_false: if (mk_ge_tot(sz, args, k, result)) return result; else break;
+                case l_false: if (mk_ge_tot(sz, args, k, result)) return result; else break;
-            case l_undef: break;
+                case l_undef: break;
+                }
             }
-#endif
             
-#if 0
+            if (m_pb_num_system) {
-            expr_ref result(m);
+                expr_ref result(m);
-            switch (is_le) {
+                switch (is_le) {
-            case l_true:  if (mk_le(sz, args, k, result)) return result; else break;
+                case l_true:  if (mk_le(sz, args, k, result)) return result; else break;
-            case l_false: if (mk_ge(sz, args, k, result)) return result; else break;
+                case l_false: if (mk_ge(sz, args, k, result)) return result; else break;
-            case l_undef: if (mk_eq(sz, args, k, result)) return result; else break;
+                case l_undef: if (mk_eq(sz, args, k, result)) return result; else break;
+                }
             }
-#endif
+
             // fall back to divide and conquer encoding.
             SASSERT(k.is_pos());
             expr_ref zero(m), bound(m);
@@ -397,22 +400,30 @@ struct pb2bv_rewriter::imp {
             for (unsigned j = 0; j + lim - 1 < out.size(); j += n) {
                 expr_ref tmp(m);
                 tmp = out[j + lim - 1];
-                if (j + n < out.size()) {
+                if (j + n - 1 < out.size()) {
-                    tmp = m.mk_and(tmp, m.mk_not(out[j + n]));
+                    tmp = m.mk_and(tmp, m.mk_not(out[j + n - 1]));
                 }
                 ors.push_back(tmp);
             }
             return ::mk_or(ors);
         }
 
+        // x0 + 5x1 + 3x2 >= k
+        // x0 x1 x1 -> s0 s1 s2
+        // s2 x1 x2 -> s3 s4 s5
+        // k = 7: s5 or (s4 & not s2 & s0)
+        // k = 6: s4
+        // k = 5: s4 or (s3 & not s2 & s1)
+        // k = 4: s4 or (s3 & not s2 & s0)
+        // k = 3: s3
+        // 
         bool mk_ge(unsigned sz, expr * const* args, rational bound, expr_ref& result) {
             if (!create_basis()) return false;
             if (!bound.is_unsigned()) return false;
             vector<rational> coeffs(m_coeffs);
             result = m.mk_true();
             expr_ref_vector carry(m), new_carry(m);
-            for (unsigned i = 0; i < m_base.size(); ++i) {
+            for (rational b_i : m_base) {
-                rational b_i = m_base[i];
                 unsigned B   = b_i.get_unsigned();
                 unsigned d_i = (bound % b_i).get_unsigned();
                 bound = div(bound, b_i);                
@@ -425,7 +436,7 @@ struct pb2bv_rewriter::imp {
                     coeffs[j] = div(coeffs[j], b_i);
                 }
                 TRACE("pb", tout << "Carry: " << carry << "\n";
-                      for (unsigned j = 0; j < coeffs.size(); ++j) tout << coeffs[j] << " ";
+                      for (auto c : coeffs) tout << c << " ";
                       tout << "\n";
                       );
                 ptr_vector<expr> out;
@@ -434,7 +445,7 @@ struct pb2bv_rewriter::imp {
                 expr_ref gt = mod_ge(out, B, d_i + 1);
                 expr_ref ge = mod_ge(out, B, d_i);
                 result = mk_or(gt, mk_and(ge, result));                
-                TRACE("pb", tout << result << "\n";);
+                TRACE("pb", tout << "b: " << b_i << " d: " << d_i << " gt: " << gt << " ge: " << ge << " " << result << "\n";);
 
                 new_carry.reset();
                 for (unsigned j = B - 1; j < out.size(); j += B) {
@@ -443,7 +454,10 @@ struct pb2bv_rewriter::imp {
                 carry.reset();
                 carry.append(new_carry);
             }
-            TRACE("pb", tout << result << "\n";);
+            if (!carry.empty()) {
+                result = m.mk_or(result, carry[0].get());
+            }
+            TRACE("pb", tout << "Carry: " << carry << " result: " << result << "\n";);
             return true;
         }
 
@@ -567,6 +581,8 @@ struct pb2bv_rewriter::imp {
             m_args(m),
             m_keep_cardinality_constraints(false),
             m_keep_pb_constraints(false),
+            m_pb_num_system(false),
+            m_pb_totalizer(false),
             m_min_arity(2)
         {}
 
@@ -761,6 +777,14 @@ struct pb2bv_rewriter::imp {
         void keep_pb_constraints(bool f) {
             m_keep_pb_constraints = f;
         }
+
+        void pb_num_system(bool f) {
+            m_pb_num_system = f;
+        }
+
+        void pb_totalizer(bool f) {
+            m_pb_totalizer = f;
+        }
     };
 
     struct card2bv_rewriter_cfg : public default_rewriter_cfg {
@@ -774,6 +798,8 @@ struct pb2bv_rewriter::imp {
         card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {}
         void keep_cardinality_constraints(bool f) { m_r.keep_cardinality_constraints(f); }
         void keep_pb_constraints(bool f) { m_r.keep_pb_constraints(f); }
+        void pb_num_system(bool f) { m_r.pb_num_system(f); }
+        void pb_totalizer(bool f) { m_r.pb_totalizer(f); }
     };
     
     class card_pb_rewriter : public rewriter_tpl<card2bv_rewriter_cfg> {
@@ -784,27 +810,59 @@ struct pb2bv_rewriter::imp {
             m_cfg(i, m) {}
         void keep_cardinality_constraints(bool f) { m_cfg.keep_cardinality_constraints(f); }
         void keep_pb_constraints(bool f) { m_cfg.keep_pb_constraints(f); }
+        void pb_num_system(bool f) { m_cfg.pb_num_system(f); }
+        void pb_totalizer(bool f) { m_cfg.pb_totalizer(f); }
     };
 
     card_pb_rewriter m_rw;
     
+    bool keep_cardinality() const {
+        params_ref const& p = m_params;
+        return 
+            p.get_bool("keep_cardinality_constraints", false) ||
+            p.get_bool("sat.cardinality.solver", false) ||
+            p.get_bool("cardinality.solver", false) || keep_pb();
+    }
+
+    bool keep_pb() const {
+        params_ref const& p = m_params;
+        return 
+            p.get_bool("keep_pb_constraints", false) ||
+            p.get_bool("sat.pb.solver", false) ||
+            p.get_bool("pb.solver", false);
+    }
+
+    bool pb_num_system() const {
+        return m_params.get_bool("pb_num_system", false);
+    }
+
+    bool pb_totalizer() const {
+        return m_params.get_bool("pb_totalizer", false);
+    }
+
     imp(ast_manager& m, params_ref const& p): 
         m(m), m_params(p), m_lemmas(m),
         m_fresh(m),
         m_num_translated(0), 
         m_rw(*this, m) {
-        m_rw.keep_cardinality_constraints(p.get_bool("keep_cardinality_constraints", false));
+        m_rw.keep_cardinality_constraints(keep_cardinality());
-        m_rw.keep_pb_constraints(p.get_bool("keep_pb_constraints", false));
+        m_rw.keep_pb_constraints(keep_pb());
+        m_rw.pb_num_system(pb_num_system());
+        m_rw.pb_totalizer(pb_totalizer());
     }
 
     void updt_params(params_ref const & p) {
         m_params.append(p);
-        m_rw.keep_cardinality_constraints(m_params.get_bool("keep_cardinality_constraints", false));
+        m_rw.keep_cardinality_constraints(keep_cardinality());
-        m_rw.keep_pb_constraints(m_params.get_bool("keep_pb_constraints", false));
+        m_rw.keep_pb_constraints(keep_pb());
+        m_rw.pb_num_system(pb_num_system());
+        m_rw.pb_totalizer(pb_totalizer());
     }
     void collect_param_descrs(param_descrs& r) const {
         r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints (don't bit-blast them) and use built-in cardinality solver");
         r.insert("keep_pb_constraints", CPK_BOOL, "(default: true) retain pb constraints (don't bit-blast them) and use built-in pb solver");
+        r.insert("pb_num_system", CPK_BOOL, "(default: false) use pb number system encoding");
+        r.insert("pb_totalizer", CPK_BOOL, "(default: false) use pb totalizer encoding");
     }
 
     unsigned get_num_steps() const { return m_rw.get_num_steps(); }

src/sat/card_extension.cpp

@@ -250,7 +250,7 @@ namespace sat {
                     p.swap(i, j);
                 }
                 if (slack < bound) {
-                    slack += p[i].first;
+                    slack += p[j].first;
                     ++num_watch;
                 }
                 ++j;
@@ -267,7 +267,7 @@ namespace sat {
         if (slack < bound) {
             literal lit = p[j].second;
             SASSERT(value(p[j].second) == l_false);
-            for (unsigned i = j + 1; j < sz; ++i) {
+            for (unsigned i = j + 1; i < sz; ++i) {
                 if (lvl(lit) < lvl(p[i].second)) {
                     lit = p[i].second;
                 }
@@ -386,13 +386,21 @@ namespace sat {
         p.swap(num_watch, index);
 
         if (slack < bound + m_a_max) {
-            while (!s().inconsistent() && !m_pb_undef.empty()) {
+            TRACE("sat", display(tout, p, false); for(auto j : m_pb_undef) tout << j << "\n";);
+            literal_vector to_assign;
+            while (!m_pb_undef.empty()) {
                 index1 = m_pb_undef.back();
                 literal lit = p[index1].second;
+                TRACE("sat", tout << index1 << " " << lit << "\n";);
                 if (slack >= bound + p[index1].first) {
                     break;
                 }
                 m_pb_undef.pop_back();
+                to_assign.push_back(lit);
+            }
+
+            for (literal lit : to_assign) {
+                if (s().inconsistent()) break;
                 if (value(lit) == l_undef) {
                     assign(p, lit);
                 }				
@@ -474,7 +482,8 @@ namespace sat {
     }
 
     void card_extension::display(std::ostream& out, pb const& p, bool values) const {
-        out << p.lit() << "[ watch: " << p.num_watch() << ", slack: " << p.slack() << "]";
+        if (p.lit() != null_literal) out << p.lit();
+        out << "[watch: " << p.num_watch() << ", slack: " << p.slack() << "]";
         if (p.lit() != null_literal && values) {
             out << "@(" << value(p.lit());
             if (value(p.lit()) != l_undef) {
@@ -1350,7 +1359,25 @@ namespace sat {
         if (p.lit() != null_literal) r.push_back(p.lit());
         SASSERT(p.lit() == null_literal || value(p.lit()) == l_true);
         TRACE("sat", display(tout, p, true););
-        for (unsigned i = p.num_watch(); i < p.size(); ++i) {
+
+        // unsigned coeff = get_coeff(p, l);
+        unsigned coeff = 0;
+        for (unsigned j = 0; j < p.num_watch(); ++j) {
+            if (p[j].second == l) {
+                coeff = p[j].first;
+                break;
+            }
+        }
+        unsigned slack = p.slack() - coeff;
+        unsigned i = p.num_watch();
+
+        // skip entries that are not required for unit propagation.
+        // slack - coeff + w_head < k
+        unsigned h = 0;
+        for (; i < p.size() && p[i].first + h + slack < p.k(); ++i) { 
+            h += p[i].first;
+        }
+        for (; i < p.size(); ++i) {
             literal lit = p[i].second;
             SASSERT(l_false == value(lit));
             r.push_back(~lit);
@@ -1714,7 +1741,9 @@ namespace sat {
     std::ostream& card_extension::display_justification(std::ostream& out, ext_justification_idx idx) const {
         if (is_card_index(idx)) {
             card& c = index2card(idx);
-            out << "bound " << c.lit() << ": ";
+            out << "bound ";
+            if (c.lit() != null_literal) out << c.lit();
+            out << ": ";
             for (unsigned i = 0; i < c.size(); ++i) {
                 out << c[i] << " ";
             }
@@ -1722,14 +1751,18 @@ namespace sat {
         }
         else if (is_xor_index(idx)) {
             xor& x = index2xor(idx);
-            out << "xor " << x.lit() << ": ";
+            out << "xor ";
+            if (x.lit() != null_literal) out << x.lit();
+            out << ": ";
             for (unsigned i = 0; i < x.size(); ++i) {
                 out << x[i] << " ";
             }            
         }
         else if (is_pb_index(idx)) {
             pb& p = index2pb(idx);
-            out << "pb " << p.lit() << ": ";
+            out << "pb ";
+            if (p.lit() != null_literal) out << p.lit();
+            out << ": ";
             for (unsigned i = 0; i < p.size(); ++i) {
                 out << p[i].first << "*" << p[i].second << " ";
             }
@@ -1773,26 +1806,16 @@ namespace sat {
     bool card_extension::validate_unit_propagation(pb const& p, literal alit) { 
         if (p.lit() != null_literal && value(p.lit()) != l_true) return false;
 
-        unsigned k = p.k();
         unsigned sum = 0;
-        unsigned a_min = 0;
         TRACE("sat", display(tout << "validate: " << alit << "\n", p, true););
         for (unsigned i = 0; i < p.size(); ++i) {
             literal lit = p[i].second;
             lbool val = value(lit);
-            if (val == l_false) {
+            if (val != l_false && lit != alit) {
-                // no-op
-            }
-            else if (lit == alit) {
-                a_min = p[i].first;
-                sum += p[i].first;
-            }
-            else {
                 sum += p[i].first;
             }
         }
-        return sum < k + a_min;
+        return sum < p.k();
-        return true;
     }
 
     bool card_extension::validate_lemma() { 

src/tactic/portfolio/pb2bv_solver.cpp

@@ -20,6 +20,7 @@ Notes:
 #include "solver_na2as.h"
 #include "tactic.h"
 #include "pb2bv_rewriter.h"
+#include "th_rewriter.h"
 #include "filter_model_converter.h"
 #include "ast_pp.h"
 #include "model_smt2_pp.h"
@@ -29,6 +30,7 @@ class pb2bv_solver : public solver_na2as {
     params_ref       m_params;
     mutable expr_ref_vector  m_assertions;
     mutable ref<solver>      m_solver;
+    mutable th_rewriter      m_th_rewriter;
     mutable pb2bv_rewriter   m_rewriter;
 
 public:
@@ -39,6 +41,7 @@ public:
         m_params(p),
         m_assertions(m),
         m_solver(s),
+        m_th_rewriter(m, p),
         m_rewriter(m, p)
     {
     }
@@ -121,10 +124,11 @@ public:
 private:
     void flush_assertions() const {
         proof_ref proof(m);
-        expr_ref fml(m);
+        expr_ref fml1(m), fml(m);
         expr_ref_vector fmls(m);
         for (unsigned i = 0; i < m_assertions.size(); ++i) {
-            m_rewriter(m_assertions[i].get(), fml, proof);
+            m_th_rewriter(m_assertions[i].get(), fml1, proof);
+            m_rewriter(fml1, fml, proof);
             m_solver->assert_expr(fml);
         }
         m_rewriter.flush_side_constraints(fmls);