STPMgr* ASTNode::GetSTPMgr() const
{
- return GlobalSTP->bm;
+ return ParserBM;
} //End of GetSTPMgr()
// Checks if the node has alreadybeen printed or not
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
--- /dev/null
+// -*- 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
--- /dev/null
+// -*- 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<BBNodeAIG> _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<ASTNode, vector<BBNodeAIG> > 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<BBNodeAIG>& children)
+ {
+ deque<Aig_Obj_t*> 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<BBNodeAIG> &b = it->second;
+ if (nodeToVar.find(n) == nodeToVar.end())
+ {
+ const int width = (n.GetType() == BOOLEAN_TYPE) ? 1: n.GetValueWidth();
+ vector<unsigned> v(width, ~((unsigned) 0));
+ nodeToVar.insert(make_pair(n, v));
+ }
+
+ vector<unsigned>& 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<BBNodeAIG> (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<BBNodeAIG>& 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<BBNodeAIG> & back_children = _empty_BBNodeAIGVec)
+ {
+ vector<BBNodeAIG> 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<BBNodeAIG> & back_children = _empty_BBNodeAIGVec)
+ {
+ vector<BBNodeAIG> 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<BBNodeAIG> & back_children =
+ _empty_BBNodeAIGVec)
+ {
+ vector<BBNodeAIG> 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_ */
--- /dev/null
+// -*- 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 <cmath>
+
+#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<BBNodeAIG, BBNodeManagerAIG> bb(bm);
+ BitBlasterNew<BBNodeAIG, BBNodeManagerAIG>::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
+++ /dev/null
-#ifndef BBNODE_H_
-#define BBNODE_H_
-
-#include "../AST/AST.h"
-
-namespace BEEV {
-typedef ASTNode BBNode;
-
-typedef vector<BBNode> BBNodeVec;
-typedef vector<vector<BBNode> > BBNodeVecVec;
-typedef map<ASTNode, BBNode> BBNodeMap;
-typedef map<ASTNode, BBNodeVec> BBNodeVecMap;
-typedef set<BBNode> BBNodeSet;
-}
-;
-
-#endif
#ifndef BBNodeManager_H_
#define BBNodeManager_H_
-#include "BBNode.h"
#include "../STPManager/STPManager.h"
namespace BEEV {
class ASTNode;
typedef std::vector<ASTNode> 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;
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<ASTNode>& 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_ */
#include <cmath>
#include <cassert>
#include "BitBlastNew.h"
+#include "AIG/BBNodeManagerAIG.h"
+#include "BBNodeManagerASTNode.h"
namespace BEEV {
* the vector corresponds to bit 0 -- the low-order bit.
********************************************************************/
-BBNodeVec _empty_BBNodeVec;
+#define BBNodeVec vector<BBNode>
+#define BBNodeVecMap map<ASTNode, vector<BBNode> >
+#define BBNodeSet set<BBNode>
+
+vector<BBNodeAIG> _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
// that should have already been applied.
const bool debug_do_check = false;
-void check(const BBNode& x, const ASTNode& n, BBNodeManager* nf)
+
+template <class BBNode, class BBNodeManagerT>
+void check(const BBNode& x, const ASTNode& n, BBNodeManagerT* nf)
{
if (n.isConstant())
return;
}
-
-void check(const BBNodeVec& x, const ASTNode& n, BBNodeManager* nf)
+template <class BBNode, class BBNodeManagerT>
+void check(BBNodeVec& x, const ASTNode& n, BBNodeManagerT* nf)
{
if (n.isConstant())
return;
}
-const BBNodeVec BitBlasterNew::BBTerm(const ASTNode& term, BBNodeSet& support) {
- BBNodeVecMap::iterator it = BBTermMemo.find(term);
+
+template <class BBNode, class BBNodeManagerT>
+const BBNodeVec BitBlasterNew<BBNode,BBNodeManagerT>::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;
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++)) {
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);
}
// 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 <class BBNode, class BBNodeManagerT>
+const BBNode BitBlasterNew<BBNode,BBNodeManagerT>::BBForm(const ASTNode& form, BBNodeSet& support) {
+ typename map<ASTNode,BBNode>::iterator it = BBFormMemo.find(form);
if (it != BBFormMemo.end()) {
// already there. Just return it.
return it->second;
// 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 <class BBNode, class BBNodeManagerT>
+void BitBlasterNew<BBNode,BBNodeManagerT>::BBPlus2(BBNodeVec& sum, const BBNodeVec& y, BBNode cin) {
const int n = sum.size();
assert(y.size() == (unsigned)n);
}
// Stores result - x in result, destructively
-void BitBlasterNew::BBSub(BBNodeVec& result, const BBNodeVec& y,
+template <class BBNode, class BBNodeManagerT>
+void BitBlasterNew<BBNode,BBNodeManagerT>::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 <class BBNode, class BBNodeManagerT>
+BBNodeVec BitBlasterNew<BBNode,BBNodeManagerT>::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;
}
// Increment bit-blasted vector and return result.
-BBNodeVec BitBlasterNew::BBInc(const BBNodeVec& x) {
+template <class BBNode, class BBNodeManagerT>
+BBNodeVec BitBlasterNew<BBNode,BBNodeManagerT>::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 <class BBNode, class BBNodeManagerT>
+BBNode BitBlasterNew<BBNode,BBNodeManagerT>::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.
}
// Bitwise complement
-BBNodeVec BitBlasterNew::BBNeg(const BBNodeVec& x) {
+template <class BBNode, class BBNodeManagerT>
+BBNodeVec BitBlasterNew<BBNode,BBNodeManagerT>::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 <class BBNode, class BBNodeManagerT>
+BBNodeVec BitBlasterNew<BBNode,BBNodeManagerT>::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 <class BBNode, class BBNodeManagerT>
+BBNodeVec BitBlasterNew<BBNode,BBNodeManagerT>::BBAndBit(const BBNodeVec& y, BBNode b) {
if (nf->getTrue() == b) {
return y;
}
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;
}
}
-void convert(const BBNodeVec& v, BBNodeManager*nf, mult_type* result)
+template <class BBNode, class BBNodeManagerT>
+void convert(const BBNodeVec& v, BBNodeManagerT*nf, mult_type* result)
{
const BBNode& BBTrue = nf->getTrue();
const BBNode& BBFalse = nf->getFalse();
}
// Multiply "multiplier" by y[start ... bitWidth].
-void pushP(stack<BBNode> *products, const int start, const BBNodeVec& y, const BBNode& multiplier, BBNodeManager*nf)
+template <class BBNode, class BBNodeManagerT>
+void pushP(stack<BBNode> *products, const int start, const BBNodeVec& y, const BBNode& multiplier, BBNodeManagerT*nf)
{
const int bitWidth = y.size();
const bool debug_multiply = false;
-BBNodeVec BitBlasterNew::pairWiseAdd(stack<BBNode>* products,
+template <class BBNode, class BBNodeManagerT>
+BBNodeVec BitBlasterNew<BBNode,BBNodeManagerT>::pairWiseAdd(stack<BBNode>* products,
const int bitWidth)
{
const BBNode& BBFalse = nf->getFalse();
// Use full adders to create an addition network that adds together each of the
// partial products.
+template <class BBNode, class BBNodeManagerT>
BBNodeVec buildAdditionNetworkResult(stack<BBNode>* 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.
return result;
}
-void BitBlasterNew::mult_Booth(const BBNodeVec& x_i, const BBNodeVec& y_i, BBNodeSet& support, const ASTNode& xN, const ASTNode& yN, stack<BBNode> * products)
+template <class BBNode, class BBNodeManagerT>
+void BitBlasterNew<BBNode,BBNodeManagerT>::mult_Booth(const BBNodeVec& x_i, const BBNodeVec& y_i, BBNodeSet& support, const ASTNode& xN, const ASTNode& yN, stack<BBNode> * products)
{
const int bitWidth = x_i.size();
assert(x_i.size() == y_i.size());
// 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<BBNode> * products)
+template <class BBNode, class BBNodeManagerT>
+void BitBlasterNew<BBNode,BBNodeManagerT>::mult_allPairs(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support, stack<BBNode> * products)
{
// Make a table of partial products.
const int bitWidth = x.size();
// But it didn't help.
}
-
-BBNodeVec BitBlasterNew::mult_normal(const BBNodeVec& x,
+template <class BBNode, class BBNodeManagerT>
+BBNodeVec BitBlasterNew<BBNode,BBNodeManagerT>::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.
const bool multiplication_variant3 = true; // multiplication with booth recoding.
// Multiply two bitblasted numbers
-BBNodeVec BitBlasterNew::BBMult(const BBNodeVec& x, const BBNodeVec& y,
+template <class BBNode, class BBNodeManagerT>
+BBNodeVec BitBlasterNew<BBNode,BBNodeManagerT>::BBMult(const BBNodeVec& x, const BBNodeVec& y,
BBNodeSet& support, const ASTNode& xN, const ASTNode& yN) {
if (multiplication_variant1) {
// 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 <class BBNode, class BBNodeManagerT>
+void BitBlasterNew<BBNode,BBNodeManagerT>::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());
}
// build ITE's (ITE cond then[i] else[i]) for each i.
-BBNodeVec BitBlasterNew::BBITE(const BBNode& cond, const BBNodeVec& thn,
+template <class BBNode, class BBNodeManagerT>
+BBNodeVec BitBlasterNew<BBNode,BBNodeManagerT>::BBITE(const BBNode& cond, const BBNodeVec& thn,
const BBNodeVec& els) {
// Fast exits.
if (cond == nf->getTrue()) {
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;
// 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 <class BBNode, class BBNodeManagerT>
+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
// 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++)
{
// 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 <class BBNode, class BBNodeManagerT>
+BBNode BitBlasterNew<BBNode,BBNodeManagerT>::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,
// Left shift within fixed field inserting zeros at LSB.
// Writes result into first argument.
-void BitBlasterNew::BBLShift(BBNodeVec& x, unsigned int shift) {
+template <class BBNode, class BBNodeManagerT>
+void BitBlasterNew<BBNode,BBNodeManagerT>::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--)
// Right shift within fixed field inserting zeros at MSB.
// Writes result into first argument.
-void BitBlasterNew::BBRShift(BBNodeVec& x, unsigned int shift) {
+template <class BBNode, class BBNodeManagerT>
+void BitBlasterNew<BBNode,BBNodeManagerT>::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);
}
// Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc.
-BBNode BitBlasterNew::BBcompare(const ASTNode& form, BBNodeSet& support) {
+template <class BBNode, class BBNodeManagerT>
+BBNode BitBlasterNew<BBNode,BBNodeManagerT>::BBcompare(const ASTNode& form, BBNodeSet& support) {
const BBNodeVec& left = BBTerm(form[0], support);
const BBNodeVec& right = BBTerm(form[1], support);
}
// return a vector with n copies of fillval
-BBNodeVec BitBlasterNew::BBfill(unsigned int width, BBNode fillval) {
+template <class BBNode, class BBNodeManagerT>
+BBNodeVec BitBlasterNew<BBNode,BBNodeManagerT>::BBfill(unsigned int width, BBNode fillval) {
BBNodeVec zvec(width, fillval);
return zvec;
}
-BBNode BitBlasterNew::BBEQ(const BBNodeVec& left, const BBNodeVec& right) {
+template <class BBNode, class BBNodeManagerT>
+BBNode BitBlasterNew<BBNode,BBNodeManagerT>::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++) {
return nf->CreateNode(IFF, *lit, *rit);
}
+// This creates all the specialisations of the class that are ever needed.
+template class BitBlasterNew<ASTNode, BBNodeManagerASTNode>;
+template class BitBlasterNew<BBNodeAIG, BBNodeManagerAIG>;
+
+#undef BBNodeVec
+#undef BBNodeVecMap
+#undef BBNodeSet
+
+
} // BEEV namespace
#include <cmath>
#include <cassert>
-#include "BBNodeManager.h"
+#include <map>
+#include "../STPManager/STPManager.h"
namespace BEEV {
-class BitBlasterNew;
-class BitBlasterNew {
+class ASTNode;
+typedef std::vector<ASTNode> ASTVec;
+
+template <class BBNode, class BBNodeManagerT> class BitBlasterNew;
+template <class BBNode, class BBNodeManagerT>
+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<ASTNode, vector<BBNode> > 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<ASTNode, BBNode> BBFormMemo;
/****************************************************************
* Private Member Functions *
// 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<BBNode>& sum, const vector<BBNode>& y, BBNode cin);
// Increment
- BBNodeVec BBInc(const BBNodeVec& x);
+ vector<BBNode> BBInc(const vector<BBNode>& x);
// Add one bit to a vector of bits.
- BBNodeVec BBAddOneBit(const BBNodeVec& x, BBNode cin);
+ vector<BBNode> BBAddOneBit(const vector<BBNode>& x, BBNode cin);
// Bitwise complement
- BBNodeVec BBNeg(const BBNodeVec& x);
+ vector<BBNode> BBNeg(const vector<BBNode>& x);
// Unary minus
- BBNodeVec BBUminus(const BBNodeVec& x);
+ vector<BBNode> BBUminus(const vector<BBNode>& 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<BBNode> * products);
- void mult_Booth(const BBNodeVec& x_i, const BBNodeVec& y_i, BBNodeSet& support, const BEEV::ASTNode& xN, const BEEV::ASTNode& yN, stack<BBNode> * products);
- BBNodeVec mult_normal(const BBNodeVec& x, const BBNodeVec& y, BBNodeSet& support);
+ vector<BBNode> BBMult(const vector<BBNode>& x, const vector<BBNode>& y,
+ set<BBNode>& support, const ASTNode& xN, const ASTNode& yN);
+ void mult_allPairs(const vector<BBNode>& x, const vector<BBNode>& y, set<BBNode>& support, stack<BBNode> * products);
+ void mult_Booth(const vector<BBNode>& x_i, const vector<BBNode>& y_i, set<BBNode>& support, const BEEV::ASTNode& xN, const BEEV::ASTNode& yN, stack<BBNode> * products);
+ vector<BBNode> mult_normal(const vector<BBNode>& x, const vector<BBNode>& y, set<BBNode>& support);
- BBNodeVec pairWiseAdd(stack<BBNode>* products,
+ vector<BBNode> pairWiseAdd(stack<BBNode>* products,
const int bitWidth);
- BBNodeVec BBAndBit(const BBNodeVec& y, BBNode b);
+ vector<BBNode> BBAndBit(const vector<BBNode>& 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<BBNode> BBAndBit(const vector<BBNode>& y, ASTNode b);
- // Returns BBNodeVec for result - y. This destroys "result".
- void BBSub(BBNodeVec& result, const BBNodeVec& y, BBNodeSet& support);
+ // Returns vector<BBNode> for result - y. This destroys "result".
+ void BBSub(vector<BBNode>& result, const vector<BBNode>& y, set<BBNode>& 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<BBNode> BBITE(const BBNode& cond, const vector<BBNode>& thn,
+ const vector<BBNode>& els);
// Build a vector of zeros.
- BBNodeVec BBfill(unsigned int width, BBNode fillval);
+ vector<BBNode> BBfill(unsigned int width, BBNode fillval);
// build an EQ formula
- BBNode BBEQ(const BBNodeVec& left, const BBNodeVec& right);
+ BBNode BBEQ(const vector<BBNode>& left, const vector<BBNode>& 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<BBNode> &y, const vector<BBNode> &x, vector<BBNode> &q,
+ vector<BBNode> &r, unsigned int rwidth, set<BBNode>& 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<BBNode>& x, const vector<BBNode>& 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<BBNode>& support);
- void BBLShift(BBNodeVec& x, unsigned int shift);
- void BBRShift(BBNodeVec& x, unsigned int shift);
+ void BBLShift(vector<BBNode>& x, unsigned int shift);
+ void BBRShift(vector<BBNode>& 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<BBNode> BBTerm(const ASTNode& term, set<BBNode>& support);
public:
BitBlasterNew(STPMgr * bm)
{
- nf = new BBNodeManager(bm);
+ nf = new BBNodeManagerT(bm);
}
~BitBlasterNew() {
}
//Bitblast a formula
- const BBNode BBForm(const ASTNode& form, BBNodeSet& support);
+ const BBNode BBForm(const ASTNode& form, set<BBNode>& support);
}; //end of class BitBlaster
}
* 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 <iostream>
#include <fstream>
+#include "BBNodeManagerASTNode.h"
namespace BEEV
{
ASTNode BBFormula;
{
- BitBlasterNew BB(bm);
- BBNodeSet set;
+ BitBlasterNew<ASTNode,BBNodeManagerASTNode> BB(bm);
+ set<ASTNode> set;
BBFormula = BB.BBForm(input,set);
assert(set.size() == 0); // doesn't yet work.
}
* 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
#ifndef TOSAT_H
#define TOSAT_H
-#include <cmath>
#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<unsigned>,
- ASTNode::ASTNodeHasher,
- ASTNode::ASTNodeEqual> ASTNodeToVar;
+ class ToSAT :public ToSATBase
+ {
private:
/****************************************************************
// 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 *
****************************************************************/
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()
ClauseList& cll,
bool final,
CNFMgr*& cm,
-
bool add_xor_clauses=false,
bool enable_clausal_abstraction=false);
// 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;
SATVar_to_SymbolIndex.clear();
}
+
~ToSAT()
{
ClearAllTables();
-#if 0
- RepLitMap.clear();
- CheckBBandCNFMemo.clear();
-#endif
}
}; //end of class ToSAT
}; //end of namespace
--- /dev/null
+#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()
+
+}
--- /dev/null
+#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<unsigned>,
+ 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
projects / francis / stp.git / commitdiff