From: vijay_ganesh Date: Fri, 16 Oct 2009 18:08:59 +0000 (+0000) Subject: minor edits X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=5977913631f5e54a59641663dbdd01305dae0456;p=francis%2Fstp.git minor edits git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@311 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp index 35491d0..ccd0d00 100644 --- a/src/to-sat/BitBlast.cpp +++ b/src/to-sat/BitBlast.cpp @@ -86,59 +86,59 @@ namespace BEEV if (k == BVSRSHIFT || k == BVRIGHTSHIFT) - { - for (unsigned int i = 0; i < log2Width; i++) - { - if (bbarg2[i] == ASTFalse) - continue; // Not shifting by anything. - - unsigned int shift_amount = 1 << i; - - for (unsigned int j = 0; j < width; j++) - { - if (j + shift_amount >= width) - { - temp_result[j] = - _bm->CreateSimpForm(ITE, bbarg2[i], - toFill, temp_result[j]); - } - else - { - temp_result[j] = - _bm->CreateSimpForm(ITE, bbarg2[i], - temp_result[j + shift_amount], - temp_result[j]); - } - } - } - } + { + for (unsigned int i = 0; i < log2Width; i++) + { + if (bbarg2[i] == ASTFalse) + continue; // Not shifting by anything. + + unsigned int shift_amount = 1 << i; + + for (unsigned int j = 0; j < width; j++) + { + if (j + shift_amount >= width) + { + temp_result[j] = + _bm->CreateSimpForm(ITE, bbarg2[i], + toFill, temp_result[j]); + } + else + { + temp_result[j] = + _bm->CreateSimpForm(ITE, bbarg2[i], + temp_result[j + shift_amount], + temp_result[j]); + } + } + } + } else - { - for (unsigned int i = 0; i < log2Width; i++) - { - if (bbarg2[i] == ASTFalse) - continue; // Not shifting by anything. - - int shift_amount = 1 << i; - - for (signed int j = width - 1; j > 0; j--) - { - if (j < shift_amount) - { - temp_result[j] = - _bm->CreateSimpForm(ITE, bbarg2[i], - toFill, temp_result[j]); - } - else - { - temp_result[j] = - _bm->CreateSimpForm(ITE, bbarg2[i], - temp_result[j - shift_amount], - temp_result[j]); - } - } - } - } + { + for (unsigned int i = 0; i < log2Width; i++) + { + if (bbarg2[i] == ASTFalse) + continue; // Not shifting by anything. + + int shift_amount = 1 << i; + + for (signed int j = width - 1; j > 0; j--) + { + if (j < shift_amount) + { + temp_result[j] = + _bm->CreateSimpForm(ITE, bbarg2[i], + toFill, temp_result[j]); + } + else + { + temp_result[j] = + _bm->CreateSimpForm(ITE, bbarg2[i], + temp_result[j - shift_amount], + temp_result[j]); + } + } + } + } // If any of the remainder are true. Then the whole thing // gets the fill value. ASTNode remainder = ASTFalse; @@ -150,7 +150,7 @@ namespace BEEV for (unsigned int i = 0; i < width; i++) { temp_result[i] = - _bm->CreateSimpForm(ITE, remainder, toFill, temp_result[i]); + _bm->CreateSimpForm(ITE, remainder, toFill, temp_result[i]); } result = _bm->CreateNode(BOOLVEC, temp_result); @@ -158,7 +158,7 @@ namespace BEEV break; case BVVARSHIFT: FatalError("BBTerm: These kinds have not "\ - "been implemented in the BitBlaster: ", term); + "been implemented in the BitBlaster: ", term); break; case ITE: { @@ -170,9 +170,9 @@ namespace BEEV const ASTNode& thn = BBTerm(term[1]); const ASTNode& els = BBTerm(term[2]); result = - _bm->CreateNode(BOOLVEC, - BBITE(cond, thn.GetChildren(), - els.GetChildren())); + _bm->CreateNode(BOOLVEC, + BBITE(cond, thn.GetChildren(), + els.GetChildren())); break; } @@ -227,7 +227,7 @@ namespace BEEV //FIXME Should these be gotten from result? ASTVec::const_iterator bb_it = bbarg.begin(); ASTVec::iterator res_it = tmp_res.begin(); - // first bit of extended part + // first bit of extended part ASTVec::iterator res_ext = res_it + arg_width; ASTVec::iterator res_end = tmp_res.end(); // copy LSBs directly from bbvec @@ -295,7 +295,7 @@ namespace BEEV //FIXME _bm->Creates a new local ASTVec and does the //_bm->CreateNode from that result = - _bm->CreateNode(BOOLVEC, ASTVec(bbkfit + low, bbkfit + high + 1)); + _bm->CreateNode(BOOLVEC, ASTVec(bbkfit + low, bbkfit + high + 1)); /* if(weregood){ printf("spot05\n"); @@ -369,16 +369,16 @@ namespace BEEV if ((BVCONST != t0.GetKind()) && (BVCONST == t1.GetKind())) { result = - _bm->CreateNode(BOOLVEC, - BBMult(mpcd2.GetChildren(), - mpcd1.GetChildren())); + _bm->CreateNode(BOOLVEC, + BBMult(mpcd2.GetChildren(), + mpcd1.GetChildren())); } else { result = - _bm->CreateNode(BOOLVEC, - BBMult(mpcd1.GetChildren(), - mpcd2.GetChildren())); + _bm->CreateNode(BOOLVEC, + BBMult(mpcd1.GetChildren(), + mpcd2.GetChildren())); } break; } @@ -466,7 +466,7 @@ namespace BEEV for (unsigned int i = 0; i < num_bits; i++) { ASTNode bit_node = - _bm->CreateNode(BVGETBIT, term, _bm->CreateBVConst(32, i)); + _bm->CreateNode(BVGETBIT, term, _bm->CreateBVConst(32, i)); bbvec.push_back(bit_node); } result = _bm->CreateNode(BOOLVEC, bbvec); @@ -557,8 +557,8 @@ namespace BEEV case ITE: // FIXME: SHould this be _bm->CreateSimpITE? result = - _bm->CreateNode(ITE, BBForm(form[0]), - BBForm(form[1]), BBForm(form[2])); + _bm->CreateNode(ITE, BBForm(form[0]), + BBForm(form[1]), BBForm(form[2])); break; case AND: @@ -597,8 +597,8 @@ namespace BEEV if (left.Degree() != right.Degree()) { cerr << "BBForm: Size mismatch" - << endl << form[0] - << endl << form[1] << endl; + << endl << form[0] + << endl << form[1] << endl; FatalError("", ASTUndefined); } result = BBEQ(left.GetChildren(), right.GetChildren()); @@ -625,10 +625,10 @@ namespace BEEV if(_bm->UserFlags.stats_flag) { - cout << "================" << endl - << "BBForm: " << form << endl - << "----------------" << endl - << "BBForm Result: " << result << endl; +// cout << "================" << endl +// << "BBForm: " << form << endl +// << "----------------" << endl +// << "BBForm Result: " << result << endl; } return (BBFormMemo[form] = result); @@ -652,9 +652,9 @@ namespace BEEV { ASTNode nextcin = Majority(sum[i], y[i], cin); sum[i] = - _bm->CreateSimpForm(XOR, - _bm->CreateSimpForm(XOR, sum[i], y[i]), - cin); + _bm->CreateSimpForm(XOR, + _bm->CreateSimpForm(XOR, sum[i], y[i]), + cin); cin = nextcin; } @@ -695,7 +695,7 @@ namespace BEEV // Return formula for majority function of three bits. // Pass arguments by reference to reduce refcounting. ASTNode BitBlaster::Majority(const ASTNode& a, - const ASTNode& b, const ASTNode& c) + 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. @@ -728,9 +728,9 @@ namespace BEEV else { return _bm->CreateSimpForm(OR, - _bm->CreateSimpForm(AND, a, b), - _bm->CreateSimpForm(AND, b, c), - _bm->CreateSimpForm(AND, a, c)); + _bm->CreateSimpForm(AND, a, b), + _bm->CreateSimpForm(AND, b, c), + _bm->CreateSimpForm(AND, a, c)); } } @@ -788,7 +788,7 @@ namespace BEEV // q and r are "out" parameters. rwidth puts a bound on the // recursion depth. void BitBlaster::BBDivMod(const ASTVec &y, const ASTVec &x, - ASTVec &q, ASTVec &r, unsigned int rwidth) + ASTVec &q, ASTVec &r, unsigned int rwidth) { unsigned int width = y.size(); if (rwidth == 0) @@ -838,8 +838,8 @@ namespace BEEV // build ITE's (ITE cond then[i] else[i]) for each i. ASTVec BitBlaster::BBITE(const ASTNode& cond, - const ASTVec& thn, - const ASTVec& els) + const ASTVec& thn, + const ASTVec& els) { // Fast exits. if (ASTTrue == cond) @@ -855,7 +855,7 @@ namespace BEEV ASTVec::const_iterator th_it_end = thn.end(); ASTVec::const_iterator el_it = els.begin(); for (ASTVec::const_iterator - th_it = thn.begin(); th_it < th_it_end; th_it++, el_it++) + th_it = thn.begin(); th_it < th_it_end; th_it++, el_it++) { result.push_back(_bm->CreateSimpForm(ITE, cond, *th_it, *el_it)); } @@ -888,7 +888,7 @@ namespace BEEV // constant, deciding the result without looking at the rest of the // bits. ASTNode BitBlaster::BBBVLE(const ASTVec& left, - const ASTVec& right, bool is_signed) + 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 @@ -904,13 +904,13 @@ namespace BEEV { ASTNode neglit = _bm->CreateSimpNot(*lit); ASTNode thisbit = - _bm->CreateSimpForm(OR, - _bm->CreateSimpForm(AND, neglit, *rit), - _bm->CreateSimpForm(AND, - _bm->CreateSimpForm(OR, - neglit, - *rit), - prevbit)); + _bm->CreateSimpForm(OR, + _bm->CreateSimpForm(AND, neglit, *rit), + _bm->CreateSimpForm(AND, + _bm->CreateSimpForm(OR, + neglit, + *rit), + prevbit)); prevbit = thisbit; } @@ -928,11 +928,11 @@ namespace BEEV ASTNode msb = // TRUE if l < r _bm->CreateSimpForm(OR, _bm->CreateSimpForm(AND, neglmsb, rmsb), - _bm->CreateSimpForm(AND, - _bm->CreateSimpForm(OR, - neglmsb, - rmsb), - prevbit)); // else prevbit + _bm->CreateSimpForm(AND, + _bm->CreateSimpForm(OR, + neglmsb, + rmsb), + prevbit)); // else prevbit return msb; } diff --git a/src/to-sat/ToCNF.cpp b/src/to-sat/ToCNF.cpp index c0d8415..f6e1718 100644 --- a/src/to-sat/ToCNF.cpp +++ b/src/to-sat/ToCNF.cpp @@ -402,7 +402,7 @@ namespace BEEV } //End of SINGLETON() ClauseList* CNFMgr::UNION(const ClauseList& varphi1, - const ClauseList& varphi2) + const ClauseList& varphi2) { ClauseList* psi1 = COPY(varphi1); ClauseList* psi2 = COPY(varphi2); @@ -413,7 +413,7 @@ namespace BEEV } //End of UNION() void CNFMgr::INPLACE_UNION(ClauseList* varphi1, - const ClauseList& varphi2) + const ClauseList& varphi2) { ClauseList* psi2 = COPY(varphi2); varphi1->insert(varphi1->end(), psi2->begin(), psi2->end()); @@ -421,14 +421,14 @@ namespace BEEV } //End of INPLACE_UNION() void CNFMgr::NOCOPY_INPLACE_UNION(ClauseList* varphi1, - ClauseList* varphi2) + 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) + const ClauseList& varphi2) { ClauseList* psi = new ClauseList(); psi->reserve(varphi1.size() * varphi2.size()); @@ -812,7 +812,7 @@ namespace BEEV //main switch for individual cnf conversion cases void CNFMgr::convertFormulaToCNFPosCases(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { if (isPred(varphi)) { @@ -886,14 +886,14 @@ namespace BEEV default: { fprintf(stderr, "convertFormulaToCNFPosCases: "\ - "doesn't handle kind %d\n", k); + "doesn't handle kind %d\n", k); FatalError(""); } } } //End of convertFormulaToCNFPosCases() void CNFMgr::convertFormulaToCNFNegCases(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { if (isPred(varphi)) @@ -968,7 +968,7 @@ namespace BEEV default: { fprintf(stderr, "convertFormulaToCNFNegCases: "\ - "doesn't handle kind %d\n", k); + "doesn't handle kind %d\n", k); FatalError(""); } } @@ -979,7 +979,7 @@ namespace BEEV // individual cnf conversion cases void CNFMgr::convertFormulaToCNFPosPred(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { ASTVec psis; @@ -995,7 +995,7 @@ namespace BEEV } //End of convertFormulaToCNFPosPred() void CNFMgr::convertFormulaToCNFPosFALSE(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { ASTNode dummy_false_var = bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*")); @@ -1003,26 +1003,26 @@ namespace BEEV } //End of convertFormulaToCNFPosFALSE() void CNFMgr::convertFormulaToCNFPosTRUE(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*"); info[varphi]->clausespos = SINGLETON(dummy_true_var); } //End of convertFormulaToCNFPosTRUE void CNFMgr::convertFormulaToCNFPosBVGETBIT(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { info[varphi]->clausespos = SINGLETON(varphi); }//End of convertFormulaToCNFPosBVGETBIT() void CNFMgr::convertFormulaToCNFPosSYMBOL(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { info[varphi]->clausespos = SINGLETON(varphi); } //End of convertFormulaToCNFPosSYMBOL() void CNFMgr::convertFormulaToCNFPosNOT(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { convertFormulaToCNF(varphi[0], defs); info[varphi]->clausespos = COPY(*(info[varphi[0]]->clausesneg)); @@ -1030,7 +1030,7 @@ namespace BEEV } //End of convertFormulaToCNFPosNOT() void CNFMgr::convertFormulaToCNFPosAND(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { //**************************************** // (pos) AND ~> UNION @@ -1049,7 +1049,7 @@ namespace BEEV } //End of convertFormulaToCNFPosAND() void CNFMgr::convertFormulaToCNFPosNAND(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { bool renamesibs = false; ClauseList* clauses; @@ -1092,7 +1092,7 @@ namespace BEEV } //End of convertFormulaToCNFPosNAND() void CNFMgr::convertFormulaToCNFPosOR(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { bool renamesibs = false; ClauseList* clauses; @@ -1134,7 +1134,7 @@ namespace BEEV } //End of convertFormulaToCNFPosOR() void CNFMgr::convertFormulaToCNFPosNOR(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { //**************************************** // (pos) NOR ~> UNION NOT @@ -1154,7 +1154,7 @@ namespace BEEV } //End of convertFormulaToCNFPosNOR() void CNFMgr::convertFormulaToCNFPosIMPLIES(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { //**************************************** // (pos) IMPLIES ~> PRODUCT NOT [0] ; [1] @@ -1174,7 +1174,7 @@ namespace BEEV } //End of convertFormulaToCNFPosIMPLIES() void CNFMgr::convertFormulaToCNFPosITE(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { //**************************************** // (pos) ITE ~> UNION (PRODUCT NOT [0] ; [1]) @@ -1206,7 +1206,7 @@ namespace BEEV } //End of convertFormulaToCNFPosITE() void CNFMgr::convertFormulaToCNFPosXOR(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { ASTVec::const_iterator it = varphi.GetChildren().begin(); for (; it != varphi.GetChildren().end(); it++) @@ -1223,8 +1223,8 @@ namespace BEEV } //End of convertFormulaToCNFPosXOR() ClauseList* CNFMgr::convertFormulaToCNFPosXORAux(const ASTNode& varphi, - unsigned int idx, - ClauseList* defs) + unsigned int idx, + ClauseList* defs) { bool renamesibs; @@ -1240,24 +1240,24 @@ namespace BEEV // ; (PRODUCT NOT [idx] ; NOT [idx+1]) //**************************************** renamesibs = - (info[varphi[idx]]->clausespos)->size() > 1 ? true : false; + (info[varphi[idx]]->clausespos)->size() > 1 ? true : false; if (renamesibs) { setDoSibRenamingPos(*info[varphi[idx + 1]]); } renamesibs = - (info[varphi[idx]]->clausesneg)->size() > 1 ? true : false; + (info[varphi[idx]]->clausesneg)->size() > 1 ? true : false; if (renamesibs) { setDoSibRenamingNeg(*info[varphi[idx + 1]]); } psi1 = - PRODUCT(*(info[varphi[idx]]->clausespos), - *(info[varphi[idx + 1]]->clausespos)); + PRODUCT(*(info[varphi[idx]]->clausespos), + *(info[varphi[idx + 1]]->clausespos)); psi2 = - PRODUCT(*(info[varphi[idx]]->clausesneg), - *(info[varphi[idx + 1]]->clausesneg)); + PRODUCT(*(info[varphi[idx]]->clausesneg), + *(info[varphi[idx + 1]]->clausesneg)); NOCOPY_INPLACE_UNION(psi1, psi2); psi = psi1; @@ -1297,7 +1297,7 @@ namespace BEEV } //End of convertFormulaToCNFPosXORAux() void CNFMgr::convertFormulaToCNFNegPred(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { ASTVec psis; @@ -1311,18 +1311,18 @@ namespace BEEV info[varphi]->clausesneg = SINGLETON(bm->CreateNode(NOT, - bm->CreateNode(varphi.GetKind(), psis))); + bm->CreateNode(varphi.GetKind(), psis))); } //End of convertFormulaToCNFNegPred() void CNFMgr::convertFormulaToCNFNegFALSE(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { ASTNode dummy_true_var = bm->CreateSymbol("*TrueDummy*"); info[varphi]->clausesneg = SINGLETON(dummy_true_var); } //End of convertFormulaToCNFNegFALSE() void CNFMgr::convertFormulaToCNFNegTRUE(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { ASTNode dummy_false_var = bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*")); @@ -1330,20 +1330,20 @@ namespace BEEV } //End of convertFormulaToCNFNegTRUE() void CNFMgr::convertFormulaToCNFNegBVGETBIT(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { ClauseList* psi = SINGLETON(bm->CreateNode(NOT, varphi)); info[varphi]->clausesneg = psi; } //End of convertFormulaToCNFNegBVGETBIT() void CNFMgr::convertFormulaToCNFNegSYMBOL(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { info[varphi]->clausesneg = SINGLETON(bm->CreateNode(NOT, varphi)); } //End of convertFormulaToCNFNegSYMBOL() void CNFMgr::convertFormulaToCNFNegNOT(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { convertFormulaToCNF(varphi[0], defs); info[varphi]->clausesneg = COPY(*(info[varphi[0]]->clausespos)); @@ -1351,7 +1351,7 @@ namespace BEEV } //End of convertFormulaToCNFNegNOT() void CNFMgr::convertFormulaToCNFNegAND(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { bool renamesibs = false; ClauseList* clauses; @@ -1394,7 +1394,7 @@ namespace BEEV } //End of convertFormulaToCNFNegAND() void CNFMgr::convertFormulaToCNFNegNAND(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { //**************************************** // (neg) NAND ~> UNION @@ -1414,7 +1414,7 @@ namespace BEEV } //End of convertFormulaToCNFNegNAND() void CNFMgr::convertFormulaToCNFNegOR(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { //**************************************** // (neg) OR ~> UNION NOT @@ -1434,7 +1434,7 @@ namespace BEEV } //End of convertFormulaToCNFNegOR() void CNFMgr::convertFormulaToCNFNegNOR(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { bool renamesibs = false; ClauseList* clauses; @@ -1476,7 +1476,7 @@ namespace BEEV } //End of convertFormulaToCNFNegNOR() void CNFMgr::convertFormulaToCNFNegIMPLIES(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { //**************************************** // (neg) IMPLIES ~> UNION [0] ; NOT [1] @@ -1492,7 +1492,7 @@ namespace BEEV } //End of convertFormulaToCNFNegIMPLIES() void CNFMgr::convertFormulaToCNFNegITE(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { //**************************************** // (neg) ITE ~> UNION (PRODUCT NOT [0] ; NOT [1]) @@ -1524,7 +1524,7 @@ namespace BEEV } //End of convertFormulaToCNFNegITE() void CNFMgr::convertFormulaToCNFNegXOR(const ASTNode& varphi, - ClauseList* defs) + ClauseList* defs) { ASTVec::const_iterator it = varphi.GetChildren().begin(); for (; it != varphi.GetChildren().end(); it++) @@ -1541,8 +1541,8 @@ namespace BEEV } //End of convertFormulaToCNFNegXOR() ClauseList* CNFMgr::convertFormulaToCNFNegXORAux(const ASTNode& varphi, - unsigned int idx, - ClauseList* defs) + unsigned int idx, + ClauseList* defs) { bool renamesibs; ClauseList* psi; @@ -1559,7 +1559,7 @@ namespace BEEV //**************************************** convertFormulaToCNF(varphi[idx], defs); renamesibs = - (info[varphi[idx]]->clausesneg)->size() > 1 ? true : false; + (info[varphi[idx]]->clausesneg)->size() > 1 ? true : false; if (renamesibs) { setDoSibRenamingPos(*info[varphi[idx + 1]]); @@ -1567,18 +1567,18 @@ namespace BEEV convertFormulaToCNF(varphi[idx], defs); renamesibs = - (info[varphi[idx]]->clausespos)->size() > 1 ? true : false; + (info[varphi[idx]]->clausespos)->size() > 1 ? true : false; if (renamesibs) { setDoSibRenamingNeg(*info[varphi[idx + 1]]); } psi1 = - PRODUCT(*(info[varphi[idx]]->clausesneg), - *(info[varphi[idx + 1]]->clausespos)); + PRODUCT(*(info[varphi[idx]]->clausesneg), + *(info[varphi[idx + 1]]->clausespos)); psi2 = - PRODUCT(*(info[varphi[idx]]->clausespos), - *(info[varphi[idx + 1]]->clausesneg)); + PRODUCT(*(info[varphi[idx]]->clausespos), + *(info[varphi[idx + 1]]->clausesneg)); NOCOPY_INPLACE_UNION(psi1, psi2); psi = psi1; @@ -1746,7 +1746,7 @@ namespace BEEV if (bm->UserFlags.stats_flag) { cerr << "Number of clauses:" << defs->size() << endl; - PrintClauseList(cout, *defs); + //PrintClauseList(cout, *defs); } return defs; @@ -1772,12 +1772,12 @@ namespace BEEV << "=========================================" << endl; for (int i = 0; i < num_clauses; i++) { - os << "Clause " - << i << endl - << "-------------------------------------------" << endl; - LispPrintVecSpecial(os, *cll[i], 0); - os << endl - << "-------------------------------------------" << endl; + os << "Clause " + << i << endl + << "-------------------------------------------" << endl; + LispPrintVecSpecial(os, *cll[i], 0); + os << endl + << "-------------------------------------------" << endl; } } //end of PrintClauseList() } // end namespace BEEV diff --git a/src/to-sat/ToCNF.h b/src/to-sat/ToCNF.h index abfde5d..bc707b5 100644 --- a/src/to-sat/ToCNF.h +++ b/src/to-sat/ToCNF.h @@ -136,7 +136,7 @@ namespace BEEV void NOCOPY_INPLACE_UNION(ClauseList* varphi1, ClauseList* varphi2); ClauseList* PRODUCT(const ClauseList& varphi1, - const ClauseList& varphi2); + const ClauseList& varphi2); //######################################## //######################################## @@ -179,7 +179,7 @@ namespace BEEV void convertFormulaToCNFPosFALSE(const ASTNode& varphi, ClauseList* defs); void convertFormulaToCNFPosTRUE(const ASTNode& varphi, ClauseList* defs); void convertFormulaToCNFPosBVGETBIT(const ASTNode& varphi, - ClauseList* defs); + ClauseList* defs); void convertFormulaToCNFPosSYMBOL(const ASTNode& varphi, ClauseList* defs); void convertFormulaToCNFPosNOT(const ASTNode& varphi, ClauseList* defs); void convertFormulaToCNFPosAND(const ASTNode& varphi, ClauseList* defs); @@ -190,13 +190,13 @@ namespace BEEV void convertFormulaToCNFPosITE(const ASTNode& varphi, ClauseList* defs); void convertFormulaToCNFPosXOR(const ASTNode& varphi, ClauseList* defs); ClauseList* convertFormulaToCNFPosXORAux(const ASTNode& varphi, - unsigned int idx, - ClauseList* defs); + 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); + ClauseList* defs); void convertFormulaToCNFNegSYMBOL(const ASTNode& varphi, ClauseList* defs); void convertFormulaToCNFNegNOT(const ASTNode& varphi, ClauseList* defs); void convertFormulaToCNFNegAND(const ASTNode& varphi, ClauseList* defs); @@ -207,8 +207,8 @@ namespace BEEV void convertFormulaToCNFNegITE(const ASTNode& varphi, ClauseList* defs); void convertFormulaToCNFNegXOR(const ASTNode& varphi, ClauseList* defs); ClauseList* convertFormulaToCNFNegXORAux(const ASTNode& varphi, - unsigned int idx, - ClauseList* defs); + unsigned int idx, + ClauseList* defs); //######################################## //######################################## diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index fbcfb89..d4a0ed2 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -203,12 +203,12 @@ namespace BEEV result = SymbolTruthValue(newS, form); cout << "================" - << endl - << "Checking BB formula:" - << form << endl; + << endl + << "Checking BB formula:" + << form << endl; cout << "----------------" - << endl - << "Result:" << result << endl; + << endl + << "Result:" << result << endl; break; } @@ -225,11 +225,11 @@ namespace BEEV result = bm->CreateSimpForm(k, eval_children); cout << "================" - << endl - << "Checking BB formula:" << form << endl; + << endl + << "Checking BB formula:" << form << endl; cout << "----------------" - << endl - << "Result:" << result << endl; + << endl + << "Result:" << result << endl; ASTNode replit_eval; // Compare with replit, if there is one. @@ -246,21 +246,21 @@ namespace BEEV { // It's (NOT sym). Get value of sym and complement. replit_eval = - bm->CreateSimpNot(SymbolTruthValue(newS, replit[0])); + bm->CreateSimpNot(SymbolTruthValue(newS, replit[0])); } cout << "----------------" - << endl - << "Rep lit: " << replit << endl; + << endl + << "Rep lit: " << replit << endl; cout << "----------------" - << endl - << "Rep lit value: " << replit_eval << endl; + << endl + << "Rep lit value: " << replit_eval << endl; if (result != replit_eval) { // Hit the panic button. FatalError("Truth value of BitBlasted formula "\ - "disagrees with representative literal in CNF."); + "disagrees with representative literal in CNF."); } } else