#include <cassert>
#include "../AST/AST.h"
#include "../STPManager/STPManager.h"
+#include "BitBlast.h"
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
// 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;
}
// 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)
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
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]);
}
}
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:
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;
}
//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.
// lp(result);
// cout << endl;
- result = CreateNode(BOOLVEC, tmp_res);
+ result = _bm->CreateNode(BOOLVEC, tmp_res);
break;
}
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");
//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:
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:
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:
//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;
}
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.
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:
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:
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:
FatalError("BBTerm: Illegal kind to BBTerm", term);
}
- //if(result == ASTJunk)
- // cout<<"result does not change"<<endl;
- // cout << "================" << endl << "BBTerm:" << term << endl;
- // cout << "----------------" << endl << "BBTerm result:";
- // lpvec(result);
- // cout << endl;
-
assert(!result.IsNull());
return (BBTermMemo[term] = result);
// bit blast a formula (boolean term). Result is one bit wide,
// so it returns a single ASTNode.
// FIXME: Add IsNegated flag.
- const ASTNode BeevMgr::BBForm(const ASTNode& form)
+ const ASTNode BitBlaster::BBForm(const ASTNode& form)
{
-
ASTNodeMap::iterator it = BBFormMemo.find(form);
if (it != BBFormMemo.end())
{
}
case NOT:
- result = CreateSimpNot(BBForm(form[0]));
+ result = _bm->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:
{
bbkids.push_back(BBForm(*it));
}
- result = CreateSimpForm(k, bbkids);
+ result = _bm->CreateSimpForm(k, bbkids);
break;
}
// 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);
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;
}
}
// 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?
}
// 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();
// 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)
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);
}
// 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)
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);
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;
}
// 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
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;
}
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!)
// 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();
// 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();
}
// 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]);
}
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:
}
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:
}
// 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();
{
for (; lit != litend; lit++, rit++)
{
- ASTNode biteq = CreateSimpForm(IFF, *lit, *rit);
+ ASTNode biteq = _bm->CreateSimpForm(IFF, *lit, *rit);
// fast path exit
if (biteq == ASTFalse)
{
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
#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<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 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<const ASTNode*> (**it));
- }
-
- return psi;
- }
-
- BeevMgr::ClauseList* SINGLETON(const ASTNode& varphi)
- {
- ASTNode* copy = ASTNodeToASTNodePtr(varphi);
-
- BeevMgr::ClausePtr clause = new vector<const ASTNode*> ();
- 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<const ASTNode*> ();
- 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<const ASTNode*> (**it));
+ }
+
+ return psi;
+ } //End of COPY()
+
+ ClauseList* CNFMgr::SINGLETON(const ASTNode& varphi)
+ {
+ ASTNode* copy = ASTNodeToASTNodePtr(varphi);
+
+ ClausePtr clause = new vector<const ASTNode*> ();
+ 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<const ASTNode*> ();
+ 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:
{
FatalError("");
}
}
- }
+ } //End of convertFormulaToCNFPosCases()
- void convertFormulaToCNFNegCases(const ASTNode& varphi, BeevMgr::ClauseList* defs)
+ void CNFMgr::convertFormulaToCNFNegCases(const ASTNode& varphi, ClauseList* defs)
{
if (isPred(varphi))
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();
}
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);
}
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
}
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
}
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++)
{
}
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]
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])
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]);
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)
{
// (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)
}
return psi;
- }
+ } //End of convertFormulaToCNFPosXORAux()
- void convertFormulaToCNFNegPred(const ASTNode& varphi, BeevMgr::ClauseList* defs)
+ void CNFMgr::convertFormulaToCNFNegPred(const ASTNode& varphi, ClauseList* defs)
{
ASTVec psis;
}
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
}
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++)
{
}
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++)
{
}
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
}
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]
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])
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]);
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)
{
// (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)
}
convertFormulaToCNF(varphi[idx], defs);
- BeevMgr::ClauseList* theta2;
+ ClauseList* theta2;
theta2 = convertFormulaToCNFNegXORAux(varphi, idx + 1, defs);
renamesibs = theta2->size() > 1 ? true : false;
if (renamesibs)
}
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)
{
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)
{
info.erase(varphi);
}
}
- }
+ } //End of reduceMemoryFootprintNeg()
//########################################
//########################################
- ASTNode* ASTNodeToASTNodePtr(const ASTNode& varphi)
+ ASTNode* CNFMgr::ASTNodeToASTNodePtr(const ASTNode& varphi)
{
ASTNode* psi;
}
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.
}
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
projects / francis / stp.git / commitdiff