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;
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);
break;
case BVVARSHIFT:
FatalError("BBTerm: These kinds have not "\
- "been implemented in the BitBlaster: ", term);
+ "been implemented in the BitBlaster: ", term);
break;
case ITE:
{
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;
}
//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
//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");
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;
}
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);
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:
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());
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);
{
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;
}
// 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.
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));
}
}
// 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)
// 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)
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));
}
// 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
{
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;
}
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;
}
} //End of SINGLETON()
ClauseList* CNFMgr::UNION(const ClauseList& varphi1,
- const ClauseList& varphi2)
+ const ClauseList& varphi2)
{
ClauseList* psi1 = COPY(varphi1);
ClauseList* psi2 = COPY(varphi2);
} //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());
} //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());
//main switch for individual cnf conversion cases
void CNFMgr::convertFormulaToCNFPosCases(const ASTNode& varphi,
- ClauseList* defs)
+ ClauseList* defs)
{
if (isPred(varphi))
{
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))
default:
{
fprintf(stderr, "convertFormulaToCNFNegCases: "\
- "doesn't handle kind %d\n", k);
+ "doesn't handle kind %d\n", k);
FatalError("");
}
}
// individual cnf conversion cases
void CNFMgr::convertFormulaToCNFPosPred(const ASTNode& varphi,
- ClauseList* defs)
+ ClauseList* defs)
{
ASTVec psis;
} //End of convertFormulaToCNFPosPred()
void CNFMgr::convertFormulaToCNFPosFALSE(const ASTNode& varphi,
- ClauseList* defs)
+ ClauseList* defs)
{
ASTNode dummy_false_var =
bm->CreateNode(NOT, bm->CreateSymbol("*TrueDummy*"));
} //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));
} //End of convertFormulaToCNFPosNOT()
void CNFMgr::convertFormulaToCNFPosAND(const ASTNode& varphi,
- ClauseList* defs)
+ ClauseList* defs)
{
//****************************************
// (pos) AND ~> UNION
} //End of convertFormulaToCNFPosAND()
void CNFMgr::convertFormulaToCNFPosNAND(const ASTNode& varphi,
- ClauseList* defs)
+ ClauseList* defs)
{
bool renamesibs = false;
ClauseList* clauses;
} //End of convertFormulaToCNFPosNAND()
void CNFMgr::convertFormulaToCNFPosOR(const ASTNode& varphi,
- ClauseList* defs)
+ ClauseList* defs)
{
bool renamesibs = false;
ClauseList* clauses;
} //End of convertFormulaToCNFPosOR()
void CNFMgr::convertFormulaToCNFPosNOR(const ASTNode& varphi,
- ClauseList* defs)
+ ClauseList* defs)
{
//****************************************
// (pos) NOR ~> UNION NOT
} //End of convertFormulaToCNFPosNOR()
void CNFMgr::convertFormulaToCNFPosIMPLIES(const ASTNode& varphi,
- ClauseList* defs)
+ ClauseList* defs)
{
//****************************************
// (pos) IMPLIES ~> PRODUCT NOT [0] ; [1]
} //End of convertFormulaToCNFPosIMPLIES()
void CNFMgr::convertFormulaToCNFPosITE(const ASTNode& varphi,
- ClauseList* defs)
+ ClauseList* defs)
{
//****************************************
// (pos) ITE ~> UNION (PRODUCT NOT [0] ; [1])
} //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++)
} //End of convertFormulaToCNFPosXOR()
ClauseList* CNFMgr::convertFormulaToCNFPosXORAux(const ASTNode& varphi,
- unsigned int idx,
- ClauseList* defs)
+ unsigned int idx,
+ ClauseList* defs)
{
bool renamesibs;
// ; (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;
} //End of convertFormulaToCNFPosXORAux()
void CNFMgr::convertFormulaToCNFNegPred(const ASTNode& varphi,
- ClauseList* defs)
+ ClauseList* defs)
{
ASTVec psis;
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*"));
} //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));
} //End of convertFormulaToCNFNegNOT()
void CNFMgr::convertFormulaToCNFNegAND(const ASTNode& varphi,
- ClauseList* defs)
+ ClauseList* defs)
{
bool renamesibs = false;
ClauseList* clauses;
} //End of convertFormulaToCNFNegAND()
void CNFMgr::convertFormulaToCNFNegNAND(const ASTNode& varphi,
- ClauseList* defs)
+ ClauseList* defs)
{
//****************************************
// (neg) NAND ~> UNION
} //End of convertFormulaToCNFNegNAND()
void CNFMgr::convertFormulaToCNFNegOR(const ASTNode& varphi,
- ClauseList* defs)
+ ClauseList* defs)
{
//****************************************
// (neg) OR ~> UNION NOT
} //End of convertFormulaToCNFNegOR()
void CNFMgr::convertFormulaToCNFNegNOR(const ASTNode& varphi,
- ClauseList* defs)
+ ClauseList* defs)
{
bool renamesibs = false;
ClauseList* clauses;
} //End of convertFormulaToCNFNegNOR()
void CNFMgr::convertFormulaToCNFNegIMPLIES(const ASTNode& varphi,
- ClauseList* defs)
+ ClauseList* defs)
{
//****************************************
// (neg) IMPLIES ~> UNION [0] ; NOT [1]
} //End of convertFormulaToCNFNegIMPLIES()
void CNFMgr::convertFormulaToCNFNegITE(const ASTNode& varphi,
- ClauseList* defs)
+ ClauseList* defs)
{
//****************************************
// (neg) ITE ~> UNION (PRODUCT NOT [0] ; NOT [1])
} //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++)
} //End of convertFormulaToCNFNegXOR()
ClauseList* CNFMgr::convertFormulaToCNFNegXORAux(const ASTNode& varphi,
- unsigned int idx,
- ClauseList* defs)
+ unsigned int idx,
+ ClauseList* defs)
{
bool renamesibs;
ClauseList* psi;
//****************************************
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]]);
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;
if (bm->UserFlags.stats_flag)
{
cerr << "Number of clauses:" << defs->size() << endl;
- PrintClauseList(cout, *defs);
+ //PrintClauseList(cout, *defs);
}
return defs;
<< "=========================================" << 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
void NOCOPY_INPLACE_UNION(ClauseList* varphi1, ClauseList* varphi2);
ClauseList* PRODUCT(const ClauseList& varphi1,
- const ClauseList& varphi2);
+ const ClauseList& varphi2);
//########################################
//########################################
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);
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);
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);
//########################################
//########################################
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;
}
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.
{
// 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
projects / francis / stp.git / commitdiff