From d7f439430c3bd093916b582080348ea63def7cf3 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 24 Jun 2025 08:45:50 -0700 Subject: [PATCH] compile Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.cpp | 7 ++++--- src/math/lp/nla_monotone_lemmas.cpp | 4 ++-- src/math/lp/nla_order_lemmas.cpp | 10 +++++----- src/math/lp/nla_powers.cpp | 18 +++++++++--------- src/math/lp/nla_types.h | 10 ++++++---- src/sat/smt/arith_solver.cpp | 3 ++- src/smt/theory_lra.cpp | 5 +++-- 7 files changed, 31 insertions(+), 26 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 744e3ff04..31db59986 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1043,8 +1043,9 @@ rational core::val(const factorization& f) const { return r; } -new_lemma::new_lemma(core& c, char const* name):name(name), c(c) { - c.m_lemmas.push_back(lemma()); +new_lemma::new_lemma(core& c, char const* name, const std::string & location):name(name), c(c) { + + c.m_lemmas.push_back(lemma(location)); } new_lemma& new_lemma::operator|=(ineq const& ineq) { @@ -1221,7 +1222,7 @@ void core::print_rational_smt2(std::ostream& out, const rational& r) const { // Display a lemma as SMT2 to the given output stream std::ostream& core::display_new_lemma_as_smt2(std::ostream& out, const new_lemma& l) const { // SMT2 header - out << "(set-info :source |NLA lemma from Z3|)\n"; + out << "(set-info :source |" << l.current().m_location << "|)\n"; out << "(set-logic QF_NRA)\n"; // Collect all variables used in the lemma diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp index cc9241446..82a13fbb2 100644 --- a/src/math/lp/nla_monotone_lemmas.cpp +++ b/src/math/lp/nla_monotone_lemmas.cpp @@ -54,7 +54,7 @@ void monotone::monotonicity_lemma(monic const& m) { */ void monotone::monotonicity_lemma_gt(const monic& m) { - new_lemma lemma(c(), "monotonicity > "); + new_lemma lemma(c(), "monotonicity > ", std::string(__FUNCTION__) + std::string(std::to_string(__LINE__))); rational product(1); for (lpvar j : m.vars()) { auto v = c().val(j); @@ -76,7 +76,7 @@ void monotone::monotonicity_lemma_gt(const monic& m) { x <= -2 & y >= 3 => x*y <= -6 */ void monotone::monotonicity_lemma_lt(const monic& m) { - new_lemma lemma(c(), "monotonicity <"); + new_lemma lemma(c(), "monotonicity <", std::string(__FUNCTION__) + std::string(std::to_string(__LINE__))); rational product(1); for (lpvar j : m.vars()) { auto v = c().val(j); diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index 386ac8b9a..f769b1da9 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -89,7 +89,7 @@ void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int SASSERT(!_().mon_has_zero(xy.vars())); int sy = rat_sign(val(y)); - new_lemma lemma(c(), __FUNCTION__); + new_lemma lemma(c(), __FUNCTION__, std::string(__FUNCTION__) + std::string(std::to_string(__LINE__))); lemma |= ineq(y, sy == 1 ? llc::LE : llc::GE, 0); // negate sy lemma |= ineq(x, sy*sign == 1 ? llc::GT : llc::LT , val(x)); lemma |= ineq(term(xy.var(), - val(x), y), sign == 1 ? llc::LE : llc::GE, 0); @@ -189,7 +189,7 @@ void order::generate_mon_ol(const monic& ac, SASSERT(ab_cmp != llc::LT || (var_val(ac) >= var_val(bd) && val(a)*c_sign < val(b)*d_sign)); SASSERT(ab_cmp != llc::GT || (var_val(ac) <= var_val(bd) && val(a)*c_sign > val(b)*d_sign)); - new_lemma lemma(_(), __FUNCTION__); + new_lemma lemma(_(), __FUNCTION__, std::string(__FUNCTION__) + std::string(std::to_string(__LINE__))); lemma |= ineq(term(c_sign, c), llc::LE, 0); lemma &= c; // this explains c == +- d lemma |= ineq(term(c_sign, a, -d_sign * b.rat_sign(), b.var()), negate(ab_cmp), 0); @@ -239,7 +239,7 @@ void order::order_lemma_on_factorization(const monic& m, const factorization& ab if (mv != fv && !c().has_real(m)) { bool gt = mv > fv; for (unsigned j = 0, k = 1; j < 2; j++, k--) { - new_lemma lemma(_(), __FUNCTION__); + new_lemma lemma(_(), __FUNCTION__,""); order_lemma_on_ab(lemma, m, rsign, var(ab[k]), var(ab[j]), gt); lemma &= ab; lemma &= m; @@ -274,7 +274,7 @@ void order::generate_ol_eq(const monic& ac, const monic& bc, const factor& b) { - new_lemma lemma(_(), __FUNCTION__); + new_lemma lemma(_(), __FUNCTION__,""); IF_VERBOSE(100, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac @@ -299,7 +299,7 @@ void order::generate_ol(const monic& ac, const monic& bc, const factor& b) { - new_lemma lemma(_(), __FUNCTION__); + new_lemma lemma(_(), __FUNCTION__, ""); TRACE(nla_solver, _().trace_print_ol(ac, a, c, bc, b, tout);); IF_VERBOSE(10, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n" diff --git a/src/math/lp/nla_powers.cpp b/src/math/lp/nla_powers.cpp index b934ad16a..00e90f6cb 100644 --- a/src/math/lp/nla_powers.cpp +++ b/src/math/lp/nla_powers.cpp @@ -89,7 +89,7 @@ namespace nla { lemmas.reset(); auto x_exp_0 = [&]() { - new_lemma lemma(c, "x != 0 => x^0 = 1"); + new_lemma lemma(c, "x != 0 => x^0 = 1", std::string(__FUNCTION__) + std::string(std::to_string(__LINE__))); lemma |= ineq(x, llc::EQ, rational::zero()); lemma |= ineq(y, llc::NE, rational::zero()); lemma |= ineq(r, llc::EQ, rational::one()); @@ -97,7 +97,7 @@ namespace nla { }; auto zero_exp_y = [&]() { - new_lemma lemma(c, "y != 0 => 0^y = 0"); + new_lemma lemma(c, "y != 0 => 0^y = 0", std::string(__FUNCTION__) + std::string(std::to_string(__LINE__))); lemma |= ineq(x, llc::NE, rational::zero()); lemma |= ineq(y, llc::EQ, rational::zero()); lemma |= ineq(r, llc::EQ, rational::zero()); @@ -105,14 +105,14 @@ namespace nla { }; auto x_gt_0 = [&]() { - new_lemma lemma(c, "x > 0 => x^y > 0"); + new_lemma lemma(c, "x > 0 => x^y > 0", std::string(__FUNCTION__) + std::string(std::to_string(__LINE__))); lemma |= ineq(x, llc::LE, rational::zero()); lemma |= ineq(r, llc::GT, rational::zero()); return l_false; }; auto y_lt_1 = [&]() { - new_lemma lemma(c, "x > 1, y < 0 => x^y < 1"); + new_lemma lemma(c, "x > 1, y < 0 => x^y < 1", std::string(__FUNCTION__) + std::string(std::to_string(__LINE__))); lemma |= ineq(x, llc::LE, rational::one()); lemma |= ineq(y, llc::GE, rational::zero()); lemma |= ineq(r, llc::LT, rational::one()); @@ -120,7 +120,7 @@ namespace nla { }; auto y_gt_1 = [&]() { - new_lemma lemma(c, "x > 1, y > 0 => x^y > 1"); + new_lemma lemma(c, "x > 1, y > 0 => x^y > 1", std::string(__FUNCTION__) + std::string(std::to_string(__LINE__))); lemma |= ineq(x, llc::LE, rational::one()); lemma |= ineq(y, llc::LE, rational::zero()); lemma |= ineq(r, llc::GT, rational::one()); @@ -128,7 +128,7 @@ namespace nla { }; auto x_ge_3 = [&]() { - new_lemma lemma(c, "x >= 3, y != 0 => x^y > ln(x)y + 1"); + new_lemma lemma(c, "x >= 3, y != 0 => x^y > ln(x)y + 1", std::string(__FUNCTION__) + std::string(std::to_string(__LINE__))); lemma |= ineq(x, llc::LT, rational(3)); lemma |= ineq(y, llc::EQ, rational::zero()); lemma |= ineq(lp::lar_term(r, rational::minus_one(), y), llc::GT, rational::one()); @@ -172,21 +172,21 @@ namespace nla { if (rval == r2val) return l_true; if (c.random() % 2 == 0) { - new_lemma lemma(c, "x == x0, y == y0 => r = x0^y0"); + new_lemma lemma(c, "x == x0, y == y0 => r = x0^y0", std::string(__FUNCTION__) + std::string(std::to_string(__LINE__))); lemma |= ineq(x, llc::NE, xval); lemma |= ineq(y, llc::NE, yval); lemma |= ineq(r, llc::EQ, r2val); return l_false; } if (yval > 0 && r2val > rval) { - new_lemma lemma(c, "x >= x0 > 0, y >= y0 > 0 => r >= x0^y0"); + new_lemma lemma(c, "x >= x0 > 0, y >= y0 > 0 => r >= x0^y0", std::string(__FUNCTION__) + std::string(std::to_string(__LINE__))); lemma |= ineq(x, llc::LT, xval); lemma |= ineq(y, llc::LT, yval); lemma |= ineq(r, llc::GE, r2val); return l_false; } if (r2val < rval) { - new_lemma lemma(c, "0 < x <= x0, y <= y0 => r <= x0^y0"); + new_lemma lemma(c, "0 < x <= x0, y <= y0 => r <= x0^y0", std::string(__FUNCTION__) + std::string(std::to_string(__LINE__))); lemma |= ineq(x, llc::LE, rational::zero()); lemma |= ineq(x, llc::GT, xval); lemma |= ineq(y, llc::GT, yval); diff --git a/src/math/lp/nla_types.h b/src/math/lp/nla_types.h index 5596906ed..d6136e4f0 100644 --- a/src/math/lp/nla_types.h +++ b/src/math/lp/nla_types.h @@ -52,7 +52,11 @@ namespace nla { class lemma { vector m_ineqs; lp::explanation m_expl; + public: + lemma(const std::string& location):m_location(location) { + } + std::string m_location; void push_back(const ineq& i) { m_ineqs.push_back(i);} size_t size() const { return m_ineqs.size() + m_expl.size(); } const vector& ineqs() const { return m_ineqs; } @@ -72,10 +76,9 @@ namespace nla { class new_lemma { char const* name; core& c; - lemma& current() const; - public: - new_lemma(core& c, char const* name); + lemma& current() const; + new_lemma(core& c, char const* name, const std::string& location="default"); ~new_lemma(); lemma& operator()() { return current(); } const lemma& operator()() const { return current(); } @@ -91,7 +94,6 @@ namespace nla { new_lemma& explain_var_separated_from_zero(lpvar j); new_lemma& explain_existing_lower_bound(lpvar j); new_lemma& explain_existing_upper_bound(lpvar j); - void dump_lemma_as_smt2() const; lp::explanation& expl() { return current().expl(); } diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 1632cd3e8..5a12e6c71 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -26,6 +26,7 @@ namespace arith { m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)), m_resource_limit(*this), m_bp(*this, m_implied_bounds), + m_lemma("arith_solver"), a(m), m_bound_terms(m), m_bound_predicate(m) @@ -1540,7 +1541,7 @@ namespace arith { // verbose_stream() << lit << ":= " << s().value(lit) << "\n"; // force trichotomy axiom for equality literals if (ineq.cmp() == lp::EQ && false) { - nla::lemma l; + nla::lemma l("arith::solver::add_lemmas"); l.push_back(ineq); l.push_back(nla::ineq(lp::LT, ineq.term(), ineq.rs())); l.push_back(nla::ineq(lp::GT, ineq.term(), ineq.rs())); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 252bf473f..9679f8864 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -178,6 +178,9 @@ class theory_lra::imp { // integer arithmetic scoped_ptr m_lia; + // temporary lemma storage + nla::lemma m_lemma{"theory_lra_tmp"}; + struct var_value_eq { imp & m_th; @@ -1962,8 +1965,6 @@ public: return FC_DONE; } - nla::lemma m_lemma; - literal mk_literal(nla::ineq const& ineq) { bool is_lower = true, pos = true, is_eq = false; switch (ineq.cmp()) {