changed the majority function for bvplus-bitblasing to clausal form. Thus improved...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@322 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index b2cf9f20e54a069edc98eaabfa108e27946b024f..127b40f35da4fd2e5c791e275bd540dd9da4590c 100644 (file)
--- 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 2c0b9125c0776613bf75e00b604e5ff44f9026fb..0d8e37b7a0ef398be55f65fe863a1e899c9ed375 100644 (file)
--- 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);