From: trevor_hansen Date: Tue, 2 Mar 2010 12:40:46 +0000 (+0000) Subject: * Merged in all the changes made to the bitblaster while I was working on it. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=5c939fc4d629b7ab1a530b4d60bd127e0dbe3cb8;p=francis%2Fstp.git * Merged in all the changes made to the bitblaster while I was working on it. * Removed the BOOLVEC object type. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@623 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/ASTKind.kinds b/src/AST/ASTKind.kinds index 4569083..6871816 100644 --- a/src/AST/ASTKind.kinds +++ b/src/AST/ASTKind.kinds @@ -33,7 +33,7 @@ SBVREM 2 2 Term SBVMOD 2 2 Term BVSX 1 1 Term BVZX 1 1 Term -BOOLVEC 0 - Term +#BOOLVEC 0 - Term # Formula OR term, depending on context ITE 3 3 Term Form diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index 345ba25..a967e6e 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -12,7 +12,7 @@ ASTNode SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec & children) { // If all the parameters are constant, return the constant value. // The bitblaster calls CreateNode with a boolean vector. We don't try to simplify those. - if (kind != BEEV::BOOLVEC && kind != BEEV::UNDEFINED) + if (kind != BEEV::UNDEFINED) { bool allConstant = true; diff --git a/src/c_interface/c_interface.h b/src/c_interface/c_interface.h index 2a30c27..c795c52 100644 --- a/src/c_interface/c_interface.h +++ b/src/c_interface/c_interface.h @@ -349,7 +349,6 @@ extern "C" { SBVMOD, BVSX, BVZX, - BOOLVEC, ITE, BVGETBIT, BVLT, diff --git a/src/to-sat/BitBlastNew.cpp b/src/to-sat/BitBlastNew.cpp index 18e2d2d..f6ba02a 100644 --- a/src/to-sat/BitBlastNew.cpp +++ b/src/to-sat/BitBlastNew.cpp @@ -7,44 +7,37 @@ ********************************************************************/ // -*- c++ -*- -#include "BitBlastNew.h" -#include "../AST/AST.h" -#include #include #include +#include "BitBlastNew.h" +#include "../AST/AST.h" - -namespace BEEV -{ +namespace BEEV { /******************************************************************** - * BitBlast - * - * Convert bitvector terms and formulas to boolean formulas. A term - * is something that can represent a multi-bit bitvector, such as - * BVPLUS or BVXOR (or a BV variable or constant). A formula (form) - * represents a boolean value, such as EQ or BVLE. Bit blasting a - * term representing an n-bit bitvector with BBTerm yields a vector - * of n boolean formulas (returning ASTVec). Bit blasting a formula - * returns a single boolean formula (type ASTNode). A bitblasted - * term is a vector of ASTNodes for formulas. The 0th element of - * the vector corresponds to bit 0 -- the low-order bit. - ********************************************************************/ + * BitBlast + * + * Convert bitvector terms and formulas to boolean formulas. A term + * is something that can represent a multi-bit bitvector, such as + * BVPLUS or BVXOR (or a BV variable or constant). A formula (form) + * represents a boolean value, such as EQ or BVLE. Bit blasting a + * term representing an n-bit bitvector with BBTerm yields a vector + * of n boolean formulas (returning ASTVec). Bit blasting a formula + * returns a single boolean formula (type ASTNode). A bitblasted + * term is a vector of ASTNodes for formulas. The 0th element of + * the vector corresponds to bit 0 -- the low-order bit. + ********************************************************************/ BBNodeVec _empty_BBNodeVec; - // Bit blast a bitvector term. The term must have a kind for a // bitvector term. Result is a ref to a vector of formula nodes // representing the boolean formula. - -const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) -{ +const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) { BBNodeVecMap::iterator it = BBTermMemo.find(term); - if (it != BBTermMemo.end()) - { + if (it != BBTermMemo.end()) { // already there. Just return it. return it->second; } @@ -55,12 +48,10 @@ const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) if (!is_Term_kind(k)) FatalError("BBTerm: Illegal kind to BBTerm", term); - ASTVec::const_iterator kids_end = term.end(); - unsigned int num_bits = term.GetValueWidth(); - switch (k) - { - case BVNEG: - { + const ASTVec::const_iterator kids_end = term.end(); + const unsigned int num_bits = term.GetValueWidth(); + switch (k) { + case BVNEG: { // bitwise complement const BBNodeVec& bbkids = BBTerm(term[0], support); result = BBNeg(bbkids); @@ -69,8 +60,7 @@ const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) case BVRIGHTSHIFT: case BVSRSHIFT: - case BVLEFTSHIFT: - { + case BVLEFTSHIFT: { // Barrel shifter const BBNodeVec& bbarg1 = BBTerm(term[0], support); const BBNodeVec& bbarg2 = BBTerm(term[1], support); @@ -88,18 +78,16 @@ const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) // 8.2 so round up to 9. const unsigned width = bbarg1.size(); - unsigned log2Width = log2(width) + 1; + const unsigned log2Width = (unsigned) log2(width) + 1; if (k == BVSRSHIFT || k == BVRIGHTSHIFT) - for (unsigned int i = 0; i < log2Width; i++) - { + for (unsigned int i = 0; i < log2Width; i++) { if (bbarg2[i] == nf->getFalse()) continue; // Not shifting by anything. unsigned int shift_amount = 1 << i; - for (unsigned int j = 0; j < width; j++) - { + for (unsigned int j = 0; j < width; j++) { if (j + shift_amount >= width) temp_result[j] = nf->CreateNode(ITE, bbarg2[i], toFill, temp_result[j]); @@ -109,15 +97,13 @@ const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) } } else - for (unsigned int i = 0; i < log2Width; i++) - { + for (unsigned int i = 0; i < log2Width; i++) { if (bbarg2[i] == nf->getFalse()) continue; // Not shifting by anything. int shift_amount = 1 << i; - for (signed int j = width - 1; j >= 0; j--) - { + for (signed int j = width - 1; j >= 0; j--) { if (j < shift_amount) temp_result[j] = nf->CreateNode(ITE, bbarg2[i], toFill, temp_result[j]); @@ -129,13 +115,11 @@ const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) // If any of the remainder are true. Then the whole thing gets the fill value. BBNode remainder = nf->getFalse(); - for (unsigned int i = log2Width; i < width; i++) - { + for (unsigned int i = log2Width; i < width; i++) { remainder = nf->CreateNode(OR, remainder, bbarg2[i]); } - for (unsigned int i = 0; i < width; i++) - { + for (unsigned int i = 0; i < width; i++) { temp_result[i] = nf->CreateNode(ITE, remainder, toFill, temp_result[i]); } @@ -144,114 +128,69 @@ const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) } break; - case ITE: - { + case ITE: { // Term version of ITE. const BBNode& cond = BBForm(term[0], support); const BBNodeVec& thn = BBTerm(term[1], support); const BBNodeVec& els = BBTerm(term[2], support); - result = BBITE(cond, thn, - els); + result = BBITE(cond, thn, els); break; } - case BVSX: - { + case BVSX: { // Replicate high-order bit as many times as necessary. // Arg 0 is expression to be sign extended. const ASTNode& arg = term[0]; - unsigned long result_width = term.GetValueWidth(); - unsigned long arg_width = arg.GetValueWidth(); + const unsigned long result_width = term.GetValueWidth(); + const unsigned long arg_width = arg.GetValueWidth(); const BBNodeVec& bbarg = BBTerm(arg, support); - if (result_width == arg_width) - { + if (result_width == arg_width) { //nothing to sign extend result = bbarg; break; - } - else - { + } else { //we need to sign extend const BBNode& msb = bbarg.back(); - //const ASTNode& msb1 = msbX; - - //BBNodeVec ccc = msbX; - //const BBNode& msb = nf->CreateNode(msbX.GetKind(), ccc); - - // Old version - // ASTNode msb = bbarg.back(); - // const ASTNode msb1 = msb; - - // ASTVec ccc = msb.GetChildren(); - // msb = CreateSimpForm(msb.GetKind(),ccc); - // DD 1/14/07 Simplify silently drops all but first two args of XOR. - // I expanded XOR to N args with flattening optimization. - // This bug took 2 days to track down! - - // msb = SimplifyFormula(msb,false); - - // cout << "!!!!!!!!!!!!!!!!" << endl - // << "Simplify msb:" << msb2 << endl - // << "Simplify result:" << msb << endl; - - //FIXME Dynamically allocate the result vector? - //Is this doing multiple copies? - //ASTVec& tmp_res = *(new ASTVec(result_width)); BBNodeVec tmp_res(result_width); - //FIXME Should these be gotten from result? BBNodeVec::const_iterator bb_it = bbarg.begin(); BBNodeVec::iterator res_it = tmp_res.begin(); BBNodeVec::iterator res_ext = res_it + arg_width; // first bit of extended part BBNodeVec::iterator res_end = tmp_res.end(); + // copy LSBs directly from bbvec - for (; res_it < res_ext; (res_it++, bb_it++)) - { + for (; res_it < res_ext; (res_it++, bb_it++)) { *res_it = *bb_it; } // repeat MSB to fill up rest of result. - for (; res_it < res_end; (res_it++)) - { + for (; res_it < res_end; (res_it++)) { *res_it = msb; } - //Temporary debugging code - // cout << "Sign extending:" << endl - // << " Vec "; - // lpvec( bbarg.GetChildren() ); - // cout << " Extended to "; - // lp(result); - // cout << endl; - result = tmp_res; - break; } } - case BVEXTRACT: - { + case BVEXTRACT: { // bitblast the child, then extract the relevant bits. // Note: This could be optimized by not bitblasting the bits // that aren't fetched. But that would be tricky, especially // with memo-ization. - //FIXME Using const ASTNode w/out reference const BBNodeVec& bbkids = BBTerm(term[0], support); - unsigned int high = GetUnsignedConst(term[1]); - unsigned int low = GetUnsignedConst(term[2]); + const unsigned int high = GetUnsignedConst(term[1]); + const unsigned int low = GetUnsignedConst(term[2]); BBNodeVec::const_iterator bbkfit = bbkids.begin(); // I should have used pointers to BBNodeVec, to avoid this crock - //FIXME Creates a new local BBNodeVec and does the CreateNode from that - result =BBNodeVec(bbkfit + low, bbkfit + high + 1); + result = BBNodeVec(bbkfit + low, bbkfit + high + 1); break; } - case BVCONCAT: - { + case BVCONCAT: { const BBNodeVec& vec1 = BBTerm(term[0], support); const BBNodeVec& vec2 = BBTerm(term[1], support); @@ -260,46 +199,38 @@ const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) result = tmp_res; break; } - case BVPLUS: - { - // ASSERT: at least one child. - // ASSERT: all children and result are the same size. - // Previous phase must make sure this is true. + case BVPLUS: { + assert(term.Degree() >=1); // Add children pairwise and accumulate in BBsum - // FIXME: Unnecessary array copies. ASTVec::const_iterator it = term.begin(); BBNodeVec tmp_res = BBTerm(*it, support); - for (++it; it < kids_end; it++) - { + for (++it; it < kids_end; it++) { const BBNodeVec& tmp = BBTerm(*it, support); + assert(tmp.size() == num_bits); BBPlus2(tmp_res, tmp, nf->getFalse()); } - result = tmp_res; + result = tmp_res; break; } - case BVUMINUS: - { + case BVUMINUS: { const BBNodeVec& bbkid = BBTerm(term[0], support); - result =BBUminus(bbkid); + result = BBUminus(bbkid); break; } - case BVSUB: - { + case BVSUB: { // complement of subtrahend // copy, since BBSub writes into it. - //FIXME: Unnecessary array copies? BBNodeVec tmp_res = BBTerm(term[0], support); const BBNodeVec& bbkid1 = BBTerm(term[1], support); BBSub(tmp_res, bbkid1, support); - result =tmp_res; + result = tmp_res; break; } - case BVMULT: - { + case BVMULT: { assert(BVTypeCheck(term)); const ASTNode& t0 = term[0]; @@ -307,30 +238,26 @@ const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) const BBNodeVec& mpcd1 = BBTerm(t0, support); const BBNodeVec& mpcd2 = BBTerm(t1, support); - //Reverese the order of the nodes w/out the need for temporaries + assert(mpcd1.size() == mpcd2.size()); + //Revereses the order of the nodes w/out the need for temporaries //This is needed because t0 an t1 must be const - if ((BVCONST != t0.GetKind()) && (BVCONST == t1.GetKind())) - { - assert(mpcd1.size() == mpcd2.size()); - result = BBMult( mpcd2, - mpcd1, support); - } - else - { - assert(mpcd1.size() == mpcd2.size()); - result = BBMult(mpcd1,mpcd2, support); + if ((BVCONST != t0.GetKind()) && (BVCONST == t1.GetKind())) { + + result = BBMult(mpcd2, mpcd1, support); + } else { + result = BBMult(mpcd1, mpcd2, support); } break; } case BVDIV: - case BVMOD: - { + case BVMOD: { const BBNodeVec& dvdd = BBTerm(term[0], support); const BBNodeVec& dvsr = BBTerm(term[1], support); - unsigned int width = dvdd.size(); - BBNodeVec q(width); - BBNodeVec r(width); - BBDivMod(dvdd, dvsr, q, r, width, support); + assert (dvdd.size() == num_bits); + assert (dvsr.size() == num_bits); + BBNodeVec q(num_bits); + BBNodeVec r(num_bits); + BBDivMod(dvdd, dvsr, q, r, num_bits, support); if (k == BVDIV) result = q; else @@ -343,13 +270,11 @@ const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) case BVAND: case BVOR: case BVNOR: - case BVNAND: - { + case BVNAND: { // Add children pairwise and accumulate in BBsum ASTVec::const_iterator it = term.begin(); Kind bk = UNDEFINED; // Kind of individual bit op. - switch (k) - { + switch (k) { case BVXOR: bk = XOR; break; @@ -379,83 +304,63 @@ const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) BBNodeVec sum(temp); // First operand. // Iterate over remaining bitvector term operands - for (++it; it < kids_end; it++) - { + for (++it; it < kids_end; it++) { //FIXME FIXME FIXME: Why does using a temp. var change the behavior? temp = BBTerm(*it, support); const BBNodeVec& y = temp; - int n = y.size(); - for (int i = 0; i < n; i++) - { + assert(y.size() == num_bits); + for (unsigned i = 0; i < num_bits; i++) { sum[i] = nf->CreateNode(bk, sum[i], y[i]); } } result = sum; break; } - case SYMBOL: - { + case SYMBOL: { assert(num_bits >0); BBNodeVec bbvec; bbvec.reserve(num_bits); - for (unsigned int i = 0; i < num_bits; i++) - { + for (unsigned int i = 0; i < num_bits; i++) { BBNode bit_node = nf->CreateSymbol(term, i); bbvec.push_back(bit_node); } result = bbvec; break; } - case BVCONST: - { + case BVCONST: { BBNodeVec tmp_res(num_bits); CBV bv = term.GetBVConst(); - for (unsigned int i = 0; i < num_bits; i++) - { + for (unsigned int i = 0; i < num_bits; i++) { tmp_res[i] = CONSTANTBV::BitVector_bit_test(bv, i) ? nf->getTrue() : nf->getFalse(); } result = tmp_res; break; } - case BOOLVEC: - { - cerr << "Hit a boolvec! what to do?" << endl; - break; - } default: FatalError("BBTerm: Illegal kind to BBTerm", term); } - if (result.size() != term.GetValueWidth()) - { - //cerr << result; - //cerr << term; - //cerr << term.GetValueWidth(); - assert(result.size() == term.GetValueWidth()); - } assert(result.size() == term.GetValueWidth()); + return (BBTermMemo[term] = result); } // bit blast a formula (boolean term). Result is one bit wide, -const BBNode BitBlasterNew::BBForm(const ASTNode& form, BBNodeSet& support) -{ +const BBNode BitBlasterNew::BBForm(const ASTNode& form, BBNodeSet& support) { BBNodeMap::iterator it = BBFormMemo.find(form); - if (it != BBFormMemo.end()) - { + if (it != BBFormMemo.end()) { // already there. Just return it. return it->second; } BBNode result; - Kind k = form.GetKind(); - if (!is_Form_kind(k)) - { + const Kind k = form.GetKind(); + if (!is_Form_kind(k)) { FatalError("BBForm: Illegal kind: ", form); } @@ -463,17 +368,14 @@ const BBNode BitBlasterNew::BBForm(const ASTNode& form, BBNodeSet& support) // to trace coherently. // Various special cases - switch (k) - { + switch (k) { - case TRUE: - { + case TRUE: { result = nf->getTrue(); break; } - case FALSE: - { + case FALSE: { result = nf->getFalse(); break; } @@ -481,24 +383,14 @@ const BBNode BitBlasterNew::BBForm(const ASTNode& form, BBNodeSet& support) case SYMBOL: assert (form.GetType() == BOOLEAN_TYPE); - result = nf->CreateSymbol(form,0); // 1 bit symbol. + result = nf->CreateSymbol(form, 0); // 1 bit symbol. break; - case BVGETBIT: - { - // exactly two children - const BBNodeVec bbchild = BBTerm(form[0], support); - unsigned int index = GetUnsignedConst(form[1]); - result = bbchild[index]; - break; - } - case NOT: result = nf->CreateNode(NOT, BBForm(form[0], support)); break; case ITE: - // FIXME: SHould this be CreateSimpITE? result = nf->CreateNode(ITE, BBForm(form[0], support), BBForm(form[1], support), BBForm(form[2], support)); break; @@ -509,22 +401,18 @@ const BBNode BitBlasterNew::BBForm(const ASTNode& form, BBNodeSet& support) case NOR: case IFF: case XOR: - case IMPLIES: - { - //printf("bit-blasting AND or OR\n"); + case IMPLIES: { BBNodeVec bbkids; // bit-blasted children (formulas) ASTVec::const_iterator kids_end = form.end(); - for (ASTVec::const_iterator it = form.begin(); it != kids_end; it++) - { + for (ASTVec::const_iterator it = form.begin(); it != kids_end; it++) { bbkids.push_back(BBForm(*it, support)); } result = nf->CreateNode(k, bbkids); break; } - case EQ: - { + case EQ: { const BBNodeVec left = BBTerm(form[0], support); const BBNodeVec right = BBTerm(form[1], support); assert (left.size() == right.size()); @@ -540,8 +428,7 @@ const BBNode BitBlasterNew::BBForm(const ASTNode& form, BBNodeSet& support) case BVSLE: case BVSGE: case BVSGT: - case BVSLT: - { + case BVSLT: { result = BBcompare(form, support); break; } @@ -557,45 +444,31 @@ const BBNode BitBlasterNew::BBForm(const ASTNode& form, BBNodeSet& support) // Bit blast a sum of two equal length BVs. // Update sum vector destructively with new sum. -void BitBlasterNew::BBPlus2(BBNodeVec& sum, const BBNodeVec& y, BBNode cin) -{ - // cout << "Bitblasting plus. Operand 1: " << endl; - // lpvec(sum); - // cout << endl << " operand 2: " << endl; - // lpvec(y); - // cout << endl << "carry: " << endl << cin << endl; - +void BitBlasterNew::BBPlus2(BBNodeVec& sum, const BBNodeVec& y, BBNode cin) { const int n = sum.size(); assert(y.size() == (unsigned)n); - // FIXME: Don't bother computing i+1 carry, which is discarded. - for (int i = 0; i < n; i++) - { + // Revision 320 avoided creating the nextcin, at I suspect unjustified cost. + for (int i = 0; i < n; i++) { BBNode nextcin = Majority(sum[i], y[i], cin); - sum[i] = nf->CreateNode(XOR, nf->CreateNode(XOR, sum[i], y[i]), cin); + sum[i] = nf->CreateNode(XOR, sum[i], y[i], cin); cin = nextcin; } - - // cout << "----------------" << endl << "Result: " << endl; - // lpvec(sum); - // cout << endl; - } // Stores result - x in result, destructively -void BitBlasterNew::BBSub(BBNodeVec& result, const BBNodeVec& y, BBNodeSet& support) -{ +void BitBlasterNew::BBSub(BBNodeVec& result, const BBNodeVec& y, + BBNodeSet& support) { BBNodeVec compsubtrahend = BBNeg(y); BBPlus2(result, compsubtrahend, nf->getTrue()); } // Add one bit -BBNodeVec BitBlasterNew::BBAddOneBit(BBNodeVec& x, BBNode cin) -{ - BBNodeVec result = BBNodeVec(); - BBNodeVec::const_iterator itend = x.end(); - for (BBNodeVec::const_iterator it = x.begin(); it < itend; it++) - { +BBNodeVec BitBlasterNew::BBAddOneBit(BBNodeVec& x, BBNode cin) { + BBNodeVec result; + result.reserve(x.size()); + const BBNodeVec::const_iterator itend = x.end(); + for (BBNodeVec::const_iterator it = x.begin(); it < itend; it++) { BBNode nextcin = nf->CreateNode(AND, *it, cin); result.push_back(nf->CreateNode(XOR, *it, cin)); cin = nextcin; @@ -604,135 +477,108 @@ BBNodeVec BitBlasterNew::BBAddOneBit(BBNodeVec& x, BBNode cin) } // Increment bit-blasted vector and return result. -BBNodeVec BitBlasterNew::BBInc(BBNodeVec& x) -{ +BBNodeVec BitBlasterNew::BBInc(BBNodeVec& x) { return BBAddOneBit(x, nf->getTrue()); } // Return formula for majority function of three bits. // Pass arguments by reference to reduce refcounting. BBNode BitBlasterNew::Majority(const BBNode& a, const BBNode& b, - const BBNode& c) -{ + const BBNode& c) { // Checking explicitly for constant a, b and c could // be more efficient, because they are repeated in the logic. - if (nf->getTrue() == a) - { + if (nf->getTrue() == a) { return nf->CreateNode(OR, b, c); - } - else if (nf->getFalse() == a) - { + } else if (nf->getFalse() == a) { return nf->CreateNode(AND, b, c); - } - else if (nf->getTrue() == b) - { + } else if (nf->getTrue() == b) { return nf->CreateNode(OR, a, c); - } - else if (nf->getFalse() == b) - { + } else if (nf->getFalse() == b) { return nf->CreateNode(AND, a, c); - } - else if (nf->getTrue() == c) - { + } else if (nf->getTrue() == c) { return nf->CreateNode(OR, a, b); - } - else if (nf->getFalse() == c) - { + } else if (nf->getFalse() == c) { return nf->CreateNode(AND, a, b); } // there are lots more simplifications, but I'm not sure they're // worth doing explicitly (e.g., a = b, a = ~b, etc.) - else - { + else { return nf->CreateNode(OR, nf->CreateNode(AND, a, b), nf->CreateNode( AND, b, c), nf->CreateNode(AND, a, c)); } } // Bitwise complement -BBNodeVec BitBlasterNew::BBNeg(const BBNodeVec& x) -{ +BBNodeVec BitBlasterNew::BBNeg(const BBNodeVec& x) { BBNodeVec result; result.reserve(x.size()); // Negate each bit. const BBNodeVec::const_iterator& xend = x.end(); - for (BBNodeVec::const_iterator it = x.begin(); it < xend; it++) - { + for (BBNodeVec::const_iterator it = x.begin(); it < xend; it++) { result.push_back(nf->CreateNode(NOT, *it)); } return result; } // Compute unary minus -BBNodeVec BitBlasterNew::BBUminus(const BBNodeVec& x) -{ +BBNodeVec BitBlasterNew::BBUminus(const BBNodeVec& x) { BBNodeVec xneg = BBNeg(x); return BBInc(xneg); } // AND each bit of vector y with single bit b and return the result. -BBNodeVec BitBlasterNew::BBAndBit(const BBNodeVec& y, BBNode b) -{ - BBNodeVec result(0); - - if (nf->getTrue() == b) - { - return y; - } - - BBNodeVec::const_iterator yend = y.end(); - for (BBNodeVec::const_iterator yit = y.begin(); yit < yend; yit++) - { - result.push_back(nf->CreateNode(AND, *yit, b)); - } - return result; -} +BBNodeVec BitBlasterNew::BBAndBit(const BBNodeVec& y, BBNode b) { + if (nf->getTrue() == b) { + return y; + } + BBNodeVec result; + result.reserve(y.size()); + const BBNodeVec::const_iterator yend = y.end(); + for (BBNodeVec::const_iterator yit = y.begin(); yit < yend; yit++) { + result.push_back(nf->CreateNode(AND, *yit, b)); + } + return result; +} // Multiply two bitblasted numbers -ASTVec BitBlasterNew::BBMult(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support) -{ - BBNodeVec ycopy(y); - BBNodeVec::const_iterator xend = x.end(); - BBNodeVec::const_iterator xit = x.begin(); - // start prod with first partial product. - BBNodeVec prod = BBNodeVec(BBAndBit(y, *xit)); - // start loop at next bit. - for (xit++; xit < xend; xit++) - { - // shift first - BBLShift(ycopy,1); - - if (nf->getFalse() == *xit) - { - // If this bit is zero, the partial product will - // be zero. No reason to add that in. - continue; - } - - BBNodeVec pprod = BBAndBit(ycopy, *xit); - // accumulate in the product. - BBPlus2(prod, pprod, ASTFalse); - } - return prod; +ASTVec BitBlasterNew::BBMult(const BBNodeVec& x, const BBNodeVec& y, + BBNodeSet& support) { + BBNodeVec ycopy(y); + const BBNodeVec::const_iterator xend = x.end(); + BBNodeVec::const_iterator xit = x.begin(); + // start prod with first partial product. + BBNodeVec prod = BBNodeVec(BBAndBit(y, *xit)); + // start loop at next bit. + for (xit++; xit < xend; xit++) { + // shift first + BBLShift(ycopy, 1); + + if (nf->getFalse() == *xit) { + // If this bit is zero, the partial product will + // be zero. No reason to add that in. + continue; + } + + BBNodeVec pprod = BBAndBit(ycopy, *xit); + // accumulate in the product. + BBPlus2(prod, pprod, ASTFalse); + } + return prod; } // This implements a variant of binary long division. // q and r are "out" parameters. rwidth puts a bound on the // recursion depth. -void BitBlasterNew::BBDivMod(const BBNodeVec &y, const BBNodeVec &x, BBNodeVec &q, - BBNodeVec &r, unsigned int rwidth, BBNodeSet& support) -{ - unsigned int width = y.size(); - if (rwidth == 0) - { +void BitBlasterNew::BBDivMod(const BBNodeVec &y, const BBNodeVec &x, + BBNodeVec &q, BBNodeVec &r, unsigned int rwidth, BBNodeSet& support) { + const unsigned int width = y.size(); + if (rwidth == 0) { // When we have shifted the entire width, y is guaranteed to be 0. q = BBfill(width, nf->getFalse()); r = BBfill(width, nf->getFalse()); - } - else - { + } else { BBNodeVec q1, r1; BBNodeVec yrshift1(y); BBRShift(yrshift1, 1); @@ -761,9 +607,10 @@ void BitBlasterNew::BBDivMod(const BBNodeVec &y, const BBNodeVec &x, BBNodeVec & BBNodeVec one = BBfill(width, nf->getFalse()); one[0] = nf->getTrue(); BBNodeVec notylessxqval = BBITE(yeqx, one, ygtrxqval); - BBNodeVec notylessxrval = BBITE(yeqx, BBfill(width, nf->getFalse()), ygtrxrval); + BBNodeVec notylessxrval = BBITE(yeqx, BBfill(width, nf->getFalse()), + ygtrxrval); // y < x <=> not x >= y. - BBNode ylessx = nf->CreateNode(NOT, BBBVLE(x, y, false)); + BBNode ylessx = BBBVLE(y, x, false, true); // final values of q and r q = BBITE(ylessx, BBfill(width, nf->getFalse()), notylessxqval); r = BBITE(ylessx, y, notylessxrval); @@ -772,23 +619,19 @@ void BitBlasterNew::BBDivMod(const BBNodeVec &y, const BBNodeVec &x, BBNodeVec & // build ITE's (ITE cond then[i] else[i]) for each i. BBNodeVec BitBlasterNew::BBITE(const BBNode& cond, const BBNodeVec& thn, - const BBNodeVec& els) -{ + const BBNodeVec& els) { // Fast exits. - if (cond == nf->getTrue()) - { + if (cond == nf->getTrue()) { return thn; - } - else if (cond == nf->getFalse()) - { + } else if (cond == nf->getFalse()) { return els; } - BBNodeVec result(0); - BBNodeVec::const_iterator th_it_end = thn.end(); + BBNodeVec result; + result.reserve(els.size()); + const BBNodeVec::const_iterator th_it_end = thn.end(); BBNodeVec::const_iterator el_it = els.begin(); - for (BBNodeVec::const_iterator th_it = thn.begin(); th_it < th_it_end; th_it++, el_it++) - { + for (BBNodeVec::const_iterator th_it = thn.begin(); th_it < th_it_end; th_it++, el_it++) { result.push_back(nf->CreateNode(ITE, cond, *th_it, *el_it)); } return result; @@ -800,52 +643,57 @@ BBNodeVec BitBlasterNew::BBITE(const BBNode& cond, const BBNodeVec& thn, // 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. -BBNode BitBlasterNew::BBBVLE(const BBNodeVec& left, const BBNodeVec& right, - bool is_signed, bool is_bvlt) -{ - // "thisbit" represents BVLE of the suffixes of the BVs - // from that position . if R < L, return TRUE, else if L < R - // return FALSE, else return BVLE of lower-order bits. MSB is - // treated separately, because signed comparison is done by - // complementing the MSB of each BV, then doing an unsigned - // comparison. - BBNodeVec::const_iterator lit = left.begin(); - BBNodeVec::const_iterator litend = left.end(); - BBNodeVec::const_iterator rit = right.begin(); - BBNode prevbit = nf->getTrue(); - for (; lit < litend - 1; lit++, rit++) - { - assert(!prevbit.IsNull()); - assert(!rit->IsNull()); - BBNode thisbit = nf->CreateNode(ITE, nf->CreateNode(IFF, *rit, *lit), - prevbit, *rit); - prevbit = thisbit; - } - - // Handle MSB -- negate MSBs if signed comparison - BBNode lmsb = *lit; - BBNode rmsb = *rit; - if (is_signed) - { - lmsb = nf->CreateNode(NOT, *lit); - rmsb = nf->CreateNode(NOT, *rit); - } - - BBNode msb = nf->CreateNode(ITE, nf->CreateNode(IFF, rmsb, lmsb), prevbit, - rmsb); - return msb; +ASTNode BitBlasterNew::BBBVLE(const BBNodeVec& left, const BBNodeVec& right, + bool is_signed, bool is_bvlt) { + BBNodeVec::const_reverse_iterator lit = left.rbegin(); + const BBNodeVec::const_reverse_iterator litend = left.rend(); + BBNodeVec::const_reverse_iterator rit = right.rbegin(); + + BBNode this_compare_bit = is_signed ? nf->CreateNode(AND, *lit, + nf->CreateNode(NOT,*rit)) : nf->CreateNode(AND, + nf->CreateNode(NOT,*lit), *rit); + + BBNodeVec bit_comparisons; + bit_comparisons.reserve(left.size() +1); + + bit_comparisons.push_back(this_compare_bit); + + //(lit IFF rit) is the same as (NOT(lit) XOR rit) + BBNode prev_eq_bit = nf->CreateNode(XOR, nf->CreateNode(NOT, + *lit), *rit); + for (lit++, rit++; lit < litend; lit++, rit++) { + this_compare_bit = nf->CreateNode(AND, nf->CreateNode(NOT,*lit), + *rit); + + BBNode thisbit_output = nf->CreateNode(AND, this_compare_bit, + prev_eq_bit); + bit_comparisons.push_back(thisbit_output); + + BBNode this_eq_bit = nf->CreateNode(AND, nf->CreateNode(XOR, + nf->CreateNode(NOT, *lit), *rit), prev_eq_bit); + prev_eq_bit = this_eq_bit; + } + + if (!is_bvlt) { + bit_comparisons.push_back(prev_eq_bit); + } + BBNode output = +#ifdef CRYPTOMINISAT2 + _bm->CreateSimpForm(XOR, bit_comparisons); +#else + _bm->CreateSimpForm(OR, bit_comparisons); +#endif + return output; } // Left shift within fixed field inserting zeros at LSB. // Writes result into first argument. -void BitBlasterNew::BBLShift(BBNodeVec& x, unsigned int shift) -{ +void BitBlasterNew::BBLShift(BBNodeVec& x, unsigned int shift) { // left shift x (destructively) within width. // loop backwards so that copy to self works correctly. (DON'T use STL insert!) - BBNodeVec::iterator xbeg = x.begin(); + const BBNodeVec::iterator xbeg = x.begin(); BBNodeVec::iterator xit = x.end() - 1; - for (; xit >= xbeg; xit--) - { + for (; xit >= xbeg; xit--) { if (xit - shift >= xbeg) *xit = *(xit - shift); else @@ -855,13 +703,11 @@ void BitBlasterNew::BBLShift(BBNodeVec& x, unsigned int shift) // Right shift within fixed field inserting zeros at MSB. // Writes result into first argument. -void BitBlasterNew::BBRShift(BBNodeVec& x, unsigned int shift) -{ +void BitBlasterNew::BBRShift(BBNodeVec& x, unsigned int shift) { // right shift x (destructively) within width. - BBNodeVec::iterator xend = x.end(); + const BBNodeVec::iterator xend = x.end(); BBNodeVec::iterator xit = x.begin(); - for (; xit < xend; xit++) - { + for (; xit < xend; xit++) { if (xit + shift < xend) *xit = *(xit + shift); else @@ -869,69 +715,42 @@ void BitBlasterNew::BBRShift(BBNodeVec& x, unsigned int shift) } } -// Right shift within fixed field copying the MSB. -// Writes result into first argument. -void BitBlasterNew::BBRSignedShift(BBNodeVec& x, unsigned int shift) -{ - // right shift x (destructively) within width. - BBNode & MSB = x.back(); - BBNodeVec::iterator xend = x.end(); - BBNodeVec::iterator xit = x.begin(); - for (; xit < xend; xit++) - { - if (xit + shift < xend) - *xit = *(xit + shift); - else - *xit = MSB; // new MSB is zero. - } -} - // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. -BBNode BitBlasterNew::BBcompare(const ASTNode& form, BBNodeSet& support) -{ +BBNode BitBlasterNew::BBcompare(const ASTNode& form, BBNodeSet& support) { const BBNodeVec& left = BBTerm(form[0], support); const BBNodeVec& right = BBTerm(form[1], support); - Kind k = form.GetKind(); - switch (k) - { - case BVLE: - { + const Kind k = form.GetKind(); + switch (k) { + case BVLE: { return BBBVLE(left, right, false); break; } - case BVGE: - { + case BVGE: { return BBBVLE(right, left, false); break; } - case BVGT: - { - return nf->CreateNode(NOT, BBBVLE(left, right, false)); + case BVGT: { + return BBBVLE(right, left, false, true); break; } - case BVLT: - { - return nf->CreateNode(NOT, BBBVLE(right, left, false)); + case BVLT: { + return BBBVLE(left, right, false, true); break; } - case BVSLE: - { + case BVSLE: { return BBBVLE(left, right, true); break; } - case BVSGE: - { + case BVSGE: { return BBBVLE(right, left, true); break; } - case BVSGT: - { + case BVSGT: { return nf->CreateNode(NOT, BBBVLE(left, right, true)); break; } - case BVSLT: - { + case BVSLT: { return nf->CreateNode(NOT, BBBVLE(right, left, true)); break; } @@ -939,43 +758,34 @@ BBNode BitBlasterNew::BBcompare(const ASTNode& form, BBNodeSet& support) cerr << "BBCompare: Illegal kind" << form << endl; FatalError("", ASTUndefined); } - throw new std::runtime_error("sdafsaf12``"); } // return a vector with n copies of fillval -BBNodeVec BitBlasterNew::BBfill(unsigned int width, BBNode fillval) -{ +BBNodeVec BitBlasterNew::BBfill(unsigned int width, BBNode fillval) { BBNodeVec zvec(width, fillval); return zvec; } -BBNode BitBlasterNew::BBEQ(const BBNodeVec& left, const BBNodeVec& right) -{ +BBNode BitBlasterNew::BBEQ(const BBNodeVec& left, const BBNodeVec& right) { BBNodeVec andvec; andvec.reserve(left.size()); BBNodeVec::const_iterator lit = left.begin(); - BBNodeVec::const_iterator litend = left.end(); + const BBNodeVec::const_iterator litend = left.end(); BBNodeVec::const_iterator rit = right.begin(); - if (left.size() > 1) - { - for (; lit != litend; lit++, rit++) - { + if (left.size() > 1) { + for (; lit != litend; lit++, rit++) { BBNode biteq = nf->CreateNode(IFF, *lit, *rit); // fast path exit - if (biteq == nf->getFalse()) - { + if (biteq == nf->getFalse()) { return nf->getFalse(); - } - else - { + } else { andvec.push_back(biteq); } } BBNode n = nf->CreateNode(AND, andvec); return n; - } - else + } else return nf->CreateNode(IFF, *lit, *rit); } diff --git a/src/to-sat/BitBlastNew.h b/src/to-sat/BitBlastNew.h index 50f6b72..cfb61c6 100644 --- a/src/to-sat/BitBlastNew.h +++ b/src/to-sat/BitBlastNew.h @@ -84,7 +84,6 @@ class BitBlasterNew { // Return formula for majority function of three formulas. BBNode Majority(const BBNode& a, const BBNode& b, const BBNode& c); - BBNode Sum(const BBNode& xi, const BBNode& yi, const BBNode& cin); // Internal bit blasting routines. BBNode BBBVLE(const BBNodeVec& x, const BBNodeVec& y, bool is_signed, @@ -93,7 +92,6 @@ class BitBlasterNew { // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. BBNode BBcompare(const ASTNode& form, BBNodeSet& support); - void BBRSignedShift(BBNodeVec& x, unsigned int shift); void BBLShift(BBNodeVec& x, unsigned int shift); void BBRShift(BBNodeVec& x, unsigned int shift);