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

hack to avoid wrong propagation justifications due to fallback solver

Browse source
This commit is contained in:
Jakob Rath 2023-03-10 12:42:00 +01:00
parent ffb7b5f85d
commit 538c4ee25f
2 changed files with 15 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1343,8 +1343,13 @@ namespace {
find_t viable::find_viable(pvar v, rational& lo) {
rational hi;
switch (find_viable(v, lo, hi)) {
switch (find_viable2(v, lo, hi)) {
case l_true:
if (hi < 0) {
// fallback solver, treat propagations as decisions for now
// (this is because the propagation justification currently always uses intervals, which is unsound in this case)
return find_t::multiple;
}
return (lo == hi) ? find_t::singleton : find_t::multiple;
case l_false:
return find_t::empty;
@ -1353,7 +1358,7 @@ namespace {
}
}
lbool viable::find_viable(pvar v, rational& lo, rational& hi) {
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);
}
@ -1789,7 +1794,10 @@ namespace {
}
lbool viable::query_find_fallback(pvar v, univariate_solver& us, rational& lo, rational& hi) {
return us.find_two(lo, hi) ? l_true : l_undef;
lo = us.model();
hi = -1;
return l_true;
// return us.find_two(lo, hi) ? l_true : l_undef;
}
lbool viable::query_min_fallback(pvar v, univariate_solver& us, rational& lo) {
@ -1817,7 +1825,6 @@ namespace {
SASSERT(!core.vars().contains(v));
core.add_lemma("viable unsat core", core.build_lemma());
verbose_stream() << "unsat core " << core << "\n";
//exit(0);
return true;
}

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

@ -225,11 +225,14 @@ namespace polysat {
*/
find_t find_viable(pvar v, rational& out_val);
private:
/**
* 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_viable(pvar v, rational& out_lo, rational& out_hi);
lbool find_viable2(pvar v, rational& out_lo, rational& out_hi);
public:
#if 0
void make_bit_justification(pvar v);