From 449137798aa0ca44014f4f2fa51fe7fb32042a86 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 1 Mar 2010 15:03:22 +0000 Subject: [PATCH] First step of integrating Bitblasting to AIGs. * The Bitblaster now produces BBNodes, not ASTNodes. Currently BBNodes are typedefed to ASTNodes. * Improvements were made to the trunk's Bitblaster while I was working on this. I'll merge them in next. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@622 e59a4935-1847-0410-ae03-e826735625c1 --- src/to-sat/BBNode.h | 17 + src/to-sat/BBNodeManager.h | 65 ++ src/to-sat/BitBlastNew.cpp | 982 ++++++++++++++++++++++++++++++ src/to-sat/BitBlastNew.h | 133 ++++ src/to-sat/CallSAT.cpp | 12 + src/to-sat/ToSAT.h | 1 - src/to-sat/{ => old}/BitBlast.cpp | 0 src/to-sat/{ => old}/BitBlast.h | 0 8 files changed, 1209 insertions(+), 1 deletion(-) create mode 100644 src/to-sat/BBNode.h create mode 100644 src/to-sat/BBNodeManager.h create mode 100644 src/to-sat/BitBlastNew.cpp create mode 100644 src/to-sat/BitBlastNew.h rename src/to-sat/{ => old}/BitBlast.cpp (100%) rename src/to-sat/{ => old}/BitBlast.h (100%) diff --git a/src/to-sat/BBNode.h b/src/to-sat/BBNode.h new file mode 100644 index 0000000..f79341b --- /dev/null +++ b/src/to-sat/BBNode.h @@ -0,0 +1,17 @@ +#ifndef BBNODE_H_ +#define BBNODE_H_ + +#include "../AST/AST.h" + +namespace BEEV { +typedef ASTNode BBNode; + +typedef vector BBNodeVec; +typedef vector > BBNodeVecVec; +typedef map BBNodeMap; +typedef map BBNodeVecMap; +typedef set BBNodeSet; +} +; + +#endif diff --git a/src/to-sat/BBNodeManager.h b/src/to-sat/BBNodeManager.h new file mode 100644 index 0000000..6aadbc3 --- /dev/null +++ b/src/to-sat/BBNodeManager.h @@ -0,0 +1,65 @@ +#ifndef BBNodeManager_H_ +#define BBNodeManager_H_ + +#include "BBNode.h" +#include "../STPManager/STPManager.h" + +namespace BEEV { +class ASTNode; +typedef std::vector ASTVec; + +extern BBNodeVec _empty_BBNodeVec; + +class BBNodeManager { + ASTNode ASTTrue, ASTFalse; + STPMgr *stp; + +public: + BBNodeManager(STPMgr *_stp) { + stp = _stp; + ASTTrue = stp->CreateNode(TRUE); + ASTFalse = stp->CreateNode(FALSE); + } + + ~BBNodeManager() { + } + + BBNode getFalse() { + return ASTFalse; + } + + BBNode CreateSymbol(const ASTNode& n, unsigned i) { + if (n.GetType() == BOOLEAN_TYPE) { + assert(i == 0); + return n; + } else + return stp->CreateNode(BVGETBIT, n, stp->CreateBVConst(32, i)); + } + + BBNode getTrue() { + return ASTTrue; + } + + // CreateSimpForm removes IFF which aren't handled by the cnf converter. + BBNode CreateNode(Kind kind, BBNodeVec& children) { + return stp->CreateSimpForm(kind, children); + } + + BBNode CreateNode(Kind kind, const BBNode& child0) { + return stp->CreateSimpForm(kind, child0); + } + + BBNode CreateNode(Kind kind, const BBNode& child0, const BBNode& child1) { + return stp->CreateSimpForm(kind, child0, child1); + } + + BBNode CreateNode(Kind kind, const BBNode& child0, const BBNode& child1, + const BBNode& child2) { + return stp->CreateSimpForm(kind, child0, child1, child2); + } +}; + +} +; + +#endif /* BBNodeManager_H_ */ diff --git a/src/to-sat/BitBlastNew.cpp b/src/to-sat/BitBlastNew.cpp new file mode 100644 index 0000000..18e2d2d --- /dev/null +++ b/src/to-sat/BitBlastNew.cpp @@ -0,0 +1,982 @@ +/******************************************************************** + * AUTHORS: David L. Dill, Vijay Ganesh, Trevor Hansen + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- + +#include "BitBlastNew.h" +#include "../AST/AST.h" +#include +#include +#include + + +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. + ********************************************************************/ + +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) +{ + BBNodeVecMap::iterator it = BBTermMemo.find(term); + if (it != BBTermMemo.end()) + { + // already there. Just return it. + return it->second; + } + + BBNodeVec result; + + const Kind k = term.GetKind(); + 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: + { + // bitwise complement + const BBNodeVec& bbkids = BBTerm(term[0], support); + result = BBNeg(bbkids); + break; + } + + case BVRIGHTSHIFT: + case BVSRSHIFT: + case BVLEFTSHIFT: + { + // Barrel shifter + const BBNodeVec& bbarg1 = BBTerm(term[0], support); + const BBNodeVec& bbarg2 = BBTerm(term[1], support); + + // Signed right shift, need to copy the sign bit. + BBNode toFill; + if (BVSRSHIFT == k) + toFill = bbarg1.back(); + else + toFill = nf->getFalse(); + + BBNodeVec temp_result(bbarg1); + // if any bit is set in bbarg2 higher than log2Width, then we know that the result is zero. + // Add one to make allowance for rounding down. For example, given 300 bits, the log2 is about + // 8.2 so round up to 9. + + const unsigned width = bbarg1.size(); + unsigned log2Width = log2(width) + 1; + + if (k == BVSRSHIFT || k == BVRIGHTSHIFT) + 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++) + { + if (j + shift_amount >= width) + temp_result[j] = nf->CreateNode(ITE, bbarg2[i], toFill, + temp_result[j]); + else + temp_result[j] = nf->CreateNode(ITE, bbarg2[i], + temp_result[j + shift_amount], temp_result[j]); + } + } + else + 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--) + { + if (j < shift_amount) + temp_result[j] = nf->CreateNode(ITE, bbarg2[i], toFill, + temp_result[j]); + else + temp_result[j] = nf->CreateNode(ITE, bbarg2[i], + temp_result[j - shift_amount], temp_result[j]); + } + } + + // 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++) + { + remainder = nf->CreateNode(OR, remainder, bbarg2[i]); + } + + for (unsigned int i = 0; i < width; i++) + { + temp_result[i] = nf->CreateNode(ITE, remainder, toFill, + temp_result[i]); + } + + result = temp_result; + } + break; + + 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); + break; + } + + 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 BBNodeVec& bbarg = BBTerm(arg, support); + + if (result_width == arg_width) + { + //nothing to sign extend + result = bbarg; + break; + } + 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++)) + { + *res_it = *bb_it; + } + // repeat MSB to fill up rest of result. + 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: + { + // 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]); + + 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); + break; + } + case BVCONCAT: + { + const BBNodeVec& vec1 = BBTerm(term[0], support); + const BBNodeVec& vec2 = BBTerm(term[1], support); + + BBNodeVec tmp_res(vec2); + tmp_res.insert(tmp_res.end(), vec1.begin(), vec1.end()); + 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. + // 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++) + { + const BBNodeVec& tmp = BBTerm(*it, support); + BBPlus2(tmp_res, tmp, nf->getFalse()); + } + + result = tmp_res; + break; + } + case BVUMINUS: + { + const BBNodeVec& bbkid = BBTerm(term[0], support); + result =BBUminus(bbkid); + break; + } + 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; + break; + } + case BVMULT: + { + assert(BVTypeCheck(term)); + + const ASTNode& t0 = term[0]; + const ASTNode& t1 = term[1]; + + const BBNodeVec& mpcd1 = BBTerm(t0, support); + const BBNodeVec& mpcd2 = BBTerm(t1, support); + //Reverese 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); + } + break; + } + case BVDIV: + 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); + if (k == BVDIV) + result = q; + else + result = r; + break; + } + // n-ary bitwise operators. + case BVXOR: + case BVXNOR: + case BVAND: + case BVOR: + case BVNOR: + 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) + { + case BVXOR: + bk = XOR; + break; + case BVXNOR: + bk = IFF; + break; + case BVAND: + bk = AND; + break; + case BVOR: + bk = OR; + break; + case BVNOR: + bk = NOR; + break; + case BVNAND: + bk = NAND; + break; + default: + FatalError("BBTerm: Illegal kind to BBTerm", term); + break; + } + + // Sum is destructively modified in the loop, so make a copy of value + // returned by BBTerm. + BBNodeVec temp = BBTerm(*it, support); + BBNodeVec sum(temp); // First operand. + + // Iterate over remaining bitvector term operands + 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++) + { + sum[i] = nf->CreateNode(bk, sum[i], y[i]); + } + } + result = sum; + break; + } + case SYMBOL: + { + assert(num_bits >0); + + BBNodeVec bbvec; + bbvec.reserve(num_bits); + + 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: + { + BBNodeVec tmp_res(num_bits); + CBV bv = term.GetBVConst(); + 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) +{ + BBNodeMap::iterator it = BBFormMemo.find(form); + if (it != BBFormMemo.end()) + { + // already there. Just return it. + return it->second; + } + + BBNode result; + + Kind k = form.GetKind(); + if (!is_Form_kind(k)) + { + FatalError("BBForm: Illegal kind: ", form); + } + + // Not returning until end, and memoizing everything, makes it easier + // to trace coherently. + + // Various special cases + switch (k) + { + + case TRUE: + { + result = nf->getTrue(); + break; + } + + case FALSE: + { + result = nf->getFalse(); + break; + } + + case SYMBOL: + assert (form.GetType() == BOOLEAN_TYPE); + + 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; + + case AND: + case OR: + case NAND: + case NOR: + case IFF: + case XOR: + case IMPLIES: + { + //printf("bit-blasting AND or OR\n"); + BBNodeVec bbkids; // bit-blasted children (formulas) + + ASTVec::const_iterator kids_end = form.end(); + 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: + { + const BBNodeVec left = BBTerm(form[0], support); + const BBNodeVec right = BBTerm(form[1], support); + assert (left.size() == right.size()); + + result = BBEQ(left, right); + break; + } + + case BVLE: + case BVGE: + case BVGT: + case BVLT: + case BVSLE: + case BVSGE: + case BVSGT: + case BVSLT: + { + result = BBcompare(form, support); + break; + } + default: + FatalError("BBForm: Illegal kind: ", form); + break; + } + + assert(!result.IsNull()); + + return (BBFormMemo[form] = result); +} + +// 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; + + + 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++) + { + BBNode nextcin = Majority(sum[i], y[i], cin); + sum[i] = nf->CreateNode(XOR, 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) +{ + 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++) + { + BBNode nextcin = nf->CreateNode(AND, *it, cin); + result.push_back(nf->CreateNode(XOR, *it, cin)); + cin = nextcin; + } + return result; +} + +// Increment bit-blasted vector and return result. +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) +{ + // Checking explicitly for constant a, b and c could + // be more efficient, because they are repeated in the logic. + if (nf->getTrue() == a) + { + return nf->CreateNode(OR, b, c); + } + else if (nf->getFalse() == a) + { + return nf->CreateNode(AND, b, c); + } + else if (nf->getTrue() == b) + { + return nf->CreateNode(OR, a, c); + } + else if (nf->getFalse() == b) + { + return nf->CreateNode(AND, a, c); + } + else if (nf->getTrue() == c) + { + return nf->CreateNode(OR, a, b); + } + 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 + { + 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 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++) + { + result.push_back(nf->CreateNode(NOT, *it)); + } + return result; +} + +// Compute unary minus +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; +} + + + +// 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; +} + +// 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) + { + // When we have shifted the entire width, y is guaranteed to be 0. + q = BBfill(width, nf->getFalse()); + r = BBfill(width, nf->getFalse()); + } + else + { + BBNodeVec q1, r1; + BBNodeVec yrshift1(y); + BBRShift(yrshift1, 1); + + // recursively divide y/2 by x. + BBDivMod(yrshift1, x, q1, r1, rwidth - 1, support); + + BBNodeVec q1lshift1(q1); + BBLShift(q1lshift1, 1); + + BBNodeVec r1lshift1(r1); + BBLShift(r1lshift1, 1); + + BBNodeVec r1lshift1plusyodd = BBAddOneBit(r1lshift1, y[0]); + BBNodeVec rminusx(r1lshift1plusyodd); + BBSub(rminusx, x, support); + + // Adjusted q, r values when when r is too large. + BBNode rtoolarge = BBBVLE(x, r1lshift1plusyodd, false); + BBNodeVec ygtrxqval = BBITE(rtoolarge, BBInc(q1lshift1), q1lshift1); + BBNodeVec ygtrxrval = BBITE(rtoolarge, rminusx, r1lshift1plusyodd); + + // q & r values when y >= x + BBNode yeqx = BBEQ(y, x); + // *** Problem: the bbfill for qval is wrong. Should be 1, not -1. + 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); + // y < x <=> not x >= y. + BBNode ylessx = nf->CreateNode(NOT, BBBVLE(x, y, false)); + // final values of q and r + q = BBITE(ylessx, BBfill(width, nf->getFalse()), notylessxqval); + r = BBITE(ylessx, y, notylessxrval); + } +} + +// build ITE's (ITE cond then[i] else[i]) for each i. +BBNodeVec BitBlasterNew::BBITE(const BBNode& cond, const BBNodeVec& thn, + const BBNodeVec& els) +{ + // Fast exits. + if (cond == nf->getTrue()) + { + return thn; + } + else if (cond == nf->getFalse()) + { + return els; + } + + BBNodeVec result(0); + 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++) + { + result.push_back(nf->CreateNode(ITE, cond, *th_it, *el_it)); + } + return result; +} + +// 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. +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; +} + +// Left shift within fixed field inserting zeros at LSB. +// Writes result into first argument. +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(); + BBNodeVec::iterator xit = x.end() - 1; + for (; xit >= xbeg; xit--) + { + if (xit - shift >= xbeg) + *xit = *(xit - shift); + else + *xit = nf->getFalse(); // new LSB is zero. + } +} + +// Right shift within fixed field inserting zeros at MSB. +// Writes result into first argument. +void BitBlasterNew::BBRShift(BBNodeVec& x, unsigned int shift) +{ + // right shift x (destructively) within width. + BBNodeVec::iterator xend = x.end(); + BBNodeVec::iterator xit = x.begin(); + for (; xit < xend; xit++) + { + if (xit + shift < xend) + *xit = *(xit + shift); + else + *xit = nf->getFalse(); // new MSB is zero. + } +} + +// 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) +{ + const BBNodeVec& left = BBTerm(form[0], support); + const BBNodeVec& right = BBTerm(form[1], support); + + Kind k = form.GetKind(); + switch (k) + { + case BVLE: + { + return BBBVLE(left, right, false); + break; + } + case BVGE: + { + return BBBVLE(right, left, false); + break; + } + case BVGT: + { + return nf->CreateNode(NOT, BBBVLE(left, right, false)); + break; + } + case BVLT: + { + return nf->CreateNode(NOT, BBBVLE(right, left, false)); + break; + } + case BVSLE: + { + return BBBVLE(left, right, true); + break; + } + case BVSGE: + { + return BBBVLE(right, left, true); + break; + } + case BVSGT: + { + return nf->CreateNode(NOT, BBBVLE(left, right, true)); + break; + } + case BVSLT: + { + return nf->CreateNode(NOT, BBBVLE(right, left, true)); + break; + } + default: + 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 zvec(width, fillval); + return zvec; +} + +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(); + BBNodeVec::const_iterator rit = right.begin(); + + if (left.size() > 1) + { + for (; lit != litend; lit++, rit++) + { + BBNode biteq = nf->CreateNode(IFF, *lit, *rit); + // fast path exit + if (biteq == nf->getFalse()) + { + return nf->getFalse(); + } + else + { + andvec.push_back(biteq); + } + } + BBNode n = nf->CreateNode(AND, andvec); + return n; + } + else + return nf->CreateNode(IFF, *lit, *rit); +} + +} // BEEV namespace diff --git a/src/to-sat/BitBlastNew.h b/src/to-sat/BitBlastNew.h new file mode 100644 index 0000000..50f6b72 --- /dev/null +++ b/src/to-sat/BitBlastNew.h @@ -0,0 +1,133 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Vijay Ganesh, Trevor Hansen + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ + +#ifndef BITBLASTNEW_H +#define BITBLASTNEW_H + +#include +#include +#include "../AST/AST.h" +#include "BBNodeManager.h" +#include "../STPManager/STPManager.h" + +namespace BEEV { +class BitBlasterNew; + +class BitBlasterNew { + + // Memo table for bit blasted terms. If a node has already been + // bitblasted, it is mapped to a vector of Boolean formulas for + // the + BBNodeVecMap BBTermMemo; + + // Memo table for bit blasted formulas. If a node has already + // been bitblasted, it is mapped to a node representing the + // bitblasted equivalent + BBNodeMap BBFormMemo; + + STPMgr * _bm; + ASTNode ASTTrue, ASTFalse, ASTUndefined; + + /**************************************************************** + * Private Member Functions * + ****************************************************************/ + + // Get vector of Boolean formulas for sum of two + // vectors of Boolean formulas + void BBPlus2(BBNodeVec& sum, const BBNodeVec& y, BBNode cin); + + // Increment + BBNodeVec BBInc(BBNodeVec& x); + + // Add one bit to a vector of bits. + BBNodeVec BBAddOneBit(BBNodeVec& x, BBNode cin); + + // Bitwise complement + BBNodeVec BBNeg(const BBNodeVec& x); + + // Unary minus + BBNodeVec BBUminus(const BBNodeVec& x); + + // Multiply. + ASTVec BBMult(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support); + + BBNodeVec BBAndBit(const BBNodeVec& y, BBNode b); + + // AND each bit of vector y with single bit b and return the result. + // (used in BBMult) + //BBNodeVec BBAndBit(const BBNodeVec& y, ASTNode b); + + // Returns BBNodeVec for result - y. This destroys "result". + void BBSub(BBNodeVec& result, const BBNodeVec& y, BBNodeSet& support); + + // build ITE's (ITE cond then[i] else[i]) for each i. + BBNodeVec BBITE(const BBNode& cond, const BBNodeVec& thn, + const BBNodeVec& els); + + // Build a vector of zeros. + BBNodeVec BBfill(unsigned int width, BBNode fillval); + + // build an EQ formula + BBNode BBEQ(const BBNodeVec& left, const BBNodeVec& right); + + // This implements a variant of binary long division. + // q and r are "out" parameters. rwidth puts a bound on the + // recursion depth. Unsigned only, for now. + void BBDivMod(const BBNodeVec &y, const BBNodeVec &x, BBNodeVec &q, + BBNodeVec &r, unsigned int rwidth, BBNodeSet& support); + + // 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, + bool is_bvlt = false); + + // 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); + + BBNodeManager* nf; + + // 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 BBTerm(const ASTNode& term, BBNodeSet& support); + +public: + + /**************************************************************** + * Public Member Functions * + ****************************************************************/ + + BitBlasterNew(STPMgr * bm) : + _bm(bm) { + ASTTrue = _bm->CreateNode(TRUE); + ASTFalse = _bm->CreateNode(FALSE); + ASTUndefined = _bm->CreateNode(UNDEFINED); + nf = new BBNodeManager(bm); + } + + ~BitBlasterNew() { + BBTermMemo.clear(); + BBFormMemo.clear(); + delete nf; + } + + //Bitblast a formula + const BBNode BBForm(const ASTNode& form, BBNodeSet& support); + +}; //end of class BitBlaster +} +; //end of namespace +#endif diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp index a0de401..eae8831 100644 --- a/src/to-sat/CallSAT.cpp +++ b/src/to-sat/CallSAT.cpp @@ -7,6 +7,7 @@ * LICENSE: Please view LICENSE file in the home dir of this Program ********************************************************************/ #include "ToSAT.h" +#include "BitBlastNew.h" namespace BEEV { @@ -74,6 +75,8 @@ namespace BEEV return sat; } + + //Call the SAT solver, and check the result before returning. This //can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or //SOLVER_UNDECIDED @@ -82,8 +85,17 @@ namespace BEEV const ASTNode& original_input) { bm->GetRunTimes()->start(RunTimes::BitBlasting); + +#if 1 + BitBlasterNew BB(bm); + BBNodeSet set; + ASTNode BBFormula = BB.BBForm(modified_input,set); + assert(set.size() == 0); // doesn't yet work. +#else BitBlaster BB(bm); ASTNode BBFormula = BB.BBForm(modified_input); +#endif + bm->ASTNodeStats("after bitblasting: ", BBFormula); bm->GetRunTimes()->stop(RunTimes::BitBlasting); diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h index af53590..8359ae5 100644 --- a/src/to-sat/ToSAT.h +++ b/src/to-sat/ToSAT.h @@ -11,7 +11,6 @@ #define TOSAT_H #include -#include "BitBlast.h" #include "ToCNF.h" #include "../AST/AST.h" diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/old/BitBlast.cpp similarity index 100% rename from src/to-sat/BitBlast.cpp rename to src/to-sat/old/BitBlast.cpp diff --git a/src/to-sat/BitBlast.h b/src/to-sat/old/BitBlast.h similarity index 100% rename from src/to-sat/BitBlast.h rename to src/to-sat/old/BitBlast.h -- 2.47.3