From df652d04e73a18cceccd59094bb284cf2a390592 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 12 Sep 2010 12:36:04 +0000 Subject: [PATCH] Cleanup. Removes some clauses that must be "false". git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1018 e59a4935-1847-0410-ae03-e826735625c1 --- src/to-sat/BitBlaster.cpp | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index 40655c3..485e24b 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -1005,7 +1005,8 @@ void pushP(stack *products, const int start, const BBNodeVec& y, const B for (int i = start; i < bitWidth; i++) { BBNode n = nf->CreateNode(AND, y[c], multiplier); - products[i].push(n); + if (n!= nf->getFalse()) + products[i].push(n); c++; } } @@ -1106,7 +1107,7 @@ void BitBlaster::buildAdditionNetworkResult(stack { support.insert(nf->CreateNode(NOT, carry)); } - else if (i + 1 != bitWidth) + else if (i + 1 != bitWidth && carry != BBFalse) { products[i + 1].push(carry); } @@ -1236,7 +1237,7 @@ void BitBlaster::mult_Booth(const BBNodeVec& x_i, const B for (int i =0 ; i < bitWidth;i++) { - products[i].push(BBFalse); + assert(products[i].size() == 0); } BBNodeVec notY; @@ -1274,16 +1275,19 @@ void BitBlaster::mult_Booth(const BBNodeVec& x_i, const B pushP(products,i,y,x[i],nf); } - if (xt[i] == MINUS_ONE_MT) + else if (xt[i] == MINUS_ONE_MT) { pushP(products,i,notY,BBTrue,nf); products[i].push(BBTrue); } - if (xt[i] == ONE_MT) + else if (xt[i] == ONE_MT) { pushP(products,i,y,BBTrue,nf); } + + else if (products[i].size() == 0) + products[i].push(BBFalse); } } -- 2.47.3