From 947ea66cad233f8d4b14d3bc594e15d71a611864 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 18 Jun 2021 17:39:13 -0700
Subject: [PATCH] simplify output to use signed constants

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/dd/dd_bdd.cpp | 45 +++++++++++++++++++-----------------------
 src/math/dd/dd_bdd.h   |  2 ++
 2 files changed, 22 insertions(+), 25 deletions(-)

diff --git a/src/math/dd/dd_bdd.cpp b/src/math/dd/dd_bdd.cpp
index a19c39ba0..357409877 100644
--- a/src/math/dd/dd_bdd.cpp
+++ b/src/math/dd/dd_bdd.cpp
@@ -1002,6 +1002,20 @@ namespace dd {
         return result;
     }
 
+    bool_vector bdd_manager::mk_usub(bool_vector const& b) {
+        bool_vector result;
+        if (b.empty())
+            return result;
+        bool carry = false;
+        result.push_back(b[0]);
+        for (unsigned i = 1; i < b.size(); ++i) {
+            carry |= b[i-1];
+            result.push_back(carry ^ b[i]);
+        }
+        return result;
+    }
+
+
     bddv bdd_manager::mk_mul(bddv const& a, bddv const& b) {
         SASSERT(a.size() == b.size());
         bddv a_shifted = a;
@@ -1029,32 +1043,13 @@ namespace dd {
         bddv a_shifted = a;
         bddv result = mk_zero(a.size());
 
-#if 0
-        // 
-        // check correctness and tune mk_usub
-        // multiplication by a constant is dead slow.
-        // this can also be tuned.
-        // 
-        unsigned cnt = 0;
-        bool negated = false;
-        for (auto v : b) if (v) cnt++;
-        
+       
         // use identity (bvmul a b) == (bvneg (bvmul (bvneg a) b))
-        if (cnt*2 > b.size()) {
-            bool_vector b_inv;
-            for (auto v : b)
-                b_inv.push_back(!v);
-            for (unsigned i = 0; i < b_inv.size(); ++i) {
-                if (b_inv[i])
-                    b_inv[i] = false;
-                else {
-                    b_inv[i] = true;
-                    break;
-                }
-            }
-            return mk_usub(mk_mul(a, b_inv));
-        }
-#endif
+        unsigned cnt = 0;
+        for (auto v : b) if (v) cnt++; 
+        if (cnt*2 > b.size()) 
+            return mk_usub(mk_mul(a, mk_usub(b)));
+
         for (unsigned i = 0; i < a.size(); ++i) {
             if (b[i])
                 result = mk_add(result, a_shifted);
diff --git a/src/math/dd/dd_bdd.h b/src/math/dd/dd_bdd.h
index d91df160a..5938f6048 100644
--- a/src/math/dd/dd_bdd.h
+++ b/src/math/dd/dd_bdd.h
@@ -204,6 +204,8 @@ namespace dd {
             ~scoped_push() { m.m_bdd_stack.shrink(m_size); }
         };
 
+        bool_vector mk_usub(bool_vector const& b);
+
     public:
         struct mem_out {};