From 60a9472c8c3e40c288d15dcbcee7149581619c54 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 6 Nov 2023 10:37:14 +0100 Subject: [PATCH] Simplify find_viable --- src/math/polysat/viable.cpp | 61 +++++++++++-------------------------- src/math/polysat/viable.h | 34 ++++----------------- 2 files changed, 24 insertions(+), 71 deletions(-) diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index 62d570120..24941fad5 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -35,8 +35,6 @@ TODO: plan to fix the FI "pumping": namespace polysat { - using namespace viable_query; - struct inf_fi : public inference { viable& v; pvar var; @@ -1441,11 +1439,6 @@ namespace { } } - lbool viable::find_viable2(pvar v, rational& lo, rational& hi) { - std::pair args{lo, hi}; - return query(v, args); - } - bool viable::has_upper_bound(pvar v, rational& out_hi, vector& out_c) { entry const* first = m_units[v].get_entries(s.size(v)); // TODO: take other sizes into account entry const* e = first; @@ -1618,8 +1611,7 @@ namespace { } - template - lbool viable::query(pvar v, typename query_result::result_t& result) { + lbool viable::find_viable2(pvar v, rational& lo, rational& hi) { fixed_bits_info fbi; @@ -1695,16 +1687,7 @@ namespace { unsigned refinements = refinement_budget; while (refinements--) { - lbool res = l_undef; - - if constexpr (mode == query_t::find_viable) - res = query_find(v, result.first, result.second, fbi); - else if constexpr (mode == query_t::has_viable) { - NOT_IMPLEMENTED_YET(); - } - else { - UNREACHABLE(); - } + lbool res = query_find(v, lo, hi, fbi); IF_VERBOSE(10, { if (refinements % 100 == 0) verbose_stream() << "Refinements " << refinements << "\n"; @@ -1714,7 +1697,8 @@ namespace { } IF_VERBOSE(10, verbose_stream() << "Fallback\n";); LOG("Refinement budget exhausted! Fall back to univariate solver."); - return query_fallback(v, result); + + return find_viable_fallback(v, lo, hi); } lbool viable::query_find(pvar v, rational& lo, rational& hi, fixed_bits_info const& fbi) { @@ -1770,6 +1754,14 @@ namespace { return l_false; } + // TODO: we could also try to continue the search at lo+1, if we get stuck at the upper bound. + + // TODO: we only need (any) 2 viable values. some possibilities: + // - find lower and upper bound + // - find lower bound and next lowest value + // - find upper bound and next highest value + // - try a random sample and chase value from there + // find upper bound hi = max_value; e = last; @@ -1788,14 +1780,13 @@ namespace { return l_true; } - template - lbool viable::query_fallback(pvar v, typename query_result::result_t& result) { + lbool viable::find_viable_fallback(pvar v, rational& lo, rational& hi) { unsigned const bit_width = s.size(v); univariate_solver* us = s.m_viable_fallback.usolver(bit_width); sat::literal_set added; // First step: only query the looping constraints and see if they alone are already UNSAT. - // The constraints which caused the refinement loop will be reached from m_units. + // The constraints which caused the refinement loop can always be reached from m_units. LOG_H3("Checking looping univariate constraints for v" << v << "..."); LOG("Assignment: " << assignments_pp(s)); entry const* first = m_units[v].get_entries(s.size(v)); // TODO: take other sizes into account @@ -1847,30 +1838,14 @@ namespace { s.set_conflict_by_viable_fallback(v, *us); return l_false; case l_true: - // pass solver to mode-specific query - break; + lo = us->model(); + hi = -1; + return l_true; + // TODO: return us.find_two(lo, hi) ? l_true : l_undef; ??? default: // resource limit return l_undef; } - - if constexpr (mode == query_t::find_viable) - return query_find_fallback(v, *us, result.first, result.second); - - if constexpr (mode == query_t::has_viable) { - NOT_IMPLEMENTED_YET(); - return l_undef; - } - - UNREACHABLE(); - return l_undef; - } - - lbool viable::query_find_fallback(pvar v, univariate_solver& us, rational& lo, rational& hi) { - lo = us.model(); - hi = -1; - return l_true; - // return us.find_two(lo, hi) ? l_true : l_undef; } bool viable::resolve_fallback(pvar v, univariate_solver& us, conflict& core) { diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index 196edac17..e10a846c5 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -43,22 +43,6 @@ namespace polysat { std::ostream& operator<<(std::ostream& out, find_t x); - namespace viable_query { - enum class query_t { - has_viable, // currently only used internally in resolve_viable - find_viable, - }; - - template - struct query_result { - }; - - template <> - struct query_result { - using result_t = std::pair; - }; - } - class viable { friend class test_fi; friend class test_polysat; @@ -203,25 +187,17 @@ namespace polysat { lbool query_find(pvar v, rational& out_lo, rational& out_hi, fixed_bits_info const& fbi); /** - * Bitblasting-based queries. - * The univariate solver has already been filled with all relevant constraints and check() returned l_true. + * Find a next viable value for variable. Attempts to find two different values, to distinguish propagation/decision. + * NOTE: out_hi is set to -1 by the fallback solver. * @return l_true on success, l_false on conflict, l_undef on resource limit */ - lbool query_find_fallback(pvar v, univariate_solver& us, rational& out_lo, rational& out_hi); - - /** - * Interval-based query with bounded refinement and fallback to bitblasting. - * @return l_true on success, l_false on conflict, l_undef on resource limit - */ - template - lbool query(pvar v, typename viable_query::query_result::result_t& out_result); + lbool find_viable2(pvar v, rational& out_lo, rational& out_hi); /** * Bitblasting-based query. * @return l_true on success, l_false on conflict, l_undef on resource limit */ - template - lbool query_fallback(pvar v, typename viable_query::query_result::result_t& out_result); + lbool find_viable_fallback(pvar v, rational& out_lo, rational& out_hi); public: viable(solver& s); @@ -291,6 +267,8 @@ namespace polysat { * @return l_true on success, l_false on conflict, l_undef on resource limit */ lbool find_viable2(pvar v, rational& out_lo, rational& out_hi); + + lbool find_viable_fallback(pvar v, rational& out_lo, rational& out_hi); public: #if 0