mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 23:03:41 +00:00
Code Activity

compile

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-06-24 08:45:50 -07:00
parent e64aabafe8
commit d7f439430c
7 changed files with 31 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/math/lp/nla_core.cpp
View file

@ -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

4
src/math/lp/nla_monotone_lemmas.cpp
View file

@ -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);

10
src/math/lp/nla_order_lemmas.cpp
View file

@ -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"

18
src/math/lp/nla_powers.cpp
View file

@ -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);

10
src/math/lp/nla_types.h
View file

@ -52,7 +52,11 @@ namespace nla {
class lemma {
vector<ineq> 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<ineq>& 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(); }

3
src/sat/smt/arith_solver.cpp
View file

@ -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()));

5
src/smt/theory_lra.cpp
View file

@ -178,6 +178,9 @@ class theory_lra::imp {
// integer arithmetic
scoped_ptr<lp::int_solver> 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()) {