From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 9 Jan 2018 00:52:36 +0000 (-0800)
Subject: Added division by constant handling for CBQI BV. (#1498)
X-Git-Tag: cvc5-1.0.0~5370
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=97324ee367bb4b270b948d2a7686862cbc7937b9;p=cvc5.git

Added division by constant handling for CBQI BV. (#1498)
---

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index f0ad4f797..9559ffc45 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -2316,19 +2316,27 @@ Node BvInverter::solveBvLit(Node sv,
       {
         t_new = nm->mkNode(BITVECTOR_XOR, t, s);
       }
-      else if (k == BITVECTOR_MULT)
+      else if (k == BITVECTOR_MULT
+           || (k == BITVECTOR_UDIV_TOTAL && index == 0))
       {
         if (s.isConst() && bv::utils::getBit(s, 0))
         {
-          unsigned ssize = bv::utils::getSize(s);
-          Integer a = s.getConst<BitVector>().toInteger();
-          Integer w = Integer(1).multiplyByPow2(ssize);
+          unsigned w = bv::utils::getSize(s);
+          Integer s_val = s.getConst<BitVector>().toInteger();
+          Integer mod_val = Integer(1).multiplyByPow2(w);
           Trace("bv-invert-debug")
-              << "Compute inverse : " << a << " " << w << std::endl;
-          Integer inv = a.modInverse(w);
-          Trace("bv-invert-debug") << "Inverse : " << inv << std::endl;
-          Node inv_val = nm->mkConst(BitVector(ssize, inv));
-          t_new = nm->mkNode(BITVECTOR_MULT, inv_val, t);
+              << "Compute inverse : " << s_val << " " << mod_val << std::endl;
+          Integer inv_val = s_val.modInverse(mod_val);
+          Trace("bv-invert-debug") << "Inverse : " << inv_val << std::endl;
+          Node inv = nm->mkConst(BitVector(w, inv_val));
+          if (k == BITVECTOR_MULT)
+          {
+            t_new = nm->mkNode(BITVECTOR_MULT, inv, t);
+          }
+          else
+          {
+            t_new = nm->mkNode(BITVECTOR_UDIV_TOTAL, t, inv);
+          }
         }
       }