mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

allow for propagations the trigger make-feasible check

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-10-19 16:08:35 -07:00
parent 8c00181815
commit 97058b0d5d
5 changed files with 23 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -819,6 +819,7 @@ void core::clear() {
m_fixed_equalities.clear();
m_equalities.clear();
m_conflicts = 0;
m_check_feasible = false;
}
void core::init_search() {
@ -1192,11 +1193,7 @@ void core::negate_relation(new_lemma& lemma, unsigned j, const rational& a) {
}
bool core::conflict_found() const {
for (const auto & l : m_lemmas) {
if (l.is_conflict())
return true;
}
return false;
return any_of(m_lemmas, [&](const auto& l) { return l.is_conflict(); });
}
bool core::done() const {
@ -1555,7 +1552,7 @@ lbool core::check() {
bool run_bounded_nlsat = should_run_bounded_nlsat();
bool run_bounds = params().arith_nl_branching();
auto no_effect = [&]() { return !done() && m_lemmas.empty() && m_literals.empty(); };
auto no_effect = [&]() { return !done() && m_lemmas.empty() && m_literals.empty() && !m_check_feasible; };
if (no_effect())
m_monomial_bounds.propagate();
@ -1573,6 +1570,7 @@ lbool core::check() {
{1, check2},
{1, check3} };
check_weighted(3, checks);
if (!m_lemmas.empty() || !m_literals.empty())
return l_false;
}
@ -1610,7 +1608,7 @@ lbool core::check() {
lp_settings().stats().m_nra_calls++;
}
if (ret == l_undef && !m_lemmas.empty() && m_reslim.inc())
if (ret == l_undef && !no_effect() && m_reslim.inc())
ret = l_false;
lp_settings().stats().m_nla_lemmas += m_lemmas.size();

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

@ -87,6 +87,7 @@ class core {
intervals m_intervals;
monomial_bounds m_monomial_bounds;
unsigned m_conflicts;
bool m_check_feasible = false;
horner m_horner;
grobner m_grobner;
emonics m_emons;
@ -424,6 +425,7 @@ public:
vector<nla::ineq> const& literals() const { return m_literals; }
vector<equality> const& equalities() const { return m_equalities; }
vector<fixed_equality> const& fixed_equalities() const { return m_fixed_equalities; }
bool check_feasible() const { return m_check_feasible; }
void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e) { m_fixed_equalities.push_back({v, k, e}); }
void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e) { m_equalities.push_back({i, j, e}); }

6
src/math/lp/nla_grobner.cpp
View file

@ -401,9 +401,7 @@ namespace nla {
auto q = e.poly();
#if 0
// TODO: instead add a row to lra solver, make sure that make_feasible
// gets invoked (for example, bail out of final check).
#if 1
vector<std::pair<lp::mpq, unsigned>> coeffs;
while (!q.is_val()) {
coeffs.push_back({lc*q.hi().val(), q.var()});
@ -413,7 +411,7 @@ namespace nla {
lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX);
term_index = c().lra.map_term_index_to_column_index(term_index);
c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, -lc*q.val(), e.dep());
c().m_check_feasible = true;
#else
new_lemma lemma(m_core,"nla-linear");

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

@ -51,5 +51,6 @@ namespace nla {
vector<nla::ineq> const& literals() const;
vector<nla::fixed_equality> const& fixed_equalities() const;
vector<nla::equality> const& equalities() const;
bool check_feasible() const { return m_core->check_feasible(); }
};
}