From 0d8a472aacd6541200466d83cf8b06f538751b07 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 Jan 2023 16:55:44 -0800 Subject: [PATCH] pass sign into literal definition for pbge --- src/sat/smt/pb_internalize.cpp | 12 ++++++------ src/sat/smt/pb_solver.cpp | 4 ++-- src/sat/smt/pb_solver.h | 2 +- src/tactic/tactic.cpp | 6 +++--- 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/src/sat/smt/pb_internalize.cpp b/src/sat/smt/pb_internalize.cpp index af25e7a9252..1a83dbc87ca 100644 --- a/src/sat/smt/pb_internalize.cpp +++ b/src/sat/smt/pb_internalize.cpp @@ -113,13 +113,13 @@ namespace pb { k1 += wl.first; } } - add_pb_ge(sat::null_bool_var, wlits, k1); + add_pb_ge(sat::null_bool_var, sign, wlits, k1); return sat::null_literal; } else { bool_var v = s().add_var(true); literal lit(v, sign); - add_pb_ge(v, wlits, k.get_unsigned()); + add_pb_ge(v, sign, wlits, k.get_unsigned()); TRACE("ba", tout << "root: " << root << " lit: " << lit << "\n";); return lit; } @@ -140,13 +140,13 @@ namespace pb { k1 += wl.first; } } - add_pb_ge(sat::null_bool_var, wlits, k1); + add_pb_ge(sat::null_bool_var, sign, wlits, k1); return sat::null_literal; } else { sat::bool_var v = s().add_var(true); sat::literal lit(v, sign); - add_pb_ge(v, wlits, k.get_unsigned()); + add_pb_ge(v, sign, wlits, k.get_unsigned()); TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";); return lit; } @@ -160,14 +160,14 @@ namespace pb { bool base_assert = (root && !sign && s().num_user_scopes() == 0); bool_var v1 = base_assert ? sat::null_bool_var : s().add_var(true); bool_var v2 = base_assert ? sat::null_bool_var : s().add_var(true); - add_pb_ge(v1, wlits, k.get_unsigned()); + add_pb_ge(v1, false, wlits, k.get_unsigned()); k.neg(); for (wliteral& wl : wlits) { wl.second.neg(); k += rational(wl.first); } check_unsigned(k); - add_pb_ge(v2, wlits, k.get_unsigned()); + add_pb_ge(v2, false, wlits, k.get_unsigned()); if (base_assert) { return sat::null_literal; } diff --git a/src/sat/smt/pb_solver.cpp b/src/sat/smt/pb_solver.cpp index 424b20d4e2c..ade48c42bfd 100644 --- a/src/sat/smt/pb_solver.cpp +++ b/src/sat/smt/pb_solver.cpp @@ -1472,8 +1472,8 @@ namespace pb { return p; } - void solver::add_pb_ge(bool_var v, svector const& wlits, unsigned k) { - literal lit = v == sat::null_bool_var ? sat::null_literal : literal(v, false); + void solver::add_pb_ge(bool_var v, bool sign, svector const& wlits, unsigned k) { + literal lit = v == sat::null_bool_var ? sat::null_literal : literal(v, sign); add_pb_ge(lit, wlits, k, m_is_redundant); } diff --git a/src/sat/smt/pb_solver.h b/src/sat/smt/pb_solver.h index f6a0c049e1f..99ea459839e 100644 --- a/src/sat/smt/pb_solver.h +++ b/src/sat/smt/pb_solver.h @@ -371,7 +371,7 @@ namespace pb { ~solver() override; void set_lookahead(sat::lookahead* l) override { m_lookahead = l; } void add_at_least(bool_var v, literal_vector const& lits, unsigned k); - void add_pb_ge(bool_var v, svector const& wlits, unsigned k); + void add_pb_ge(bool_var v, bool sign, svector const& wlits, unsigned k); bool is_external(bool_var v) override; bool propagated(literal l, sat::ext_constraint_idx idx) override; diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp index 8bf6efac5ee..179a42ab857 100644 --- a/src/tactic/tactic.cpp +++ b/src/tactic/tactic.cpp @@ -51,7 +51,7 @@ struct tactic_report::imp { << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds() << " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory << " :after-memory " << std::fixed << std::setprecision(2) << end_memory - << ")" << std::endl); + << ")\n"); IF_VERBOSE(20, m_goal.display(verbose_stream() << m_id << "\n")); SASSERT(m_goal.is_well_formed()); } @@ -71,7 +71,7 @@ tactic_report::~tactic_report() { void report_tactic_progress(char const * id, unsigned val) { if (val > 0) { - IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(" << id << " " << val << ")" << std::endl;); + IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(" << id << " " << val << ")\n"); } } @@ -166,7 +166,7 @@ void exec(tactic & t, goal_ref const & in, goal_ref_buffer & result) { t.cleanup(); } catch (tactic_exception & ex) { - IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(tactic-exception \"" << escaped(ex.msg()) << "\")" << std::endl;); + IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(tactic-exception \"" << escaped(ex.msg()) << "\")\n"); t.cleanup(); throw ex; }