From f2e22c0cd74a767aa166d5de3c36897263eb5aae Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 11 Aug 2010 00:58:57 +0000
Subject: [PATCH] Add a sorting network implementation. This code is not
 currently enabled so this patch should do nothing.

Sorting networks should have better propagation (at higher cost) than addition networks (which we currently encode multiplication to).

In my experiments the sorting networks aren't clearly better than the addition networks.




git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@979 e59a4935-1847-0410-ae03-e826735625c1
---
 src/to-sat/BitBlaster.cpp | 80 +++++++++++++++++++++++++++++++++++++--
 src/to-sat/BitBlaster.h   |  3 ++
 2 files changed, 79 insertions(+), 4 deletions(-)

diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp
index 603d50b..b1b00e8 100644
--- a/src/to-sat/BitBlaster.cpp
+++ b/src/to-sat/BitBlaster.cpp
@@ -1042,34 +1042,106 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::mult_normal(const BBNodeVec& x,
 	return prod;
 }
 
+
+  template<class BBNode, class BBNodeManagerT>
+    void
+    BitBlaster<BBNode, BBNodeManagerT>::mult_SortingNetwork(const BBNodeVec& x_i, const BBNodeVec& y_i,
+        BBNodeSet& support, const ASTNode& xN, const ASTNode& yN, stack<BBNode> * products, int i)
+    {
+      const int width = products[i].size();
+      const int bitWidth = xN.GetValueWidth();
+
+      vector<BBNode> sorted(width, nf->getFalse());
+
+      for (int l = 0; l < width; l++)
+        {
+          vector<BBNode> oldSorted(sorted);
+          BBNode c = products[i].top();
+          products[i].pop();
+          sorted[0] = nf->CreateNode(OR, oldSorted[0], c);
+
+          for (int j = 1; j <= std::min(l, width - 1); j++)
+            {
+              sorted[j] = nf->CreateNode(OR, nf->CreateNode(AND, oldSorted[j - 1], c), oldSorted[j]);
+            }
+        }
+
+      for (int k = 0; k < width; k++)
+        assert(!sorted[k].IsNull());
+
+      assert(products[i].size() == 0);
+
+      // Add to next up columns.
+      if (i + 1 != bitWidth)
+        {
+          for (int k = 1; k < width; k += 2)
+            {
+              products[i + 1].push(sorted[k]);
+            }
+        }
+
+      BBNode resultNode = nf->getFalse();
+
+      // Constrain to equal the result
+      for (int k = 1; k < width; k += 2)
+        {
+          BBNode part = nf->CreateNode(AND, nf->CreateNode(NOT, sorted[k]), sorted[k - 1]);
+          resultNode = nf->CreateNode(OR, resultNode, part);
+        }
+
+      // constraint the all '1's case.
+      if (width % 2 == 1)
+        resultNode = nf->CreateNode(OR, resultNode, sorted.at(width - 1));
+
+      products[i].push(resultNode);
+    }
+
+
 // ONLY SELECT ONE OF THESE!
 const bool multiplication_variant1 = false; // multiplication with repeat addition.
 const bool multiplication_variant2 = false; // multiplication with partial products.
 const bool multiplication_variant3 = true; // multiplication with booth recoding.
+const bool multiplication_variant4 = false;  // multiplication via sorting networks.
+
 
 // Multiply two bitblasted numbers
 template <class BBNode, class BBNodeManagerT>
 BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBMult(const BBNodeVec& x, const BBNodeVec& y,
 		BBNodeSet& support, const ASTNode& xN, const ASTNode& yN) {
 
+        const int bitWidth = x.size();
+
 	if (multiplication_variant1) {
 		return mult_normal(x, y, support);
 	}
 
+	stack<BBNode> products[bitWidth];
+
 	if (multiplication_variant2) {
-		const int bitWidth = x.size();
-		stack<BBNode> products[bitWidth];
 		mult_allPairs(x, y, support,products);
 		return buildAdditionNetworkResult(products,bitWidth);
 	}
 
 	if (multiplication_variant3) {
-		const int bitWidth = x.size();
-		stack<BBNode> products[bitWidth];
 		mult_Booth(x, y, support,xN,yN,products);
 		return buildAdditionNetworkResult(products,bitWidth);
 	}
 
+        if (multiplication_variant4)
+        {
+          mult_Booth(x, y, support,xN,yN,products);
+          for (int i = 0; i < bitWidth; i++)
+            {
+              if (products[i].size() < 6)
+                {
+                    mult_SortingNetwork(x, y, support, xN, yN, products, i);
+                    assert(products[i].size() == 1);
+                }
+            }
+          return buildAdditionNetworkResult(products, bitWidth);
+        }
+
+
 	FatalError("sda44f");
 }
 
diff --git a/src/to-sat/BitBlaster.h b/src/to-sat/BitBlaster.h
index 5be0579..210de9e 100644
--- a/src/to-sat/BitBlaster.h
+++ b/src/to-sat/BitBlaster.h
@@ -75,6 +75,9 @@ class BitBlaster {
 	void mult_Booth(const vector<BBNode>& x_i, const vector<BBNode>& y_i, set<BBNode>& support, const BEEV::ASTNode& xN, const BEEV::ASTNode& yN, stack<BBNode> * products);
 	vector<BBNode> mult_normal(const vector<BBNode>& x,	const vector<BBNode>& y, set<BBNode>& support);
 
+        void mult_SortingNetwork(const vector<BBNode>& x_i, const vector<BBNode>& y_i,
+            set<BBNode>& support, const ASTNode& xN, const ASTNode& yN, stack<BBNode> * products, int i);
+
 	vector<BBNode> buildAdditionNetworkResult(stack<BBNode>* products, const int bitWidth);
 
 	vector<BBNode> BBAndBit(const vector<BBNode>& y, BBNode b);
-- 
2.47.3