diff options
Diffstat (limited to 'src/theory/quantifiers/bv_inverter.cpp')
| -rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 26 |
1 files 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<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); + } } } |