mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

add monotonicity lemma

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-02-09 09:31:43 -08:00
parent bf03886a87
commit e31eb9a6b1
1 changed files with 15 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1991,6 +1991,17 @@ namespace polysat {
<< s.var(q1) << "\n");
};
// monotonicity0 lemma should be asserted eagerly.
auto monotonicity0 = [&](auto& x1, auto& x1_val, auto& y1, auto& y1_val, auto& q1, auto& q1_val) {
if (q1_val * y1_val <= x1_val)
return;
// q1*y1 + r1 = x1, q1*y1 <= -r1 - 1, q1*y1 <= x1
propagated = true;
set_rule("[x1, y1] (x1 / y1) * y1 <= x1");
m_lemma.reset();
propagate(q1, core, s.ule(s.var(q1) * y1, x1));
};
auto monotonicity1 = [&](auto& x1, auto& x1_val, auto& y1, auto& y1_val, auto& q1, auto& q1_val,
auto& x2, auto& x2_val, auto& y2, auto& y2_val, auto& q2, auto& q2_val) {
if (!(x1_val <= x2_val && y1_val >= y2_val && q1_val > q2_val))
@ -2027,6 +2038,10 @@ namespace polysat {
if (q1_val == expected1)
continue;
// force that q1 * y1 <= x1 if it isn't the case.
// monotonicity0(x1, x1_val, y1, y1_val, q1, q1_val);
for (auto const& [x2, y2, q2, r2] : s.m_constraints.div_constraints()) {
if (x1 == x2 && y1 == y2)