From f1f5b9e3110b7b0f6de152af585d65165541de85 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Aug 2021 21:40:23 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/math/polysat/fixplex_def.h | 52 +++++++++++++++++++++------------- src/math/polysat/log.cpp | 4 ++- src/test/fixplex.cpp | 42 ++++++++++++++++++--------- 3 files changed, 64 insertions(+), 34 deletions(-) diff --git a/src/math/polysat/fixplex_def.h b/src/math/polysat/fixplex_def.h index 6a5db1ef7..bdc59d85e 100644 --- a/src/math/polysat/fixplex_def.h +++ b/src/math/polysat/fixplex_def.h @@ -530,27 +530,34 @@ namespace polysat { void fixplex::set_bounds(var_t v, numeral const& l, numeral const& h, unsigned dep) { ensure_var(v); update_bounds(v, l, h, mk_leaf(dep)); + } + + template + void fixplex::update_bounds(var_t v, numeral const& l, numeral const& h, u_dependency* dep) { + if (inconsistent()) + return; + auto lo0 = m_vars[v].lo; + auto hi0 = m_vars[v].hi; + m_stashed_bounds.push_back(stashed_bound(v, m_vars[v])); + m_trail.push_back(trail_i::set_bound_i); + std::cout << "new bound " << v << " " << m_vars[v] << " " << mod_interval(l, h) << " -> "; + m_vars[v] &= mod_interval(l, h); + if (lo0 != m_vars[v].lo) + m_vars[v].m_lo_dep = dep; + if (hi0 != m_vars[v].hi) + m_vars[v].m_hi_dep = dep; + std::cout << m_vars[v] << "\n"; + if (m_vars[v].is_empty()) { + conflict(m_vars[v].m_lo_dep, m_vars[v].m_hi_dep); + return; + } if (in_bounds(v)) return; if (is_base(v)) add_patch(v); else update_value(v, value2delta(v, value(v))); - } - - template - void fixplex::update_bounds(var_t v, numeral const& l, numeral const& h, u_dependency* dep) { - auto lo0 = m_vars[v].lo; - auto hi0 = m_vars[v].hi; - m_stashed_bounds.push_back(stashed_bound(v, m_vars[v])); - m_trail.push_back(trail_i::set_bound_i); - // std::cout << "new bound " << x << " " << m_vars[x] << " " << mod_interval(l, h) << " -> "; - m_vars[v] &= mod_interval(l, h); - if (lo0 != m_vars[v].lo) - m_vars[v].m_lo_dep = dep; - if (hi0 != m_vars[v].hi) - m_vars[v].m_hi_dep = dep; - // std::cout << m_vars[x] << "\n"; + SASSERT(in_bounds(v)); } template @@ -1155,6 +1162,8 @@ namespace polysat { template lbool fixplex::propagate_ineqs(ineq const& i0) { numeral old_lo = m_vars[i0.w].lo; + SASSERT(!m_inconsistent); + std::cout << "propagate " << i0 << "\n"; if (!propagate_ineq(i0)) return l_false; if (old_lo == m_vars[i0.w].lo) @@ -1172,6 +1181,9 @@ namespace polysat { auto& i_out = m_ineqs[ineqs[ineq_out]]; if (i.w != i_out.v) continue; + for (unsigned j = 0; j < stack.size(); ++j) + std::cout << " "; + std::cout << " -> " << i_out << "\n"; old_lo = m_vars[i_out.w].lo; if (!propagate_ineq(i_out)) return l_false; @@ -1501,10 +1513,11 @@ namespace polysat { template bool fixplex::new_bound(ineq const& i, var_t x, numeral const& l, numeral const& h, u_dependency* a, u_dependency* b, u_dependency* c, u_dependency* d) { bool was_fixed = lo(x) + 1 == hi(x); + SASSERT(!inconsistent()); u_dependency* dep = m_deps.mk_join(mk_leaf(i.dep), m_deps.mk_join(a, m_deps.mk_join(b, m_deps.mk_join(c, d)))); update_bounds(x, l, h, dep); - if (m_vars[x].is_empty()) - return conflict(m_vars[x].m_lo_dep, m_vars[x].m_hi_dep), false; + if (inconsistent()) + return false; else if (!was_fixed && lo(x) + 1 == hi(x)) { // TBD: track based on inequality not row // fixed_var_eh(r, x); @@ -1516,11 +1529,12 @@ namespace polysat { bool fixplex::new_bound(row const& r, var_t x, mod_interval const& range) { if (range.is_free()) return l_true; + SASSERT(!inconsistent()); bool was_fixed = lo(x) + 1 == hi(x); update_bounds(x, range.lo, range.hi, row2dep(r)); IF_VERBOSE(0, verbose_stream() << "new-bound v" << x << " " << m_vars[x] << "\n"); - if (m_vars[x].is_empty()) - return conflict(m_vars[x].m_lo_dep, m_vars[x].m_hi_dep), false; + if (inconsistent()) + return false; else if (!was_fixed && lo(x) + 1 == hi(x)) fixed_var_eh(r, x); return true; diff --git a/src/math/polysat/log.cpp b/src/math/polysat/log.cpp index 70ebb1a8d..96d987548 100644 --- a/src/math/polysat/log.cpp +++ b/src/math/polysat/log.cpp @@ -68,7 +68,9 @@ std::pair polysat_log(LogLevel msg_level, std::string fn, s std::ostream& os = std::cerr; size_t width = 20; - size_t padding = width - std::min(width, fn.size()); + size_t padding = 0; + if (width > fn.size()) + padding = width - fn.size(); char const* color = nullptr; color = level_color(msg_level); #ifdef _MSC_VER diff --git a/src/test/fixplex.cpp b/src/test/fixplex.cpp index 5240c605c..46e0ba859 100644 --- a/src/test/fixplex.cpp +++ b/src/test/fixplex.cpp @@ -420,11 +420,9 @@ namespace polysat { solver.assert_expr(bv.mk_ule(variables.get(i.v), variables.get(i.w))); } } - unsigned v = 0; - for (auto const& b : bounds) { + for (unsigned v = 0; v < bounds.size(); ++v) { + auto const& b = bounds[v]; ++index; - if (b.is_free()) - continue; fp.set_bounds(v, rational(b.lo, rational::ui64()), rational(b.hi, rational::ui64()), index); @@ -439,31 +437,31 @@ namespace polysat { solver.assert_expr(m.mk_or(A, B)); } - solver.display(std::cout); - std::cout << fp << "\n"; - lbool r1 = solver.check(); lbool r2 = fp.make_feasible(); - std::cout << r1 << " " << r2 << "\n" << fp << "\n"; + std::cout << r1 << " " << r2 << "\n"; + +#define VALIDATE(_test_) if (!(_test_)) { std::cout << "failed " << #_test_ << "\n"; solver.display(std::cout << fp << "\n"); SASSERT(false);} if (r2 == l_true) { for (auto const& row : rows) { uint64_t sum = 0; for (auto col : row) sum += col.second * fp.value(col.first); - SASSERT(sum == 0); + VALIDATE(sum == 0); } for (unsigned i = 0; i < bounds.size(); ++i) { uint64_t val = fp.value(i); uint64_t lo = bounds[i].lo; uint64_t hi = bounds[i].hi; - SASSERT(!(lo < hi || hi == 0) || lo <= val && val < hi); - SASSERT(!(hi > lo) || val < hi || lo <= val); + VALIDATE(!(lo < hi) || (lo <= val && val < hi)); + VALIDATE(!(0 < lo && hi == 0) || lo <= val); + VALIDATE(!(hi > lo) || val < hi || lo <= val); } for (auto const& i : ineqs) { - SASSERT(fp.value(i.v) <= fp.value(i.w)); - SASSERT(!i.strict || fp.value(i.v) < fp.value(i.w)); + VALIDATE(fp.value(i.v) <= fp.value(i.w)); + VALIDATE(!i.strict || fp.value(i.v) < fp.value(i.w)); } } if (r1 == r2) { @@ -480,7 +478,17 @@ namespace polysat { std::cout << fp << "\n"; } else { + std::cout << r2 << " missed with verdict " << r1 << "\n"; + std::cout << fp << "\n"; + + if (r1 == l_false && false && rows.empty()) { + std::cout << "BUG should not miss unsat verdict when there are no rows\n"; + solver.display(std::cout); + std::cout << "\n"; + std::cout << fp << "\n"; + SASSERT(false); + } } } @@ -503,8 +511,14 @@ namespace polysat { svector> row; uint64_t coeff = (r() % 2 == 0) ? r() % 100 : (0 - r() % 10); row.push_back(std::make_pair(i, coeff)); + uint_set seen; for (unsigned j = 0; j + 1 < num_vars_per_row; ++j) { - var_t v = (r() % (num_vars - num_vars_per_row)) + num_vars_per_row; + var_t v; + do { + v = (r() % (num_vars - num_vars_per_row)) + num_vars_per_row; + } + while (seen.contains(v)); + seen.insert(v); coeff = (r() % 2 == 0) ? r() % 100 : (0 - r() % 10); row.push_back(std::make_pair(v, coeff)); }