add handling of pseudo-boolean inequalities that use if-expressions over Booleans and arihmetic instead of built-in PB predicates

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

src/ast/arith_decl_plugin.h

@@ -264,6 +264,10 @@ public:
     bool is_ge(expr const * n) const { return is_app_of(n, m_afid, OP_GE); }
     bool is_lt(expr const * n) const { return is_app_of(n, m_afid, OP_LT); }
     bool is_gt(expr const * n) const { return is_app_of(n, m_afid, OP_GT); }
+    bool is_le(func_decl const * n) const { return is_decl_of(n, m_afid, OP_LE); }
+    bool is_ge(func_decl const * n) const { return is_decl_of(n, m_afid, OP_GE); }
+    bool is_lt(func_decl const * n) const { return is_decl_of(n, m_afid, OP_LT); }
+    bool is_gt(func_decl const * n) const { return is_decl_of(n, m_afid, OP_GT); }
     bool is_add(expr const * n) const { return is_app_of(n, m_afid, OP_ADD); }
     bool is_sub(expr const * n) const { return is_app_of(n, m_afid, OP_SUB); }
     bool is_uminus(expr const * n) const { return is_app_of(n, m_afid, OP_UMINUS); }

src/ast/rewriter/pb2bv_rewriter.cpp

@@ -79,6 +79,9 @@ struct pb2bv_rewriter::imp {
         pb_util      pb;
         bv_util      bv;
         expr_ref_vector m_trail;
+        expr_ref_vector m_args;
+        rational     m_k;
+        vector<rational> m_coeffs;
 
         template<lbool is_le>
         expr_ref mk_le_ge(expr_ref_vector& fmls, expr* a, expr* b, expr* bound) {
@@ -109,8 +112,22 @@ struct pb2bv_rewriter::imp {
         // The procedure for checking >= k is symmetric and checking for = k is
         // achieved by checking <= k on intermediary addends and the resulting sum is = k.
         // 
+        // is_le = l_true  -  <=
+        // is_le = l_undef -  =
+        // is_le = l_false -  >= 
+        //
         template<lbool is_le>
-        expr_ref mk_le_ge(func_decl *f, unsigned sz, expr * const* args, rational const & k) {
+        expr_ref mk_le_ge(unsigned sz, expr * const* args, rational const & k) {
+            TRACE("pb", 
+                  for (unsigned i = 0; i < sz; ++i) {
+                      tout << m_coeffs[i] << "*" << mk_pp(args[i], m) << " ";
+                  }
+                  switch (is_le) {
+                  case l_true: tout << "<= "; break;
+                  case l_undef: tout << "= "; break;
+                  case l_false: tout << ">= "; break;
+                  }
+                  tout << m_k << "\n";);
             if (k.is_zero()) {
                 if (is_le != l_false) {
                     return expr_ref(m.mk_not(mk_or(m, sz, args)), m);
@@ -119,6 +136,9 @@ struct pb2bv_rewriter::imp {
                     return expr_ref(m.mk_true(), m);
                 }
             }
+            if (k.is_neg()) {
+                return expr_ref((is_le == l_false)?m.mk_true():m.mk_false(), m);
+            }
             SASSERT(k.is_pos());
             expr_ref zero(m), bound(m);
             expr_ref_vector es(m), fmls(m);
@@ -126,7 +146,8 @@ struct pb2bv_rewriter::imp {
             zero = bv.mk_numeral(rational(0), nb);
             bound = bv.mk_numeral(k, nb);
             for (unsigned i = 0; i < sz; ++i) {
-                if (pb.get_coeff(f, i) > k) {
+                SASSERT(!m_coeffs[i].is_neg());
+                if (m_coeffs[i] > k) {
                     if (is_le != l_false) {
                         fmls.push_back(m.mk_not(args[i]));
                     }
@@ -135,7 +156,7 @@ struct pb2bv_rewriter::imp {
                     }
                 }
                 else {
-                    es.push_back(mk_ite(args[i], bv.mk_numeral(pb.get_coeff(f, i), nb), zero));
+                    es.push_back(mk_ite(args[i], bv.mk_numeral(m_coeffs[i], nb), zero));
                 }
             }
             while (es.size() > 1) {
@@ -165,6 +186,10 @@ struct pb2bv_rewriter::imp {
         expr_ref mk_bv(func_decl * f, unsigned sz, expr * const* args) {
             decl_kind kind = f->get_decl_kind();
             rational k = pb.get_k(f);
+            m_coeffs.reset();
+            for (unsigned i = 0; i < sz; ++i) {
+                m_coeffs.push_back(pb.get_coeff(f, i));
+            }
             SASSERT(!k.is_neg());
             switch (kind) {
             case OP_PB_GE:
@@ -173,13 +198,13 @@ struct pb2bv_rewriter::imp {
                 nargs.append(sz, args);
                 dualize(f, nargs, k);
                 SASSERT(!k.is_neg());
-                return mk_le_ge<l_true>(f, sz, nargs.c_ptr(), k);
+                return mk_le_ge<l_true>(sz, nargs.c_ptr(), k);
             }
             case OP_PB_LE:
             case OP_AT_MOST_K:
-                return mk_le_ge<l_true>(f, sz, args, k);
+                return mk_le_ge<l_true>(sz, args, k);
             case OP_PB_EQ:
-                return mk_le_ge<l_undef>(f, sz, args, k);
+                return mk_le_ge<l_undef>(sz, args, k);
             default:
                 UNREACHABLE();
                 return expr_ref(m.mk_true(), m);
@@ -228,7 +253,6 @@ struct pb2bv_rewriter::imp {
             }
         }
 
-
     public:
 
         card2bv_rewriter(imp& i, ast_manager& m):
@@ -238,7 +262,8 @@ struct pb2bv_rewriter::imp {
             pb(m),
             bv(m),
             m_sort(*this),
-            m_trail(m)
+            m_trail(m),
+            m_args(m)
         {}
 
         br_status mk_app_core(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
@@ -247,8 +272,31 @@ struct pb2bv_rewriter::imp {
                 ++m_imp.m_num_translated;
                 return BR_DONE;
             }
-            else if (f->get_family_id() == au.get_family_id() && mk_arith(f, sz, args, result)) {
+            else if (au.is_le(f) && is_pb(args[0], args[1])) {
                 ++m_imp.m_num_translated;
+                result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
+                return BR_DONE;
+            }
+            else if (au.is_lt(f) && is_pb(args[0], args[1])) {
+                ++m_imp.m_num_translated;
+                ++m_k;
+                result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
+                return BR_DONE;
+            }
+            else if (au.is_ge(f) && is_pb(args[1], args[0])) {
+                ++m_imp.m_num_translated;
+                result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
+                return BR_DONE;
+            }
+            else if (au.is_gt(f) && is_pb(args[1], args[0])) {
+                ++m_imp.m_num_translated;
+                ++m_k;
+                result = mk_le_ge<l_true>(m_args.size(), m_args.c_ptr(), m_k);
+                return BR_DONE;
+            }
+            else if (m.is_eq(f) && is_pb(args[0], args[1])) {
+                ++m_imp.m_num_translated;
+                result = mk_le_ge<l_undef>(m_args.size(), m_args.c_ptr(), m_k);
                 return BR_DONE;
             }
             else {
@@ -256,43 +304,75 @@ struct pb2bv_rewriter::imp {
             }
         }
 
-        //
+        bool is_pb(expr* x, expr* y) {
-        // NSB: review
+            m_args.reset();
-        // we should remove this code and rely on a layer above to deal with 
+            m_coeffs.reset();
-        // whatever it accomplishes. It seems to break types.
+            m_k.reset();
-        // 
+            return is_pb(x, rational::one()) && is_pb(y, rational::minus_one());
-        bool mk_arith(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {
+        }
-            if (f->get_decl_kind() == OP_ADD) {
+
-                unsigned bits = 0;
+        bool is_pb(expr* e, rational const& mul) {
-                for (unsigned i = 0; i < sz; i++) {
+            if (!is_app(e)) {
-                    rational val1, val2;
+                return false;
-                    if (au.is_int(args[i]) && au.is_numeral(args[i], val1)) {
+            }
-                        bits += val1.get_num_bits();
+            app* a = to_app(e);
+            rational r, r1, r2;
+            expr* c, *th, *el;
+            unsigned sz = a->get_num_args();
+            if (a->get_family_id() == au.get_family_id()) {
+                switch (a->get_decl_kind()) {
+                case OP_ADD:
+                    for (unsigned i = 0; i < sz; ++i) {
+                        if (!is_pb(a->get_arg(i), mul)) return false;
                     }
-                    else if (m.is_ite(args[i]) &&
+                    return true;
-                             au.is_numeral(to_app(args[i])->get_arg(1), val1) && val1.is_one() &&
+                case OP_SUB: {
-                             au.is_numeral(to_app(args[i])->get_arg(2), val2) && val2.is_zero()) {
+                    if (!is_pb(a->get_arg(0), mul)) return false;
-                        bits++;                        
+                    r = -mul;
+                    for (unsigned i = 1; i < sz; ++i) {
+                        if (!is_pb(a->get_arg(1), r)) return false;
                     }
-                    else
+                    return true;
-                        return false;
+                }
+                case OP_UMINUS:
+                    return is_pb(a->get_arg(0), -mul);
+                case OP_NUM:
+                    VERIFY(au.is_numeral(a, r));
+                    m_k += mul * r;
+                    return true;
+                case OP_MUL:
+                    if (sz != 2) {
+                        return false;
+                    }
+                    if (au.is_numeral(a->get_arg(0), r)) {
+                        r *= mul;
+                        return is_pb(a->get_arg(1), r);
+                    }
+                    if (au.is_numeral(a->get_arg(1), r)) {
+                        r *= mul;
+                        return is_pb(a->get_arg(0), r);
+                    }
+                    return false;
+                default:
+                    return false;
+                }
+            }
+            if (m.is_ite(a, c, th, el) && au.is_numeral(th, r1) && au.is_numeral(el, r2)) {
+                r1 *= mul;
+                r2 *= mul;
+                if (r1 < r2) {
+                    m_args.push_back(::mk_not(m, c));
+                    m_coeffs.push_back(r2-r1);
+                    m_k -= r1;
+                }
+                else {
+                    m_args.push_back(c);
+                    m_coeffs.push_back(r1-r2);
+                    m_k -= r2;
                 }
-                
-                result = 0;
-                for (unsigned i = 0; i < sz; i++) {
-                    rational val1, val2;
-                    expr * q;
-                    if (au.is_int(args[i]) && au.is_numeral(args[i], val1))
-                        q = bv.mk_numeral(val1, bits);
-                    else
-                        q = mk_ite(to_app(args[i])->get_arg(0), bv.mk_numeral(1, bits), bv.mk_numeral(0, bits));
-                    result = (i == 0) ? q : bv.mk_bv_add(result.get(), q);
-                }                
                 return true;
             }
-            else {
+            return false;
-                return false;
-            } 
         }
 
         void mk_pb(func_decl * f, unsigned sz, expr * const* args, expr_ref & result) {

src/tactic/portfolio/enum2bv_solver.cpp

@@ -115,8 +115,6 @@ public:
             }
         }
         lbool r = m_solver->get_consequences(asms, bvars, consequences);
-        std::cout << consequences.size() << "\n";
-
 
         // translate bit-vector consequences back to enumeration types
         for (unsigned i = 0; i < consequences.size(); ++i) {