From 4f5b0667ef387b18d73c0cb10c4b9d19ebb09dc4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Jul 2016 12:34:18 -0700 Subject: [PATCH] fix rounding mode for pseudo-boolean constraint creation, Issue #683 Signed-off-by: Nikolaj Bjorner --- src/ast/pb_decl_plugin.cpp | 64 ++++++++++++++++++++------------------ src/ast/pb_decl_plugin.h | 3 ++ src/opt/opt_context.cpp | 7 +++-- 3 files changed, 41 insertions(+), 33 deletions(-) diff --git a/src/ast/pb_decl_plugin.cpp b/src/ast/pb_decl_plugin.cpp index f4e3fdf97..e87bc15ac 100644 --- a/src/ast/pb_decl_plugin.cpp +++ b/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 & op_names, symbol const } } -app * pb_util::mk_le(unsigned num_args, rational const * coeffs, expr * const * args, rational const& k) { - vector params; - params.push_back(parameter(k)); +void pb_util::normalize(unsigned num_args, rational const* coeffs, rational const& k) { + rational d(1); 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 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 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 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 coeffs; - rational k(_k); + normalize(num_args, _coeffs, _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]); - d = lcm(d, denominator(coeffs[i])); - if (m.is_not(_args[i], f)) { - args.push_back(f); - } - else { - args.push_back(m.mk_not(_args[i])); - } + args.push_back(mk_not(m, _args[i])); } - if (!d.is_one()) { - k *= d; - for (unsigned i = 0; i < num_args; ++i) { - coeffs[i] *= d; - } - } - k.neg(); - k += rational::one(); + m_k = floor(m_k); + m_k.neg(); + m_k += rational::one(); for (unsigned i = 0; i < num_args; ++i) { - k += coeffs[i]; + m_k += m_coeffs[i]; } - return mk_ge(num_args, coeffs.c_ptr(), args.c_ptr(), k); + return mk_ge(num_args, m_coeffs.c_ptr(), args.c_ptr(), m_k); } diff --git a/src/ast/pb_decl_plugin.h b/src/ast/pb_decl_plugin.h index d4264b9b9..e1b16f0c9 100644 --- a/src/ast/pb_decl_plugin.h +++ b/src/ast/pb_decl_plugin.h @@ -79,6 +79,9 @@ public: class pb_util { ast_manager & m; family_id m_fid; + vector 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; } diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 7a59c1ddb..4de602ec4 100644 --- a/src/opt/opt_context.cpp +++ b/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]; }