From: vijay_ganesh Date: Mon, 5 Oct 2009 23:10:08 +0000 (+0000) Subject: reorganized ToCNF X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=306c3612ae65a38547d32797d518589461dc19aa;p=francis%2Fstp.git reorganized ToCNF git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@281 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/Makefile b/Makefile index de87db7..c457f19 100644 --- a/Makefile +++ b/Makefile @@ -71,7 +71,7 @@ clean: $(MAKE) clean -C $(SRC)/extlib-constbv $(MAKE) clean -C $(SRC)/parser $(MAKE) clean -C $(SRC)/main - + $(MAKE) clean -C tests/c-api-tests .PHONY: regressall regressall: diff --git a/scripts/Makefile.in b/scripts/Makefile.in index de87db7..c457f19 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -71,7 +71,7 @@ clean: $(MAKE) clean -C $(SRC)/extlib-constbv $(MAKE) clean -C $(SRC)/parser $(MAKE) clean -C $(SRC)/main - + $(MAKE) clean -C tests/c-api-tests .PHONY: regressall regressall: diff --git a/src/AST/AST.h b/src/AST/AST.h index fbb9cad..7d1bc43 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -48,6 +48,12 @@ namespace BEEV ASTNode::ASTNodeHasher, ASTNode::ASTNodeEqual> ASTNodeMultiSet; + // Datatype for clauses + typedef vector* ClausePtr; + + // Datatype for Clauselists + typedef vector ClauseList; + // Function to dump contents of ASTNodeMap ostream &operator<<(ostream &os, const ASTNodeMap &nmap); }; // end namespace BEEV diff --git a/src/AST/ASTNode.h b/src/AST/ASTNode.h index 809e665..3f7b8a1 100644 --- a/src/AST/ASTNode.h +++ b/src/AST/ASTNode.h @@ -68,6 +68,7 @@ namespace BEEV /**************************************************************** * Public Member Functions * ****************************************************************/ + // Default constructor. ASTNode() :_int_node_ptr(NULL) {}; diff --git a/src/STPManager/STPManager.cpp b/src/STPManager/STPManager.cpp index 0e84781..0842935 100644 --- a/src/STPManager/STPManager.cpp +++ b/src/STPManager/STPManager.cpp @@ -815,19 +815,6 @@ namespace BEEV } _ASTNode_to_Bitvector.clear(); - /* OLD Destructor - * for(ASTNodeToVecMap::iterator ivec = BBTermMemo.begin(), - ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) { - ivec->second.clear(); - }*/ - - /*What should I do here? For ASTNodes? - * for(ASTNodeMap::iterator ivec = BBTermMemo.begin(), - ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) { - ivec->second.clear(); - }*/ - BBTermMemo.clear(); - BBFormMemo.clear(); NodeLetVarMap.clear(); NodeLetVarMap1.clear(); PLPrintNodeSet.clear(); @@ -875,19 +862,6 @@ namespace BEEV } _ASTNode_to_Bitvector.clear(); - /*OLD destructor - * for(ASTNodeToVecMap::iterator ivec = BBTermMemo.begin(), - ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) { - ivec->second.clear(); - }*/ - - /*What should I do here? - *for(ASTNodeMap::iterator ivec = BBTermMemo.begin(), - ivec_end=BBTermMemo.end();ivec!=ivec_end;ivec++) { - ivec->second.clear(); - }*/ - BBTermMemo.clear(); - BBFormMemo.clear(); NodeLetVarMap.clear(); NodeLetVarMap1.clear(); PLPrintNodeSet.clear(); diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 714b05e..bc5c65c 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -114,8 +114,6 @@ void vc_setFlags(char c) { BEEV::FatalError(s.c_str()); break; } - - } //Create a validity Checker. This is the global BeevMgr diff --git a/src/main/Globals.h b/src/main/Globals.h index fca9d40..1a475d5 100644 --- a/src/main/Globals.h +++ b/src/main/Globals.h @@ -127,7 +127,8 @@ namespace BEEV extern BeevMgr * GlobalBeevMgr; //Empty vector - extern std::vector _empty_ASTVec; + extern std::vector _empty_ASTVec; + extern ASTNode ASTFalse, ASTTrue, ASTUndefined; //Some global vars for the Main function. extern const char * prog; diff --git a/src/main/main.cpp b/src/main/main.cpp index e94bef6..4826384 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -39,8 +39,6 @@ int main(int argc, char ** argv) { // individual hash tables are being allocated if (sbrk(INITIAL_MEMORY_PREALLOCATION_SIZE) == ((void *) -1)) { - // FIXME: figure out how to get and print the real error - // message. FatalError("Initial allocation of memory failed."); } @@ -101,7 +99,6 @@ int main(int argc, char ** argv) { case 'h': fprintf(stderr,usage,prog); cout << helpstring; - //FatalError(""); return -1; break; case 'n': diff --git a/src/printer/AssortedPrinters.cpp b/src/printer/AssortedPrinters.cpp index e2600d1..3a0a87b 100644 --- a/src/printer/AssortedPrinters.cpp +++ b/src/printer/AssortedPrinters.cpp @@ -338,17 +338,17 @@ namespace BEEV } //end of PrintOutput() - void BeevMgr::PrintClauseList(ostream& os, BeevMgr::ClauseList& cll) - { - int num_clauses = cll.size(); - os << "Clauses: " << endl << "=========================================" << endl; - for (int i = 0; i < num_clauses; i++) - { - os << "Clause " << i << endl << "-------------------------------------------" << endl; - LispPrintVecSpecial(os, *cll[i], 0); - os << endl << "-------------------------------------------" << endl; - } - } //end of PrintClauseList() +// void BeevMgr::PrintClauseList(ostream& os, BeevMgr::ClauseList& cll) +// { +// int num_clauses = cll.size(); +// os << "Clauses: " << endl << "=========================================" << endl; +// for (int i = 0; i < num_clauses; i++) +// { +// os << "Clause " << i << endl << "-------------------------------------------" << endl; +// LispPrintVecSpecial(os, *cll[i], 0); +// os << endl << "-------------------------------------------" << endl; +// } +// } //end of PrintClauseList() //Variable Order Printer: A global function which converts a MINISAT //var into a ASTNODE var. It then prints this var along with diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp index abf9f3b..a0c5e2b 100644 --- a/src/simplifier/bvsolver.cpp +++ b/src/simplifier/bvsolver.cpp @@ -251,7 +251,7 @@ namespace BEEV //handle BVPLUS case ASTVec c = lhs.GetChildren(); ASTVec o; - ASTNode outmonom = _bm->CreateNode(UNDEFINED); + ASTNode outmonom = ASTUndefined; bool chosen_symbol = false; bool chosen_odd = false; diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h index 49adb53..c4b8db6 100644 --- a/src/simplifier/bvsolver.h +++ b/src/simplifier/bvsolver.h @@ -38,7 +38,7 @@ namespace BEEV //(i.e. construct various kinds of expressions), and also has //member functions that simplify bit-vector expressions BeevMgr * _bm; - ASTNode ASTTrue, ASTFalse; + ASTNode ASTTrue, ASTFalse, ASTUndefined; //Those formulas which have already been solved. If the same //formula occurs twice then do not solve the second occurence, and @@ -123,6 +123,7 @@ namespace BEEV { ASTTrue = _bm->CreateNode(TRUE); ASTFalse = _bm->CreateNode(FALSE); + ASTUndefined = _bm->CreateNode(UNDEFINED); } ; diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp index 186e90e..974ed67 100644 --- a/src/to-sat/BitBlast.cpp +++ b/src/to-sat/BitBlast.cpp @@ -11,6 +11,7 @@ #include #include "../AST/AST.h" #include "../STPManager/STPManager.h" +#include "BitBlast.h" namespace BEEV { @@ -29,8 +30,7 @@ namespace BEEV * vector corresponds to bit 0 -- the low-order bit. ********************************************************************/ - ASTNode ASTJunk; - const ASTNode BeevMgr::BBTerm(const ASTNode& term) + const ASTNode BitBlaster::BBTerm(const ASTNode& term) { //CHANGED TermMemo is now an ASTNodeMap. Based on BBFormMemo @@ -57,7 +57,7 @@ namespace BEEV // bitblast the child. //FIXME Uses a tempory const ASTNode const ASTNode& bbkids = BBTerm(term[0]); - result = CreateNode(BOOLVEC, BBNeg(bbkids.GetChildren())); + result = _bm->CreateNode(BOOLVEC, BBNeg(bbkids.GetChildren())); break; } @@ -82,7 +82,7 @@ namespace BEEV // 8.2 so round up to 9. const unsigned width = bbarg1.size(); - unsigned log2Width = log2(width) + 1; + unsigned log2Width = (unsigned)log2(width) + 1; if (k == BVSRSHIFT || k == BVRIGHTSHIFT) @@ -96,9 +96,9 @@ namespace BEEV for (unsigned int j = 0; j < width; j++) { if (j + shift_amount >= width) - temp_result[j] = CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]); + temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]); else - temp_result[j] = CreateSimpForm(ITE, bbarg2[i], temp_result[j + shift_amount], temp_result[j]); + temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], temp_result[j + shift_amount], temp_result[j]); } } else @@ -112,9 +112,9 @@ namespace BEEV for (signed int j = width - 1; j > 0; j--) { if (j < shift_amount) - temp_result[j] = CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]); + temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], toFill, temp_result[j]); else - temp_result[j] = CreateSimpForm(ITE, bbarg2[i], temp_result[j - shift_amount], temp_result[j]); + temp_result[j] = _bm->CreateSimpForm(ITE, bbarg2[i], temp_result[j - shift_amount], temp_result[j]); } } @@ -122,15 +122,15 @@ namespace BEEV ASTNode remainder = ASTFalse; for (unsigned int i = log2Width; i < width; i++) { - remainder = CreateNode(OR, remainder, bbarg2[i]); + remainder = _bm->CreateNode(OR, remainder, bbarg2[i]); } for (unsigned int i = 0; i < width; i++) { - temp_result[i] = CreateSimpForm(ITE, remainder, toFill, temp_result[i]); + temp_result[i] = _bm->CreateSimpForm(ITE, remainder, toFill, temp_result[i]); } - result = CreateNode(BOOLVEC, temp_result); + result = _bm->CreateNode(BOOLVEC, temp_result); } break; case BVVARSHIFT: @@ -146,7 +146,7 @@ namespace BEEV const ASTNode& cond = BBForm(term[0]); const ASTNode& thn = BBTerm(term[1]); const ASTNode& els = BBTerm(term[2]); - result = CreateNode(BOOLVEC, BBITE(cond, thn.GetChildren(), els.GetChildren())); + result = _bm->CreateNode(BOOLVEC, BBITE(cond, thn.GetChildren(), els.GetChildren())); break; } @@ -173,14 +173,14 @@ namespace BEEV //const ASTNode& msb1 = msbX; ASTVec ccc = msbX.GetChildren(); - const ASTNode& msb = CreateSimpForm(msbX.GetKind(), ccc); + const ASTNode& msb = _bm->CreateSimpForm(msbX.GetKind(), ccc); // Old version // ASTNode msb = bbarg.back(); // const ASTNode msb1 = msb; // ASTVec ccc = msb.GetChildren(); - // msb = CreateSimpForm(msb.GetKind(),ccc); + // msb = _bm->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. @@ -221,7 +221,7 @@ namespace BEEV // lp(result); // cout << endl; - result = CreateNode(BOOLVEC, tmp_res); + result = _bm->CreateNode(BOOLVEC, tmp_res); break; } @@ -264,8 +264,8 @@ namespace BEEV ASTVec::const_iterator bbkfit = bbkids.begin(); // I should have used pointers to ASTVec, to avoid this crock - //FIXME Creates a new local ASTVec and does the CreateNode from that - result = CreateNode(BOOLVEC, ASTVec(bbkfit + low, bbkfit + high + 1)); + //FIXME _bm->Creates a new local ASTVec and does the _bm->CreateNode from that + result = _bm->CreateNode(BOOLVEC, ASTVec(bbkfit + low, bbkfit + high + 1)); /* if(weregood){ printf("spot05\n"); @@ -283,7 +283,7 @@ namespace BEEV //Leaking ASTVec tmp_res = *(new ASTVec(vec2.GetChildren())); ASTVec tmp_res(vec2.GetChildren()); tmp_res.insert(tmp_res.end(), vec1.begin(), vec1.end()); - result = CreateNode(BOOLVEC, tmp_res); + result = _bm->CreateNode(BOOLVEC, tmp_res); break; } case BVPLUS: @@ -302,14 +302,14 @@ namespace BEEV BBPlus2(tmp_res, tmp, ASTFalse); } - result = CreateNode(BOOLVEC, tmp_res); + result = _bm->CreateNode(BOOLVEC, tmp_res); break; } case BVUMINUS: { //FIXME Using const ASTNode reference const ASTNode& bbkid = BBTerm(term[0]); - result = CreateNode(BOOLVEC, BBUminus(bbkid.GetChildren())); + result = _bm->CreateNode(BOOLVEC, BBUminus(bbkid.GetChildren())); break; } case BVSUB: @@ -322,7 +322,7 @@ namespace BEEV const ASTVec& bbkid1 = BBTerm(term[1]).GetChildren(); BBSub(tmp_res, bbkid1); - result = CreateNode(BOOLVEC, tmp_res); + result = _bm->CreateNode(BOOLVEC, tmp_res); break; } case BVMULT: @@ -338,11 +338,11 @@ namespace BEEV //This is needed because t0 an t1 must be const if ((BVCONST != t0.GetKind()) && (BVCONST == t1.GetKind())) { - result = CreateNode(BOOLVEC, BBMult(mpcd2.GetChildren(), mpcd1.GetChildren())); + result = _bm->CreateNode(BOOLVEC, BBMult(mpcd2.GetChildren(), mpcd1.GetChildren())); } else { - result = CreateNode(BOOLVEC, BBMult(mpcd1.GetChildren(), mpcd2.GetChildren())); + result = _bm->CreateNode(BOOLVEC, BBMult(mpcd1.GetChildren(), mpcd2.GetChildren())); } break; } @@ -356,9 +356,9 @@ namespace BEEV ASTVec r(width); BBDivMod(dvdd.GetChildren(), dvsr.GetChildren(), q, r, width); if (k == BVDIV) - result = CreateNode(BOOLVEC, q); + result = _bm->CreateNode(BOOLVEC, q); else - result = CreateNode(BOOLVEC, r); + result = _bm->CreateNode(BOOLVEC, r); break; } // n-ary bitwise operators. @@ -414,10 +414,10 @@ namespace BEEV int n = y.size(); for (int i = 0; i < n; i++) { - sum[i] = CreateSimpForm(bk, sum[i], y[i]); + sum[i] = _bm->CreateSimpForm(bk, sum[i], y[i]); } } - result = CreateNode(BOOLVEC, sum); + result = _bm->CreateNode(BOOLVEC, sum); break; } case SYMBOL: @@ -428,10 +428,10 @@ namespace BEEV ASTVec bbvec; for (unsigned int i = 0; i < num_bits; i++) { - ASTNode bit_node = CreateNode(BVGETBIT, term, CreateBVConst(32, i)); + ASTNode bit_node = _bm->CreateNode(BVGETBIT, term, _bm->CreateBVConst(32, i)); bbvec.push_back(bit_node); } - result = CreateNode(BOOLVEC, bbvec); + result = _bm->CreateNode(BOOLVEC, bbvec); break; } case BVCONST: @@ -443,7 +443,7 @@ namespace BEEV tmp_res[i] = CONSTANTBV::BitVector_bit_test(bv, i) ? ASTTrue : ASTFalse; } - result = CreateNode(BOOLVEC, tmp_res); + result = _bm->CreateNode(BOOLVEC, tmp_res); break; } case BOOLVEC: @@ -455,13 +455,6 @@ namespace BEEV FatalError("BBTerm: Illegal kind to BBTerm", term); } - //if(result == ASTJunk) - // cout<<"result does not change"<CreateSimpNot(BBForm(form[0])); break; case ITE: - // FIXME: SHould this be CreateSimpITE? - result = CreateNode(ITE, BBForm(form[0]), BBForm(form[1]), BBForm(form[2])); + // FIXME: SHould this be _bm->CreateSimpITE? + result = _bm->CreateNode(ITE, BBForm(form[0]), BBForm(form[1]), BBForm(form[2])); break; case AND: @@ -546,7 +538,7 @@ namespace BEEV { bbkids.push_back(BBForm(*it)); } - result = CreateSimpForm(k, bbkids); + result = _bm->CreateSimpForm(k, bbkids); break; } @@ -599,7 +591,7 @@ namespace BEEV // Bit blast a sum of two equal length BVs. // Update sum vector destructively with new sum. - void BeevMgr::BBPlus2(ASTVec& sum, const ASTVec& y, ASTNode cin) + void BitBlaster::BBPlus2(ASTVec& sum, const ASTVec& y, ASTNode cin) { // cout << "Bitblasting plus. Operand 1: " << endl; // lpvec(sum); @@ -614,7 +606,7 @@ namespace BEEV for (int i = 0; i < n; i++) { ASTNode nextcin = Majority(sum[i], y[i], cin); - sum[i] = CreateSimpForm(XOR, CreateSimpForm(XOR, sum[i], y[i]), cin); + sum[i] = _bm->CreateSimpForm(XOR, _bm->CreateSimpForm(XOR, sum[i], y[i]), cin); cin = nextcin; } @@ -625,21 +617,21 @@ namespace BEEV } // Stores result - x in result, destructively - void BeevMgr::BBSub(ASTVec& result, const ASTVec& y) + void BitBlaster::BBSub(ASTVec& result, const ASTVec& y) { ASTVec compsubtrahend = BBNeg(y); BBPlus2(result, compsubtrahend, ASTTrue); } // Add one bit - ASTVec BeevMgr::BBAddOneBit(ASTVec& x, ASTNode cin) + ASTVec BitBlaster::BBAddOneBit(ASTVec& x, ASTNode cin) { ASTVec result = ASTVec(0); ASTVec::const_iterator itend = x.end(); for (ASTVec::const_iterator it = x.begin(); it < itend; it++) { - ASTNode nextcin = CreateSimpForm(AND, *it, cin); - result.push_back(CreateSimpForm(XOR, *it, cin)); + ASTNode nextcin = _bm->CreateSimpForm(AND, *it, cin); + result.push_back(_bm->CreateSimpForm(XOR, *it, cin)); cin = nextcin; } // FIXME: unnecessary array copy on return? @@ -647,72 +639,72 @@ namespace BEEV } // Increment bit-blasted vector and return result. - ASTVec BeevMgr::BBInc(ASTVec& x) + ASTVec BitBlaster::BBInc(ASTVec& x) { return BBAddOneBit(x, ASTTrue); } // Return formula for majority function of three bits. // Pass arguments by reference to reduce refcounting. - ASTNode BeevMgr::Majority(const ASTNode& a, const ASTNode& b, const ASTNode& c) + ASTNode BitBlaster::Majority(const ASTNode& a, const ASTNode& b, const ASTNode& c) { // Checking explicitly for constant a, b and c could // be more efficient, because they are repeated in the logic. if (ASTTrue == a) { - return CreateSimpForm(OR, b, c); + return _bm->CreateSimpForm(OR, b, c); } else if (ASTFalse == a) { - return CreateSimpForm(AND, b, c); + return _bm->CreateSimpForm(AND, b, c); } else if (ASTTrue == b) { - return CreateSimpForm(OR, a, c); + return _bm->CreateSimpForm(OR, a, c); } else if (ASTFalse == b) { - return CreateSimpForm(AND, a, c); + return _bm->CreateSimpForm(AND, a, c); } else if (ASTTrue == c) { - return CreateSimpForm(OR, a, b); + return _bm->CreateSimpForm(OR, a, b); } else if (ASTFalse == c) { - return CreateSimpForm(AND, a, b); + return _bm->CreateSimpForm(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 CreateSimpForm(OR, CreateSimpForm(AND, a, b), CreateSimpForm(AND, b, c), CreateSimpForm(AND, a, c)); + return _bm->CreateSimpForm(OR, _bm->CreateSimpForm(AND, a, b), _bm->CreateSimpForm(AND, b, c), _bm->CreateSimpForm(AND, a, c)); } } // Bitwise complement - ASTVec BeevMgr::BBNeg(const ASTVec& x) + ASTVec BitBlaster::BBNeg(const ASTVec& x) { ASTVec result = ASTVec(0); // FIXME: faster to preallocate n entries? // Negate each bit. ASTVec::const_iterator xend = x.end(); for (ASTVec::const_iterator it = x.begin(); it < xend; it++) { - result.push_back(CreateSimpNot(*it)); + result.push_back(_bm->CreateSimpNot(*it)); } // FIXME: unecessary array copy when it returns? return result; } // Compute unary minus - ASTVec BeevMgr::BBUminus(const ASTVec& x) + ASTVec BitBlaster::BBUminus(const ASTVec& x) { ASTVec xneg = BBNeg(x); return BBInc(xneg); } // Multiply two bitblasted numbers - ASTVec BeevMgr::BBMult(const ASTVec& x, const ASTVec& y) + ASTVec BitBlaster::BBMult(const ASTVec& x, const ASTVec& y) { ASTVec ycopy(y); ASTVec::const_iterator xend = x.end(); @@ -743,7 +735,7 @@ namespace BEEV // This implements a variant of binary long division. // q and r are "out" parameters. rwidth puts a bound on the // recursion depth. - void BeevMgr::BBDivMod(const ASTVec &y, const ASTVec &x, ASTVec &q, ASTVec &r, unsigned int rwidth) + void BitBlaster::BBDivMod(const ASTVec &y, const ASTVec &x, ASTVec &q, ASTVec &r, unsigned int rwidth) { unsigned int width = y.size(); if (rwidth == 0) @@ -784,7 +776,7 @@ namespace BEEV ASTVec notylessxqval = BBITE(yeqx, one, ygtrxqval); ASTVec notylessxrval = BBITE(yeqx, BBfill(width, ASTFalse), ygtrxrval); // y < x <=> not x >= y. - ASTNode ylessx = CreateSimpNot(BBBVLE(x, y, false)); + ASTNode ylessx = _bm->CreateSimpNot(BBBVLE(x, y, false)); // final values of q and r q = BBITE(ylessx, BBfill(width, ASTFalse), notylessxqval); r = BBITE(ylessx, y, notylessxrval); @@ -792,7 +784,7 @@ namespace BEEV } // build ITE's (ITE cond then[i] else[i]) for each i. - ASTVec BeevMgr::BBITE(const ASTNode& cond, const ASTVec& thn, const ASTVec& els) + ASTVec BitBlaster::BBITE(const ASTNode& cond, const ASTVec& thn, const ASTVec& els) { // Fast exits. if (ASTTrue == cond) @@ -809,12 +801,12 @@ namespace BEEV ASTVec::const_iterator el_it = els.begin(); for (ASTVec::const_iterator th_it = thn.begin(); th_it < th_it_end; th_it++, el_it++) { - result.push_back(CreateSimpForm(ITE, cond, *th_it, *el_it)); + result.push_back(_bm->CreateSimpForm(ITE, cond, *th_it, *el_it)); } return result; } // AND each bit of vector y with single bit b and return the result. - ASTVec BeevMgr::BBAndBit(const ASTVec& y, ASTNode b) + ASTVec BitBlaster::BBAndBit(const ASTVec& y, ASTNode b) { ASTVec result(0); @@ -827,7 +819,7 @@ namespace BEEV ASTVec::const_iterator yend = y.end(); for (ASTVec::const_iterator yit = y.begin(); yit < yend; yit++) { - result.push_back(CreateSimpForm(AND, *yit, b)); + result.push_back(_bm->CreateSimpForm(AND, *yit, b)); } return result; } @@ -838,7 +830,7 @@ namespace BEEV // 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 BeevMgr::BBBVLE(const ASTVec& left, const ASTVec& right, bool is_signed) + ASTNode BitBlaster::BBBVLE(const ASTVec& left, const ASTVec& right, bool is_signed) { // "thisbit" represents BVLE of the suffixes of the BVs // from that position . if R < L, return TRUE, else if L < R @@ -852,9 +844,9 @@ namespace BEEV ASTNode prevbit = ASTTrue; for (; lit < litend - 1; lit++, rit++) { - ASTNode neglit = CreateSimpNot(*lit); - ASTNode thisbit = CreateSimpForm(OR, CreateSimpForm(AND, neglit, *rit), // TRUE if l < r - CreateSimpForm(AND, CreateSimpForm(OR, neglit, *rit), // false if not equal + ASTNode neglit = _bm->CreateSimpNot(*lit); + ASTNode thisbit = _bm->CreateSimpForm(OR, _bm->CreateSimpForm(AND, neglit, *rit), // TRUE if l < r + _bm->CreateSimpForm(AND, _bm->CreateSimpForm(OR, neglit, *rit), // false if not equal prevbit)); // else prevbit prevbit = thisbit; } @@ -865,20 +857,20 @@ namespace BEEV ASTNode rmsb = *rit; if (is_signed) { - lmsb = CreateSimpNot(*lit); - rmsb = CreateSimpNot(*rit); + lmsb = _bm->CreateSimpNot(*lit); + rmsb = _bm->CreateSimpNot(*rit); } - ASTNode neglmsb = CreateSimpNot(lmsb); - ASTNode msb = CreateSimpForm(OR, CreateSimpForm(AND, neglmsb, rmsb), // TRUE if l < r - CreateSimpForm(AND, CreateSimpForm(OR, neglmsb, rmsb), // false if not equal + ASTNode neglmsb = _bm->CreateSimpNot(lmsb); + ASTNode msb = _bm->CreateSimpForm(OR, _bm->CreateSimpForm(AND, neglmsb, rmsb), // TRUE if l < r + _bm->CreateSimpForm(AND, _bm->CreateSimpForm(OR, neglmsb, rmsb), // false if not equal prevbit)); // else prevbit return msb; } // Left shift within fixed field inserting zeros at LSB. // Writes result into first argument. - void BeevMgr::BBLShift(ASTVec& x, unsigned int shift) + void BitBlaster::BBLShift(ASTVec& x, unsigned int shift) { // left shift x (destructively) within width. // loop backwards so that copy to self works correctly. (DON'T use STL insert!) @@ -895,7 +887,7 @@ namespace BEEV // Right shift within fixed field inserting zeros at MSB. // Writes result into first argument. - void BeevMgr::BBRShift(ASTVec& x, unsigned int shift) + void BitBlaster::BBRShift(ASTVec& x, unsigned int shift) { // right shift x (destructively) within width. ASTVec::iterator xend = x.end(); @@ -911,7 +903,7 @@ namespace BEEV // Right shift within fixed field copying the MSB. // Writes result into first argument. - void BeevMgr::BBRSignedShift(ASTVec& x, unsigned int shift) + void BitBlaster::BBRSignedShift(ASTVec& x, unsigned int shift) { // right shift x (destructively) within width. ASTNode & MSB = x.back(); @@ -927,7 +919,7 @@ namespace BEEV } // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. - ASTNode BeevMgr::BBcompare(const ASTNode& form) + ASTNode BitBlaster::BBcompare(const ASTNode& form) { const ASTNode lnode = BBTerm(form[0]); const ASTNode rnode = BBTerm(form[1]); @@ -952,12 +944,12 @@ namespace BEEV } case BVGT: { - return CreateSimpNot(BBBVLE(left, right, false)); + return _bm->CreateSimpNot(BBBVLE(left, right, false)); break; } case BVLT: { - return CreateSimpNot(BBBVLE(right, left, false)); + return _bm->CreateSimpNot(BBBVLE(right, left, false)); break; } case BVSLE: @@ -972,12 +964,12 @@ namespace BEEV } case BVSGT: { - return CreateSimpNot(BBBVLE(left, right, true)); + return _bm->CreateSimpNot(BBBVLE(left, right, true)); break; } case BVSLT: { - return CreateSimpNot(BBBVLE(right, left, true)); + return _bm->CreateSimpNot(BBBVLE(right, left, true)); break; } default: @@ -988,13 +980,13 @@ namespace BEEV } // return a vector with n copies of fillval - ASTVec BeevMgr::BBfill(unsigned int width, ASTNode fillval) + ASTVec BitBlaster::BBfill(unsigned int width, ASTNode fillval) { ASTVec zvec(width, fillval); return zvec; } - ASTNode BeevMgr::BBEQ(const ASTVec& left, const ASTVec& right) + ASTNode BitBlaster::BBEQ(const ASTVec& left, const ASTVec& right) { ASTVec andvec; ASTVec::const_iterator lit = left.begin(); @@ -1005,7 +997,7 @@ namespace BEEV { for (; lit != litend; lit++, rit++) { - ASTNode biteq = CreateSimpForm(IFF, *lit, *rit); + ASTNode biteq = _bm->CreateSimpForm(IFF, *lit, *rit); // fast path exit if (biteq == ASTFalse) { @@ -1016,10 +1008,10 @@ namespace BEEV andvec.push_back(biteq); } } - ASTNode n = CreateSimpForm(AND, andvec); + ASTNode n = _bm->CreateSimpForm(AND, andvec); return n; } else - return CreateSimpForm(IFF, *lit, *rit); + return _bm->CreateSimpForm(IFF, *lit, *rit); } } // BEEV namespace diff --git a/src/to-sat/BitBlast.h b/src/to-sat/BitBlast.h new file mode 100644 index 0000000..a0aedd3 --- /dev/null +++ b/src/to-sat/BitBlast.h @@ -0,0 +1,127 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ + +#ifndef BITBLAST_H +#define BITBLAST_H + +#include +#include +#include "../AST/AST.h" +#include "../STPManager/STPManager.h" + +namespace BEEV +{ + class BitBlaster { + private: + /**************************************************************** + * Private Data * + ****************************************************************/ + BeevMgr * _bm; + ASTNode ASTTrue, ASTFalse, ASTUndefined; + + // Memo table for bit blasted terms. If a node has already been + // bitblasted, it is mapped to a vector of Boolean formulas for + // the + ASTNodeMap BBTermMemo; + + // Memo table for bit blasted formulas. If a node has already + // been bitblasted, it is mapped to a node representing the + // bitblasted equivalent + ASTNodeMap BBFormMemo; + + /**************************************************************** + * Private Member Functions * + ****************************************************************/ + + // Get vector of Boolean formulas for sum of two + // vectors of Boolean formulas + void BBPlus2(ASTVec& sum, const ASTVec& y, ASTNode cin); + + // Increment + ASTVec BBInc(ASTVec& x); + + // Add one bit to a vector of bits. + ASTVec BBAddOneBit(ASTVec& x, ASTNode cin); + + // Bitwise complement + ASTVec BBNeg(const ASTVec& x); + + // Unary minus + ASTVec BBUminus(const ASTVec& x); + + // Multiply. + ASTVec BBMult(const ASTVec& x, const ASTVec& y); + + // AND each bit of vector y with single bit b and return the result. + // (used in BBMult) + ASTVec BBAndBit(const ASTVec& y, ASTNode b); + + // Returns ASTVec for result - y. This destroys "result". + void BBSub(ASTVec& result, const ASTVec& y); + + // build ITE's (ITE cond then[i] else[i]) for each i. + ASTVec BBITE(const ASTNode& cond, const ASTVec& thn, const ASTVec& els); + + // Build a vector of zeros. + ASTVec BBfill(unsigned int width, ASTNode fillval); + + // build an EQ formula + ASTNode BBEQ(const ASTVec& left, const ASTVec& 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 ASTVec &y, const ASTVec &x, + ASTVec &q, ASTVec &r, unsigned int rwidth); + + // Return formula for majority function of three formulas. + ASTNode Majority(const ASTNode& a, const ASTNode& b, const ASTNode& c); + + // Internal bit blasting routines. + ASTNode BBBVLE(const ASTVec& x, const ASTVec& y, bool is_signed); + + // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. + ASTNode BBcompare(const ASTNode& form); + + void BBRSignedShift(ASTVec& x, unsigned int shift); + void BBLShift(ASTVec& x, unsigned int shift); + void BBRShift(ASTVec& x, unsigned int shift); + + public: + + /**************************************************************** + * Public Member Functions * + ****************************************************************/ + + BitBlaster(BeevMgr * bm) : _bm(bm) + { + ASTTrue = _bm->CreateNode(TRUE); + ASTFalse = _bm->CreateNode(FALSE); + ASTUndefined = _bm->CreateNode(UNDEFINED); + } + + ~BitBlaster() + { + } + + + // Adds or removes a NOT as necessary to negate a literal. + ASTNode Negate(const ASTNode& form); + + // 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 ASTNode BBTerm(const ASTNode& term); + + //Bitblast a formula + const ASTNode BBForm(const ASTNode& formula); + + }; //end of class BitBlaster +}; //end of namespace +#endif diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp index 64a2711..1770e2f 100644 --- a/src/to-sat/ToCNF.cpp +++ b/src/to-sat/ToCNF.cpp @@ -9,958 +9,859 @@ #include "../AST/AST.h" #include "../STPManager/STPManager.h" -//#include "../simplifier/bvsolver.h" #include "../sat/sat.h" +#include "ToCNF.h" namespace BEEV { + //############################################################ + //############################################################ + void DeleteClauseList(ClauseList *cllp) + { + ClauseList::const_iterator iend = cllp->end(); + for (ClauseList::const_iterator i = cllp->begin(); i < iend; i++) + { + delete *i; + } + delete cllp; + } //End of DeleteClauseList + + bool CNFMgr::isAtom(const ASTNode& varphi) + { + bool result; + + Kind k = varphi.GetKind(); + switch (k) + { + case TRUE: + { + result = true; + break; + } + case FALSE: + { + result = true; + break; + } + case SYMBOL: + { + result = true; + break; + } + case BVCONST: + { + result = true; + break; + } + default: + { + result = false; + break; + } + } + + return result; + } //End of isAtom() + + bool CNFMgr::isPred(const ASTNode& varphi) + { + bool result; + + Kind k = varphi.GetKind(); + switch (k) + { + case BVLT: + { + result = true; + break; + } + case BVLE: + { + result = true; + break; + } + case BVGT: + { + result = true; + break; + } + case BVGE: + { + result = true; + break; + } + case BVSLT: + { + result = true; + break; + } + case BVSLE: + { + result = true; + break; + } + case BVSGT: + { + result = true; + break; + } + case BVSGE: + { + result = true; + break; + } + case EQ: + { + result = true; + break; + } + default: + { + result = false; + break; + } + } + + return result; + } //End of isPred() - class CNFMgr - { - - public: - - //######################################## - //######################################## - // constructor - - CNFMgr(BeevMgr *bmgr) - { - bm = bmgr; - } - - //######################################## - //######################################## - // destructor - - ~CNFMgr() - { - ASTNodeToASTNodePtrMap::const_iterator it1 = store.begin(); - for (; it1 != store.end(); it1++) - { - delete it1->second; - } - - store.clear(); - - } - - //######################################## - //######################################## - // top-level conversion function - - BeevMgr::ClauseList* convertToCNF(const ASTNode& varphi) - { - varphi.GetBeevMgr()->runTimes.start(RunTimes::CNFConversion); - scanFormula(varphi, true); - ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*"); - BeevMgr::ClauseList* defs = SINGLETON(dummy_true_var); - convertFormulaToCNF(varphi, defs); - BeevMgr::ClauseList* top = info[varphi]->clausespos; - defs->insert(defs->begin() + 1, top->begin(), top->end()); - - cleanup(varphi); - varphi.GetBeevMgr()->runTimes.stop(RunTimes::CNFConversion); - return defs; - } - - void DELETE(BeevMgr::ClauseList* varphi) - { - BeevMgr::ClauseList::const_iterator it = varphi->begin(); - for (; it != varphi->end(); it++) - { - delete *it; - } - - delete varphi; - } - - private: - - //######################################## - //######################################## - // data types - - // for the meaning of control bits, see "utilities for contol bits". - typedef struct - { - int control; - BeevMgr::ClauseList* clausespos; - union - { - BeevMgr::ClauseList* clausesneg; - ASTNode* termforcnf; - }; - } CNFInfo; - - typedef hash_map ASTNodeToCNFInfoMap; - - typedef hash_map ASTNodeToASTNodePtrMap; - - //######################################## - //######################################## - // this is the data - - BeevMgr *bm; - ASTNodeToCNFInfoMap info; - ASTNodeToASTNodePtrMap store; - - //######################################## - //######################################## - // utility predicates - - bool isAtom(const ASTNode& varphi) - { - bool result; - - Kind k = varphi.GetKind(); - switch (k) - { - case TRUE: - { - result = true; - break; - } - case FALSE: - { - result = true; - break; - } - case SYMBOL: - { - result = true; - break; - } - case BVCONST: - { - result = true; - break; - } - default: - { - result = false; - break; - } - } - - return result; - } - - bool isPred(const ASTNode& varphi) - { - bool result; - - Kind k = varphi.GetKind(); - switch (k) - { - case BVLT: - { - result = true; - break; - } - case BVLE: - { - result = true; - break; - } - case BVGT: - { - result = true; - break; - } - case BVGE: - { - result = true; - break; - } - case BVSLT: - { - result = true; - break; - } - case BVSLE: - { - result = true; - break; - } - case BVSGT: - { - result = true; - break; - } - case BVSGE: - { - result = true; - break; - } - case EQ: - { - result = true; - break; - } - default: - { - result = false; - break; - } - } - - return result; - } - - bool isITE(const ASTNode& varphi) - { - bool result; - - Kind k = varphi.GetKind(); - switch (k) - { - case ITE: - { - result = true; - break; - } - default: - { - result = false; - break; - } - } - - return result; - } - - bool onChildDoPos(const ASTNode& varphi, unsigned int idx) - { - bool result = true; - - Kind k = varphi.GetKind(); - switch (k) - { - case NOT: - { - result = false; - break; - } - case NAND: - { - result = false; - break; - } - case NOR: - { - result = false; - break; - } - case IMPLIES: - { - if (idx == 0) - { - result = false; - } - break; - } - default: - { - break; - } - } - - return result; - } - - bool onChildDoNeg(const ASTNode& varphi, unsigned int idx) - { - bool result = false; - - Kind k = varphi.GetKind(); - switch (k) - { - case NOT: - { - result = true; - break; - } - case NAND: - { - result = true; - break; - } - case NOR: - { - result = true; - break; - } - case XOR: - { - result = true; - break; - } - case IFF: - { - result = true; - break; - } - case IMPLIES: - { - if (idx == 0) - { - result = true; - } - break; - } - case ITE: - { - if (idx == 0) - { - result = true; - } - break; - } - default: - { - break; - } - } - - return result; - } - - //######################################## - //######################################## - //utilities for control bits. - - void initializeCNFInfo(CNFInfo& x) - { - x.control = 0; - x.clausespos = NULL; - x.clausesneg = NULL; - } - - void incrementSharesPos(CNFInfo& x) - { - x.control += ((x.control & 3) < 2) ? 1 : 0; - } - - int sharesPos(CNFInfo& x) - { - return (x.control & 3); - } - - void incrementSharesNeg(CNFInfo& x) - { - x.control += ((x.control & 12) < 8) ? 4 : 0; - } - - int sharesNeg(CNFInfo& x) - { - return ((x.control & 12) >> 2); - } - - void setControlBit(CNFInfo& x, unsigned int idx) - { - x.control |= (1 << idx); - } - - bool getControlBit(CNFInfo& x, unsigned int idx) - { - bool result = false; - - if (x.control & (1 << idx)) - { - - result = true; - } - - return result; - } - - void setIsTerm(CNFInfo& x) - { - setControlBit(x, 4); - } - - bool isTerm(CNFInfo& x) - { - return getControlBit(x, 4); - } - - void setDoRenamePos(CNFInfo& x) - { - setControlBit(x, 5); - } - - bool doRenamePos(CNFInfo& x) - { - return getControlBit(x, 5); - } - - void setWasRenamedPos(CNFInfo& x) - { - setControlBit(x, 6); - } - - bool wasRenamedPos(CNFInfo& x) - { - return getControlBit(x, 6); - } - - void setDoRenameNeg(CNFInfo& x) - { - setControlBit(x, 7); - } - - bool doRenameNeg(CNFInfo& x) - { - return getControlBit(x, 7); - } - - void setWasRenamedNeg(CNFInfo& x) - { - setControlBit(x, 8); - } - - bool wasRenamedNeg(CNFInfo& x) - { - return getControlBit(x, 8); - } - - void setDoSibRenamingPos(CNFInfo& x) - { - setControlBit(x, 9); - } - - bool doSibRenamingPos(CNFInfo& x) - { - return getControlBit(x, 9); - } - - void setDoSibRenamingNeg(CNFInfo& x) - { - setControlBit(x, 10); - } - - bool doSibRenamingNeg(CNFInfo& x) - { - return getControlBit(x, 10); - } - - void setWasVisited(CNFInfo& x) - { - setControlBit(x, 11); - } - - bool wasVisited(CNFInfo& x) - { - return getControlBit(x, 11); - } - - //######################################## - //######################################## - //utilities for clause sets - - - BeevMgr::ClauseList* COPY(const BeevMgr::ClauseList& varphi) - { - BeevMgr::ClauseList* psi = new BeevMgr::ClauseList(); - - BeevMgr::ClauseList::const_iterator it = varphi.begin(); - for (; it != varphi.end(); it++) - { - psi->push_back(new vector (**it)); - } - - return psi; - } - - BeevMgr::ClauseList* SINGLETON(const ASTNode& varphi) - { - ASTNode* copy = ASTNodeToASTNodePtr(varphi); - - BeevMgr::ClausePtr clause = new vector (); - clause->push_back(copy); - - BeevMgr::ClauseList* psi = new BeevMgr::ClauseList(); - psi->push_back(clause); - return psi; - } - - BeevMgr::ClauseList* UNION(const BeevMgr::ClauseList& varphi1, const BeevMgr::ClauseList& varphi2) - { - - BeevMgr::ClauseList* psi1 = COPY(varphi1); - BeevMgr::ClauseList* psi2 = COPY(varphi2); - psi1->insert(psi1->end(), psi2->begin(), psi2->end()); - delete psi2; - - return psi1; - - } - - void INPLACE_UNION(BeevMgr::ClauseList* varphi1, const BeevMgr::ClauseList& varphi2) - { - - BeevMgr::ClauseList* psi2 = COPY(varphi2); - varphi1->insert(varphi1->end(), psi2->begin(), psi2->end()); - delete psi2; - } - - void NOCOPY_INPLACE_UNION(BeevMgr::ClauseList* varphi1, BeevMgr::ClauseList* varphi2) - { - - varphi1->insert(varphi1->end(), varphi2->begin(), varphi2->end()); - delete varphi2; - } - - BeevMgr::ClauseList* PRODUCT(const BeevMgr::ClauseList& varphi1, const BeevMgr::ClauseList& varphi2) - { - - BeevMgr::ClauseList* psi = new BeevMgr::ClauseList(); - psi->reserve(varphi1.size() * varphi2.size()); + bool CNFMgr::isITE(const ASTNode& varphi) + { + bool result; + + Kind k = varphi.GetKind(); + switch (k) + { + case ITE: + { + result = true; + break; + } + default: + { + result = false; + break; + } + } + + return result; + } //End of isITE() - BeevMgr::ClauseList::const_iterator it1 = varphi1.begin(); - for (; it1 != varphi1.end(); it1++) - { - BeevMgr::ClausePtr clause1 = *it1; - BeevMgr::ClauseList::const_iterator it2 = varphi2.begin(); - for (; it2 != varphi2.end(); it2++) - { - BeevMgr::ClausePtr clause2 = *it2; - BeevMgr::ClausePtr clause = new vector (); - clause->reserve(clause1->size() + clause2->size()); - clause->insert(clause->end(), clause1->begin(), clause1->end()); - clause->insert(clause->end(), clause2->begin(), clause2->end()); - psi->push_back(clause); - } - } + bool CNFMgr::onChildDoPos(const ASTNode& varphi, unsigned int idx) + { + bool result = true; + + Kind k = varphi.GetKind(); + switch (k) + { + case NOT: + { + result = false; + break; + } + case NAND: + { + result = false; + break; + } + case NOR: + { + result = false; + break; + } + case IMPLIES: + { + if (idx == 0) + { + result = false; + } + break; + } + default: + { + break; + } + } + + return result; + } //End of onChildDoPos() - return psi; - } + bool CNFMgr::onChildDoNeg(const ASTNode& varphi, unsigned int idx) + { + bool result = false; + Kind k = varphi.GetKind(); + switch (k) + { + case NOT: + { + result = true; + break; + } + case NAND: + { + result = true; + break; + } + case NOR: + { + result = true; + break; + } + case XOR: + { + result = true; + break; + } + case IFF: + { + result = true; + break; + } + case IMPLIES: + { + if (idx == 0) + { + result = true; + } + break; + } + case ITE: + { + if (idx == 0) + { + result = true; + } + break; + } + default: + { + break; + } + } + + return result; + } //End of onChildDoNeg() + //######################################## //######################################## - //prep. for cnf conversion - - void scanFormula(const ASTNode& varphi, bool isPos) - { - - CNFInfo* x; - - //######################################## - // step 1, get the info associated with this node - //######################################## + //utilities for control bits. - if (info.find(varphi) == info.end()) - { - x = new CNFInfo(); - initializeCNFInfo(*x); - info[varphi] = x; - } - else - { - x = info[varphi]; - } + void CNFMgr::initializeCNFInfo(CNFInfo& x) + { + x.control = 0; + x.clausespos = NULL; + x.clausesneg = NULL; + } //End of initlializeCNFInfo() + + void CNFMgr::incrementSharesPos(CNFInfo& x) + { + x.control += ((x.control & 3) < 2) ? 1 : 0; + } //End of incrementSharesPos() + + int CNFMgr::sharesPos(CNFInfo& x) + { + return (x.control & 3); + } //End of sharesPos() + + void CNFMgr::incrementSharesNeg(CNFInfo& x) + { + x.control += ((x.control & 12) < 8) ? 4 : 0; + } //End of incrementSharesNeg() + + int CNFMgr::sharesNeg(CNFInfo& x) + { + return ((x.control & 12) >> 2); + } //End of sharesNeg() - //######################################## - // step 2, we only need to know if shares >= 2 - //######################################## + void CNFMgr::setControlBit(CNFInfo& x, unsigned int idx) + { + x.control |= (1 << idx); + } //End of setControlBit() + + bool CNFMgr::getControlBit(CNFInfo& x, unsigned int idx) + { + bool result = false; + + if (x.control & (1 << idx)) + { + result = true; + } - if (isPos && sharesPos(*x) == 2) - { - return; - } + return result; + } //End of getControlBit() - if (!isPos && sharesNeg(*x) == 2) - { - return; - } + void CNFMgr::setIsTerm(CNFInfo& x) + { + setControlBit(x, 4); + } //End of setIsTerm() - //######################################## - // step 3, set appropriate information fields - //######################################## + bool CNFMgr::isTerm(CNFInfo& x) + { + return getControlBit(x, 4); + } - if (isPos) - { - incrementSharesPos(*x); - } + void CNFMgr::setDoRenamePos(CNFInfo& x) + { + setControlBit(x, 5); + } - if (!isPos) - { - incrementSharesNeg(*x); - } + bool CNFMgr::doRenamePos(CNFInfo& x) + { + return getControlBit(x, 5); + } - //######################################## - // step 4, recurse over children - //######################################## + void CNFMgr::setWasRenamedPos(CNFInfo& x) + { + setControlBit(x, 6); + } - if (isAtom(varphi)) - { - return; - } - else if (isPred(varphi)) - { - for (unsigned int i = 0; i < varphi.GetChildren().size(); i++) - { - scanTerm(varphi[i]); - } - } - else - { - for (unsigned int i = 0; i < varphi.GetChildren().size(); i++) - { - if (onChildDoPos(varphi, i)) - { - scanFormula(varphi[i], isPos); - } - if (onChildDoNeg(varphi, i)) - { - scanFormula(varphi[i], !isPos); - } - } - } + bool CNFMgr::wasRenamedPos(CNFInfo& x) + { + return getControlBit(x, 6); + } - } + void CNFMgr::setDoRenameNeg(CNFInfo& x) + { + setControlBit(x, 7); + } - void scanTerm(const ASTNode& varphi) - { + bool CNFMgr::doRenameNeg(CNFInfo& x) + { + return getControlBit(x, 7); + } - CNFInfo* x; + void CNFMgr::setWasRenamedNeg(CNFInfo& x) + { + setControlBit(x, 8); + } - //######################################## - // step 1, get the info associated with this node - //######################################## + bool CNFMgr::wasRenamedNeg(CNFInfo& x) + { + return getControlBit(x, 8); + } - if (info.find(varphi) == info.end()) - { - x = new CNFInfo(); - initializeCNFInfo(*x); - info[varphi] = x; - } - else - { - x = info[varphi]; - } + void CNFMgr::setDoSibRenamingPos(CNFInfo& x) + { + setControlBit(x, 9); + } - //######################################## - // step 2, need two hits because of term ITEs. - //######################################## + bool CNFMgr::doSibRenamingPos(CNFInfo& x) + { + return getControlBit(x, 9); + } - if (sharesPos(*x) == 2) - { - return; - } + void CNFMgr::setDoSibRenamingNeg(CNFInfo& x) + { + setControlBit(x, 10); + } - //######################################## - // step 3, set appropriate data fields, always rename - // term ITEs - //######################################## + bool CNFMgr::doSibRenamingNeg(CNFInfo& x) + { + return getControlBit(x, 10); + } - incrementSharesPos(*x); - setIsTerm(*x); + void CNFMgr::setWasVisited(CNFInfo& x) + { + setControlBit(x, 11); + } - //######################################## - // step 4, recurse over children - //######################################## + bool CNFMgr::wasVisited(CNFInfo& x) + { + return getControlBit(x, 11); + } + + //######################################## + //######################################## + //utilities for clause sets + - if (isAtom(varphi)) - { - return; - } - else if (isITE(varphi)) - { - scanFormula(varphi[0], true); - scanFormula(varphi[0], false); - scanTerm(varphi[1]); - scanTerm(varphi[2]); - } - else - { - for (unsigned int i = 0; i < varphi.GetChildren().size(); i++) - { - scanTerm(varphi[i]); - } - } - } + ClauseList* CNFMgr::COPY(const ClauseList& varphi) + { + ClauseList* psi = new ClauseList(); + + ClauseList::const_iterator it = varphi.begin(); + for (; it != varphi.end(); it++) + { + psi->push_back(new vector (**it)); + } + + return psi; + } //End of COPY() + + ClauseList* CNFMgr::SINGLETON(const ASTNode& varphi) + { + ASTNode* copy = ASTNodeToASTNodePtr(varphi); + + ClausePtr clause = new vector (); + clause->push_back(copy); + + ClauseList* psi = new ClauseList(); + psi->push_back(clause); + return psi; + } //End of SINGLETON() + + ClauseList* CNFMgr::UNION(const ClauseList& varphi1, const ClauseList& varphi2) + { + ClauseList* psi1 = COPY(varphi1); + ClauseList* psi2 = COPY(varphi2); + psi1->insert(psi1->end(), psi2->begin(), psi2->end()); + delete psi2; + + return psi1; + } //End of UNION() + + void CNFMgr::INPLACE_UNION(ClauseList* varphi1, const ClauseList& varphi2) + { + ClauseList* psi2 = COPY(varphi2); + varphi1->insert(varphi1->end(), psi2->begin(), psi2->end()); + delete psi2; + } //End of INPLACE_UNION() + + void CNFMgr::NOCOPY_INPLACE_UNION(ClauseList* varphi1, ClauseList* varphi2) + { + varphi1->insert(varphi1->end(), varphi2->begin(), varphi2->end()); + delete varphi2; + } //End of NOCOPY_INPLACE_UNION + + ClauseList* CNFMgr::PRODUCT(const ClauseList& varphi1, const ClauseList& varphi2) + { + ClauseList* psi = new ClauseList(); + psi->reserve(varphi1.size() * varphi2.size()); + + ClauseList::const_iterator it1 = varphi1.begin(); + for (; it1 != varphi1.end(); it1++) + { + ClausePtr clause1 = *it1; + ClauseList::const_iterator it2 = varphi2.begin(); + for (; it2 != varphi2.end(); it2++) + { + ClausePtr clause2 = *it2; + ClausePtr clause = new vector (); + clause->reserve(clause1->size() + clause2->size()); + clause->insert(clause->end(), clause1->begin(), clause1->end()); + clause->insert(clause->end(), clause2->begin(), clause2->end()); + psi->push_back(clause); + } + } + + return psi; + } //End of Product //######################################## //######################################## - // main cnf conversion function - - void convertFormulaToCNF(const ASTNode& varphi, BeevMgr::ClauseList* defs) - { - - CNFInfo* x = info[varphi]; - - //######################################## - // divert to special case if term (word-level cnf) - - if (isTerm(*x)) - { - convertTermForCNF(varphi, defs); - setWasVisited(*x); - return; - } - - //######################################## - // do work - - if (sharesPos(*x) > 0 && !wasVisited(*x)) - { - convertFormulaToCNFPosCases(varphi, defs); - } - - if (x->clausespos != NULL && x->clausespos->size() > 1) - { - if (doSibRenamingPos(*x) || sharesPos(*x) > 1) - { - doRenamingPos(varphi, defs); - } - } - - if (sharesNeg(*x) > 0 && !wasVisited(*x)) - { - convertFormulaToCNFNegCases(varphi, defs); - } - - if (x->clausesneg != NULL && x->clausesneg->size() > 1) - { - if (doSibRenamingNeg(*x) || sharesNeg(*x) > 1) - { - doRenamingNeg(varphi, defs); - } - } - - //######################################## - //mark that we've already done the hard work - - setWasVisited(*x); - } - - void convertTermForCNF(const ASTNode& varphi, BeevMgr::ClauseList* defs) - { - - CNFInfo* x = info[varphi]; - - //######################################## - // step 1, done if we've already visited - //######################################## + //prep. for cnf conversion - if (x->termforcnf != NULL) - { + void CNFMgr::scanFormula(const ASTNode& varphi, bool isPos) + { + CNFInfo* x; + + //######################################## + // step 1, get the info associated with this node + //######################################## + + if (info.find(varphi) == info.end()) + { + x = new CNFInfo(); + initializeCNFInfo(*x); + info[varphi] = x; + } + else + { + x = info[varphi]; + } + + //######################################## + // step 2, we only need to know if shares >= 2 + //######################################## + + if (isPos && sharesPos(*x) == 2) + { + return; + } + + if (!isPos && sharesNeg(*x) == 2) + { + return; + } + + //######################################## + // step 3, set appropriate information fields + //######################################## + + if (isPos) + { + incrementSharesPos(*x); + } + + if (!isPos) + { + incrementSharesNeg(*x); + } + + //######################################## + // step 4, recurse over children + //######################################## + + if (isAtom(varphi)) + { return; - } - - //######################################## - // step 2, ITE's always get renamed - //######################################## - - if (isITE(varphi)) - { - x->termforcnf = doRenameITE(varphi, defs); - reduceMemoryFootprintPos(varphi[0]); - reduceMemoryFootprintNeg(varphi[0]); - - } - else if (isAtom(varphi)) - { - x->termforcnf = ASTNodeToASTNodePtr(varphi); - } - else - { + } + else if (isPred(varphi)) + { + for (unsigned int i = 0; i < varphi.GetChildren().size(); i++) + { + scanTerm(varphi[i]); + } + } + else + { + for (unsigned int i = 0; i < varphi.GetChildren().size(); i++) + { + if (onChildDoPos(varphi, i)) + { + scanFormula(varphi[i], isPos); + } + if (onChildDoNeg(varphi, i)) + { + scanFormula(varphi[i], !isPos); + } + } + } + + } //End of ScanFormula() - ASTVec psis; - ASTVec::const_iterator it = varphi.GetChildren().begin(); - for (; it != varphi.GetChildren().end(); it++) - { - convertTermForCNF(*it, defs); - psis.push_back(*(info[*it]->termforcnf)); - } + void CNFMgr::scanTerm(const ASTNode& varphi) + { + CNFInfo* x; + + //######################################## + // step 1, get the info associated with this node + //######################################## + + if (info.find(varphi) == info.end()) + { + x = new CNFInfo(); + initializeCNFInfo(*x); + info[varphi] = x; + } + else + { + x = info[varphi]; + } + + //######################################## + // step 2, need two hits because of term ITEs. + //######################################## + + if (sharesPos(*x) == 2) + { + return; + } + + //######################################## + // step 3, set appropriate data fields, always rename + // term ITEs + //######################################## + + incrementSharesPos(*x); + setIsTerm(*x); + + //######################################## + // step 4, recurse over children + //######################################## + + if (isAtom(varphi)) + { + return; + } + else if (isITE(varphi)) + { + scanFormula(varphi[0], true); + scanFormula(varphi[0], false); + scanTerm(varphi[1]); + scanTerm(varphi[2]); + } + else + { + for (unsigned int i = 0; i < varphi.GetChildren().size(); i++) + { + scanTerm(varphi[i]); + } + } + }//End of scanterm() + + //######################################## + //######################################## + // main cnf conversion function - ASTNode psi = bm->CreateNode(varphi.GetKind(), psis); + void CNFMgr::convertFormulaToCNF(const ASTNode& varphi, ClauseList* defs) + { + CNFInfo* x = info[varphi]; + + //######################################## + // divert to special case if term (word-level cnf) + + if (isTerm(*x)) + { + convertTermForCNF(varphi, defs); + setWasVisited(*x); + return; + } + + //######################################## + // do work + + if (sharesPos(*x) > 0 && !wasVisited(*x)) + { + convertFormulaToCNFPosCases(varphi, defs); + } + + if (x->clausespos != NULL && x->clausespos->size() > 1) + { + if (doSibRenamingPos(*x) || sharesPos(*x) > 1) + { + doRenamingPos(varphi, defs); + } + } + + if (sharesNeg(*x) > 0 && !wasVisited(*x)) + { + convertFormulaToCNFNegCases(varphi, defs); + } + + if (x->clausesneg != NULL && x->clausesneg->size() > 1) + { + if (doSibRenamingNeg(*x) || sharesNeg(*x) > 1) + { + doRenamingNeg(varphi, defs); + } + } + + //######################################## + //mark that we've already done the hard work + + setWasVisited(*x); + } //End of convertFormulaToCNF() + + void CNFMgr::convertTermForCNF(const ASTNode& varphi, ClauseList* defs) + { + CNFInfo* x = info[varphi]; + + //######################################## + // step 1, done if we've already visited + //######################################## + + if (x->termforcnf != NULL) + { + return; + } + + //######################################## + // step 2, ITE's always get renamed + //######################################## + + if (isITE(varphi)) + { + x->termforcnf = doRenameITE(varphi, defs); + reduceMemoryFootprintPos(varphi[0]); + reduceMemoryFootprintNeg(varphi[0]); + + } + else if (isAtom(varphi)) + { + x->termforcnf = ASTNodeToASTNodePtr(varphi); + } + else + { + ASTVec psis; + ASTVec::const_iterator it = varphi.GetChildren().begin(); + for (; it != varphi.GetChildren().end(); it++) + { + convertTermForCNF(*it, defs); + psis.push_back(*(info[*it]->termforcnf)); + } + + ASTNode psi = bm->CreateNode(varphi.GetKind(), psis); psi.SetValueWidth(varphi.GetValueWidth()); psi.SetIndexWidth(varphi.GetIndexWidth()); x->termforcnf = ASTNodeToASTNodePtr(psi); - } - } + } + } //End of convertTermForCNF() //######################################## //######################################## // functions for renaming nodes during cnf conversion - ASTNode* doRenameITE(const ASTNode& varphi, BeevMgr::ClauseList* defs) - { - - ASTNode psi; - - //######################################## - // step 1, old "RepLit" code - //######################################## - - ostringstream oss; - oss << "cnf" << "{" << varphi.GetNodeNum() << "}"; - psi = bm->CreateSymbol(oss.str().c_str()); - - //######################################## - // step 2, set widths appropriately - //######################################## - - psi.SetValueWidth(varphi.GetValueWidth()); - psi.SetIndexWidth(varphi.GetIndexWidth()); - - //######################################## - // step 3, recurse over children - //######################################## - - convertFormulaToCNF(varphi[0], defs); - convertTermForCNF(varphi[1], defs); - ASTNode t1 = *(info[varphi[1]]->termforcnf); - convertTermForCNF(varphi[2], defs); - ASTNode t2 = *(info[varphi[2]]->termforcnf); - - //######################################## - // step 4, add def clauses - //######################################## - - BeevMgr::ClauseList* cl1 = SINGLETON(bm->CreateNode(EQ, psi, t1)); - BeevMgr::ClauseList* cl2 = PRODUCT(*(info[varphi[0]]->clausesneg), *cl1); - DELETE(cl1); - defs->insert(defs->end(), cl2->begin(), cl2->end()); - - BeevMgr::ClauseList* cl3 = SINGLETON(bm->CreateNode(EQ, psi, t2)); - BeevMgr::ClauseList* cl4 = PRODUCT(*(info[varphi[0]]->clausespos), *cl3); - DELETE(cl3); - defs->insert(defs->end(), cl4->begin(), cl4->end()); - - return ASTNodeToASTNodePtr(psi); - } - - void doRenamingPos(const ASTNode& varphi, BeevMgr::ClauseList* defs) - { - - CNFInfo* x = info[varphi]; - - //######################################## - // step 1, calc new variable - //######################################## - - ostringstream oss; - oss << "cnf" << "{" << varphi.GetNodeNum() << "}"; - ASTNode psi = bm->CreateSymbol(oss.str().c_str()); - - //######################################## - // step 2, add defs - //######################################## - - BeevMgr::ClauseList* cl1; - cl1 = SINGLETON(bm->CreateNode(NOT, psi)); - BeevMgr::ClauseList* cl2 = PRODUCT(*(info[varphi]->clausespos), *cl1); - defs->insert(defs->end(), cl2->begin(), cl2->end()); - DELETE(info[varphi]->clausespos); - DELETE(cl1); - delete cl2; - - //######################################## - // step 3, update info[varphi] - //######################################## - - x->clausespos = SINGLETON(psi); - setWasRenamedPos(*x); - } - - void doRenamingNeg(const ASTNode& varphi, BeevMgr::ClauseList* defs) - { - - CNFInfo* x = info[varphi]; - - //######################################## - // step 2, calc new variable - //######################################## - - ostringstream oss; - oss << "cnf" << "{" << varphi.GetNodeNum() << "}"; - ASTNode psi = bm->CreateSymbol(oss.str().c_str()); - - //######################################## - // step 3, add defs - //######################################## - - BeevMgr::ClauseList* cl1; - cl1 = SINGLETON(psi); - BeevMgr::ClauseList* cl2 = PRODUCT(*(info[varphi]->clausesneg), *cl1); - defs->insert(defs->end(), cl2->begin(), cl2->end()); - DELETE(info[varphi]->clausesneg); - DELETE(cl1); - delete cl2; - - //######################################## - // step 4, update info[varphi] + ASTNode* CNFMgr::doRenameITE(const ASTNode& varphi, ClauseList* defs) + { + ASTNode psi; + + //######################################## + // step 1, old "RepLit" code + //######################################## + + ostringstream oss; + oss << "cnf" << "{" << varphi.GetNodeNum() << "}"; + psi = bm->CreateSymbol(oss.str().c_str()); + + //######################################## + // step 2, set widths appropriately + //######################################## + + psi.SetValueWidth(varphi.GetValueWidth()); + psi.SetIndexWidth(varphi.GetIndexWidth()); + + //######################################## + // step 3, recurse over children + //######################################## + + convertFormulaToCNF(varphi[0], defs); + convertTermForCNF(varphi[1], defs); + ASTNode t1 = *(info[varphi[1]]->termforcnf); + convertTermForCNF(varphi[2], defs); + ASTNode t2 = *(info[varphi[2]]->termforcnf); + + //######################################## + // step 4, add def clauses + //######################################## + + ClauseList* cl1 = SINGLETON(bm->CreateNode(EQ, psi, t1)); + ClauseList* cl2 = PRODUCT(*(info[varphi[0]]->clausesneg), *cl1); + DELETE(cl1); + defs->insert(defs->end(), cl2->begin(), cl2->end()); + + ClauseList* cl3 = SINGLETON(bm->CreateNode(EQ, psi, t2)); + ClauseList* cl4 = PRODUCT(*(info[varphi[0]]->clausespos), *cl3); + DELETE(cl3); + defs->insert(defs->end(), cl4->begin(), cl4->end()); + + return ASTNodeToASTNodePtr(psi); + }//End of doRenameITE() + + void CNFMgr::doRenamingPos(const ASTNode& varphi, ClauseList* defs) + { + CNFInfo* x = info[varphi]; + + //######################################## + // step 1, calc new variable + //######################################## + + ostringstream oss; + oss << "cnf" << "{" << varphi.GetNodeNum() << "}"; + ASTNode psi = bm->CreateSymbol(oss.str().c_str()); + + //######################################## + // step 2, add defs + //######################################## + + ClauseList* cl1; + cl1 = SINGLETON(bm->CreateNode(NOT, psi)); + ClauseList* cl2 = PRODUCT(*(info[varphi]->clausespos), *cl1); + defs->insert(defs->end(), cl2->begin(), cl2->end()); + DELETE(info[varphi]->clausespos); + DELETE(cl1); + delete cl2; + + //######################################## + // step 3, update info[varphi] + //######################################## + + x->clausespos = SINGLETON(psi); + setWasRenamedPos(*x); + }//End of doRenamingPos + + void CNFMgr::doRenamingNeg(const ASTNode& varphi, ClauseList* defs) + { + CNFInfo* x = info[varphi]; + + //######################################## + // step 2, calc new variable //######################################## - - x->clausesneg = SINGLETON(bm->CreateNode(NOT, psi)); - setWasRenamedNeg(*x); - - } + + ostringstream oss; + oss << "cnf" << "{" << varphi.GetNodeNum() << "}"; + ASTNode psi = bm->CreateSymbol(oss.str().c_str()); + + //######################################## + // step 3, add defs + //######################################## + + ClauseList* cl1; + cl1 = SINGLETON(psi); + ClauseList* cl2 = PRODUCT(*(info[varphi]->clausesneg), *cl1); + defs->insert(defs->end(), cl2->begin(), cl2->end()); + DELETE(info[varphi]->clausesneg); + DELETE(cl1); + delete cl2; + + //######################################## + // step 4, update info[varphi] + //######################################## + + x->clausesneg = SINGLETON(bm->CreateNode(NOT, psi)); + setWasRenamedNeg(*x); + } //End of doRenamingNeg() //######################################## //######################################## //main switch for individual cnf conversion cases - void convertFormulaToCNFPosCases(const ASTNode& varphi, BeevMgr::ClauseList* defs) - { - - if (isPred(varphi)) - { - convertFormulaToCNFPosPred(varphi, defs); - return; - } - - Kind k = varphi.GetKind(); - switch (k) - { - case FALSE: - { - convertFormulaToCNFPosFALSE(varphi, defs); - break; - } + void CNFMgr::convertFormulaToCNFPosCases(const ASTNode& varphi, ClauseList* defs) + { + if (isPred(varphi)) + { + convertFormulaToCNFPosPred(varphi, defs); + return; + } + + Kind k = varphi.GetKind(); + switch (k) + { + case FALSE: + { + convertFormulaToCNFPosFALSE(varphi, defs); + break; + } case TRUE: { convertFormulaToCNFPosTRUE(varphi, defs); break; } - case BVGETBIT: - { - convertFormulaToCNFPosBVGETBIT(varphi, defs); - break; - } - case SYMBOL: - { - convertFormulaToCNFPosSYMBOL(varphi, defs); - break; - } - case NOT: - { - convertFormulaToCNFPosNOT(varphi, defs); - break; - } - case AND: - { - convertFormulaToCNFPosAND(varphi, defs); - break; - } - case NAND: - { - convertFormulaToCNFPosNAND(varphi, defs); - break; - } - case OR: - { + case BVGETBIT: + { + convertFormulaToCNFPosBVGETBIT(varphi, defs); + break; + } + case SYMBOL: + { + convertFormulaToCNFPosSYMBOL(varphi, defs); + break; + } + case NOT: + { + convertFormulaToCNFPosNOT(varphi, defs); + break; + } + case AND: + { + convertFormulaToCNFPosAND(varphi, defs); + break; + } + case NAND: + { + convertFormulaToCNFPosNAND(varphi, defs); + break; + } + case OR: + { convertFormulaToCNFPosOR(varphi, defs); break; - } - case NOR: - { - convertFormulaToCNFPosNOR(varphi, defs); - break; + } + case NOR: + { + convertFormulaToCNFPosNOR(varphi, defs); + break; } case XOR: { @@ -983,9 +884,9 @@ namespace BEEV FatalError(""); } } - } + } //End of convertFormulaToCNFPosCases() - void convertFormulaToCNFNegCases(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFNegCases(const ASTNode& varphi, ClauseList* defs) { if (isPred(varphi)) @@ -1063,15 +964,14 @@ namespace BEEV FatalError(""); } } - } + } //convertFormulaToCNFNegCases() //######################################## //######################################## // individual cnf conversion cases - void convertFormulaToCNFPosPred(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFPosPred(const ASTNode& varphi, ClauseList* defs) { - ASTVec psis; ASTVec::const_iterator it = varphi.GetChildren().begin(); @@ -1082,45 +982,45 @@ namespace BEEV } info[varphi]->clausespos = SINGLETON(bm->CreateNode(varphi.GetKind(), psis)); - } + } //End of convertFormulaToCNFPosPred() - void convertFormulaToCNFPosFALSE(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFPosFALSE(const ASTNode& varphi, ClauseList* defs) { ASTNode dummy_false_var = bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*")); info[varphi]->clausespos = SINGLETON(dummy_false_var); - } + } //End of convertFormulaToCNFPosFALSE() - void convertFormulaToCNFPosTRUE(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFPosTRUE(const ASTNode& varphi, ClauseList* defs) { ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*"); info[varphi]->clausespos = SINGLETON(dummy_true_var); - } + } //End of convertFormulaToCNFPosTRUE - void convertFormulaToCNFPosBVGETBIT(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFPosBVGETBIT(const ASTNode& varphi, ClauseList* defs) { info[varphi]->clausespos = SINGLETON(varphi); - } + }//End of convertFormulaToCNFPosBVGETBIT() - void convertFormulaToCNFPosSYMBOL(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFPosSYMBOL(const ASTNode& varphi, ClauseList* defs) { info[varphi]->clausespos = SINGLETON(varphi); - } + } //End of convertFormulaToCNFPosSYMBOL() - void convertFormulaToCNFPosNOT(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFPosNOT(const ASTNode& varphi, ClauseList* defs) { convertFormulaToCNF(varphi[0], defs); info[varphi]->clausespos = COPY(*(info[varphi[0]]->clausesneg)); reduceMemoryFootprintNeg(varphi[0]); - } + } //End of convertFormulaToCNFPosNOT() - void convertFormulaToCNFPosAND(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFPosAND(const ASTNode& varphi, ClauseList* defs) { //**************************************** // (pos) AND ~> UNION //**************************************** ASTVec::const_iterator it = varphi.GetChildren().begin(); convertFormulaToCNF(*it, defs); - BeevMgr::ClauseList* psi = COPY(*(info[*it]->clausespos)); + ClauseList* psi = COPY(*(info[*it]->clausespos)); for (it++; it != varphi.GetChildren().end(); it++) { convertFormulaToCNF(*it, defs); @@ -1129,14 +1029,14 @@ namespace BEEV } info[varphi]->clausespos = psi; - } + } //End of convertFormulaToCNFPosAND() - void convertFormulaToCNFPosNAND(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFPosNAND(const ASTNode& varphi, ClauseList* defs) { bool renamesibs = false; - BeevMgr::ClauseList* clauses; - BeevMgr::ClauseList* psi; - BeevMgr::ClauseList* oldpsi; + ClauseList* clauses; + ClauseList* psi; + ClauseList* oldpsi; //**************************************** // (pos) NAND ~> PRODUCT NOT @@ -1171,14 +1071,14 @@ namespace BEEV } info[varphi]->clausespos = psi; - } + } //End of convertFormulaToCNFPosNAND() - void convertFormulaToCNFPosOR(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFPosOR(const ASTNode& varphi, ClauseList* defs) { bool renamesibs = false; - BeevMgr::ClauseList* clauses; - BeevMgr::ClauseList* psi; - BeevMgr::ClauseList* oldpsi; + ClauseList* clauses; + ClauseList* psi; + ClauseList* oldpsi; //**************************************** // (pos) OR ~> PRODUCT @@ -1212,16 +1112,16 @@ namespace BEEV } info[varphi]->clausespos = psi; - } + } //End of convertFormulaToCNFPosOR() - void convertFormulaToCNFPosNOR(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFPosNOR(const ASTNode& varphi, ClauseList* defs) { //**************************************** // (pos) NOR ~> UNION NOT //**************************************** ASTVec::const_iterator it = varphi.GetChildren().begin(); convertFormulaToCNF(*it, defs); - BeevMgr::ClauseList* psi = COPY(*(info[*it]->clausesneg)); + ClauseList* psi = COPY(*(info[*it]->clausesneg)); reduceMemoryFootprintNeg(*it); for (it++; it != varphi.GetChildren().end(); it++) { @@ -1231,9 +1131,9 @@ namespace BEEV } info[varphi]->clausespos = psi; - } + } //End of convertFormulaToCNFPosNOR() - void convertFormulaToCNFPosIMPLIES(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFPosIMPLIES(const ASTNode& varphi, ClauseList* defs) { //**************************************** // (pos) IMPLIES ~> PRODUCT NOT [0] ; [1] @@ -1246,13 +1146,13 @@ namespace BEEV setDoSibRenamingPos(*x1); } convertFormulaToCNF(varphi[1], defs); - BeevMgr::ClauseList* psi = PRODUCT(*(x0->clausesneg), *(x1->clausespos)); + ClauseList* psi = PRODUCT(*(x0->clausesneg), *(x1->clausespos)); reduceMemoryFootprintNeg(varphi[0]); reduceMemoryFootprintPos(varphi[1]); info[varphi]->clausespos = psi; - } + } //End of convertFormulaToCNFPosIMPLIES() - void convertFormulaToCNFPosITE(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFPosITE(const ASTNode& varphi, ClauseList* defs) { //**************************************** // (pos) ITE ~> UNION (PRODUCT NOT [0] ; [1]) @@ -1272,8 +1172,8 @@ namespace BEEV setDoSibRenamingPos(*x2); } convertFormulaToCNF(varphi[2], defs); - BeevMgr::ClauseList* psi1 = PRODUCT(*(x0->clausesneg), *(x1->clausespos)); - BeevMgr::ClauseList* psi2 = PRODUCT(*(x0->clausespos), *(x2->clausespos)); + ClauseList* psi1 = PRODUCT(*(x0->clausesneg), *(x1->clausespos)); + ClauseList* psi2 = PRODUCT(*(x0->clausespos), *(x2->clausespos)); NOCOPY_INPLACE_UNION(psi1, psi2); reduceMemoryFootprintNeg(varphi[0]); reduceMemoryFootprintPos(varphi[1]); @@ -1281,31 +1181,31 @@ namespace BEEV reduceMemoryFootprintPos(varphi[2]); info[varphi]->clausespos = psi1; - } + } //End of convertFormulaToCNFPosITE() - void convertFormulaToCNFPosXOR(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFPosXOR(const ASTNode& varphi, ClauseList* defs) { ASTVec::const_iterator it = varphi.GetChildren().begin(); for (; it != varphi.GetChildren().end(); it++) { convertFormulaToCNF(*it, defs); // make pos and neg clause sets } - BeevMgr::ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs); + ClauseList* psi = convertFormulaToCNFPosXORAux(varphi, 0, defs); info[varphi]->clausespos = psi; ASTVec::const_iterator it2 = varphi.GetChildren().begin(); for (; it2 != varphi.GetChildren().end(); it2++){ reduceMemoryFootprintPos(*it2); reduceMemoryFootprintNeg(*it2); } - } + } //End of convertFormulaToCNFPosXOR() - BeevMgr::ClauseList* convertFormulaToCNFPosXORAux(const ASTNode& varphi, unsigned int idx, BeevMgr::ClauseList* defs) + ClauseList* CNFMgr::convertFormulaToCNFPosXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs) { bool renamesibs; - BeevMgr::ClauseList* psi; - BeevMgr::ClauseList* psi1; - BeevMgr::ClauseList* psi2; + ClauseList* psi; + ClauseList* psi1; + ClauseList* psi2; if (idx == varphi.GetChildren().size() - 2) { @@ -1338,14 +1238,14 @@ namespace BEEV // (PRODUCT [idx] ; XOR [idx+1..]) // ; (PRODUCT NOT [idx] ; NOT XOR [idx+1..]) //**************************************** - BeevMgr::ClauseList* theta1; + ClauseList* theta1; theta1 = convertFormulaToCNFPosXORAux(varphi, idx + 1, defs); renamesibs = theta1->size() > 1 ? true : false; if (renamesibs) { setDoSibRenamingPos(*info[varphi[idx]]); } - BeevMgr::ClauseList* theta2; + ClauseList* theta2; theta2 = convertFormulaToCNFNegXORAux(varphi, idx + 1, defs); renamesibs = theta2->size() > 1 ? true : false; if (renamesibs) @@ -1363,9 +1263,9 @@ namespace BEEV } return psi; - } + } //End of convertFormulaToCNFPosXORAux() - void convertFormulaToCNFNegPred(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFNegPred(const ASTNode& varphi, ClauseList* defs) { ASTVec psis; @@ -1378,44 +1278,44 @@ namespace BEEV } info[varphi]->clausesneg = SINGLETON(bm->CreateNode(NOT, bm->CreateNode(varphi.GetKind(), psis))); - } + } //End of convertFormulaToCNFNegPred() - void convertFormulaToCNFNegFALSE(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFNegFALSE(const ASTNode& varphi, ClauseList* defs) { ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*"); info[varphi]->clausesneg = SINGLETON(dummy_true_var); - } + } //End of convertFormulaToCNFNegFALSE() - void convertFormulaToCNFNegTRUE(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFNegTRUE(const ASTNode& varphi, ClauseList* defs) { ASTNode dummy_false_var = bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*")); info[varphi]->clausesneg = SINGLETON(dummy_false_var); - } + } //End of convertFormulaToCNFNegTRUE() - void convertFormulaToCNFNegBVGETBIT(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFNegBVGETBIT(const ASTNode& varphi, ClauseList* defs) { - BeevMgr::ClauseList* psi = SINGLETON(bm->CreateNode(NOT, varphi)); + ClauseList* psi = SINGLETON(bm->CreateNode(NOT, varphi)); info[varphi]->clausesneg = psi; - } + } //End of convertFormulaToCNFNegBVGETBIT() - void convertFormulaToCNFNegSYMBOL(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFNegSYMBOL(const ASTNode& varphi, ClauseList* defs) { info[varphi]->clausesneg = SINGLETON(bm->CreateNode(NOT, varphi)); - } + } //End of convertFormulaToCNFNegSYMBOL() - void convertFormulaToCNFNegNOT(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFNegNOT(const ASTNode& varphi, ClauseList* defs) { convertFormulaToCNF(varphi[0], defs); info[varphi]->clausesneg = COPY(*(info[varphi[0]]->clausespos)); reduceMemoryFootprintPos(varphi[0]); - } + } //End of convertFormulaToCNFNegNOT() - void convertFormulaToCNFNegAND(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFNegAND(const ASTNode& varphi, ClauseList* defs) { bool renamesibs = false; - BeevMgr::ClauseList* clauses; - BeevMgr::ClauseList* psi; - BeevMgr::ClauseList* oldpsi; + ClauseList* clauses; + ClauseList* psi; + ClauseList* oldpsi; //**************************************** // (neg) AND ~> PRODUCT NOT @@ -1450,16 +1350,16 @@ namespace BEEV } info[varphi]->clausesneg = psi; - } + } //End of convertFormulaToCNFNegAND() - void convertFormulaToCNFNegNAND(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFNegNAND(const ASTNode& varphi, ClauseList* defs) { //**************************************** // (neg) NAND ~> UNION //**************************************** ASTVec::const_iterator it = varphi.GetChildren().begin(); convertFormulaToCNF(*it, defs); - BeevMgr::ClauseList* psi = COPY(*(info[*it]->clausespos)); + ClauseList* psi = COPY(*(info[*it]->clausespos)); reduceMemoryFootprintPos(*it); for (it++; it != varphi.GetChildren().end(); it++) { @@ -1469,16 +1369,16 @@ namespace BEEV } info[varphi]->clausespos = psi; - } + } //End of convertFormulaToCNFNegNAND() - void convertFormulaToCNFNegOR(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFNegOR(const ASTNode& varphi, ClauseList* defs) { //**************************************** // (neg) OR ~> UNION NOT //**************************************** ASTVec::const_iterator it = varphi.GetChildren().begin(); convertFormulaToCNF(*it, defs); - BeevMgr::ClauseList* psi = COPY(*(info[*it]->clausesneg)); + ClauseList* psi = COPY(*(info[*it]->clausesneg)); reduceMemoryFootprintNeg(*it); for (it++; it != varphi.GetChildren().end(); it++) { @@ -1488,14 +1388,14 @@ namespace BEEV } info[varphi]->clausesneg = psi; - } + } //End of convertFormulaToCNFNegOR() - void convertFormulaToCNFNegNOR(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFNegNOR(const ASTNode& varphi, ClauseList* defs) { bool renamesibs = false; - BeevMgr::ClauseList* clauses; - BeevMgr::ClauseList* psi; - BeevMgr::ClauseList* oldpsi; + ClauseList* clauses; + ClauseList* psi; + ClauseList* oldpsi; //**************************************** // (neg) NOR ~> PRODUCT @@ -1529,9 +1429,9 @@ namespace BEEV } info[varphi]->clausesneg = psi; - } + } //End of convertFormulaToCNFNegNOR() - void convertFormulaToCNFNegIMPLIES(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFNegIMPLIES(const ASTNode& varphi, ClauseList* defs) { //**************************************** // (neg) IMPLIES ~> UNION [0] ; NOT [1] @@ -1540,13 +1440,13 @@ namespace BEEV CNFInfo* x1 = info[varphi[1]]; convertFormulaToCNF(varphi[0], defs); convertFormulaToCNF(varphi[1], defs); - BeevMgr::ClauseList* psi = UNION(*(x0->clausespos), *(x1->clausesneg)); + ClauseList* psi = UNION(*(x0->clausespos), *(x1->clausesneg)); info[varphi]->clausesneg = psi; reduceMemoryFootprintPos(varphi[0]); reduceMemoryFootprintNeg(varphi[1]); - } + } //End of convertFormulaToCNFNegIMPLIES() - void convertFormulaToCNFNegITE(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFNegITE(const ASTNode& varphi, ClauseList* defs) { //**************************************** // (neg) ITE ~> UNION (PRODUCT NOT [0] ; NOT [1]) @@ -1566,8 +1466,8 @@ namespace BEEV setDoSibRenamingNeg(*x2); } convertFormulaToCNF(varphi[2], defs); - BeevMgr::ClauseList* psi1 = PRODUCT(*(x0->clausesneg), *(x1->clausesneg)); - BeevMgr::ClauseList* psi2 = PRODUCT(*(x0->clausespos), *(x2->clausesneg)); + ClauseList* psi1 = PRODUCT(*(x0->clausesneg), *(x1->clausesneg)); + ClauseList* psi2 = PRODUCT(*(x0->clausespos), *(x2->clausesneg)); NOCOPY_INPLACE_UNION(psi1, psi2); reduceMemoryFootprintNeg(varphi[0]); reduceMemoryFootprintNeg(varphi[1]); @@ -1575,31 +1475,30 @@ namespace BEEV reduceMemoryFootprintNeg(varphi[2]); info[varphi]->clausesneg = psi1; - } + } //End of convertFormulaToCNFNegITE() - void convertFormulaToCNFNegXOR(const ASTNode& varphi, BeevMgr::ClauseList* defs) + void CNFMgr::convertFormulaToCNFNegXOR(const ASTNode& varphi, ClauseList* defs) { ASTVec::const_iterator it = varphi.GetChildren().begin(); for (; it != varphi.GetChildren().end(); it++) { convertFormulaToCNF(*it, defs); // make pos and neg clause sets } - BeevMgr::ClauseList* psi = convertFormulaToCNFNegXORAux(varphi, 0, defs); + ClauseList* psi = convertFormulaToCNFNegXORAux(varphi, 0, defs); info[varphi]->clausesneg = psi; ASTVec::const_iterator it2 = varphi.GetChildren().begin(); for (; it2 != varphi.GetChildren().end(); it2++){ reduceMemoryFootprintPos(*it2); reduceMemoryFootprintNeg(*it2); } - } + } //End of convertFormulaToCNFNegXOR() - BeevMgr::ClauseList* convertFormulaToCNFNegXORAux(const ASTNode& varphi, unsigned int idx, BeevMgr::ClauseList* defs) + ClauseList* CNFMgr::convertFormulaToCNFNegXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs) { - bool renamesibs; - BeevMgr::ClauseList* psi; - BeevMgr::ClauseList* psi1; - BeevMgr::ClauseList* psi2; + ClauseList* psi; + ClauseList* psi1; + ClauseList* psi2; if (idx == varphi.GetChildren().size() - 2) { @@ -1636,7 +1535,7 @@ namespace BEEV // (PRODUCT NOT [idx] ; XOR [idx+1..]) // ; (PRODUCT [idx] ; NOT XOR [idx+1..]) //**************************************** - BeevMgr::ClauseList* theta1; + ClauseList* theta1; theta1 = convertFormulaToCNFPosXORAux(varphi, idx + 1, defs); renamesibs = theta1->size() > 1 ? true : false; if (renamesibs) @@ -1645,7 +1544,7 @@ namespace BEEV } convertFormulaToCNF(varphi[idx], defs); - BeevMgr::ClauseList* theta2; + ClauseList* theta2; theta2 = convertFormulaToCNFNegXORAux(varphi, idx + 1, defs); renamesibs = theta2->size() > 1 ? true : false; if (renamesibs) @@ -1663,15 +1562,14 @@ namespace BEEV } return psi; - } + } //End of convertFormulaToCNFNegXORAux() //######################################## //######################################## // utilities for reclaiming memory. - void reduceMemoryFootprintPos(const ASTNode& varphi) + void CNFMgr::reduceMemoryFootprintPos(const ASTNode& varphi) { - CNFInfo* x = info[varphi]; if (sharesPos(*x) == 1) { @@ -1683,11 +1581,10 @@ namespace BEEV info.erase(varphi); } } - } + } //End of reduceMemoryFootprintPos() - void reduceMemoryFootprintNeg(const ASTNode& varphi) + void CNFMgr::reduceMemoryFootprintNeg(const ASTNode& varphi) { - CNFInfo* x = info[varphi]; if (sharesNeg(*x) == 1) { @@ -1699,12 +1596,12 @@ namespace BEEV info.erase(varphi); } } - } + } //End of reduceMemoryFootprintNeg() //######################################## //######################################## - ASTNode* ASTNodeToASTNodePtr(const ASTNode& varphi) + ASTNode* CNFMgr::ASTNodeToASTNodePtr(const ASTNode& varphi) { ASTNode* psi; @@ -1719,12 +1616,12 @@ namespace BEEV } return psi; - } + } //End of ASTNodeToASTNodePtr() //######################################## //######################################## - void cleanup(const ASTNode& varphi) + void CNFMgr::cleanup(const ASTNode& varphi) { delete info[varphi]->clausespos; CNFInfo* toDelete = info[varphi]; // get the thing to delete. @@ -1751,106 +1648,57 @@ namespace BEEV } info.clear(); - } - - }; // end of CNFMgr class - - SOLVER_RETURN_TYPE BeevMgr::TopLevelSAT(const ASTNode& inputasserts, - const ASTNode& query) - { - - ASTNode q = CreateNode(AND, inputasserts, CreateNode(NOT, query)); - return TopLevelSATAux(q); - } + } //End of cleanup() - //############################################################ - //############################################################ + //######################################## + //######################################## + // constructor + CNFMgr::CNFMgr(BeevMgr *bmgr) + { + bm = bmgr; + } - void BeevMgr::DeleteClauseList(BeevMgr::ClauseList *cllp) + //######################################## + //######################################## + // destructor + CNFMgr::~CNFMgr() { - BeevMgr::ClauseList::const_iterator iend = cllp->end(); - for (BeevMgr::ClauseList::const_iterator i = cllp->begin(); i < iend; i++) + ASTNodeToASTNodePtrMap::const_iterator it1 = store.begin(); + for (; it1 != store.end(); it1++) { - delete *i; - } - delete cllp; + delete it1->second; + } + store.clear(); } - //Call the SAT solver, and check the result before returning. This - //can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or SOLVER_UNDECIDED - SOLVER_RETURN_TYPE BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& SatSolver, - const ASTNode& modified_input, - const ASTNode& original_input) - { - runTimes.start(RunTimes::BitBlasting); - ASTNode BBFormula = BBForm(modified_input); - runTimes.stop(RunTimes::BitBlasting); + //######################################## + //######################################## + // top-level conversion function - CNFMgr* cm = new CNFMgr(this); - ClauseList* cl = cm->convertToCNF(BBFormula); - if (stats_flag) - { - cerr << "Number of clauses:" << cl->size() << endl; - } - //PrintClauseList(cout, *cl); - bool sat = toSATandSolve(SatSolver, *cl); - cm->DELETE(cl); - delete cm; + ClauseList* CNFMgr::convertToCNF(const ASTNode& varphi) + { + varphi.GetBeevMgr()->runTimes.start(RunTimes::CNFConversion); + scanFormula(varphi, true); + ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*"); + ClauseList* defs = SINGLETON(dummy_true_var); + convertFormulaToCNF(varphi, defs); + ClauseList* top = info[varphi]->clausespos; + defs->insert(defs->begin() + 1, top->begin(), top->end()); - if (!sat) - { - //PrintOutput(true); - return SOLVER_VALID; - } - else if (SatSolver.okay()) - { - CounterExampleMap.clear(); - ConstructCounterExample(SatSolver); - if (stats_flag && print_nodes_flag) - { - PrintSATModel(SatSolver); - } - //check if the counterexample is good or not - ComputeFormulaMap.clear(); - if (counterexample_checking_during_refinement) - bvdiv_exception_occured = false; - ASTNode orig_result = ComputeFormulaUsingModel(original_input); - if (!(ASTTrue == orig_result || ASTFalse == orig_result)) - FatalError("TopLevelSat: Original input must compute to "\ - "true or false against model"); - - // if the counterexample is indeed a good one, then return - // invalid - if (ASTTrue == orig_result) - { - //CheckCounterExample(SatSolver.okay()); - //PrintOutput(false); - PrintCounterExample(SatSolver.okay()); - PrintCounterExample_InOrder(SatSolver.okay()); - return SOLVER_INVALID; - } - // counterexample is bogus: flag it - else - { - if (stats_flag && print_nodes_flag) - { - cout << "Supposedly bogus one: \n"; - bool tmp = print_counterexample_flag; - print_counterexample_flag = true; - PrintCounterExample(true); - print_counterexample_flag = tmp; - } - - return SOLVER_UNDECIDED; - } - } - else - { - //Control should never reach here - //PrintOutput(true); - return SOLVER_ERROR; - } - } //end of CALLSAT_ResultCheck + cleanup(varphi); + varphi.GetBeevMgr()->runTimes.stop(RunTimes::CNFConversion); + return defs; + }//End of convertToCNF() + + void CNFMgr::DELETE(ClauseList* varphi) + { + ClauseList::const_iterator it = varphi->begin(); + for (; it != varphi->end(); it++) + { + delete *it; + } + delete varphi; + } //End of DELETE() } // end namespace BEEV diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h new file mode 100644 index 0000000..be1fb23 --- /dev/null +++ b/src/to-sat/ToCNF.h @@ -0,0 +1,275 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Vijay Ganesh + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ + +#ifndef TOCNF_H +#define TOCNF_H + +#include +#include +#include "../AST/AST.h" +#include "../STPManager/STPManager.h" + +namespace BEEV +{ + class CNFMgr + { + private: + //######################################## + //######################################## + // data types + + // for the meaning of control bits, see "utilities for contol bits". + typedef struct + { + int control; + ClauseList* clausespos; + union + { + ClauseList* clausesneg; + ASTNode* termforcnf; + }; + } CNFInfo; + + typedef hash_map< + ASTNode, + CNFInfo*, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeToCNFInfoMap; + + typedef hash_map< + ASTNode, + ASTNode*, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeToASTNodePtrMap; + + //######################################## + //######################################## + // this is the data + + BeevMgr *bm; + ASTNodeToCNFInfoMap info; + ASTNodeToASTNodePtrMap store; + + //######################################## + //######################################## + // utility predicates + + bool isAtom(const ASTNode& varphi); + + bool isPred(const ASTNode& varphi); + + bool isITE(const ASTNode& varphi); + + bool onChildDoPos(const ASTNode& varphi, unsigned int idx); + + bool onChildDoNeg(const ASTNode& varphi, unsigned int idx); + + + //######################################## + //######################################## + //utilities for control bits. + + void initializeCNFInfo(CNFInfo& x); + + void incrementSharesPos(CNFInfo& x); + + int sharesPos(CNFInfo& x); + + void incrementSharesNeg(CNFInfo& x); + + int sharesNeg(CNFInfo& x); + + void setControlBit(CNFInfo& x, unsigned int idx); + + bool getControlBit(CNFInfo& x, unsigned int idx); + + void setIsTerm(CNFInfo& x); + + bool isTerm(CNFInfo& x); + + void setDoRenamePos(CNFInfo& x); + + bool doRenamePos(CNFInfo& x); + + void setWasRenamedPos(CNFInfo& x); + + bool wasRenamedPos(CNFInfo& x); + + void setDoRenameNeg(CNFInfo& x); + + bool doRenameNeg(CNFInfo& x); + + void setWasRenamedNeg(CNFInfo& x); + + bool wasRenamedNeg(CNFInfo& x); + + void setDoSibRenamingPos(CNFInfo& x); + + bool doSibRenamingPos(CNFInfo& x); + + void setDoSibRenamingNeg(CNFInfo& x); + + bool doSibRenamingNeg(CNFInfo& x); + + void setWasVisited(CNFInfo& x); + + bool wasVisited(CNFInfo& x); + + //######################################## + //######################################## + //utilities for clause sets + + ClauseList* COPY(const ClauseList& varphi); + + ClauseList* SINGLETON(const ASTNode& varphi); + + ClauseList* UNION(const ClauseList& varphi1, const ClauseList& varphi2); + + void INPLACE_UNION(ClauseList* varphi1, const ClauseList& varphi2); + + void NOCOPY_INPLACE_UNION(ClauseList* varphi1, ClauseList* varphi2); + + ClauseList* PRODUCT(const ClauseList& varphi1, const ClauseList& varphi2); + + //######################################## + //######################################## + //prep. for cnf conversion + + void scanFormula(const ASTNode& varphi, bool isPos); + + void scanTerm(const ASTNode& varphi); + + //######################################## + //######################################## + // main cnf conversion function + + void convertFormulaToCNF(const ASTNode& varphi, ClauseList* defs); + + void convertTermForCNF(const ASTNode& varphi, ClauseList* defs); + + //######################################## + //######################################## + // functions for renaming nodes during cnf conversion + + ASTNode* doRenameITE(const ASTNode& varphi, ClauseList* defs); + + void doRenamingPos(const ASTNode& varphi, ClauseList* defs); + + void doRenamingNeg(const ASTNode& varphi, ClauseList* defs); + + //######################################## + //######################################## + //main switch for individual cnf conversion cases + + void convertFormulaToCNFPosCases(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFNegCases(const ASTNode& varphi, ClauseList* defs); + + //######################################## + //######################################## + // individual cnf conversion cases + + void convertFormulaToCNFPosPred(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFPosFALSE(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFPosTRUE(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFPosBVGETBIT(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFPosSYMBOL(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFPosNOT(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFPosAND(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFPosNAND(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFPosOR(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFPosNOR(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFPosIMPLIES(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFPosITE(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFPosXOR(const ASTNode& varphi, ClauseList* defs); + + ClauseList* convertFormulaToCNFPosXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs); + + void convertFormulaToCNFNegPred(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFNegFALSE(const ASTNode& varphi, ClauseList* defs); + + + void convertFormulaToCNFNegTRUE(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFNegBVGETBIT(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFNegSYMBOL(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFNegNOT(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFNegAND(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFNegNAND(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFNegOR(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFNegNOR(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFNegIMPLIES(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFNegITE(const ASTNode& varphi, ClauseList* defs); + + void convertFormulaToCNFNegXOR(const ASTNode& varphi, ClauseList* defs); + + ClauseList* convertFormulaToCNFNegXORAux(const ASTNode& varphi, unsigned int idx, ClauseList* defs); + + //######################################## + //######################################## + // utilities for reclaiming memory. + + void reduceMemoryFootprintPos(const ASTNode& varphi); + + void reduceMemoryFootprintNeg(const ASTNode& varphi); + + //######################################## + //######################################## + + ASTNode* ASTNodeToASTNodePtr(const ASTNode& varphi); + + //######################################## + //######################################## + + void cleanup(const ASTNode& varphi); + + public: + + //######################################## + //######################################## + // constructor + CNFMgr(BeevMgr *bmgr); + + + //######################################## + //######################################## + // destructor + ~CNFMgr(); + + //######################################## + //######################################## + // top-level conversion function + + ClauseList* convertToCNF(const ASTNode& varphi); + + void DELETE(ClauseList* varphi); + }; // end of CNFMgr class +};//end of namespace +#endif diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 92908e3..4f6618c 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -12,6 +12,8 @@ #include "../simplifier/bvsolver.h" #include "../sat/sat.h" #include "../AST/RunTimes.h" +#include "BitBlast.h" +#include "ToCNF.h" namespace BEEV { @@ -50,15 +52,15 @@ namespace BEEV // FIXME: Still need to deal with TRUE/FALSE in clauses! // //bool BeevMgr::toSATandSolve(MINISAT::Solver& newS, - //BeevMgr::ClauseList& cll, ASTNodeToIntMap& heuristic) - bool BeevMgr::toSATandSolve(MINISAT::Solver& newS, BeevMgr::ClauseList& cll) + //ClauseList& cll, ASTNodeToIntMap& heuristic) + bool BeevMgr::toSATandSolve(MINISAT::Solver& newS, ClauseList& cll) { CountersAndStats("SAT Solver"); runTimes.start(RunTimes::SendingToSAT); //iterate through the list (conjunction) of ASTclauses cll - BeevMgr::ClauseList::const_iterator i = cll.begin(), iend = cll.end(); + ClauseList::const_iterator i = cll.begin(), iend = cll.end(); if (i == iend) FatalError("toSATandSolve: Nothing to Solve", ASTUndefined); @@ -1109,4 +1111,90 @@ namespace BEEV } return CreateBVConst(cc.c_str(), 2); } //end of BoolVectoBVConst() + + + //Call the SAT solver, and check the result before returning. This + //can return one of 3 values, SOLVER_VALID, SOLVER_INVALID or SOLVER_UNDECIDED + SOLVER_RETURN_TYPE BeevMgr::CallSAT_ResultCheck(MINISAT::Solver& SatSolver, + const ASTNode& modified_input, + const ASTNode& original_input) + { + runTimes.start(RunTimes::BitBlasting); + BitBlaster BB(this); + ASTNode BBFormula = BB.BBForm(modified_input); + runTimes.stop(RunTimes::BitBlasting); + + CNFMgr* cm = new CNFMgr(this); + ClauseList* cl = cm->convertToCNF(BBFormula); + if (stats_flag) + { + cerr << "Number of clauses:" << cl->size() << endl; + } + //PrintClauseList(cout, *cl); + bool sat = toSATandSolve(SatSolver, *cl); + cm->DELETE(cl); + delete cm; + + if (!sat) + { + //PrintOutput(true); + return SOLVER_VALID; + } + else if (SatSolver.okay()) + { + CounterExampleMap.clear(); + ConstructCounterExample(SatSolver); + if (stats_flag && print_nodes_flag) + { + PrintSATModel(SatSolver); + } + //check if the counterexample is good or not + ComputeFormulaMap.clear(); + if (counterexample_checking_during_refinement) + bvdiv_exception_occured = false; + ASTNode orig_result = ComputeFormulaUsingModel(original_input); + if (!(ASTTrue == orig_result || ASTFalse == orig_result)) + FatalError("TopLevelSat: Original input must compute to "\ + "true or false against model"); + + // if the counterexample is indeed a good one, then return + // invalid + if (ASTTrue == orig_result) + { + //CheckCounterExample(SatSolver.okay()); + //PrintOutput(false); + PrintCounterExample(SatSolver.okay()); + PrintCounterExample_InOrder(SatSolver.okay()); + return SOLVER_INVALID; + } + // counterexample is bogus: flag it + else + { + if (stats_flag && print_nodes_flag) + { + cout << "Supposedly bogus one: \n"; + bool tmp = print_counterexample_flag; + print_counterexample_flag = true; + PrintCounterExample(true); + print_counterexample_flag = tmp; + } + + return SOLVER_UNDECIDED; + } + } + else + { + //Control should never reach here + //PrintOutput(true); + return SOLVER_ERROR; + } + } //end of CALLSAT_ResultCheck() + + SOLVER_RETURN_TYPE BeevMgr::TopLevelSAT(const ASTNode& inputasserts, + const ASTNode& query) + { + + ASTNode q = CreateNode(AND, inputasserts, CreateNode(NOT, query)); + return TopLevelSATAux(q); + } //End of TopLevelSAT() }; //end of namespace BEEV