diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index af93c0d26..62d570120 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -1446,14 +1446,6 @@ namespace { return query(v, args); } - lbool viable::min_viable(pvar v, rational& lo) { - return query(v, lo); - } - - lbool viable::max_viable(pvar v, rational& hi) { - return query(v, hi); - } - 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; @@ -1707,10 +1699,6 @@ namespace { if constexpr (mode == query_t::find_viable) res = query_find(v, result.first, result.second, fbi); - else if constexpr (mode == query_t::min_viable) - res = query_min(v, result, fbi); - else if constexpr (mode == query_t::max_viable) - res = query_max(v, result, fbi); else if constexpr (mode == query_t::has_viable) { NOT_IMPLEMENTED_YET(); } @@ -1800,54 +1788,6 @@ namespace { return l_true; } - lbool viable::query_min(pvar v, rational& lo, fixed_bits_info const& fbi) { - // TODO: should be able to deal with UNSAT case; since also min_viable has to deal with it due to fallback solver - lo = 0; - entry* e = m_units[v].get_entries(s.size(v)); // TODO: take other sizes into account - if (!e && !refine_viable(v, lo, fbi)) - return l_undef; - if (!e) - return l_true; - entry* first = e; - entry* last = first->prev(); - if (last->interval.currently_contains(lo)) - lo = last->interval.hi_val(); - do { - if (!e->interval.currently_contains(lo)) - break; - lo = e->interval.hi_val(); - e = e->next(); - } - while (e != first); - if (!refine_viable(v, lo, fbi)) - return l_undef; - SASSERT(is_viable(v, lo)); - return l_true; - } - - lbool viable::query_max(pvar v, rational& hi, fixed_bits_info const& fbi) { - // TODO: should be able to deal with UNSAT case; since also max_viable has to deal with it due to fallback solver - hi = s.var2pdd(v).max_value(); - entry* e = m_units[v].get_entries(s.size(v)); // TODO: take other sizes into account - if (!e && !refine_viable(v, hi, fbi)) - return l_undef; - if (!e) - return l_true; - entry* last = e->prev(); - e = last; - do { - if (!e->interval.currently_contains(hi)) - break; - hi = e->interval.lo_val() - 1; - e = e->prev(); - } - while (e != last); - if (!refine_viable(v, hi, fbi)) - return l_undef; - SASSERT(is_viable(v, hi)); - return l_true; - } - template lbool viable::query_fallback(pvar v, typename query_result::result_t& result) { unsigned const bit_width = s.size(v); @@ -1917,12 +1857,6 @@ namespace { if constexpr (mode == query_t::find_viable) return query_find_fallback(v, *us, result.first, result.second); - if constexpr (mode == query_t::min_viable) - return query_min_fallback(v, *us, result); - - if constexpr (mode == query_t::max_viable) - return query_max_fallback(v, *us, result); - if constexpr (mode == query_t::has_viable) { NOT_IMPLEMENTED_YET(); return l_undef; @@ -1939,14 +1873,6 @@ namespace { // return us.find_two(lo, hi) ? l_true : l_undef; } - lbool viable::query_min_fallback(pvar v, univariate_solver& us, rational& lo) { - return us.find_min(lo) ? l_true : l_undef; - } - - lbool viable::query_max_fallback(pvar v, univariate_solver& us, rational& hi) { - return us.find_max(hi) ? l_true : l_undef; - } - bool viable::resolve_fallback(pvar v, univariate_solver& us, conflict& core) { // The conflict is the unsat core of the univariate solver, // and the current assignment (under which the constraints are univariate in v) diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index dfcc3c848..196edac17 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -46,8 +46,6 @@ namespace polysat { namespace viable_query { enum class query_t { has_viable, // currently only used internally in resolve_viable - min_viable, // currently unused - max_viable, // currently unused find_viable, }; @@ -55,16 +53,6 @@ namespace polysat { struct query_result { }; - template <> - struct query_result { - using result_t = rational; - }; - - template <> - struct query_result { - using result_t = rational; - }; - template <> struct query_result { using result_t = std::pair; @@ -212,8 +200,6 @@ namespace polysat { * Interval-based queries * @return l_true on success, l_false on conflict, l_undef on refinement */ - lbool query_min(pvar v, rational& out_lo, fixed_bits_info const& fbi); - lbool query_max(pvar v, rational& out_hi, fixed_bits_info const& fbi); lbool query_find(pvar v, rational& out_lo, rational& out_hi, fixed_bits_info const& fbi); /** @@ -221,8 +207,6 @@ namespace polysat { * The univariate solver has already been filled with all relevant constraints and check() returned l_true. * @return l_true on success, l_false on conflict, l_undef on resource limit */ - lbool query_min_fallback(pvar v, univariate_solver& us, rational& out_lo); - lbool query_max_fallback(pvar v, univariate_solver& us, rational& out_hi); lbool query_find_fallback(pvar v, univariate_solver& us, rational& out_lo, rational& out_hi); /** @@ -275,19 +259,6 @@ namespace polysat { */ bool is_viable(pvar v, rational const& val); - /** - * Extract min viable value for v. - * @return l_true on success, l_false on conflict, l_undef on resource limit - */ - lbool min_viable(pvar v, rational& out_lo); - - /** - * Extract max viable value for v. - * @return l_true on success, l_false on conflict, l_undef on resource limit - */ - lbool max_viable(pvar v, rational& out_hi); - - /** * Query for an upper bound literal for v together with justification. * On success, the conjunction of out_c implies v <= out_hi.