From 51d2682c44761e0b3a30e75188b390b791d5dd48 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 10 Jan 2018 15:18:13 -0800 Subject: [PATCH] Removed division by constant handling for CBQI BV (unsound). (#1508) This removes division by constant handling in the BV inverter introduced in #1498. Division by constant was simplified to: x / s OP t ---> x = t / s^-1 if s odd and there exists a multiplicative modular inverse s^-1. This however, is incorrect since x / s * 1 / s^-1 != x / (s * s^-1) --- src/theory/quantifiers/bv_inverter.cpp | 17 +++-------------- 1 file changed, 3 insertions(+), 14 deletions(-) diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 9559ffc45..a96f05a35 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -2316,11 +2316,8 @@ Node BvInverter::solveBvLit(Node sv, { t_new = nm->mkNode(BITVECTOR_XOR, t, s); } - else if (k == BITVECTOR_MULT - || (k == BITVECTOR_UDIV_TOTAL && index == 0)) + else if (k == BITVECTOR_MULT && s.isConst() && bv::utils::getBit(s, 0)) { - if (s.isConst() && bv::utils::getBit(s, 0)) - { unsigned w = bv::utils::getSize(s); Integer s_val = s.getConst().toInteger(); Integer mod_val = Integer(1).multiplyByPow2(w); @@ -2328,16 +2325,8 @@ Node BvInverter::solveBvLit(Node sv, << "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); - } - } + Node inv = bv::utils::mkConst(w, inv_val); + t_new = nm->mkNode(BITVECTOR_MULT, inv, t); } if (!t_new.isNull()) -- 2.30.2