From 96d3b98a441b4ee52b160f6f8fa3f2b286cc81a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Aug 2018 13:33:09 -0700 Subject: [PATCH] fix #1783, wronge clausification of negated pb inequalities. Signs were ignored Signed-off-by: Nikolaj Bjorner --- src/sat/tactic/goal2sat.cpp | 20 ++++++++++++++++++-- src/tactic/arith/lia2card_tactic.cpp | 3 ++- 2 files changed, 20 insertions(+), 3 deletions(-) diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index 7faa89370..dc4dfc3a8 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -451,7 +451,15 @@ struct goal2sat::imp { unsigned sz = m_result_stack.size(); if (root) { m_result_stack.reset(); - m_ext->add_pb_ge(sat::null_bool_var, wlits, k.get_unsigned()); + unsigned k1 = k.get_unsigned(); + if (sign) { + k1 = 1 - k1; + for (wliteral& wl : wlits) { + wl.second.neg(); + k1 += wl.first; + } + } + m_ext->add_pb_ge(sat::null_bool_var, wlits, k1); } else { sat::bool_var v = m_solver.mk_var(true); @@ -476,7 +484,15 @@ struct goal2sat::imp { unsigned sz = m_result_stack.size(); if (root) { m_result_stack.reset(); - m_ext->add_pb_ge(sat::null_bool_var, wlits, k.get_unsigned()); + unsigned k1 = k.get_unsigned(); + if (sign) { + k1 = 1 - k1; + for (wliteral& wl : wlits) { + wl.second.neg(); + k1 += wl.first; + } + } + m_ext->add_pb_ge(sat::null_bool_var, wlits, k1); } else { sat::bool_var v = m_solver.mk_var(true); diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index ec18ae2bf..88e4a5583 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -167,7 +167,8 @@ public: m_mc.reset(); expr_ref_vector axioms(m); expr_safe_replace rep(m); - + + TRACE("pb", g->display(tout);); tactic_report report("lia2card", *g); bound_manager bounds(m);