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 condition that degree is reduced

Browse source
This commit is contained in:
Jakob Rath 2021-09-09 10:54:33 +02:00
parent 611c28fc47
commit ec882d10da
2 changed files with 40 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -31,6 +31,10 @@ namespace polysat {
pdd r = a; pdd r = a;
if (!a.resolve(v, b, r) && !b.resolve(v, a, r)) if (!a.resolve(v, b, r) && !b.resolve(v, a, r))
return {}; return {};
// Only keep result if the degree in c2 was reduced.
// (this condition might be too strict, but we use it for now to prevent looping)
if (b.degree(v) >= r.degree(v))
return {};
unsigned const lvl = std::max(c1->level(), c2->level()); unsigned const lvl = std::max(c1->level(), c2->level());
signed_constraint c = cm().eq(lvl, r); signed_constraint c = cm().eq(lvl, r);
LOG("resolved: " << c << " currently false? " << c.is_currently_false(s())); LOG("resolved: " << c << " currently false? " << c.is_currently_false(s()));
@ -43,9 +47,9 @@ namespace polysat {
return c.is_positive() && c->is_eq() && c->contains_var(v); return c.is_positive() && c->is_eq() && c->contains_var(v);
} }
// TODO(later): check superposition into disequality again (see notes) // c2 ... constraint that is currently false
// true = done, false = abort, undef = continue // Try to replace it with a new false constraint (derived from superposition with a true constraint)
lbool ex_polynomial_superposition::try_explain1(pvar v, conflict_core& core) { signed_constraint ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict_core& core) {
for (auto it1 = core.begin(); it1 != core.end(); ++it1) { for (auto it1 = core.begin(); it1 != core.end(); ++it1) {
signed_constraint c1 = *it1; signed_constraint c1 = *it1;
if (!is_positive_equality_over(v, c1)) if (!is_positive_equality_over(v, c1))
@ -53,27 +57,40 @@ namespace polysat {
if (!c1.is_currently_true(s())) if (!c1.is_currently_true(s()))
continue; continue;
for (auto it2 = core.begin(); it2 != core.end(); ++it2) { signed_constraint c = resolve1(v, c1, c2);
signed_constraint c2 = *it2; if (!c)
if (!is_positive_equality_over(v, c2)) continue;
continue; vector<signed_constraint> premises;
if (!c2.is_currently_false(s())) premises.push_back(c1);
continue; premises.push_back(c2);
core.replace(c2, c, std::move(premises));
return c;
}
return {};
}
signed_constraint c = resolve1(v, c1, c2); // TODO(later): check superposition into disequality again (see notes)
if (!c) // true = done, false = abort, undef = continue
continue; lbool ex_polynomial_superposition::try_explain1(pvar v, conflict_core& core) {
vector<signed_constraint> premises; for (auto it2 = core.begin(); it2 != core.end(); ++it2) {
premises.push_back(c1); signed_constraint c2 = *it2;
premises.push_back(c2); if (!is_positive_equality_over(v, c2))
core.replace(c2, c, std::move(premises)); continue;
if (!c->contains_var(v)) { if (!c2.is_currently_false(s()))
core.keep(c); continue;
core.remove_var(v);
return l_true; // TODO: can try multiple replacements at once; then the it2 loop needs to be done only once... (requires some reorganization for storing the premises)
} else signed_constraint c = find_replacement(c2, v, core);
return l_undef; if (!c)
continue;
if (!c->contains_var(v)) {
core.keep(c);
core.remove_var(v);
return l_true;
} }
else
return l_undef;
} }
return l_false; return l_false;
} }

1
src/math/polysat/explain.h
View file

@ -38,6 +38,7 @@ namespace polysat {
private: private:
bool is_positive_equality_over(pvar v, signed_constraint const& c); bool is_positive_equality_over(pvar v, signed_constraint const& c);
signed_constraint resolve1(pvar v, signed_constraint c1, signed_constraint c2); signed_constraint resolve1(pvar v, signed_constraint c1, signed_constraint c2);
signed_constraint find_replacement(signed_constraint c2, pvar v, conflict_core& core);
lbool try_explain1(pvar v, conflict_core& core); lbool try_explain1(pvar v, conflict_core& core);
public: public:
bool try_explain(pvar v, conflict_core& core) override; bool try_explain(pvar v, conflict_core& core) override;