mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

Remove old viable query

Browse source
This commit is contained in:
Jakob Rath 2023-12-07 14:38:28 +01:00
parent 970a68e749
commit 67237efa11
2 changed files with 3 additions and 126 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1161,7 +1161,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
@ -1438,7 +1438,7 @@ namespace polysat {
// - how to integrate fallback solver?
// when lowest level fails, we can try more refinement there.
// in case of refinement loop, try fallback solver with constraints only from lower level.
lbool viable::find_viable2_new(pvar v, rational& lo, rational& hi) {
lbool viable::find_viable2(pvar v, rational& lo, rational& hi) {
fixed_bits_info fbi;
if (!collect_bit_information(v, true, fbi))
@ -1873,114 +1873,6 @@ namespace polysat {
}
}
lbool viable::find_viable2(pvar v, rational& lo, rational& hi) {
fixed_bits_info fbi;
if (!collect_bit_information(v, true, fbi))
return l_false; // conflict already added
// max number of interval refinements before falling back to the univariate solver
unsigned const refinement_budget = 1000;
unsigned refinements = refinement_budget;
while (refinements--) {
lbool res = query_find(v, lo, hi, fbi);
IF_VERBOSE(10, {
if (refinements % 100 == 0)
verbose_stream() << "Refinements " << refinements << "\n";
});
if (res != l_undef)
return res;
}
IF_VERBOSE(10, verbose_stream() << "Fallback\n";);
LOG("Refinement budget exhausted! Fall back to univariate solver.");
pvar_vector overlaps;
overlaps.push_back(v);
return find_viable_fallback(v, overlaps, lo, hi);
}
lbool viable::query_find(pvar v, rational& lo, rational& hi, fixed_bits_info const& fbi) {
auto const& max_value = s.var2pdd(v).max_value();
lbool const refined = l_undef;
// After a refinement, any of the existing entries may have been replaced
// (if it is subsumed by the new entry created during refinement).
// For this reason, we start chasing the intervals from the start again.
lo = 0;
hi = max_value;
entry* e = m_units[v].get_entries(s.size(v)); // TODO: take other sizes into account
if (!e && !refine_viable<true>(v, lo, fbi))
return refined;
if (!e && !refine_viable<false>(v, hi, fbi))
return refined;
if (!e)
return l_true;
if (e->interval.is_full()) {
s.set_conflict_by_viable_interval(v);
return l_false;
}
entry* first = e;
entry* last = first->prev();
// quick check: last interval does not wrap around
// and has space for 2 unassigned values.
if (last->interval.lo_val() < last->interval.hi_val() &&
last->interval.hi_val() < max_value) {
lo = last->interval.hi_val();
if (!refine_viable<true>(v, lo, fbi))
return refined;
if (!refine_viable<false>(v, max_value, fbi))
return refined;
return l_true;
}
// find lower bound
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 (e->interval.currently_contains(lo)) {
s.set_conflict_by_viable_interval(v);
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;
do {
if (!e->interval.currently_contains(hi))
break;
hi = e->interval.lo_val() - 1;
e = e->prev();
}
while (e != last);
if (!refine_viable<true>(v, lo, fbi))
return refined;
if (!refine_viable<false>(v, hi, fbi))
return refined;
return l_true;
}
#endif
bool viable::set_conflict_by_fallback(pvar v, univariate_solver& us, svector<std::pair<pvar, sat::literal>> const& deps) {
auto& core = s.m_conflict;
core.init_viable_begin(v, false);

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

@ -187,19 +187,6 @@ namespace polysat {
void propagate(pvar v, rational const& val);
/**
* Interval-based queries
* @return l_true on success, l_false on conflict, l_undef on refinement
*/
lbool query_find(pvar v, rational& out_lo, rational& out_hi, fixed_bits_info const& fbi);
/**
* 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 find_viable2(pvar v, rational& out_lo, rational& out_hi);
/**
* Enter conflict state when intervals cover the full domain.
* Try to create the forbidden interval lemma for v.
@ -222,14 +209,12 @@ namespace polysat {
*/
bool set_conflict_by_fallback(pvar v, univariate_solver& us, svector<std::pair<pvar, sat::literal>> const& deps);
public:
/**
* 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 find_viable2_new(pvar v, rational& out_lo, rational& out_hi);
lbool find_viable2(pvar v, rational& out_lo, rational& out_hi);
lbool find_on_layers(
pvar v,