From 06f2acc56609a58a8687c6f768aa7dabc4ce9637 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Thu, 6 May 2010 04:34:28 +0000
Subject: [PATCH] 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
---
 src/to-sat/BitBlastNew.cpp | 13 ++++++-------
 src/to-sat/BitBlastNew.h   | 10 ++--------
 2 files changed, 8 insertions(+), 15 deletions(-)

diff --git a/src/to-sat/BitBlastNew.cpp b/src/to-sat/BitBlastNew.cpp
index f0db7d3..a95e7c0 100644
--- 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 cfb61c6..1da9521 100644
--- 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);
 	}
 
-- 
2.47.3