From a1dab4fc51bfc629daf1d3cb7f59a1a0b323f9ad Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 1 Jul 2010 14:58:47 +0000 Subject: [PATCH] Refactor, getting ready for AIGs. This does add additional code, but that code isn't currently enabled. * Provide a base class for ToSAT. Bitblasting via ASTNodes and AIGs both implement this class. * BBNodeManagerAIG creates AIGs that are wrapped with a BBNode object. * BitBlastNew is now templated on the node type and the node factory. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@905 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/ASTNode.cpp | 2 +- src/main/Makefile | 9 +- src/to-sat/AIG/BBNodeAIG.h | 65 ++++ src/to-sat/AIG/BBNodeManagerAIG.h | 304 ++++++++++++++++++ src/to-sat/AIG/ToSATAIG.h | 72 +++++ src/to-sat/BBNode.h | 17 - ...BBNodeManager.h => BBNodeManagerASTNode.h} | 35 +- src/to-sat/BitBlastNew.cpp | 166 ++++++---- src/to-sat/BitBlastNew.h | 76 +++-- src/to-sat/ToSAT.cpp | 52 +-- src/to-sat/ToSAT.h | 59 +--- src/to-sat/ToSATBase.cpp | 54 ++++ src/to-sat/ToSATBase.h | 49 +++ 13 files changed, 723 insertions(+), 237 deletions(-) create mode 100644 src/to-sat/AIG/BBNodeAIG.h create mode 100644 src/to-sat/AIG/BBNodeManagerAIG.h create mode 100644 src/to-sat/AIG/ToSATAIG.h delete mode 100644 src/to-sat/BBNode.h rename src/to-sat/{BBNodeManager.h => BBNodeManagerASTNode.h} (55%) create mode 100644 src/to-sat/ToSATBase.cpp create mode 100644 src/to-sat/ToSATBase.h diff --git a/src/AST/ASTNode.cpp b/src/AST/ASTNode.cpp index 09d43f1..3e2e83b 100644 --- a/src/AST/ASTNode.cpp +++ b/src/AST/ASTNode.cpp @@ -116,7 +116,7 @@ namespace BEEV STPMgr* ASTNode::GetSTPMgr() const { - return GlobalSTP->bm; + return ParserBM; } //End of GetSTPMgr() // Checks if the node has alreadybeen printed or not diff --git a/src/main/Makefile b/src/main/Makefile index 83496cc..ca2ef94 100644 --- a/src/main/Makefile +++ b/src/main/Makefile @@ -5,16 +5,17 @@ SRCS=main.cpp versionString.cpp Globals.cpp OBJS = $(SRCS:.cpp=.o) CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE) -LIBS = -L../to-sat -ltosat \ - -L../STPManager -lstpmgr \ +LIBS = -L../STPManager -lstpmgr \ -L../absrefine_counterexample -labstractionrefinement \ + -L../to-sat -ltosat \ -L../simplifier -lsimplifier \ -L../printer -lprinter \ -L../AST -last \ -L../extlib-constbv -lconstantbv \ -L../sat -lminisat \ - -L../parser -lparser - + -L../parser -lparser \ + -L../extlib-abc -labc + # This rebuilds each time, because the target "parser" is not created # Until the dependencies on each of the libraries is included, that's safest. parser: $(OBJS) depend diff --git a/src/to-sat/AIG/BBNodeAIG.h b/src/to-sat/AIG/BBNodeAIG.h new file mode 100644 index 0000000..c050131 --- /dev/null +++ b/src/to-sat/AIG/BBNodeAIG.h @@ -0,0 +1,65 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Trevor Hansen + * + * BEGIN DATE: June, 2010 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ + +#ifndef BBNODEAIG_H_ +#define BBNODEAIG_H_ + +#include "../../extlib-abc/aig.h" + +namespace BEEV +{ + + // This class wraps around a pointer to an AIG (provided by the ABC tool). +class BBNodeAIG +{ + +public: + Aig_Obj_t * n; + + BBNodeAIG() + { + n = NULL; + } + + BBNodeAIG(Aig_Obj_t * _n) + { + n = _n; + } + + bool IsNull() const + { + return n == NULL; + } + + bool operator==(const BBNodeAIG &other) const + { + return n == other.n; + } + + bool operator!=(const BBNodeAIG &other) const + { + return !(n == other.n); + } + + + bool operator<(const BBNodeAIG &other) const + { + return n < other.n; + } + +}; +std::ostream& operator<<(std::ostream& output, const BBNodeAIG& h) +{ + FatalError("This isn't implemented yet sorry;"); + return output; +} +} +; + +#endif diff --git a/src/to-sat/AIG/BBNodeManagerAIG.h b/src/to-sat/AIG/BBNodeManagerAIG.h new file mode 100644 index 0000000..2c1afb8 --- /dev/null +++ b/src/to-sat/AIG/BBNodeManagerAIG.h @@ -0,0 +1,304 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Trevor Hansen + * + * BEGIN DATE: June, 2010 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ + +#ifndef BBNodeManagerAIG_H_ +#define BBNodeManagerAIG_H_ + +#include "BBNodeAIG.h" + +// cnf_short omits some stuff that doesn't compile in g++ that we don't need anyway. +#include "../../extlib-abc/aig.h" +#include "../../extlib-abc/cnf_short.h" +#include "../../extlib-abc/dar.h" +#include "../ToSATBase.h" + +typedef Cnf_Dat_t_ CNFData; +typedef Aig_Obj_t AIGNode; + +namespace BEEV +{ +class ASTNode; +class STPMgr; // we ignore this anyway. + +extern vector _empty_BBNodeAIGVec; + +// Creates AIG nodes with ABC and wraps them in BBNodeAIG's. +class BBNodeManagerAIG +{ + Aig_Man_t *aigMgr; + + // Map from symbols to their AIG nodes. + typedef map > SymbolToBBNode; + SymbolToBBNode symbolToBBNode; + + // AIGs can only take two parameters. This makes a log_2 height + // tower of varadic inputs. + Aig_Obj_t * makeTower(Aig_Obj_t * (*t)(Aig_Man_t *, Aig_Obj_t *, + Aig_Obj_t *), vector& children) + { + deque names; + + for (unsigned i = 0; i < children.size(); i++) + names.push_back(children[i].n); + + while (names.size() > 2) + { + Aig_Obj_t* a = names.front(); + names.pop_front(); + + Aig_Obj_t* b = names.front(); + names.pop_front(); + + Aig_Obj_t* n = t(aigMgr, a, b); + names.push_back(n); + } + + // last two now. + assert(names.size() == 2); + + Aig_Obj_t* a = names.front(); + names.pop_front(); + + Aig_Obj_t* b = names.front(); + names.pop_front(); + + return t(aigMgr, a, b); + } + +public: + + BBNodeManagerAIG(STPMgr*& _stp) + { + aigMgr = Aig_ManStart(0); + // fancier strashing. + aigMgr->fAddStrash = 1; + } + + ~BBNodeManagerAIG() + { + Aig_ManStop(aigMgr); + } + + BBNodeAIG getTrue() + { + return BBNodeAIG((aigMgr->pConst1)); + } + + BBNodeAIG getFalse() + { + return BBNodeAIG(Aig_Not(aigMgr->pConst1)); + } + + void + toCNF(BBNodeAIG& top, Cnf_Dat_t*& cnfData, ToSATBase::ASTNodeToVar& nodeToVar) + { + assert(cnfData == NULL); + + Aig_Man_t *aigMgr; + + Aig_ObjCreatePo(aigMgr, top.n); + Aig_ManCleanup( aigMgr); // remove nodes not connected to the PO. + Aig_ManCheck(aigMgr); // check that AIG looks ok. + + assert(Aig_ManPoNum(aigMgr) == 1); + + //cerr << "SAFDASDF"; + + // copied from darScript.c: Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig ) + /* + Dar_LibStart(); + Aig_Man_t * pTemp1, *pTemp2; + Dar_RwrPar_t Pars, * pPars = &Pars; + Dar_ManDefaultRwrParams( pPars ); + Dar_ManRewrite( aigMgr, pPars ); + Aig_ManCheck(aigMgr); // check that AIG looks ok. + Dar_LibStop(); + */ + + //assert(Aig_ManPoNum(aigMgr) == 1); + + //Aig_NtkReassignIds( aigMgr ); + // fix the levels + //Aig_ManUpdateLevel( aigMgr, Aig_ManPo(aigMgr,0)); + //Aig_ManVerifyLevel( aigMgr ); + + + // assert(Aig_ManPoNum(aigMgr) == 1); + + //Dar_RwrPar_t pPars; + //Dar_ManDefaultRwrParams( &pPars ); + //Dar_ManRewrite( aigMgr, &pPars ); + + + // Cnf_Derive seems more advanced, but gives assertion errors sometimes. + cnfData = Cnf_Derive(aigMgr, 0); + + BBNodeManagerAIG::SymbolToBBNode::const_iterator it; + + assert(nodeToVar.size() ==0); + + for (it = symbolToBBNode.begin(); it != symbolToBBNode.end(); it++) + { + const ASTNode& n = it->first; + const vector &b = it->second; + if (nodeToVar.find(n) == nodeToVar.end()) + { + const int width = (n.GetType() == BOOLEAN_TYPE) ? 1: n.GetValueWidth(); + vector v(width, ~((unsigned) 0)); + nodeToVar.insert(make_pair(n, v)); + } + + vector& v = nodeToVar[n]; + for (unsigned i = 0; i < b.size(); i++) + { + v[i] = cnfData->pVarNums[b[i].n->Id]; + } + } + assert(cnfData != NULL); + } + + // The same symbol always needs to return the same AIG node, + // if it doesn't you will get the wrong answer. + BBNodeAIG CreateSymbol(const ASTNode& n, unsigned i) + { + assert(n.GetKind() == SYMBOL); + + // booleans have width 0. + const unsigned width = std::max((unsigned)1, n.GetValueWidth()); + + SymbolToBBNode::iterator it; + it = symbolToBBNode.find(n); + if (symbolToBBNode.end() == it) + { + symbolToBBNode[n] = vector (width); + it = symbolToBBNode.find(n); + } + + assert(it->second.size() == width); + assert(i < width); + + if (!it->second[i].IsNull()) + return it->second[i]; + + it->second[i] = BBNodeAIG(Aig_ObjCreatePi(aigMgr)); + + return it->second[i]; + } + + BBNodeAIG CreateNode(Kind kind, vector& children) + { + Aig_Obj_t * pNode; + + switch (kind) + { + case AND: + assert (children.size() != 0); + if (children.size() == 1) + pNode = children[0].n; + else if (children.size() == 2) + pNode = Aig_And(aigMgr, children[0].n, children[1].n); + else + pNode = makeTower(Aig_And, children); + break; + + case OR: + if (children.size() == 2) + pNode = Aig_Or(aigMgr, children[0].n, children[1].n); + else + pNode = makeTower(Aig_Or, children); + break; + case NAND: + if (children.size() == 2) + pNode = Aig_And(aigMgr, children[0].n, children[1].n); + else + pNode = makeTower(Aig_And, children); + pNode = Aig_Not(pNode); + break; + case NOT: + assert(children.size() ==1); + pNode = Aig_Not(children[0].n); + break; + case NOR: + if (children.size() == 2) + pNode = Aig_Or(aigMgr, children[0].n, children[1].n); + else + pNode = makeTower(Aig_Or, children); + break; + pNode = Aig_Not(pNode); + break; + case XOR: + assert(children.size() ==2); + pNode = Aig_Exor(aigMgr, children[0].n, children[1].n); + break; + case IFF: + assert(children.size() ==2); + pNode = Aig_Exor(aigMgr, children[0].n, children[1].n); + pNode = Aig_Not(pNode); + break; + case IMPLIES: + assert(children.size() ==2); + pNode = Aig_Or(aigMgr, Aig_Not(children[0].n), children[1].n); + break; + case ITE: + assert(children.size() ==3); + pNode + = Aig_Mux(aigMgr, children[0].n, children[1].n, + children[2].n); + break; + + default: + cerr << "Not handled::!!" << _kind_names[kind]; + FatalError("Never here"); + } + return BBNodeAIG(pNode); + } + + BBNodeAIG CreateNode(Kind kind, const BBNodeAIG& child0, + const vector & back_children = _empty_BBNodeAIGVec) + { + vector front_children; + front_children.reserve(1 + back_children.size()); + front_children.push_back(child0); + front_children.insert(front_children.end(), back_children.begin(), + back_children.end()); + return CreateNode(kind, front_children); + } + + BBNodeAIG CreateNode(Kind kind, const BBNodeAIG& child0, const BBNodeAIG& child1, + const vector & back_children = _empty_BBNodeAIGVec) + { + vector front_children; + front_children.reserve(2 + back_children.size()); + front_children.push_back(child0); + front_children.push_back(child1); + front_children.insert(front_children.end(), back_children.begin(), + back_children.end()); + return CreateNode(kind, front_children); + + } + + BBNodeAIG CreateNode(Kind kind, const BBNodeAIG& child0, const BBNodeAIG& child1, + const BBNodeAIG& child2, const vector & back_children = + _empty_BBNodeAIGVec) + { + vector front_children; + front_children.reserve(3 + back_children.size()); + front_children.push_back(child0); + front_children.push_back(child1); + front_children.push_back(child2); + front_children.insert(front_children.end(), back_children.begin(), + back_children.end()); + return CreateNode(kind, front_children); + } +}; + +} +; + +#endif /* BBNodeManagerAIG_H_ */ diff --git a/src/to-sat/AIG/ToSATAIG.h b/src/to-sat/AIG/ToSATAIG.h new file mode 100644 index 0000000..2fec480 --- /dev/null +++ b/src/to-sat/AIG/ToSATAIG.h @@ -0,0 +1,72 @@ +// -*- c++ -*- +/******************************************************************** + * AUTHORS: Trevor Hansen + * + * BEGIN DATE: June, 2010 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ + +#ifndef TOSATAIG_H +#define TOSATAIG_H +#include + +#include "ToCNF.h" + +#include "../AST/AST.h" +#include "../AST/RunTimes.h" +#include "../STPManager/STPManager.h" +#include "BitBlastNew.h" +#include "BBNodeManagerAIG.h" + +namespace BEEV +{ + + class ToSATAIG : public ToSATBase + { + private: + + ASTNodeToVar nodeToVar; + public: + + ToSATAIG(STPMgr * bm) : + ToSATBase(bm) + { + } + + void ClearAllTables() + { + nodeToVar.clear(); + } + + ASTNodeToVar& SATVar_to_SymbolIndexMap() + { + return nodeToVar; + } + + bool + CallSAT(MINISAT::Solver& SatSolver, const ASTNode& input) + { + BBNodeManagerAIG mgr(bm); + BitBlasterNew bb(bm); + BitBlasterNew::BBNodeSet support; + BBNodeAIG BBFormula = bb.BBForm(input, support); + + Cnf_Dat_t* cnfData = NULL; + + mgr.toCNF(BBFormula, cnfData, nodeToVar); + + Cnf_ClearMemory(); + Cnf_DataFree(cnfData); + + // TO DO Solve. + // TODO Return the answer + FatalError("not implemented"); + return false; + + + } + }; +} + +#endif diff --git a/src/to-sat/BBNode.h b/src/to-sat/BBNode.h deleted file mode 100644 index f79341b..0000000 --- a/src/to-sat/BBNode.h +++ /dev/null @@ -1,17 +0,0 @@ -#ifndef BBNODE_H_ -#define BBNODE_H_ - -#include "../AST/AST.h" - -namespace BEEV { -typedef ASTNode BBNode; - -typedef vector BBNodeVec; -typedef vector > BBNodeVecVec; -typedef map BBNodeMap; -typedef map BBNodeVecMap; -typedef set BBNodeSet; -} -; - -#endif diff --git a/src/to-sat/BBNodeManager.h b/src/to-sat/BBNodeManagerASTNode.h similarity index 55% rename from src/to-sat/BBNodeManager.h rename to src/to-sat/BBNodeManagerASTNode.h index 6aadbc3..09a29f7 100644 --- a/src/to-sat/BBNodeManager.h +++ b/src/to-sat/BBNodeManagerASTNode.h @@ -1,34 +1,38 @@ #ifndef BBNodeManager_H_ #define BBNodeManager_H_ -#include "BBNode.h" #include "../STPManager/STPManager.h" namespace BEEV { class ASTNode; typedef std::vector ASTVec; -extern BBNodeVec _empty_BBNodeVec; - -class BBNodeManager { +// Called by the bitblaster. This returns ASTNodes after applying the +// CreateSimpForm(..) simplifications. +class BBNodeManagerASTNode { ASTNode ASTTrue, ASTFalse; STPMgr *stp; public: - BBNodeManager(STPMgr *_stp) { + + BBNodeManagerASTNode(STPMgr *_stp) { stp = _stp; ASTTrue = stp->CreateNode(TRUE); ASTFalse = stp->CreateNode(FALSE); } - ~BBNodeManager() { + ~BBNodeManagerASTNode() { } - BBNode getFalse() { + ASTNode getTrue() { + return ASTTrue; + } + + ASTNode getFalse() { return ASTFalse; } - BBNode CreateSymbol(const ASTNode& n, unsigned i) { + ASTNode CreateSymbol(const ASTNode& n, unsigned i) { if (n.GetType() == BOOLEAN_TYPE) { assert(i == 0); return n; @@ -36,30 +40,25 @@ public: return stp->CreateNode(BVGETBIT, n, stp->CreateBVConst(32, i)); } - BBNode getTrue() { - return ASTTrue; - } - // CreateSimpForm removes IFF which aren't handled by the cnf converter. - BBNode CreateNode(Kind kind, BBNodeVec& children) { + ASTNode CreateNode(Kind kind, vector& children) { return stp->CreateSimpForm(kind, children); } - BBNode CreateNode(Kind kind, const BBNode& child0) { + ASTNode CreateNode(Kind kind, const ASTNode& child0) { return stp->CreateSimpForm(kind, child0); } - BBNode CreateNode(Kind kind, const BBNode& child0, const BBNode& child1) { + ASTNode CreateNode(Kind kind, const ASTNode& child0, const ASTNode& child1) { return stp->CreateSimpForm(kind, child0, child1); } - BBNode CreateNode(Kind kind, const BBNode& child0, const BBNode& child1, - const BBNode& child2) { + ASTNode CreateNode(Kind kind, const ASTNode& child0, const ASTNode& child1, + const ASTNode& child2) { return stp->CreateSimpForm(kind, child0, child1, child2); } }; } ; - #endif /* BBNodeManager_H_ */ diff --git a/src/to-sat/BitBlastNew.cpp b/src/to-sat/BitBlastNew.cpp index 00d944c..851ef40 100644 --- a/src/to-sat/BitBlastNew.cpp +++ b/src/to-sat/BitBlastNew.cpp @@ -10,6 +10,8 @@ #include #include #include "BitBlastNew.h" +#include "AIG/BBNodeManagerAIG.h" +#include "BBNodeManagerASTNode.h" namespace BEEV { @@ -27,7 +29,11 @@ namespace BEEV { * the vector corresponds to bit 0 -- the low-order bit. ********************************************************************/ -BBNodeVec _empty_BBNodeVec; +#define BBNodeVec vector +#define BBNodeVecMap map > +#define BBNodeSet set + +vector _empty_BBNodeAIGVec; // Bit blast a bitvector term. The term must have a kind for a // bitvector term. Result is a ref to a vector of formula nodes @@ -39,7 +45,9 @@ BBNodeVec _empty_BBNodeVec; // that should have already been applied. const bool debug_do_check = false; -void check(const BBNode& x, const ASTNode& n, BBNodeManager* nf) + +template +void check(const BBNode& x, const ASTNode& n, BBNodeManagerT* nf) { if (n.isConstant()) return; @@ -57,8 +65,8 @@ void check(const BBNode& x, const ASTNode& n, BBNodeManager* nf) } - -void check(const BBNodeVec& x, const ASTNode& n, BBNodeManager* nf) +template +void check(BBNodeVec& x, const ASTNode& n, BBNodeManagerT* nf) { if (n.isConstant()) return; @@ -77,8 +85,10 @@ void check(const BBNodeVec& x, const ASTNode& n, BBNodeManager* nf) } -const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) { - BBNodeVecMap::iterator it = BBTermMemo.find(term); + +template +const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) { + typename BBNodeVecMap::iterator it = BBTermMemo.find(term); if (it != BBTermMemo.end()) { // already there. Just return it. return it->second; @@ -197,10 +207,10 @@ const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) { BBNodeVec tmp_res(result_width); - BBNodeVec::const_iterator bb_it = bbarg.begin(); - BBNodeVec::iterator res_it = tmp_res.begin(); - BBNodeVec::iterator res_ext = res_it + arg_width; // first bit of extended part - BBNodeVec::iterator res_end = tmp_res.end(); + typename BBNodeVec::const_iterator bb_it = bbarg.begin(); + typename BBNodeVec::iterator res_it = tmp_res.begin(); + typename BBNodeVec::iterator res_ext = res_it + arg_width; // first bit of extended part + typename BBNodeVec::iterator res_end = tmp_res.end(); // copy LSBs directly from bbvec for (; res_it < res_ext; (res_it++, bb_it++)) { @@ -226,7 +236,7 @@ const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) { const unsigned int high = term[1].GetUnsignedConst(); const unsigned int low = term[2].GetUnsignedConst(); - BBNodeVec::const_iterator bbkfit = bbkids.begin(); + typename BBNodeVec::const_iterator bbkfit = bbkids.begin(); // I should have used pointers to BBNodeVec, to avoid this crock result = BBNodeVec(bbkfit + low, bbkfit + high + 1); @@ -395,8 +405,9 @@ const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) { } // bit blast a formula (boolean term). Result is one bit wide, -const BBNode BitBlasterNew::BBForm(const ASTNode& form, BBNodeSet& support) { - BBNodeMap::iterator it = BBFormMemo.find(form); +template +const BBNode BitBlasterNew::BBForm(const ASTNode& form, BBNodeSet& support) { + typename map::iterator it = BBFormMemo.find(form); if (it != BBFormMemo.end()) { // already there. Just return it. return it->second; @@ -492,7 +503,8 @@ const BBNode BitBlasterNew::BBForm(const ASTNode& form, BBNodeSet& support) { // Bit blast a sum of two equal length BVs. // Update sum vector destructively with new sum. -void BitBlasterNew::BBPlus2(BBNodeVec& sum, const BBNodeVec& y, BBNode cin) { +template +void BitBlasterNew::BBPlus2(BBNodeVec& sum, const BBNodeVec& y, BBNode cin) { const int n = sum.size(); assert(y.size() == (unsigned)n); @@ -505,18 +517,20 @@ void BitBlasterNew::BBPlus2(BBNodeVec& sum, const BBNodeVec& y, BBNode cin) { } // Stores result - x in result, destructively -void BitBlasterNew::BBSub(BBNodeVec& result, const BBNodeVec& y, +template +void BitBlasterNew::BBSub(BBNodeVec& result, const BBNodeVec& y, BBNodeSet& support) { BBNodeVec compsubtrahend = BBNeg(y); BBPlus2(result, compsubtrahend, nf->getTrue()); } // Add one bit -BBNodeVec BitBlasterNew::BBAddOneBit(const BBNodeVec& x, BBNode cin) { +template +BBNodeVec BitBlasterNew::BBAddOneBit(const BBNodeVec& x, BBNode cin) { BBNodeVec result; result.reserve(x.size()); - const BBNodeVec::const_iterator itend = x.end(); - for (BBNodeVec::const_iterator it = x.begin(); it < itend; it++) { + const typename BBNodeVec::const_iterator itend = x.end(); + for (typename BBNodeVec::const_iterator it = x.begin(); it < itend; it++) { BBNode nextcin = nf->CreateNode(AND, *it, cin); result.push_back(nf->CreateNode(XOR, *it, cin)); cin = nextcin; @@ -525,13 +539,15 @@ BBNodeVec BitBlasterNew::BBAddOneBit(const BBNodeVec& x, BBNode cin) { } // Increment bit-blasted vector and return result. -BBNodeVec BitBlasterNew::BBInc(const BBNodeVec& x) { +template +BBNodeVec BitBlasterNew::BBInc(const BBNodeVec& x) { return BBAddOneBit(x, nf->getTrue()); } // Return formula for majority function of three bits. // Pass arguments by reference to reduce refcounting. -BBNode BitBlasterNew::Majority(const BBNode& a, const BBNode& b, +template +BBNode BitBlasterNew::Majority(const BBNode& a, const BBNode& b, const BBNode& c) { // Checking explicitly for constant a, b and c could // be more efficient, because they are repeated in the logic. @@ -557,25 +573,28 @@ BBNode BitBlasterNew::Majority(const BBNode& a, const BBNode& b, } // Bitwise complement -BBNodeVec BitBlasterNew::BBNeg(const BBNodeVec& x) { +template +BBNodeVec BitBlasterNew::BBNeg(const BBNodeVec& x) { BBNodeVec result; result.reserve(x.size()); // Negate each bit. - const BBNodeVec::const_iterator& xend = x.end(); - for (BBNodeVec::const_iterator it = x.begin(); it < xend; it++) { + const typename BBNodeVec::const_iterator& xend = x.end(); + for (typename BBNodeVec::const_iterator it = x.begin(); it < xend; it++) { result.push_back(nf->CreateNode(NOT, *it)); } return result; } // Compute unary minus -BBNodeVec BitBlasterNew::BBUminus(const BBNodeVec& x) { +template +BBNodeVec BitBlasterNew::BBUminus(const BBNodeVec& x) { BBNodeVec xneg = BBNeg(x); return BBInc(xneg); } // AND each bit of vector y with single bit b and return the result. -BBNodeVec BitBlasterNew::BBAndBit(const BBNodeVec& y, BBNode b) { +template +BBNodeVec BitBlasterNew::BBAndBit(const BBNodeVec& y, BBNode b) { if (nf->getTrue() == b) { return y; } @@ -583,8 +602,8 @@ BBNodeVec BitBlasterNew::BBAndBit(const BBNodeVec& y, BBNode b) { BBNodeVec result; result.reserve(y.size()); - const BBNodeVec::const_iterator yend = y.end(); - for (BBNodeVec::const_iterator yit = y.begin(); yit < yend; yit++) { + const typename BBNodeVec::const_iterator yend = y.end(); + for (typename BBNodeVec::const_iterator yit = y.begin(); yit < yend; yit++) { result.push_back(nf->CreateNode(AND, *yit, b)); } return result; @@ -607,7 +626,8 @@ void printP(mult_type* m, int width) } } -void convert(const BBNodeVec& v, BBNodeManager*nf, mult_type* result) +template +void convert(const BBNodeVec& v, BBNodeManagerT*nf, mult_type* result) { const BBNode& BBTrue = nf->getTrue(); const BBNode& BBFalse = nf->getFalse(); @@ -653,7 +673,8 @@ void convert(const BBNodeVec& v, BBNodeManager*nf, mult_type* result) } // Multiply "multiplier" by y[start ... bitWidth]. -void pushP(stack *products, const int start, const BBNodeVec& y, const BBNode& multiplier, BBNodeManager*nf) +template +void pushP(stack *products, const int start, const BBNodeVec& y, const BBNode& multiplier, BBNodeManagerT*nf) { const int bitWidth = y.size(); @@ -668,7 +689,8 @@ void pushP(stack *products, const int start, const BBNodeVec& y, const B const bool debug_multiply = false; -BBNodeVec BitBlasterNew::pairWiseAdd(stack* products, +template +BBNodeVec BitBlasterNew::pairWiseAdd(stack* products, const int bitWidth) { const BBNode& BBFalse = nf->getFalse(); @@ -700,8 +722,9 @@ BBNodeVec BitBlasterNew::pairWiseAdd(stack* products, // Use full adders to create an addition network that adds together each of the // partial products. +template BBNodeVec buildAdditionNetworkResult(stack* products, - const int bitWidth, BBNodeManager* nf) { + const int bitWidth, BBNodeManagerT* nf) { int adderCount = 0; // I experimented with sorting the partial products to put the known values together. @@ -755,7 +778,8 @@ BBNodeVec buildAdditionNetworkResult(stack* products, return result; } -void BitBlasterNew::mult_Booth(const BBNodeVec& x_i, const BBNodeVec& y_i, BBNodeSet& support, const ASTNode& xN, const ASTNode& yN, stack * products) +template +void BitBlasterNew::mult_Booth(const BBNodeVec& x_i, const BBNodeVec& y_i, BBNodeSet& support, const ASTNode& xN, const ASTNode& yN, stack * products) { const int bitWidth = x_i.size(); assert(x_i.size() == y_i.size()); @@ -824,7 +848,8 @@ void BitBlasterNew::mult_Booth(const BBNodeVec& x_i, const BBNodeVec& y_i, BBNod // Uses addition networks explicitly. // I've copied this in from my the "trevor" branch r482. // I've not measured if this is better than the current variant. -void BitBlasterNew::mult_allPairs(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support, stack * products) +template +void BitBlasterNew::mult_allPairs(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support, stack * products) { // Make a table of partial products. const int bitWidth = x.size(); @@ -843,12 +868,12 @@ void BitBlasterNew::mult_allPairs(const BBNodeVec& x, const BBNodeVec& y, BBNode // But it didn't help. } - -BBNodeVec BitBlasterNew::mult_normal(const BBNodeVec& x, +template +BBNodeVec BitBlasterNew::mult_normal(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support) { BBNodeVec ycopy(y); - const BBNodeVec::const_iterator xend = x.end(); - BBNodeVec::const_iterator xit = x.begin(); + const typename BBNodeVec::const_iterator xend = x.end(); + typename BBNodeVec::const_iterator xit = x.begin(); // start prod with first partial product. BBNodeVec prod = BBNodeVec(BBAndBit(y, *xit)); // start loop at next bit. @@ -875,7 +900,8 @@ const bool multiplication_variant2 = false; // multiplication with partial produ const bool multiplication_variant3 = true; // multiplication with booth recoding. // Multiply two bitblasted numbers -BBNodeVec BitBlasterNew::BBMult(const BBNodeVec& x, const BBNodeVec& y, +template +BBNodeVec BitBlasterNew::BBMult(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support, const ASTNode& xN, const ASTNode& yN) { if (multiplication_variant1) { @@ -913,7 +939,8 @@ const bool division_variant_2 = false; // This implements a variant of binary long division. // q and r are "out" parameters. rwidth puts a bound on the // recursion depth. -void BitBlasterNew::BBDivMod(const BBNodeVec &y, const BBNodeVec &x, +template +void BitBlasterNew::BBDivMod(const BBNodeVec &y, const BBNodeVec &x, BBNodeVec &q, BBNodeVec &r, unsigned int rwidth, BBNodeSet& support) { const unsigned int width = y.size(); const BBNodeVec zero = BBfill(width, nf->getFalse()); @@ -1020,7 +1047,8 @@ void BitBlasterNew::BBDivMod(const BBNodeVec &y, const BBNodeVec &x, } // build ITE's (ITE cond then[i] else[i]) for each i. -BBNodeVec BitBlasterNew::BBITE(const BBNode& cond, const BBNodeVec& thn, +template +BBNodeVec BitBlasterNew::BBITE(const BBNode& cond, const BBNodeVec& thn, const BBNodeVec& els) { // Fast exits. if (cond == nf->getTrue()) { @@ -1031,9 +1059,9 @@ BBNodeVec BitBlasterNew::BBITE(const BBNode& cond, const BBNodeVec& thn, BBNodeVec result; result.reserve(els.size()); - const BBNodeVec::const_iterator th_it_end = thn.end(); - BBNodeVec::const_iterator el_it = els.begin(); - for (BBNodeVec::const_iterator th_it = thn.begin(); th_it < th_it_end; th_it++, el_it++) { + const typename BBNodeVec::const_iterator th_it_end = thn.end(); + typename BBNodeVec::const_iterator el_it = els.begin(); + for (typename BBNodeVec::const_iterator th_it = thn.begin(); th_it < th_it_end; th_it++, el_it++) { result.push_back(nf->CreateNode(ITE, cond, *th_it, *el_it)); } return result; @@ -1041,7 +1069,8 @@ BBNodeVec BitBlasterNew::BBITE(const BBNode& cond, const BBNodeVec& thn, // On some cases I suspect this is better than the new variant. -BBNode BBBVLE_variant(const BBNodeVec& left, const BBNodeVec& right, bool is_signed, BBNodeManager* nf) +template +BBNode BBBVLE_variant(const BBNodeVec& left, const BBNodeVec& right, bool is_signed, BBNodeManagerASTNode* nf) { // "thisbit" represents BVLE of the suffixes of the BVs // from that position . if R < L, return TRUE, else if L < R @@ -1049,9 +1078,9 @@ BBNode BBBVLE_variant(const BBNodeVec& left, const BBNodeVec& right, bool is_sig // treated separately, because signed comparison is done by // complementing the MSB of each BV, then doing an unsigned // comparison. - BBNodeVec::const_iterator lit = left.begin(); - BBNodeVec::const_iterator litend = left.end(); - BBNodeVec::const_iterator rit = right.begin(); + typename BBNodeVec::const_iterator lit = left.begin(); + typename BBNodeVec::const_iterator litend = left.end(); + typename BBNodeVec::const_iterator rit = right.begin(); BBNode prevbit = nf->getTrue(); for (; lit < litend - 1; lit++, rit++) { @@ -1077,11 +1106,12 @@ BBNode BBBVLE_variant(const BBNodeVec& left, const BBNodeVec& right, bool is_sig // Workhorse for comparison routines. This does a signed BVLE if is_signed // is true, else it's unsigned. All other comparison operators can be reduced // to this by swapping args or complementing the result bit. -BBNode BitBlasterNew::BBBVLE(const BBNodeVec& left, const BBNodeVec& right, +template +BBNode BitBlasterNew::BBBVLE(const BBNodeVec& left, const BBNodeVec& right, bool is_signed, bool is_bvlt) { - BBNodeVec::const_reverse_iterator lit = left.rbegin(); - const BBNodeVec::const_reverse_iterator litend = left.rend(); - BBNodeVec::const_reverse_iterator rit = right.rbegin(); + typename BBNodeVec::const_reverse_iterator lit = left.rbegin(); + const typename BBNodeVec::const_reverse_iterator litend = left.rend(); + typename BBNodeVec::const_reverse_iterator rit = right.rbegin(); BBNode this_compare_bit = is_signed ? nf->CreateNode(AND, *lit, nf->CreateNode(NOT,*rit)) : nf->CreateNode(AND, @@ -1124,7 +1154,8 @@ BBNode BitBlasterNew::BBBVLE(const BBNodeVec& left, const BBNodeVec& right, // Left shift within fixed field inserting zeros at LSB. // Writes result into first argument. -void BitBlasterNew::BBLShift(BBNodeVec& x, unsigned int shift) { +template +void BitBlasterNew::BBLShift(BBNodeVec& x, unsigned int shift) { // left shift x (destructively) within width. // loop backwards so that copy to self works correctly. (DON'T use STL insert!) for (int i =((int)x.size())-1; i >=0; i--) @@ -1138,10 +1169,11 @@ void BitBlasterNew::BBLShift(BBNodeVec& x, unsigned int shift) { // Right shift within fixed field inserting zeros at MSB. // Writes result into first argument. -void BitBlasterNew::BBRShift(BBNodeVec& x, unsigned int shift) { +template +void BitBlasterNew::BBRShift(BBNodeVec& x, unsigned int shift) { // right shift x (destructively) within width. - const BBNodeVec::iterator xend = x.end(); - BBNodeVec::iterator xit = x.begin(); + const typename BBNodeVec::iterator xend = x.end(); + typename BBNodeVec::iterator xit = x.begin(); for (; xit < xend; xit++) { if (xit + shift < xend) *xit = *(xit + shift); @@ -1151,7 +1183,8 @@ void BitBlasterNew::BBRShift(BBNodeVec& x, unsigned int shift) { } // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. -BBNode BitBlasterNew::BBcompare(const ASTNode& form, BBNodeSet& support) { +template +BBNode BitBlasterNew::BBcompare(const ASTNode& form, BBNodeSet& support) { const BBNodeVec& left = BBTerm(form[0], support); const BBNodeVec& right = BBTerm(form[1], support); @@ -1196,17 +1229,19 @@ BBNode BitBlasterNew::BBcompare(const ASTNode& form, BBNodeSet& support) { } // return a vector with n copies of fillval -BBNodeVec BitBlasterNew::BBfill(unsigned int width, BBNode fillval) { +template +BBNodeVec BitBlasterNew::BBfill(unsigned int width, BBNode fillval) { BBNodeVec zvec(width, fillval); return zvec; } -BBNode BitBlasterNew::BBEQ(const BBNodeVec& left, const BBNodeVec& right) { +template +BBNode BitBlasterNew::BBEQ(const BBNodeVec& left, const BBNodeVec& right) { BBNodeVec andvec; andvec.reserve(left.size()); - BBNodeVec::const_iterator lit = left.begin(); - const BBNodeVec::const_iterator litend = left.end(); - BBNodeVec::const_iterator rit = right.begin(); + typename BBNodeVec::const_iterator lit = left.begin(); + const typename BBNodeVec::const_iterator litend = left.end(); + typename BBNodeVec::const_iterator rit = right.begin(); if (left.size() > 1) { for (; lit != litend; lit++, rit++) { @@ -1224,4 +1259,13 @@ BBNode BitBlasterNew::BBEQ(const BBNodeVec& left, const BBNodeVec& right) { return nf->CreateNode(IFF, *lit, *rit); } +// This creates all the specialisations of the class that are ever needed. +template class BitBlasterNew; +template class BitBlasterNew; + +#undef BBNodeVec +#undef BBNodeVecMap +#undef BBNodeSet + + } // BEEV namespace diff --git a/src/to-sat/BitBlastNew.h b/src/to-sat/BitBlastNew.h index 8850e19..2059218 100644 --- a/src/to-sat/BitBlastNew.h +++ b/src/to-sat/BitBlastNew.h @@ -12,22 +12,28 @@ #include #include -#include "BBNodeManager.h" +#include +#include "../STPManager/STPManager.h" namespace BEEV { -class BitBlasterNew; -class BitBlasterNew { +class ASTNode; +typedef std::vector ASTVec; + +template class BitBlasterNew; +template +class BitBlasterNew { +private: // Memo table for bit blasted terms. If a node has already been // bitblasted, it is mapped to a vector of Boolean formulas for // the - BBNodeVecMap BBTermMemo; + std::map > BBTermMemo; // Memo table for bit blasted formulas. If a node has already // been bitblasted, it is mapped to a node representing the // bitblasted equivalent - BBNodeMap BBFormMemo; + map BBFormMemo; /**************************************************************** * Private Member Functions * @@ -35,76 +41,78 @@ class BitBlasterNew { // Get vector of Boolean formulas for sum of two // vectors of Boolean formulas - void BBPlus2(BBNodeVec& sum, const BBNodeVec& y, BBNode cin); + void BBPlus2(vector& sum, const vector& y, BBNode cin); // Increment - BBNodeVec BBInc(const BBNodeVec& x); + vector BBInc(const vector& x); // Add one bit to a vector of bits. - BBNodeVec BBAddOneBit(const BBNodeVec& x, BBNode cin); + vector BBAddOneBit(const vector& x, BBNode cin); // Bitwise complement - BBNodeVec BBNeg(const BBNodeVec& x); + vector BBNeg(const vector& x); // Unary minus - BBNodeVec BBUminus(const BBNodeVec& x); + vector BBUminus(const vector& x); // Multiply. - BBNodeVec BBMult(const BBNodeVec& x, const BBNodeVec& y, - BBNodeSet& support, const ASTNode& xN, const ASTNode& yN); - void mult_allPairs(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support, stack * products); - void mult_Booth(const BBNodeVec& x_i, const BBNodeVec& y_i, BBNodeSet& support, const BEEV::ASTNode& xN, const BEEV::ASTNode& yN, stack * products); - BBNodeVec mult_normal(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support); + vector BBMult(const vector& x, const vector& y, + set& support, const ASTNode& xN, const ASTNode& yN); + void mult_allPairs(const vector& x, const vector& y, set& support, stack * products); + void mult_Booth(const vector& x_i, const vector& y_i, set& support, const BEEV::ASTNode& xN, const BEEV::ASTNode& yN, stack * products); + vector mult_normal(const vector& x, const vector& y, set& support); - BBNodeVec pairWiseAdd(stack* products, + vector pairWiseAdd(stack* products, const int bitWidth); - BBNodeVec BBAndBit(const BBNodeVec& y, BBNode b); + vector BBAndBit(const vector& y, BBNode b); // AND each bit of vector y with single bit b and return the result. // (used in BBMult) - //BBNodeVec BBAndBit(const BBNodeVec& y, ASTNode b); + //vector BBAndBit(const vector& y, ASTNode b); - // Returns BBNodeVec for result - y. This destroys "result". - void BBSub(BBNodeVec& result, const BBNodeVec& y, BBNodeSet& support); + // Returns vector for result - y. This destroys "result". + void BBSub(vector& result, const vector& y, set& support); // build ITE's (ITE cond then[i] else[i]) for each i. - BBNodeVec BBITE(const BBNode& cond, const BBNodeVec& thn, - const BBNodeVec& els); + vector BBITE(const BBNode& cond, const vector& thn, + const vector& els); // Build a vector of zeros. - BBNodeVec BBfill(unsigned int width, BBNode fillval); + vector BBfill(unsigned int width, BBNode fillval); // build an EQ formula - BBNode BBEQ(const BBNodeVec& left, const BBNodeVec& right); + BBNode BBEQ(const vector& left, const vector& right); // This implements a variant of binary long division. // q and r are "out" parameters. rwidth puts a bound on the // recursion depth. Unsigned only, for now. - void BBDivMod(const BBNodeVec &y, const BBNodeVec &x, BBNodeVec &q, - BBNodeVec &r, unsigned int rwidth, BBNodeSet& support); +public: + void BBDivMod(const vector &y, const vector &x, vector &q, + vector &r, unsigned int rwidth, set& support); // Return formula for majority function of three formulas. BBNode Majority(const BBNode& a, const BBNode& b, const BBNode& c); // Internal bit blasting routines. - BBNode BBBVLE(const BBNodeVec& x, const BBNodeVec& y, bool is_signed, + BBNode BBBVLE(const vector& x, const vector& y, bool is_signed, bool is_bvlt = false); // Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. - BBNode BBcompare(const ASTNode& form, BBNodeSet& support); + BBNode BBcompare(const ASTNode& form, set& support); - void BBLShift(BBNodeVec& x, unsigned int shift); - void BBRShift(BBNodeVec& x, unsigned int shift); + void BBLShift(vector& x, unsigned int shift); + void BBRShift(vector& x, unsigned int shift); - BBNodeManager* nf; +public: + BBNodeManagerT* nf; // Bit blast a bitvector term. The term must have a kind for a // bitvector term. Result is a ref to a vector of formula nodes // representing the boolean formula. - const BBNodeVec BBTerm(const ASTNode& term, BBNodeSet& support); + const vector BBTerm(const ASTNode& term, set& support); public: @@ -114,7 +122,7 @@ public: BitBlasterNew(STPMgr * bm) { - nf = new BBNodeManager(bm); + nf = new BBNodeManagerT(bm); } ~BitBlasterNew() { @@ -124,7 +132,7 @@ public: } //Bitblast a formula - const BBNode BBForm(const ASTNode& form, BBNodeSet& support); + const BBNode BBForm(const ASTNode& form, set& support); }; //end of class BitBlaster } diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index c150636..288069c 100644 --- a/src/to-sat/ToSAT.cpp +++ b/src/to-sat/ToSAT.cpp @@ -7,11 +7,11 @@ * LICENSE: Please view LICENSE file in the home dir of this Program ********************************************************************/ #include "ToSAT.h" -#include "ToSAT.h" #include "BitBlastNew.h" #include "../printer/printers.h" #include #include +#include "BBNodeManagerASTNode.h" namespace BEEV { @@ -345,8 +345,8 @@ namespace BEEV ASTNode BBFormula; { - BitBlasterNew BB(bm); - BBNodeSet set; + BitBlasterNew BB(bm); + set set; BBFormula = BB.BBForm(input,set); assert(set.size() == 0); // doesn't yet work. } @@ -409,53 +409,7 @@ namespace BEEV * Helper Functions *******************************************************************/ - //This function prints the output of the STP solver - void ToSAT::PrintOutput(SOLVER_RETURN_TYPE ret) - { - bool true_iff_valid = (SOLVER_VALID == ret); - - if (bm->UserFlags.print_output_flag) - { - if (bm->UserFlags.smtlib1_parser_flag || bm->UserFlags.smtlib2_parser_flag) - { - if (true_iff_valid && - (input_status == TO_BE_SATISFIABLE)) - { - cerr << "Warning. Expected satisfiable,"\ - " FOUND unsatisfiable" << endl; - } - else if (!true_iff_valid && - (input_status == TO_BE_UNSATISFIABLE)) - { - cerr << "Warning. Expected unsatisfiable,"\ - " FOUND satisfiable" << endl; - } - } - } - if (true_iff_valid) - { - bm->ValidFlag = true; - if (bm->UserFlags.print_output_flag) - { - if (bm->UserFlags.smtlib1_parser_flag || bm->UserFlags.smtlib2_parser_flag) - cout << "unsat\n"; - else - cout << "Valid.\n"; - } - } - else - { - bm->ValidFlag = false; - if (bm->UserFlags.print_output_flag) - { - if (bm->UserFlags.smtlib1_parser_flag || bm->UserFlags.smtlib2_parser_flag) - cout << "sat\n"; - else - cout << "Invalid.\n"; - } - } - } //end of PrintOutput() #if 0 diff --git a/src/to-sat/ToSAT.h b/src/to-sat/ToSAT.h index 53d860b..a66858a 100644 --- a/src/to-sat/ToSAT.h +++ b/src/to-sat/ToSAT.h @@ -9,27 +9,18 @@ #ifndef TOSAT_H #define TOSAT_H -#include #include "ToCNF.h" #include "../AST/AST.h" #include "../sat/sat.h" -#include "../AST/RunTimes.h" -#include "../simplifier/bvsolver.h" #include "../STPManager/STPManager.h" -#include "../simplifier/simplifier.h" +#include "ToSATBase.h" namespace BEEV { - class ToSAT { - - public: - typedef HASHMAP< - ASTNode, - vector, - ASTNode::ASTNodeHasher, - ASTNode::ASTNodeEqual> ASTNodeToVar; + class ToSAT :public ToSATBase + { private: /**************************************************************** @@ -56,22 +47,9 @@ namespace BEEV // it to a model over ASTNode variables. ASTNodeToVar SATVar_to_SymbolIndex; - // Ptr to STPManager - STPMgr * bm; int CNFFileNameCounter; int benchFileNameCounter; -#if 0 - // Memo table to check the functioning of bitblaster and CNF - // converter - ASTNodeMap CheckBBandCNFMemo; - - // Map from formulas to representative literals, for debugging. - ASTNodeMap RepLitMap; -#endif - - ASTNode ASTTrue, ASTFalse, ASTUndefined; - /**************************************************************** * Private Member Functions * ****************************************************************/ @@ -81,18 +59,6 @@ namespace BEEV MINISAT::Var LookupOrCreateSATVar(MINISAT::Solver& S, const ASTNode& n); -#if 0 - // Evaluates bitblasted formula in satisfying assignment - ASTNode CheckBBandCNF(MINISAT::Solver& newS, ASTNode form); - ASTNode CheckBBandCNF_int(MINISAT::Solver& newS, ASTNode form); - - - // Looks up truth value of ASTNode SYMBOL in MINISAT satisfying - // assignment. Returns ASTTrue if true, ASTFalse if false or - // undefined. - - ASTNode SymbolTruthValue(MINISAT::Solver &newS, ASTNode form); -#endif //Iteratively goes through the Clause Buckets, and calls //toSATandSolve() @@ -106,7 +72,6 @@ namespace BEEV ClauseList& cll, bool final, CNFMgr*& cm, - bool add_xor_clauses=false, bool enable_clausal_abstraction=false); @@ -118,26 +83,17 @@ namespace BEEV // Constructor ToSAT(STPMgr * bm) : - bm(bm) -#if 0 - ,CheckBBandCNFMemo() -#endif + ToSATBase(bm) { - ASTTrue = bm->CreateNode(TRUE); - ASTFalse = bm->CreateNode(FALSE); - ASTUndefined = bm->CreateNode(UNDEFINED); CNFFileNameCounter = 0; benchFileNameCounter = 0; } // Bitblasts, CNF conversion and calls toSATandSolve() - bool CallSAT(MINISAT::Solver& SatSolver, + bool CallSAT(MINISAT::Solver& SatSolver, const ASTNode& input); - //print the STP solver output - void PrintOutput(SOLVER_RETURN_TYPE ret); - ASTNodeToVar& SATVar_to_SymbolIndexMap() { return SATVar_to_SymbolIndex; @@ -149,13 +105,10 @@ namespace BEEV SATVar_to_SymbolIndex.clear(); } + ~ToSAT() { ClearAllTables(); -#if 0 - RepLitMap.clear(); - CheckBBandCNFMemo.clear(); -#endif } }; //end of class ToSAT }; //end of namespace diff --git a/src/to-sat/ToSATBase.cpp b/src/to-sat/ToSATBase.cpp new file mode 100644 index 0000000..2af353b --- /dev/null +++ b/src/to-sat/ToSATBase.cpp @@ -0,0 +1,54 @@ +#include "ToSATBase.h" + +namespace BEEV +{ + + //This function prints the output of the STP solver + void ToSATBase::PrintOutput(SOLVER_RETURN_TYPE ret) + { + bool true_iff_valid = (SOLVER_VALID == ret); + + if (bm->UserFlags.print_output_flag) + { + if (bm->UserFlags.smtlib1_parser_flag || bm->UserFlags.smtlib2_parser_flag) + { + if (true_iff_valid && + (input_status == TO_BE_SATISFIABLE)) + { + cerr << "Warning. Expected satisfiable,"\ + " FOUND unsatisfiable" << endl; + } + else if (!true_iff_valid && + (input_status == TO_BE_UNSATISFIABLE)) + { + cerr << "Warning. Expected unsatisfiable,"\ + " FOUND satisfiable" << endl; + } + } + } + + if (true_iff_valid) + { + bm->ValidFlag = true; + if (bm->UserFlags.print_output_flag) + { + if (bm->UserFlags.smtlib1_parser_flag || bm->UserFlags.smtlib2_parser_flag) + cout << "unsat\n"; + else + cout << "Valid.\n"; + } + } + else + { + bm->ValidFlag = false; + if (bm->UserFlags.print_output_flag) + { + if (bm->UserFlags.smtlib1_parser_flag || bm->UserFlags.smtlib2_parser_flag) + cout << "sat\n"; + else + cout << "Invalid.\n"; + } + } + } //end of PrintOutput() + +} diff --git a/src/to-sat/ToSATBase.h b/src/to-sat/ToSATBase.h new file mode 100644 index 0000000..97292ff --- /dev/null +++ b/src/to-sat/ToSATBase.h @@ -0,0 +1,49 @@ +#ifndef TOSATBASE_H +#define TOSATBASE_H + +#include "../AST/AST.h" +#include "../STPManager/STPManager.h" + +namespace BEEV +{ + class ToSATBase + { + protected: + ASTNode ASTTrue, ASTFalse, ASTUndefined; + + // Ptr to STPManager + STPMgr * bm; + + public: + + typedef HASHMAP< + ASTNode, + vector, + ASTNode::ASTNodeHasher, + ASTNode::ASTNodeEqual> ASTNodeToVar; + + // Constructor + ToSATBase(STPMgr * bm) : + bm(bm) + { + ASTTrue = bm->CreateNode(TRUE); + ASTFalse = bm->CreateNode(FALSE); + ASTUndefined = bm->CreateNode(UNDEFINED); + } + + virtual ~ToSATBase() + {} + + //print the STP solver output + void PrintOutput(SOLVER_RETURN_TYPE ret); + + // Bitblasts, CNF conversion and calls toSATandSolve() + virtual bool CallSAT(MINISAT::Solver& SatSolver, const ASTNode& input) =0; + + virtual ASTNodeToVar& SATVar_to_SymbolIndexMap()= 0; + + virtual void ClearAllTables(void) =0; + }; +} + +#endif -- 2.47.3