mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-22 13:41:27 +00:00
Code Activity

enable bound tracking

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-19 10:53:42 -08:00
parent 5de01e5d1d
commit 5d316a51d1
2 changed files with 24 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/lp/nra_solver.cpp
View file

@ -156,7 +156,7 @@ struct solver::imp {
unsigned sz = m_model_bounds.size();
m_model_bounds.push_back({v, value, true});
m_model_bounds.push_back({v, value, false});
m_nlsat->track_model_value(v, value, this + sz, this + sz + 1);
m_nlsat->track_model_value(lp2nl(v), value, this + sz, this + sz + 1);
}
}
@ -255,6 +255,7 @@ struct solver::imp {
else {
idx -= m_max_constraint_index;
auto const& [v, bound, is_lower] = m_model_bounds[idx];
TRACE(nra, tout << "bound violated for v" << v << (is_lower ? " >= " : " <= ") << bound << "\n");
if (is_lower)
lemma |= nla::ineq(v, lp::lconstraint_kind::LE, bound - 1);
else

41
src/nlsat/nlsat_solver.cpp
View file

@ -1920,34 +1920,37 @@ namespace nlsat {
<< " :learned " << m_learned.size() << ")\n");
#if 0
// todo, review, test
// cut on the first model value
if (!m_model_values.empty()) {
bool found = false;
for (auto const &[x, bound] : bounds) {
random_gen r(++m_random_seed);
auto const &[x, bound] = bounds[r(bounds.size())];
for (auto const &[mx, mvalue, lo, hi] : m_model_values) {
if (mx == x) {
polynomial_ref p(m_pm);
rational one(1);
bool is_even = false;
p = m_pm.mk_linear(1, &one, &x, mvalue);
auto* p1 = p.get();
if (mvalue < bound) {
mk_external_clause(1, &mk_ineq_literal(atom::GT, 1, &p1, &is_even), assumption(lo));
}
else {
mk_external_clause(1, &mk_ineq_literal(atom::LT, 1, &p1, &is_even), assumption(hi));
}
found = true;
break;
if (mx == x) {
polynomial_ref p(m_pm);
rational one(1);
bool is_even = false;
p = m_pm.mk_linear(1, &one, &x, -mvalue); // x - mvalue
auto *p1 = p.get();
if (mvalue < bound) {
// assert x <= mvalue
// <=>
// ~ (x > mvalue)
// assumption hi
auto lit = ~mk_ineq_literal(atom::GT, 1, &p1, &is_even);
mk_external_clause(1, &lit, assumption(hi));
}
}
if (found)
else {
auto lit = ~mk_ineq_literal(atom::LT, 1, &p1, &is_even);
mk_external_clause(1, &lit, assumption(lo));
}
found = true;
break;
}
}
continue;
}
#endif
for (auto const& b : bounds) {
var x = b.first;
rational lo = b.second;