mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Simplify find_viable

Browse source
This commit is contained in:
Jakob Rath 2023-11-06 10:37:14 +01:00
parent f309dfeac7
commit 60a9472c8c
2 changed files with 24 additions and 71 deletions
Download patch file Download diff file Expand all files Collapse all files

61
src/math/polysat/viable.cpp
View file

@ -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<rational&, rational&> args{lo, hi};
return query<query_t::find_viable>(v, args);
}
bool viable::has_upper_bound(pvar v, rational& out_hi, vector<signed_constraint>& 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 <query_t mode>
lbool viable::query(pvar v, typename query_result<mode>::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<mode>(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 <query_t mode>
lbool viable::query_fallback(pvar v, typename query_result<mode>::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) {

34
src/math/polysat/viable.h
View file

@ -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 <query_t mode>
struct query_result {
};
template <>
struct query_result<query_t::find_viable> {
using result_t = std::pair<rational&, rational&>;
};
}
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 <viable_query::query_t mode>
lbool query(pvar v, typename viable_query::query_result<mode>::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 <viable_query::query_t mode>
lbool query_fallback(pvar v, typename viable_query::query_result<mode>::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