mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
move m_nla_lemma_vector to be internal to nla_core
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
26a9b776c6
commit
0a1ade6f95
|
@ -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;
|
||||
}
|
||||
|
||||
|
||||
|
|
|
@ -829,7 +829,7 @@ void core::print_stats(std::ostream& out) {
|
|||
|
||||
|
||||
void core::clear() {
|
||||
m_lemma_vec->clear();
|
||||
m_lemmas.clear();
|
||||
m_literal_vec->clear();
|
||||
}
|
||||
|
||||
|
@ -1066,7 +1066,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) {
|
||||
|
@ -1096,7 +1096,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) {
|
||||
|
@ -1209,7 +1209,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;
|
||||
}
|
||||
|
@ -1217,7 +1217,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();
|
||||
}
|
||||
|
@ -1506,7 +1506,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))
|
||||
|
@ -1522,13 +1522,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
|
||||
|
@ -1547,11 +1547,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)) {
|
||||
|
@ -1572,7 +1571,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();
|
||||
|
@ -1590,7 +1589,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;
|
||||
}
|
||||
|
||||
|
@ -1627,15 +1626,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;
|
||||
|
@ -1670,13 +1669,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;
|
||||
|
@ -1685,10 +1684,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 {
|
||||
|
@ -2027,12 +2026,12 @@ void core::add_lower_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std:
|
|||
}
|
||||
}
|
||||
|
||||
void core::init_bound_propagation(vector<nla::lemma>& lemma_vector) {
|
||||
void core::init_bound_propagation() {
|
||||
m_implied_bounds.clear();
|
||||
m_improved_lower_bounds.reset();
|
||||
m_improved_upper_bounds.reset();
|
||||
m_column_types = &lra.get_column_types();
|
||||
lemma_vector.clear();
|
||||
m_lemmas.clear();
|
||||
}
|
||||
|
||||
} // namespace nla
|
||||
|
|
|
@ -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;
|
||||
vector<lpvar> m_monics_with_changed_bounds;
|
||||
|
@ -393,15 +393,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;
|
||||
|
@ -443,6 +443,8 @@ public:
|
|||
void add_upper_bound_monic(lpvar j, const lp::mpq& v, bool is_strict, std::function<u_dependency*()> explain_dep);
|
||||
bool upper_bound_is_available(unsigned j) const;
|
||||
bool lower_bound_is_available(unsigned j) const;
|
||||
vector<nla::lemma> const& lemmas() const { return m_lemmas; }
|
||||
|
||||
private:
|
||||
lp::column_type get_column_type(unsigned j) const { return (*m_column_types)[j]; }
|
||||
void constrain_nl_in_tableau();
|
||||
|
@ -451,7 +453,7 @@ private:
|
|||
void save_tableau();
|
||||
bool integrality_holds();
|
||||
void calculate_implied_bounds_for_monic(lp::lpvar v);
|
||||
void init_bound_propagation(vector<nla::lemma> &);
|
||||
void init_bound_propagation();
|
||||
}; // end of core
|
||||
|
||||
struct pp_mon {
|
||||
|
|
|
@ -42,8 +42,8 @@ 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::push(){
|
||||
|
@ -92,16 +92,20 @@ namespace nla {
|
|||
m_core->calculate_implied_bounds_for_monic(v);
|
||||
}
|
||||
// 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();
|
||||
}
|
||||
|
||||
void solver::init_bound_propagation(vector<nla::lemma>& nla_lemma_vector) {
|
||||
m_core->init_bound_propagation(nla_lemma_vector);
|
||||
void solver::init_bound_propagation() {
|
||||
m_core->init_bound_propagation();
|
||||
}
|
||||
|
||||
vector<nla::lemma> const& solver::lemmas() const {
|
||||
return m_core->lemmas();
|
||||
}
|
||||
|
||||
}
|
||||
|
|
|
@ -23,7 +23,7 @@ namespace nla {
|
|||
class solver {
|
||||
core* m_core;
|
||||
public:
|
||||
|
||||
|
||||
solver(lp::lar_solver& s, params_ref const& p, reslimit& limit, std_vector<lp::implied_bound> & implied_bounds);
|
||||
~solver();
|
||||
const auto& monics_with_changed_bounds() const { return m_core->monics_with_changed_bounds(); }
|
||||
|
@ -32,14 +32,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;
|
||||
|
@ -49,6 +49,8 @@ namespace nla {
|
|||
nlsat::anum const& am_value(lp::var_index v) const;
|
||||
void collect_statistics(::statistics & st);
|
||||
void calculate_implied_bounds_for_monic(lp::lpvar v);
|
||||
void init_bound_propagation(vector<nla::lemma>&);
|
||||
void init_bound_propagation();
|
||||
vector<nla::lemma> const& lemmas() const;
|
||||
|
||||
};
|
||||
}
|
||||
|
|
|
@ -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:
|
||||
|
|
|
@ -249,7 +249,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;
|
||||
|
|
|
@ -1601,11 +1601,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:
|
||||
|
@ -1802,11 +1802,10 @@ public:
|
|||
bool check_idiv_bounds() {
|
||||
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();
|
||||
return m_nla->lemmas().empty();
|
||||
}
|
||||
|
||||
expr_ref var2expr(lpvar v) {
|
||||
|
@ -2025,13 +2024,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:
|
||||
|
@ -2201,12 +2200,12 @@ public:
|
|||
}
|
||||
|
||||
void propagate_bounds_for_touched_monomials() {
|
||||
m_nla->init_bound_propagation(m_nla_lemma_vector);
|
||||
m_nla->init_bound_propagation();
|
||||
for (unsigned v : m_nla->monics_with_changed_bounds())
|
||||
m_nla->calculate_implied_bounds_for_monic(v);
|
||||
|
||||
m_nla->reset_monics_with_changed_bounds();
|
||||
for (const auto & l : m_nla_lemma_vector)
|
||||
for (const auto & l : m_nla->lemmas())
|
||||
false_case_of_check_nla(l);
|
||||
}
|
||||
|
||||
|
@ -3210,7 +3209,6 @@ public:
|
|||
}
|
||||
|
||||
lp::explanation m_explanation;
|
||||
vector<nla::lemma> m_nla_lemma_vector;
|
||||
vector<nla::ineq> m_nla_literals;
|
||||
literal_vector m_core;
|
||||
svector<enode_pair> m_eqs;
|
||||
|
|
Loading…
Reference in a new issue