Refactoring. Take out some ASTNodes from the bitblaster.

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

diff --git a/src/to-sat/BitBlastNew.cpp b/src/to-sat/BitBlastNew.cpp
index f0db7d365351b7fa274864a4692c0dd12bc22926..a95e7c099a8e5c7a6ae89059e7b43cb2f5db219d 100644 (file)
--- a/src/to-sat/BitBlastNew.cpp
+++ b/src/to-sat/BitBlastNew.cpp
@@ -563,7 +563,7 @@ ASTVec BitBlasterNew::BBMult(const BBNodeVec& x, const BBNodeVec& y,
 
                BBNodeVec pprod = BBAndBit(ycopy, *xit);
                // accumulate in the product.
-               BBPlus2(prod, pprod, ASTFalse);
+               BBPlus2(prod, pprod, nf->getFalse());
        }
        return prod;
 }
@@ -641,9 +641,6 @@ BBNodeVec BitBlasterNew::BBITE(const BBNode& cond, const BBNodeVec& thn,
 // Workhorse for comparison routines.  This does a signed BVLE if is_signed
 // is true, else it's unsigned.  All other comparison operators can be reduced
 // to this by swapping args or complementing the result bit.
-// FIXME:  If this were done MSB first, it would enable a fast exit sometimes
-// when the MSB is constant, deciding the result without looking at the rest
-// of the bits.
 ASTNode BitBlasterNew::BBBVLE(const BBNodeVec& left, const BBNodeVec& right,
                bool is_signed, bool is_bvlt) {
        BBNodeVec::const_reverse_iterator lit = left.rbegin();
@@ -678,11 +675,13 @@ ASTNode BitBlasterNew::BBBVLE(const BBNodeVec& left, const BBNodeVec& right,
        if (!is_bvlt) {
                bit_comparisons.push_back(prev_eq_bit);
        }
+
+       // Either zero or one of the nodes in bit_comparisons can be true.
        BBNode output =
 #ifdef CRYPTOMINISAT2
-                       _bm->CreateSimpForm(XOR, bit_comparisons);
+                       nf->CreateNode(XOR, bit_comparisons);
 #else
-                       _bm->CreateSimpForm(OR, bit_comparisons);
+                       nf->CreateNode(OR, bit_comparisons);
 #endif
        return output;
 }
@@ -757,7 +756,7 @@ BBNode BitBlasterNew::BBcompare(const ASTNode& form, BBNodeSet& support) {
        }
        default:
                cerr << "BBCompare: Illegal kind" << form << endl;
-               FatalError("", ASTUndefined);
+               FatalError("", form);
        }
 }
 

diff --git a/src/to-sat/BitBlastNew.h b/src/to-sat/BitBlastNew.h
index cfb61c6f7e4e1d308c5191a4527ada451f400ca1..1da9521d86f08ebc2f85c9c52c64a2d754df8272 100644 (file)
--- a/src/to-sat/BitBlastNew.h
+++ b/src/to-sat/BitBlastNew.h
@@ -31,9 +31,6 @@ class BitBlasterNew {
        // bitblasted equivalent
        BBNodeMap BBFormMemo;
 
-       STPMgr * _bm;
-       ASTNode ASTTrue, ASTFalse, ASTUndefined;
-
        /****************************************************************
         * Private Member Functions                                     *
         ****************************************************************/
@@ -108,11 +105,8 @@ public:
         * Public Member Functions                                      *
         ****************************************************************/
 
-       BitBlasterNew(STPMgr * bm) :
-               _bm(bm) {
-               ASTTrue = _bm->CreateNode(TRUE);
-               ASTFalse = _bm->CreateNode(FALSE);
-               ASTUndefined = _bm->CreateNode(UNDEFINED);
+       BitBlasterNew(STPMgr * bm)
+               {
                nf = new BBNodeManager(bm);
        }