mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

port over moving m_nla_lemmas into nla_core from the linear monomial propagation branch

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-09-26 20:08:30 -07:00
parent 8d2b65b20b
commit ec2937e2de
9 changed files with 80 additions and 84 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/nla_basics_lemmas.cpp
View file

@ -104,7 +104,7 @@ bool basics::basic_sign_lemma_model_based() {
return true;
}
}
return c().m_lemma_vec->size() > 0;
return c().m_lemmas.size() > 0;
}

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

@ -808,7 +808,7 @@ void core::print_stats(std::ostream& out) {
void core::clear() {
m_lemma_vec->clear();
m_lemmas.clear();
m_literal_vec->clear();
}
@ -1045,7 +1045,7 @@ rational core::val(const factorization& f) const {
}
new_lemma::new_lemma(core& c, char const* name):name(name), c(c) {
c.m_lemma_vec->push_back(lemma());
c.m_lemmas.push_back(lemma());
}
new_lemma& new_lemma::operator|=(ineq const& ineq) {
@ -1067,7 +1067,7 @@ new_lemma::~new_lemma() {
}
lemma& new_lemma::current() const {
return c.m_lemma_vec->back();
return c.m_lemmas.back();
}
new_lemma& new_lemma::operator&=(lp::explanation const& e) {
@ -1180,7 +1180,7 @@ void core::negate_relation(new_lemma& lemma, unsigned j, const rational& a) {
}
bool core::conflict_found() const {
for (const auto & l : * m_lemma_vec) {
for (const auto & l : m_lemmas) {
if (l.is_conflict())
return true;
}
@ -1188,7 +1188,7 @@ bool core::conflict_found() const {
}
bool core::done() const {
return m_lemma_vec->size() >= 10 ||
return m_lemmas.size() >= 10 ||
conflict_found() ||
lp_settings().get_cancel_flag();
}
@ -1477,7 +1477,7 @@ void core::check_weighted(unsigned sz, std::pair<unsigned, std::function<void(vo
for (unsigned i = 0; i < sz; ++i)
bound += checks[i].first;
uint_set seen;
while (bound > 0 && !done() && m_lemma_vec->empty()) {
while (bound > 0 && !done() && m_lemmas.empty()) {
unsigned n = random() % bound;
for (unsigned i = 0; i < sz; ++i) {
if (seen.contains(i))
@ -1493,13 +1493,13 @@ void core::check_weighted(unsigned sz, std::pair<unsigned, std::function<void(vo
}
}
lbool core::check_power(lpvar r, lpvar x, lpvar y, vector<lemma>& l_vec) {
m_lemma_vec = &l_vec;
return m_powers.check(r, x, y, l_vec);
lbool core::check_power(lpvar r, lpvar x, lpvar y) {
m_lemmas.reset();
return m_powers.check(r, x, y, m_lemmas);
}
void core::check_bounded_divisions(vector<lemma>& l_vec) {
m_lemma_vec = &l_vec;
void core::check_bounded_divisions() {
m_lemmas.reset();
m_divisions.check_bounded_divisions();
}
// looking for a free variable inside of a monic to split
@ -1518,11 +1518,10 @@ void core::add_bounds() {
}
}
lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
lbool core::check(vector<ineq>& lits) {
lp_settings().stats().m_nla_calls++;
TRACE("nla_solver", tout << "calls = " << lp_settings().stats().m_nla_calls << "\n";);
lra.get_rid_of_inf_eps();
m_lemma_vec = &l_vec;
m_literal_vec = &lits;
if (!(lra.get_status() == lp::lp_status::OPTIMAL ||
lra.get_status() == lp::lp_status::FEASIBLE)) {
@ -1543,7 +1542,7 @@ lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
bool run_bounded_nlsat = should_run_bounded_nlsat();
bool run_bounds = params().arith_nl_branching();
auto no_effect = [&]() { return !done() && l_vec.empty() && lits.empty(); };
auto no_effect = [&]() { return !done() && m_lemmas.empty() && lits.empty(); };
if (no_effect())
m_monomial_bounds.propagate();
@ -1561,7 +1560,7 @@ lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
{1, check2},
{1, check3} };
check_weighted(3, checks);
if (!l_vec.empty() || !lits.empty())
if (!m_lemmas.empty() || !lits.empty())
return l_false;
}
@ -1598,15 +1597,15 @@ lbool core::check(vector<ineq>& lits, vector<lemma>& l_vec) {
m_stats.m_nra_calls++;
}
if (ret == l_undef && !l_vec.empty() && m_reslim.inc())
if (ret == l_undef && !m_lemmas.empty() && m_reslim.inc())
ret = l_false;
m_stats.m_nla_lemmas += l_vec.size();
for (const auto& l : l_vec)
m_stats.m_nla_lemmas += m_lemmas.size();
for (const auto& l : m_lemmas)
m_stats.m_nla_explanations += static_cast<unsigned>(l.expl().size());
TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << l_vec.size() << "\n";);
TRACE("nla_solver", tout << "ret = " << ret << ", lemmas count = " << m_lemmas.size() << "\n";);
IF_VERBOSE(2, if(ret == l_undef) {verbose_stream() << "Monomials\n"; print_monics(verbose_stream());});
CTRACE("nla_solver", ret == l_undef, tout << "Monomials\n"; print_monics(tout););
return ret;
@ -1641,13 +1640,13 @@ lbool core::bounded_nlsat() {
m_nlsat_delay /= 2;
}
if (ret == l_true) {
m_lemma_vec->reset();
m_lemmas.reset();
}
return ret;
}
bool core::no_lemmas_hold() const {
for (auto & l : * m_lemma_vec) {
for (auto & l : m_lemmas) {
if (lemma_holds(l)) {
TRACE("nla_solver", print_lemma(l, tout););
return false;
@ -1656,10 +1655,10 @@ bool core::no_lemmas_hold() const {
return true;
}
lbool core::test_check(vector<lemma>& l) {
lbool core::test_check() {
vector<ineq> lits;
lra.set_status(lp::lp_status::OPTIMAL);
return check(lits, l);
return check(lits);
}
std::ostream& core::print_terms(std::ostream& out) const {
@ -1811,12 +1810,11 @@ bool core::improve_bounds() {
return bounds_improved;
}
void core::propagate(vector<lemma>& lemmas) {
void core::propagate() {
// disable for now
return;
// propagate linear monomials
lemmas.reset();
m_lemma_vec = &lemmas;
m_lemmas.reset();
m_monomial_bounds.unit_propagate();

13
src/math/lp/nla_core.h
View file

@ -85,7 +85,7 @@ class core {
reslimit& m_reslim;
smt_params_helper m_params;
std::function<bool(lpvar)> m_relevant;
vector<lemma> * m_lemma_vec;
vector<lemma> m_lemmas;
vector<ineq> * m_literal_vec = nullptr;
indexed_uint_set m_to_refine;
tangents m_tangents;
@ -386,15 +386,15 @@ public:
bool conflict_found() const;
lbool check(vector<ineq>& ineqs, vector<lemma>& l_vec);
lbool check_power(lpvar r, lpvar x, lpvar y, vector<lemma>& l_vec);
void check_bounded_divisions(vector<lemma>&);
lbool check(vector<ineq>& ineqs);
lbool check_power(lpvar r, lpvar x, lpvar y);
void check_bounded_divisions();
bool no_lemmas_hold() const;
void propagate(vector<lemma>& lemmas);
void propagate();
lbool test_check(vector<lemma>& l);
lbool test_check();
lpvar map_to_root(lpvar) const;
std::ostream& print_terms(std::ostream&) const;
std::ostream& print_term(const lp::lar_term&, std::ostream&) const;
@ -428,6 +428,7 @@ public:
void set_use_nra_model(bool m);
bool use_nra_model() const { return m_use_nra_model; }
void collect_statistics(::statistics&);
vector<nla::lemma> const& lemmas() const { return m_lemmas; }
private:
void restore_patched_values();
void constrain_nl_in_tableau();

19
src/math/lp/nla_solver.cpp
View file

@ -42,12 +42,12 @@ namespace nla {
bool solver::need_check() { return m_core->has_relevant_monomial(); }
lbool solver::check(vector<ineq>& lits, vector<lemma>& lemmas) {
return m_core->check(lits, lemmas);
lbool solver::check(vector<ineq>& lits) {
return m_core->check(lits);
}
void solver::propagate(vector<lemma>& lemmas) {
m_core->propagate(lemmas);
void solver::propagate() {
m_core->propagate();
}
void solver::push(){
@ -93,12 +93,15 @@ namespace nla {
}
// ensure r = x^y, add abstraction/refinement lemmas
lbool solver::check_power(lpvar r, lpvar x, lpvar y, vector<lemma>& lemmas) {
return m_core->check_power(r, x, y, lemmas);
lbool solver::check_power(lpvar r, lpvar x, lpvar y) {
return m_core->check_power(r, x, y);
}
void solver::check_bounded_divisions(vector<lemma>& lemmas) {
m_core->check_bounded_divisions(lemmas);
void solver::check_bounded_divisions() {
m_core->check_bounded_divisions();
}
vector<nla::lemma> const& solver::lemmas() const {
return m_core->lemmas();
}
}

9
src/math/lp/nla_solver.h
View file

@ -31,14 +31,14 @@ namespace nla {
void add_idivision(lpvar q, lpvar x, lpvar y);
void add_rdivision(lpvar q, lpvar x, lpvar y);
void add_bounded_division(lpvar q, lpvar x, lpvar y);
void check_bounded_divisions(vector<lemma>&);
void check_bounded_divisions();
void set_relevant(std::function<bool(lpvar)>& is_relevant);
void push();
void pop(unsigned scopes);
bool need_check();
lbool check(vector<ineq>& lits, vector<lemma>&);
void propagate(vector<lemma>& lemmas);
lbool check_power(lpvar r, lpvar x, lpvar y, vector<lemma>&);
lbool check(vector<ineq>& lits);
void propagate();
lbool check_power(lpvar r, lpvar x, lpvar y);
bool is_monic_var(lpvar) const;
bool influences_nl_var(lpvar) const;
std::ostream& display(std::ostream& out) const;
@ -47,5 +47,6 @@ namespace nla {
nlsat::anum_manager& am();
nlsat::anum const& am_value(lp::var_index v) const;
void collect_statistics(::statistics & st);
vector<nla::lemma> const& lemmas() const;
};
}

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

@ -1459,11 +1459,11 @@ namespace arith {
return l_true;
m_a1 = nullptr; m_a2 = nullptr;
lbool r = m_nla->check(m_nla_literals, m_nla_lemma_vector);
lbool r = m_nla->check(m_nla_literals);
switch (r) {
case l_false:
assume_literals();
for (const nla::lemma& l : m_nla_lemma_vector)
for (const nla::lemma& l : m_nla->lemmas())
false_case_of_check_nla(l);
break;
case l_true:

1
src/sat/smt/arith_solver.h
View file

@ -248,7 +248,6 @@ namespace arith {
// lemmas
lp::explanation m_explanation;
vector<nla::lemma> m_nla_lemma_vector;
vector<nla::ineq> m_nla_literals;
literal_vector m_core, m_core2;
vector<rational> m_coeffs;

16
src/smt/theory_lra.cpp
View file

@ -1598,11 +1598,11 @@ public:
return FC_DONE;
if (!m_nla)
return FC_GIVEUP;
switch (m_nla->check_power(get_lpvar(e), get_lpvar(x), get_lpvar(y), m_nla_lemma_vector)) {
switch (m_nla->check_power(get_lpvar(e), get_lpvar(x), get_lpvar(y))) {
case l_true:
return FC_DONE;
case l_false:
for (const nla::lemma & l : m_nla_lemma_vector)
for (const nla::lemma & l : m_nla->lemmas())
false_case_of_check_nla(l);
return FC_CONTINUE;
case l_undef:
@ -1800,8 +1800,8 @@ public:
if (!m_nla)
return true;
m_nla_lemma_vector.reset();
m_nla->check_bounded_divisions(m_nla_lemma_vector);
for (auto & lemma : m_nla_lemma_vector)
m_nla->check_bounded_divisions();
for (auto & lemma : m_nla->lemmas())
false_case_of_check_nla(lemma);
return m_nla_lemma_vector.empty();
}
@ -2022,13 +2022,13 @@ public:
final_check_status check_nla_continue() {
m_a1 = nullptr; m_a2 = nullptr;
lbool r = m_nla->check(m_nla_literals, m_nla_lemma_vector);
lbool r = m_nla->check(m_nla_literals);
switch (r) {
case l_false:
for (const nla::ineq& i : m_nla_literals)
assume_literal(i);
for (const nla::lemma & l : m_nla_lemma_vector)
for (const nla::lemma & l : m_nla->lemmas())
false_case_of_check_nla(l);
return FC_CONTINUE;
case l_true:
@ -2161,8 +2161,8 @@ public:
void propagate_nla() {
if (!m_nla)
return;
m_nla->propagate(m_nla_lemma_vector);
for (nla::lemma const& l : m_nla_lemma_vector)
m_nla->propagate();
for (nla::lemma const& l : m_nla->lemmas())
false_case_of_check_nla(l);
}

50
src/test/lp/nla_solver_test.cpp
View file

@ -179,7 +179,6 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
v.push_back(lp_a);v.push_back(lp_c);
nla.add_monic(lp_ac, v.size(), v.begin());
vector<lemma> lv;
// set abcde = ac * bde
// ac = 1 then abcde = bde, but we have abcde < bde
@ -193,8 +192,9 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_0() {
s.set_column_value_test(lp_bde, lp::impq(rational(16)));
VERIFY(nla.get_core().test_check(lv) == l_false);
VERIFY(nla.get_core().test_check() == l_false);
auto const& lv = nla.get_core().lemmas();
nla.get_core().print_lemma(lv.back(), std::cout);
ineq i0(lp_ac, llc::NE, 1);
@ -250,8 +250,6 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
svector<lpvar> v; v.push_back(lp_b);v.push_back(lp_d);v.push_back(lp_e);
nla.add_monic(lp_bde, v.size(), v.begin());
vector<lemma> lemma;
s_set_column_value_test(s, lp_a, rational(1));
s_set_column_value_test(s, lp_b, rational(1));
s_set_column_value_test(s, lp_c, rational(1));
@ -259,7 +257,8 @@ void test_basic_lemma_for_mon_neutral_from_factors_to_monomial_1() {
s_set_column_value_test(s, lp_e, rational(1));
s_set_column_value_test(s, lp_bde, rational(3));
VERIFY(nla.get_core().test_check(lemma) == l_false);
VERIFY(nla.get_core().test_check() == l_false);
auto const& lemma = nla.get_core().lemmas();
SASSERT(lemma[0].size() == 4);
nla.get_core().print_lemma(lemma.back(), std::cout);
@ -330,7 +329,6 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
lp_bde,
lp_acd,
lp_be);
vector<lemma> lemma;
// set vars
s_set_column_value_test(s, lp_a, rational(1));
@ -344,7 +342,8 @@ void test_basic_lemma_for_mon_zero_from_factors_to_monomial() {
s_set_column_value_test(s, lp_acd, rational(1));
s_set_column_value_test(s, lp_be, rational(1));
VERIFY(nla.get_core().test_check(lemma) == l_false);
VERIFY(nla.get_core().test_check() == l_false);
auto const& lemma = nla.get_core().lemmas();
nla.get_core().print_lemma(lemma.back(), std::cout);
SASSERT(lemma.size() == 1 && lemma[0].size() == 2);
lp::lar_term t0, t1;
@ -389,14 +388,13 @@ void test_basic_lemma_for_mon_zero_from_monomial_to_factors() {
vec.push_back(lp_d);
nla.add_monic(lp_acd, vec.size(), vec.begin());
vector<lemma> lemma;
s_set_column_value_test(s, lp_a, rational(1));
s_set_column_value_test(s, lp_c, rational(1));
s_set_column_value_test(s, lp_d, rational(1));
s_set_column_value_test(s, lp_acd, rational(0));
VERIFY(nla.get_core().test_check(lemma) == l_false);
VERIFY(nla.get_core().test_check() == l_false);
auto const& lemma = nla.get_core().lemmas();
nla.get_core().print_lemma(lemma.back(), std::cout);
ineq i0(lp_a, llc::EQ, 0);
@ -452,7 +450,6 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
lp_bde,
lp_acd,
lp_be);
vector<lemma> lemma;
// set all vars to 1
s_set_column_value_test(s, lp_a, rational(1));
@ -471,8 +468,8 @@ void test_basic_lemma_for_mon_neutral_from_monomial_to_factors() {
s_set_column_value_test(s, lp_b, - rational(2));
// we have bde = -b, therefore d = +-1 and e = +-1
s_set_column_value_test(s, lp_d, rational(3));
VERIFY(nla.get_core().test_check(lemma) == l_false);
VERIFY(nla.get_core().test_check() == l_false);
auto const& lemma = nla.get_core().lemmas();
nla.get_core().print_lemma(lemma.back(), std::cout);
ineq i0(lp_d, llc::EQ, 1);
@ -584,9 +581,8 @@ void test_basic_sign_lemma() {
s_set_column_value_test(s, lp_bde, rational(5));
s_set_column_value_test(s, lp_acd, rational(3));
vector<lemma> lemmas;
VERIFY(nla.get_core().test_check(lemmas) == l_false);
VERIFY(nla.get_core().test_check() == l_false);
auto const& lemmas = nla.get_core().lemmas();
lp::lar_term t;
t.add_var(lp_bde);
t.add_var(lp_acd);
@ -707,9 +703,9 @@ void test_order_lemma_params(bool var_equiv, int sign) {
s_set_column_value_test(s, lp_abef, nla.get_core().mon_value_by_vars(mon_cdij)
+ rational(1));
}
vector<lemma> lemma;
VERIFY(nla.get_core().test_check(lemma) == l_false);
VERIFY(nla.get_core().test_check() == l_false);
auto const& lemma = nla.get_core().lemmas();
// lp::lar_term t;
// t.add_monomial(lp_bde);
// t.add_monomial(lp_acd);
@ -792,8 +788,8 @@ void test_monotone_lemma() {
// set ef = ij while it has to be ef > ij
s_set_column_value_test(s, lp_ef, s.get_column_value(lp_ij));
vector<lemma> lemma;
VERIFY(nla.get_core().test_check(lemma) == l_false);
VERIFY(nla.get_core().test_check() == l_false);
auto const& lemma = nla.get_core().lemmas();
nla.get_core().print_lemma(lemma.back(), std::cout);
*/
}
@ -821,8 +817,8 @@ void test_tangent_lemma_rat() {
vec.push_back(lp_b);
nla.add_monic(lp_ab, vec.size(), vec.begin());
vector<lemma> lemma;
VERIFY(nla.get_core().test_check(lemma) == l_false);
VERIFY(nla.get_core().test_check() == l_false);
auto const& lemma = nla.get_core().lemmas();
nla.get_core().print_lemma(lemma.back(), std::cout);
}
@ -848,9 +844,8 @@ void test_tangent_lemma_reg() {
vec.push_back(lp_b);
nla.add_monic(lp_ab, vec.size(), vec.begin());
vector<lemma> lemma;
VERIFY(nla.get_core().test_check(lemma) == l_false);
nla.get_core().print_lemma(lemma.back(), std::cout);
VERIFY(nla.get_core().test_check() == l_false);
nla.get_core().print_lemma(nla.get_core().lemmas().back(), std::cout);
}
void test_tangent_lemma_equiv() {
@ -893,10 +888,9 @@ void test_tangent_lemma_equiv() {
int mon_ab = nla.add_monic(lp_ab, vec.size(), vec.begin());
s_set_column_value_test(s, lp_ab, nla.get_core().mon_value_by_vars(mon_ab) + rational(10)); // greater by ten than the correct value
vector<lemma> lemma;
VERIFY(nla.get_core().test_check(lemma) == l_false);
nla.get_core().print_lemma(lemma.back(), std::cout);
VERIFY(nla.get_core().test_check() == l_false);
nla.get_core().print_lemma(nla.get_core().lemmas().back(), std::cout);
*/
}