diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-01-02 16:54:32 -0800 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-01-02 16:54:32 -0800 |
commit | f8f8103229a9b84e944148985ebb05abed814619 (patch) | |
tree | 0e3ed240518f99c819feceaade6fd9273068baae /src/theory/quantifiers/bv_inverter.cpp | |
parent | ce6d8fde786eb6b4bb658ba83afd384d02853948 (diff) |
Fix handling for UGT/SGT. (#1467)
Previously, we only handled the case x s < t. With this fix, we now get BITVECTOR_[SU]GT for litk
if we encounter a literal t < x s.
Diffstat (limited to 'src/theory/quantifiers/bv_inverter.cpp')
-rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 101 |
1 files changed, 58 insertions, 43 deletions
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index c1e59e3c0..8068b563e 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -205,15 +205,15 @@ static Node dropChild(Node n, unsigned index) return nb.constructNode(); } -static Node getScBvUlt(bool pol, Kind k, unsigned idx, Node x, Node t) +static Node getScBvUltUgt(bool pol, Kind k, Node x, Node t) { - Assert(k == BITVECTOR_ULT); + Assert(k == BITVECTOR_ULT || k == BITVECTOR_UGT); NodeManager* nm = NodeManager::currentNM(); unsigned w = bv::utils::getSize(t); Node sc; - if (idx == 0) + if (k == BITVECTOR_ULT) { if (pol == true) { @@ -227,41 +227,42 @@ static Node getScBvUlt(bool pol, Kind k, unsigned idx, Node x, Node t) else { /* x >= t - * no side condition */ + * true (no side condition) */ sc = nm->mkNode(NOT, nm->mkNode(k, x, t)); } } - else if (idx == 1) + else { + Assert(k == BITVECTOR_UGT); if (pol == true) { - /* t < x + /* x > t * with side condition: * t != ~0 */ Node scl = nm->mkNode(DISTINCT, t, bv::utils::mkOnes(w)); - Node scr = nm->mkNode(k, t, x); + Node scr = nm->mkNode(k, x, t); sc = nm->mkNode(IMPLIES, scl, scr); } else { - /* t >= x - * no side condition */ - sc = nm->mkNode(NOT, nm->mkNode(k, t, x)); + /* x <= t + * true (no side condition) */ + sc = nm->mkNode(NOT, nm->mkNode(k, x, t)); } } Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; return sc; } -static Node getScBvSlt(bool pol, Kind k, unsigned idx, Node x, Node t) +static Node getScBvSltSgt(bool pol, Kind k, Node x, Node t) { - Assert(k == BITVECTOR_SLT); + Assert(k == BITVECTOR_SLT || k == BITVECTOR_SGT); NodeManager* nm = NodeManager::currentNM(); unsigned w = bv::utils::getSize(t); Node sc; - if (idx == 0) + if (k == BITVECTOR_SLT) { if (pol == true) { @@ -276,28 +277,29 @@ static Node getScBvSlt(bool pol, Kind k, unsigned idx, Node x, Node t) else { /* x >= t - * no side condition */ + * true (no side condition) */ sc = nm->mkNode(NOT, nm->mkNode(k, x, t)); } } - else if (idx == 1) + else { + Assert(k == BITVECTOR_SGT); if (pol == true) { - /* t < x + /* x > t * with side condition: * t != 01...1 */ BitVector bv = BitVector(w).setBit(w - 1); Node max = bv::utils::mkConst(~bv); Node scl = nm->mkNode(DISTINCT, t, max); - Node scr = nm->mkNode(k, t, x); + Node scr = nm->mkNode(k, x, t); sc = nm->mkNode(IMPLIES, scl, scr); } else { - /* t >= x - * no side condition */ - sc = nm->mkNode(NOT, nm->mkNode(k, t, x)); + /* x <= t + * true (no side condition) */ + sc = nm->mkNode(NOT, nm->mkNode(k, x, t)); } } Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl; @@ -363,7 +365,8 @@ static Node getScBvUrem(bool pol, Node t) { Assert(k == BITVECTOR_UREM_TOTAL); - Assert (litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT); + Assert (litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT + || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); NodeManager* nm = NodeManager::currentNM(); Node scl; @@ -472,7 +475,7 @@ static Node getScBvUrem(bool pol, } } } - else /* litk == BITVECTOR_SLT */ + else if (litk == BITVECTOR_SLT) { if (idx == 0) { @@ -531,6 +534,10 @@ static Node getScBvUrem(bool pol, } } } + else + { + return Node::null(); + } Node scr = nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t); @@ -644,7 +651,8 @@ static Node getScBvAndOr(bool pol, Node t) { Assert (k == BITVECTOR_AND || k == BITVECTOR_OR); - Assert (litk == EQUAL || litk == BITVECTOR_SLT || litk == BITVECTOR_ULT); + Assert (litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT + || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); NodeManager* nm = NodeManager::currentNM(); Node scl, scr; @@ -788,7 +796,8 @@ static Node getScBvLshr(bool pol, Node t) { Assert(k == BITVECTOR_LSHR); - Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT); + Assert(litk == EQUAL || litk == BITVECTOR_ULT || litk == BITVECTOR_SLT + || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT); NodeManager* nm = NodeManager::currentNM(); Node scl; @@ -915,7 +924,7 @@ static Node getScBvLshr(bool pol, } } } - else /* litk == BITVECTOR_SLT */ + else if (litk == BITVECTOR_SLT) { if (idx == 0) { @@ -967,6 +976,10 @@ static Node getScBvLshr(bool pol, } } } + else + { + return Node::null(); + } Node scr = nm->mkNode(litk, idx == 0 ? nm->mkNode(k, x, s) : nm->mkNode(k, s, x), t); Node sc = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode()); @@ -1258,6 +1271,14 @@ Node BvInverter::solveBvLit(Node sv, Node sv_t = lit[index]; Node t = lit[1-index]; + if (litk == BITVECTOR_ULT && index == 1) + { + litk = BITVECTOR_UGT; + } + else if (litk == BITVECTOR_SLT && index == 1) + { + litk = BITVECTOR_SGT; + } /* Bit-vector layer -------------------------------------------- */ @@ -1273,7 +1294,7 @@ Node BvInverter::solveBvLit(Node sv, { t = nm->mkNode(k, t); } - else if (k == BITVECTOR_CONCAT) + else if (k == BITVECTOR_CONCAT && litk == EQUAL) { /* x = t[upper:lower] * where @@ -1291,7 +1312,7 @@ Node BvInverter::solveBvLit(Node sv, } t = bv::utils::mkExtract(t, upper, lower); } - else if (k == BITVECTOR_SIGN_EXTEND) + else if (k == BITVECTOR_SIGN_EXTEND && litk == EQUAL) { t = bv::utils::mkExtract(t, bv::utils::getSize(sv_t[index]) - 1, 0); } @@ -1307,15 +1328,11 @@ Node BvInverter::solveBvLit(Node sv, Node s = nchildren == 2 ? sv_t[1 - index] : dropChild(sv_t, index); /* Note: All n-ary kinds except for CONCAT (i.e., AND, OR, MULT, PLUS) * are commutative (no case split based on index). */ - if (k == BITVECTOR_PLUS) + if (k == BITVECTOR_PLUS && litk == EQUAL) { t = nm->mkNode(BITVECTOR_SUB, t, s); } - else if (k == BITVECTOR_SUB) - { - t = nm->mkNode(BITVECTOR_PLUS, t, s); - } - else if (k == BITVECTOR_XOR) + else if (k == BITVECTOR_XOR && litk == EQUAL) { t = nm->mkNode(BITVECTOR_XOR, t, s); } @@ -1373,16 +1390,14 @@ Node BvInverter::solveBvLit(Node sv, if (sc.isNull()) { solve_tn = sv_t.getType(); - if (litk == BITVECTOR_ULT) + if (litk == BITVECTOR_ULT || litk == BITVECTOR_UGT) { - sc = getScBvUlt( - pol, litk, index, getSolveVariable(solve_tn), t); + sc = getScBvUltUgt(pol, litk, getSolveVariable(solve_tn), t); } else { - Assert (litk == BITVECTOR_SLT); - sc = getScBvSlt( - pol, litk, index, getSolveVariable(solve_tn), t); + Assert (litk == BITVECTOR_SLT || litk == BITVECTOR_SGT); + sc = getScBvSltSgt(pol, litk, getSolveVariable(solve_tn), t); } } /* We generate a choice term (choice x0. SC => x0 <k> s <litk> t) for @@ -1398,16 +1413,16 @@ Node BvInverter::solveBvLit(Node sv, sv_t = sv_t[index]; } Assert(sv_t == sv); - if (litk == BITVECTOR_ULT) + if (litk == BITVECTOR_ULT || litk == BITVECTOR_UGT) { TypeNode solve_tn = sv_t.getType(); - Node sc = getScBvUlt(pol, litk, index, getSolveVariable(solve_tn), t); + Node sc = getScBvUltUgt(pol, litk, getSolveVariable(solve_tn), t); t = getInversionNode(sc, solve_tn, m); } - else if (litk == BITVECTOR_SLT) + else if (litk == BITVECTOR_SLT || litk == BITVECTOR_SGT) { TypeNode solve_tn = sv_t.getType(); - Node sc = getScBvSlt(pol, litk, index, getSolveVariable(solve_tn), t); + Node sc = getScBvSltSgt(pol, litk, getSolveVariable(solve_tn), t); t = getInversionNode(sc, solve_tn, m); } else if (pol == false) |