fix rounding mode for pseudo-boolean constraint creation, Issue #683

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

src/ast/pb_decl_plugin.cpp

@@ -18,6 +18,7 @@ Revision History:
 --*/
 
 #include "pb_decl_plugin.h"
+#include "ast_util.h"
 
 pb_decl_plugin::pb_decl_plugin():
     m_at_most_sym("at-most"),
@@ -99,29 +100,47 @@ void pb_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
     }
 }
 
-app * pb_util::mk_le(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k) {
+void pb_util::normalize(unsigned num_args, rational const* coeffs, rational const& k) {
-    vector<parameter> params;
+    rational d(1);
-    params.push_back(parameter(k));
     for (unsigned i = 0; i < num_args; ++i) {
-        params.push_back(parameter(coeffs[i]));
+        d = lcm(d, denominator(coeffs[i]));
+    }
+    m_coeffs.reset();
+    for (unsigned i = 0; i < num_args; ++i) {
+        m_coeffs.push_back(d*coeffs[i]);
+    }
+    m_k = d*k;
+}
+
+app * pb_util::mk_le(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k) {
+    normalize(num_args, coeffs, k);
+    vector<parameter> params;
+    params.push_back(parameter(floor(m_k)));
+    for (unsigned i = 0; i < num_args; ++i) {
+        params.push_back(parameter(m_coeffs[i]));
     }
     return m.mk_app(m_fid, OP_PB_LE, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
 }
 
 app * pb_util::mk_ge(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k) {
+    normalize(num_args, coeffs, k);
     vector<parameter> params;
-    params.push_back(parameter(k));
+    params.push_back(parameter(ceil(m_k)));
     for (unsigned i = 0; i < num_args; ++i) {
-        params.push_back(parameter(coeffs[i]));
+        params.push_back(parameter(m_coeffs[i]));
     }
     return m.mk_app(m_fid, OP_PB_GE, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
 }
 
 app * pb_util::mk_eq(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k) {
+    normalize(num_args, coeffs, k);
+    if (!m_k.is_int()) {
+        return m.mk_false();
+    }
     vector<parameter> params;
-    params.push_back(parameter(k));
+    params.push_back(parameter(m_k));
     for (unsigned i = 0; i < num_args; ++i) {
-        params.push_back(parameter(coeffs[i]));
+        params.push_back(parameter(m_coeffs[i]));
     }
     return m.mk_app(m_fid, OP_PB_EQ, params.size(), params.c_ptr(), num_args, args, m.mk_bool_sort());
 }
@@ -132,33 +151,18 @@ app * pb_util::mk_eq(unsigned num_args, rational const * coeffs, expr * const *
 // <=>
 // a(1-x) + b(1-y) >= -k + a + b + 1
 app * pb_util::mk_lt(unsigned num_args, rational const * _coeffs, expr * const * _args, rational const& _k) {
-    vector<rational> coeffs;
+    normalize(num_args, _coeffs, _k);
-    rational k(_k);
     expr_ref_vector args(m);
-    expr* f;
-    rational d(denominator(k));
     for (unsigned i = 0; i < num_args; ++i) {
-        coeffs.push_back(_coeffs[i]);
+        args.push_back(mk_not(m, _args[i]));
-        d = lcm(d, denominator(coeffs[i]));
-        if (m.is_not(_args[i], f)) {
-            args.push_back(f);
     }
-        else {
+    m_k = floor(m_k);
-            args.push_back(m.mk_not(_args[i]));
+    m_k.neg();
-        }
+    m_k += rational::one();
-    }
-    if (!d.is_one()) {
-        k *= d;
     for (unsigned i = 0; i < num_args; ++i) {
-            coeffs[i] *= d;        
+        m_k += m_coeffs[i];
     }
-    }
+    return mk_ge(num_args, m_coeffs.c_ptr(), args.c_ptr(), m_k);
-    k.neg();
-    k += rational::one();
-    for (unsigned i = 0; i < num_args; ++i) {
-        k += coeffs[i];
-    }
-    return mk_ge(num_args, coeffs.c_ptr(), args.c_ptr(), k);
 }
 
 

src/ast/pb_decl_plugin.h

@@ -79,6 +79,9 @@ public:
 class pb_util {
     ast_manager & m;
     family_id     m_fid;
+    vector<rational> m_coeffs;
+    rational         m_k;
+    void normalize(unsigned num_args, rational const* coeffs, rational const& k);
 public:
     pb_util(ast_manager& m):m(m), m_fid(m.mk_family_id("pb")) {}
     ast_manager & get_manager() const { return m; }

src/opt/opt_context.cpp

@@ -241,6 +241,7 @@ namespace opt {
             s.get_labels(m_labels);
         }
         if (is_sat != l_true) {
+            TRACE("opt", tout << m_hard_constraints << "\n";);
             return is_sat;
         }
         IF_VERBOSE(1, verbose_stream() << "(optimize:sat)\n";);
@@ -415,7 +416,7 @@ namespace opt {
     
     expr_ref context::mk_gt(unsigned i, model_ref& mdl) {
         expr_ref result = mk_le(i, mdl);
-        result = m.mk_not(result);
+        result = mk_not(m, result);
         return result;
     }
 
@@ -776,7 +777,7 @@ namespace opt {
                     weights[i].neg();
                 }
                 else {
-                    terms[i] = m.mk_not(terms[i].get());
+                    terms[i] = mk_not(m, terms[i].get());
                 }
             }
             TRACE("opt", 
@@ -805,7 +806,7 @@ namespace opt {
             for (unsigned i = 0; i < weights.size(); ++i) {
                 if (weights[i].is_neg()) {
                     weights[i].neg();
-                    terms[i] = m.mk_not(terms[i].get());
+                    terms[i] = mk_not(m, terms[i].get());
                 }
                 offset += weights[i];
             }