From f1a150f43e0ce15556a00bdab2ba1636850d83d9 Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 20 Oct 2009 03:07:30 +0000
Subject: [PATCH] changed the majority function for bvplus-bitblasing to
 clausal form. Thus improved speed by 2X

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@322 e59a4935-1847-0410-ae03-e826735625c1
---
 src/to-sat/BitBlast.cpp | 56 +++++++++++++++++++++++++++++++++++------
 src/to-sat/BitBlast.h   |  1 +
 2 files changed, 49 insertions(+), 8 deletions(-)

diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index b2cf9f2..127b40f 100644
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -656,10 +656,7 @@ namespace BEEV
 	    //Compute this only for i=0 to n-2
 	    nextcin = Majority(sum[i], y[i], cin);
 	  }
-        sum[i] = 
-          _bm->CreateSimpForm(XOR, 
-                              _bm->CreateSimpForm(XOR, sum[i], y[i]), 
-                              cin);
+        sum[i] = Sum(sum[i], y[i], cin);        
 	if(i != n-1)
 	  {
 	    //Compute this only for i=0 to n-2
@@ -736,13 +733,56 @@ namespace BEEV
     // worth doing explicitly (e.g., a = b, a = ~b, etc.)
     else
       {
-        return _bm->CreateSimpForm(OR, 
-                                   _bm->CreateSimpForm(AND, a, b), 
-                                   _bm->CreateSimpForm(AND, b, c), 
-                                   _bm->CreateSimpForm(AND, a, c));
+	//         return _bm->CreateSimpForm(OR, 
+	//                                    _bm->CreateSimpForm(AND, a, b), 
+	//                                    _bm->CreateSimpForm(AND, b, c), 
+	//                                    _bm->CreateSimpForm(AND, a, c));
+	return _bm->CreateSimpForm(AND, 
+                                   _bm->CreateSimpForm(OR, a, b), 
+                                   _bm->CreateSimpForm(OR, b, c), 
+                                   _bm->CreateSimpForm(OR, a, c));
+      
       }
   }
 
+  ASTNode BitBlaster::Sum(const ASTNode& xi,
+			  const ASTNode& yi,
+			  const ASTNode& cin)
+  {
+    // For some unexplained reason, XORs are faster than converting
+    // them to cluases at this point
+    return _bm->CreateSimpForm(XOR, 
+    			       _bm->CreateSimpForm(XOR, xi, yi), 
+    			       cin);
+
+    if((ASTTrue == xi && ASTTrue == yi && ASTFalse == cin)
+       || (ASTTrue == xi  && ASTFalse == yi && ASTTrue == cin)
+       || (ASTFalse == xi && ASTTrue == yi  && ASTTrue == cin)
+       || (ASTFalse == xi && ASTFalse== yi && ASTFalse == cin))
+      {
+    	return ASTFalse;
+      }
+    ASTNode S1 = _bm->CreateSimpForm(OR,xi,yi,cin);
+    ASTNode S2 = _bm->CreateSimpForm(OR,
+				     _bm->CreateSimpForm(NOT,xi),
+				     _bm->CreateSimpForm(NOT,yi),
+				     cin);
+    ASTNode S3 = _bm->CreateSimpForm(OR,
+				     _bm->CreateSimpForm(NOT,xi),
+				     yi,
+				     _bm->CreateSimpForm(NOT,cin));
+    ASTNode S4 = _bm->CreateSimpForm(OR,
+				     xi,
+				     _bm->CreateSimpForm(NOT,yi),
+				     _bm->CreateSimpForm(NOT,cin));
+    ASTVec S;
+    S.push_back(S1);
+    S.push_back(S2);
+    S.push_back(S3);
+    S.push_back(S4);
+    return _bm->CreateSimpForm(AND,S);
+  }
+
   // Bitwise complement
   ASTVec BitBlaster::BBNeg(const ASTVec& x)
   {
diff --git a/src/to-sat/BitBlast.h b/src/to-sat/BitBlast.h
index 2c0b912..0d8e37b 100644
--- a/src/to-sat/BitBlast.h
+++ b/src/to-sat/BitBlast.h
@@ -82,6 +82,7 @@ namespace BEEV
 
     // Return formula for majority function of three formulas.
     ASTNode Majority(const ASTNode& a, const ASTNode& b, const ASTNode& c);
+    ASTNode Sum(const ASTNode& xi, const ASTNode& yi, const ASTNode& cin);
 
     // Internal bit blasting routines.
     ASTNode BBBVLE(const ASTVec& x, const ASTVec& y, bool is_signed);
-- 
2.47.3