From 97324ee367bb4b270b948d2a7686862cbc7937b9 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 8 Jan 2018 16:52:36 -0800 Subject: [PATCH] Added division by constant handling for CBQI BV. (#1498) --- src/theory/quantifiers/bv_inverter.cpp | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) 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().toInteger(); - Integer w = Integer(1).multiplyByPow2(ssize); + unsigned w = bv::utils::getSize(s); + Integer s_val = s.getConst().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); + } } } -- 2.30.2