From fc676e235f12f83efaf43ad8c44639402afa356d Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 9 Nov 2023 15:03:14 +0100 Subject: [PATCH] fix some bugs, add unit test --- src/math/polysat/viable.cpp | 42 +++++++++++++++++++++++++++++++------ src/math/polysat/viable.h | 1 + src/test/viable.cpp | 25 ++++++++++++++++++++++ 3 files changed, 62 insertions(+), 6 deletions(-) diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 4c14c2dc4..6b25c4be5 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -273,6 +273,27 @@ namespace polysat { return true; } else { + unsigned const v_bits = s.size(v); + unsigned const coeff_parity = ne->coeff.parity(v_bits); + unsigned const lo_parity = ne->interval.lo_val().parity(v_bits); + unsigned const hi_parity = ne->interval.hi_val().parity(v_bits); + if (coeff_parity <= lo_parity && coeff_parity <= hi_parity && ne->coeff.is_power_of_two()) { + // reduction of coeff gives us a unit entry + ne->coeff = 1; + ne->interval = eval_interval::proper( + ne->interval.lo(), + machine_div2k(ne->interval.lo_val(), coeff_parity), + ne->interval.hi(), + machine_div2k(ne->interval.hi_val(), coeff_parity) + ); + ne->bit_width -= coeff_parity; + LOG("reduced entry to unit in width " << ne->bit_width); + return intersect(v, ne); + } + + // TODO: later, can reduce according to shared_parity + // unsigned const shared_parity = std::min(coeff_parity, std::min(lo_parity, hi_parity)); + insert(ne, v, m_equal_lin, entry_kind::equal_e); return true; } @@ -1089,7 +1110,7 @@ namespace polysat { find_t viable::find_viable(pvar v, rational& lo) { rational hi; - switch (find_viable2_new(v, lo, hi)) { + switch (find_viable2(v, lo, hi)) { case l_true: if (hi < 0) { // fallback solver, treat propagations as decisions for now @@ -1399,14 +1420,22 @@ namespace polysat { for (unsigned w : widths_set) { widths.push_back(w); } + LOG("widths: " << widths); - lbool result_lo = find_on_layer(widths.size() - 1, widths, overlaps, fbi, rational::zero(), s.var2pdd(v).max_value(), lo); + rational const& max_value = s.var2pdd(v).max_value(); + + lbool result_lo = find_on_layer(widths.size() - 1, widths, overlaps, fbi, rational::zero(), max_value, lo); if (result_lo == l_false) return l_false; // conflict if (result_lo == l_undef) return l_undef; - lbool result_hi = find_on_layer(widths.size() - 1, widths, overlaps, fbi, lo, s.var2pdd(v).max_value(), hi); + if (lo == max_value) { + hi = lo; + return l_true; + } + + lbool result_hi = find_on_layer(widths.size() - 1, widths, overlaps, fbi, lo + 1, max_value, hi); if (result_hi == l_false) hi = lo; // no other viable value if (result_hi == l_undef) @@ -1419,7 +1448,8 @@ namespace polysat { // The bool component indicates whether the returned interval contains 'val'. std::pair viable::find_value(rational const& val, entry* entries) { SASSERT(entries); - SASSERT(well_formed(entries)); + // display_all(std::cerr << "entries:\n\t", 0, entries, "\n\t"); + // SASSERT(well_formed(entries)); // SASSERT(!limit || entry::contains(entries, limit)); // if (!limit) // limit = entries; @@ -1475,7 +1505,7 @@ namespace polysat { for (pvar x : overlaps) { if (s.size(x) < w) // note that overlaps are sorted by variable size descending break; - if (entry* e = m_units[x].get_entries(s.size(x))) { + if (entry* e = m_units[x].get_entries(w)) { entry_cursor ec; ec.cur = e; // ec.first = nullptr; @@ -1555,7 +1585,7 @@ namespace polysat { // replace lower bits of 'val' by 'a' val = val - lower_cover_lo + a; - SASSERT(distance(val, to_cover_hi, mod_value) < distance(next_val, to_cover_hi, mod_value)); + SASSERT(distance(val, to_cover_hi, mod_value) >= distance(next_val, to_cover_hi, mod_value)); if (result == l_true) return l_true; // done diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index ccfae347a..cf23546d2 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -200,6 +200,7 @@ namespace polysat { +public: lbool find_viable2_new(pvar v, rational& out_lo, rational& out_hi); lbool find_on_layer(unsigned w_idx, unsigned_vector const& widths, pvar_vector const& overlaps, fixed_bits_info const& fbi, rational const& to_cover_lo, rational const& to_cover_hi, rational& out_val); diff --git a/src/test/viable.cpp b/src/test/viable.cpp index 7eb286587..d27f372c2 100644 --- a/src/test/viable.cpp +++ b/src/test/viable.cpp @@ -135,6 +135,30 @@ namespace polysat { test_intervals(3, intervals); } + static void test3() { + scoped_solverv s; + auto xv = s.add_var(64); + auto x = s.var(xv); + viable& v = s.v(); + rational val; + + rational const two_to_60 = rational::power_of_two(60); + + s.add_ule(5000, x); + VERIFY_EQ(s.check_sat(), l_true); + rational lo, hi; + std::cout << "find_viable: " << v.find_viable2_new(xv, lo, hi) << "\n"; + std::cout << " lo: " << lo << "\n"; + std::cout << " hi: " << hi << "\n"; + + // 10 < x[3:0] + s.add_ule(10 * two_to_60, x * two_to_60); + VERIFY_EQ(s.check_sat(), l_true); + std::cout << "find_viable: " << v.find_viable2_new(xv, lo, hi) << "\n"; + std::cout << " lo: " << lo << "\n"; + std::cout << " hi: " << hi << "\n"; + } + static void test_univariate() { std::cout << "\ntest_univariate\n"; unsigned const bw = 32; @@ -457,6 +481,7 @@ void tst_viable() { polysat::test_univariate(); polysat::test_univariate_minmax(); polysat::test2(); + polysat::test3(); polysat::test_fi::exhaustive(); polysat::test_fi::randomized(10000, 16); polysat::test_fi::randomized(1000, 256);