mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Normalizing LE and GE with constants

Browse source
This commit is contained in:
Yakir Vizel 2017-12-27 12:44:20 -05:00 • committed by Arie Gurfinkel
parent 0c1ef7155a
commit 068b77d43a
1 changed files with 14 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/muz/spacer/spacer_term_graph.cpp
View file

@ -118,7 +118,7 @@ public:
app* mk_le_zero(expr *arg) {
expr *e1, *e2, *e3;
// XXX currently disabled
if (false && m_arith.is_add(arg, e1, e2)) {
if (m_arith.is_add(arg, e1, e2)) {
// e1-e2<=0 --> e1<=e2
if (m_arith.is_times_minus_one(e2, e3)) {
return m_arith.mk_le(e1, e3);
@ -133,7 +133,7 @@ public:
app* mk_ge_zero(expr *arg) {
expr *e1, *e2, *e3;
// XXX currently disabled
if (false && m_arith.is_add(arg, e1, e2)) {
if (m_arith.is_add(arg, e1, e2)) {
// e1-e2>=0 --> e1>=e2
if (m_arith.is_times_minus_one(e2, e3)) {
return m_arith.mk_ge(e1, e3);
@ -148,6 +148,7 @@ public:
bool mk_le_core (expr *arg1, expr * arg2, app_ref &result) {
// t <= -1 ==> t < 0 ==> ! (t >= 0)
rational n;
if (m_arith.is_int (arg1) && m_arith.is_minus_one (arg2)) {
result = m.mk_not (mk_ge_zero (arg1));
return true;
@ -156,6 +157,11 @@ public:
result = mk_le_zero(arg1);
return true;
}
else if (m_arith.is_numeral(arg2, n)) {
// t <= n ==> t < n + 1 ==> ! (t >= n + 1)
result = m.mk_not(m_arith.mk_ge(arg1, m_arith.mk_numeral(n+1, true)));
return true;
}
return false;
}
@ -167,6 +173,7 @@ public:
bool mk_ge_core (expr * arg1, expr * arg2, app_ref &result) {
// t >= 1 ==> t > 0 ==> ! (t <= 0)
rational n;
if (m_arith.is_int (arg1) && is_one (arg2)) {
result = m.mk_not (mk_le_zero (arg1));
return true;
@ -175,6 +182,11 @@ public:
result = mk_ge_zero(arg1);
return true;
}
else if (m_arith.is_numeral(arg2, n)) {
// t >= n ==> t > n - 1 ==> ! (t <= n - 1)
result = m.mk_not(m_arith.mk_le(arg1, m_arith.mk_numeral(n-1, true)));
return true;
}
return false;
}