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

throttle on degree bounds

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-10-13 20:04:21 +02:00
parent 7036dd826f
commit e711808d3e
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -41,15 +41,22 @@ namespace polysat {
LOG("c2: " << c2); LOG("c2: " << c2);
pdd a = c1.eq(); pdd a = c1.eq();
pdd b = c2.eq(); pdd b = c2.eq();
unsigned degree_a = a.degree();
unsigned degree_b = b.degree();
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 {};
unsigned degree_r = r.degree();
if (degree_a < degree_r && degree_b < degree_r)
return {};
// Only keep result if the degree in c2 was reduced. // 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) // (this condition might be too strict, but we use it for now to prevent looping)
// TODO: check total degree; only keep if total degree smaller or equal. // TODO: check total degree; only keep if total degree smaller or equal.
// can always do this if c1 is linear. // can always do this if c1 is linear.
if (b.degree(v) <= r.degree(v)) if (b.degree(v) <= r.degree(v))
return {}; return {};
if (a.degree(v) <= r.degree(v))
return {};
signed_constraint c = s.eq(r); signed_constraint c = s.eq(r);
LOG("resolved: " << c << " currently false? " << c.is_currently_false(s)); LOG("resolved: " << c << " currently false? " << c.is_currently_false(s));
if (!c.is_currently_false(s)) if (!c.is_currently_false(s))