From 34a0e4420960a2f6a34d02e53636fecd63b5c4de Mon Sep 17 00:00:00 2001
From: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Date: Wed, 25 Mar 2020 09:37:57 -0700
Subject: [PATCH] bv2int : linear mult opt (#4142)

---
 src/preprocessing/passes/bv_to_int.cpp | 23 ++++++++++++++++++++++-
 1 file changed, 22 insertions(+), 1 deletion(-)

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index cb78b0897..0e4bc41c0 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -401,7 +401,28 @@ Node BVToInt::bvToInt(Node n)
                   d_nm->mkNode(kind::MINUS, mult, multSig);
               d_rangeAssertions.insert(
                   mkRangeConstraint(d_bvToIntCache[current], bvsize));
-              d_rangeAssertions.insert(mkRangeConstraint(sigma, bvsize));
+              if (translated_children[0].isConst()
+                  || translated_children[1].isConst())
+              {
+                /*
+                 * based on equation (23), section 3.2.3 of:
+                 * Bozzano et al.
+                 * Encoding RTL Constructs for MathSAT: a Preliminary Report.
+                 */
+                // this is an optimization when one of the children is constant
+                Node c = translated_children[0].isConst()
+                             ? translated_children[0]
+                             : translated_children[1];
+                d_rangeAssertions.insert(
+                    d_nm->mkNode(kind::LEQ, d_zero, sigma));
+                // the value of sigma is bounded by (c - 1)
+                // where c is the constant multiplicand
+                d_rangeAssertions.insert(d_nm->mkNode(kind::LT, sigma, c));
+              }
+              else
+              {
+                d_rangeAssertions.insert(mkRangeConstraint(sigma, bvsize));
+              }
               break;
             }
             case kind::BITVECTOR_UDIV_TOTAL:
-- 
2.30.2