From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Sat, 16 Dec 2017 01:29:03 +0000 (-0800)
Subject: Enable side condition handling for shifts introduced in #1441. (#1444)
X-Git-Tag: cvc5-1.0.0~5413
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e764be08256591dfa183d7b3adc750394921574f;p=cvc5.git

Enable side condition handling for shifts introduced in #1441. (#1444)

PR #1441 forgot to enable the missing side condition handling for shifts. This PR enables it.
---

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index d3fa0715d..0ac22a3e4 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -901,19 +901,6 @@ Node BvInverter::solveBvLit(Node sv,
 
         case BITVECTOR_LSHR:
         {
-          if (index == 1)
-          {
-            /* s >> x = t
-             * with side condition:
-             * clz(t) >= clz(s)
-             *   && (t = 0
-             *    || "remaining shifted bits in t "
-             *       "match corresponding bits in s")  */
-            Trace("bv-invert") << "bv-invert : Unsupported for index " << index
-                               << ", from " << sv_t << std::endl;
-            return Node::null();
-          }
-
           TypeNode solve_tn = sv_t[index].getType();
           Node sc = getScBvLshr(k, index, getSolveVariable(solve_tn), s, t);
           /* t = fresh skolem constant  */
@@ -923,20 +910,6 @@ Node BvInverter::solveBvLit(Node sv,
 
         case BITVECTOR_ASHR:
         {
-          if (index == 1)
-          {
-            /* s >> x = t
-             * with side condition:
-             * clx(msb(s),t) >= clx(msb(s),s)
-             *   && (t = 0
-             *    || t = ~0
-             *    || "remaining shifted bits in t "
-             *          "match corresponding bits in s")  */
-
-            Trace("bv-invert") << "bv-invert : Unsupported for index " << index
-                               << ", from " << sv_t << std::endl;
-            return Node::null();
-          }
           TypeNode solve_tn = sv_t[index].getType();
           Node sc = getScBvAshr(k, index, getSolveVariable(solve_tn), s, t);
           /* t = fresh skolem constant  */
@@ -946,19 +919,6 @@ Node BvInverter::solveBvLit(Node sv,
 
         case BITVECTOR_SHL:
         {
-          if (index == 1)
-          {
-            /* s << x = t
-             * with side condition:
-             * ctz(t) >= ctz(s)
-             * && (t = 0 ||
-             *     "remaining shifted bits in t"
-             *     "match corresponding bits in s")
-             */
-            Trace("bv-invert") << "bv-invert : Unsupported for index " << index
-                               << "for bit-vector term " << sv_t << std::endl;
-            return Node::null();
-          }
           TypeNode solve_tn = sv_t[index].getType();
           Node sc = getScBvShl(k, index, getSolveVariable(solve_tn), s, t);
           /* t = fresh skolem constant */