Constant-fold unsigned division/remainder in bv_utils

src/solvers/flattening/bv_utils.cpp

@@ -1163,6 +1163,26 @@ void bv_utilst::unsigned_divider(
 {
   std::size_t width=op0.size();
 
+  // If both operands are constant, compute the result directly so it folds to
+  // constant literals downstream instead of introducing fresh variables and a
+  // multiplier constraint.  Division by zero falls through to the general
+  // (non-deterministic) encoding below.
+  if(is_constant(op0) && is_constant(op1))
+  {
+    mp_integer n0 = 0, n1 = 0;
+    for(std::size_t i = width; i-- > 0;)
+    {
+      n0 = (n0 << 1) + (op0[i].is_true() ? 1 : 0);
+      n1 = (n1 << 1) + (op1[i].is_true() ? 1 : 0);
+    }
+    if(n1 != 0)
+    {
+      res = build_constant(n0 / n1, width);
+      rem = build_constant(n0 % n1, width);
+      return;
+    }
+  }
+
   // check if we divide by a power of two
   #if 0
   {

unit/solvers/flattening/bv_utils.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening
 #include <util/symbol_table.h>
 
 #include <solvers/flattening/boolbv.h>
+#include <solvers/flattening/bv_utils.h>
 #include <solvers/sat/satcheck.h>
 #include <testing-utils/use_catch.h>
 
@@ -82,3 +83,54 @@ SCENARIO("1-bit signed less-than", "[core][solvers][flattening][bv_utils]")
     }
   }
 }
+
+SCENARIO(
+  "unsigned_divider folds constant operands",
+  "[core][solvers][flattening][bv_utils]")
+{
+  console_message_handlert message_handler;
+  message_handler.set_verbosity(0);
+
+  GIVEN("a bv_utilst over a SAT back-end")
+  {
+    satcheckt satcheck(message_handler);
+    bv_utilst bv_utils(satcheck);
+    const std::size_t width = 32;
+
+    WHEN("dividing two constants 100 / 7")
+    {
+      bvt res, rem;
+      bv_utils.divider(
+        bv_utilst::build_constant(100, width),
+        bv_utilst::build_constant(7, width),
+        res,
+        rem,
+        bv_utilst::representationt::UNSIGNED);
+
+      THEN("the result is constant (no fresh variables) and correct")
+      {
+        REQUIRE(bv_utilst::is_constant(res));
+        REQUIRE(bv_utilst::is_constant(rem));
+        REQUIRE(res == bv_utilst::build_constant(14, width));
+        REQUIRE(rem == bv_utilst::build_constant(2, width));
+      }
+    }
+
+    WHEN("dividing a constant by a constant zero")
+    {
+      bvt res, rem;
+      bv_utils.divider(
+        bv_utilst::build_constant(100, width),
+        bv_utilst::build_constant(0, width),
+        res,
+        rem,
+        bv_utilst::representationt::UNSIGNED);
+
+      THEN("the fall-through (nondeterministic) encoding is used")
+      {
+        // division by zero must not be folded; it keeps fresh variables
+        REQUIRE_FALSE(bv_utilst::is_constant(res));
+      }
+    }
+  }
+}