mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

add max forbidden based on constant intervals

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-27 20:49:17 -08:00
parent 45e772b223
commit 6f8b3a997e
2 changed files with 52 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -722,6 +722,52 @@ namespace polysat {
return !out_c.empty(); return !out_c.empty();
} }
bool viable::has_max_forbidden(pvar v, rational& out_lo, rational& out_hi, vector<signed_constraint>& out_c) {
out_c.reset();
entry const* first = m_units[v];
entry const* e = first;
bool found = false;
do {
found = false;
do {
if (e->refined)
goto next;
auto const& lo = e->interval.lo();
auto const& hi = e->interval.hi();
if (!lo.is_val() || !hi.is_val())
goto next;
if (out_c.empty()) {
out_c.push_back(e->src);
out_lo = lo.val();
out_hi = hi.val();
found = true;
}
// [lo, hi0, hi[
// [lo, hi0, 0, hi[
else if (lo.val() <= out_hi && (out_hi < hi.val() || hi.val() < lo.val())) {
out_c.push_back(e->src);
out_hi = hi.val();
found = true;
}
// [lo, lo0, hi[
// [lo, 0, lo0, hi[
else if (lo.val() < out_lo && (out_lo <= hi.val() || hi.val() < lo.val())) {
out_c.push_back(e->src);
out_lo = lo.val();
found = true;
}
next:
e = e->next();
}
while (e != first);
}
while (found);
return !out_c.empty();
}
template <query_t mode> template <query_t mode>
lbool viable::query(pvar v, typename query_result<mode>::result_t& result) { lbool viable::query(pvar v, typename query_result<mode>::result_t& result) {
// max number of interval refinements before falling back to the univariate solver // max number of interval refinements before falling back to the univariate solver

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

@ -197,6 +197,12 @@ namespace polysat {
*/ */
bool has_lower_bound(pvar v, rational& out_lo, vector<signed_constraint>& out_c); bool has_lower_bound(pvar v, rational& out_lo, vector<signed_constraint>& out_c);
/**
* Query for a maximal interval based on fixed bounds where v is forbidden.
*/
bool has_max_forbidden(pvar v, rational& out_lo, rational& out_hi, vector<signed_constraint>& out_c);
/** /**
* Find a next viable value for variable. * Find a next viable value for variable.
*/ */