return (bm.AlreadyPrintedSet.find(*this) != bm.AlreadyPrintedSet.end());
}
+ void ASTNode::nodeprint(ostream& os, bool c_friendly) const
+ {
+ _int_node_ptr->nodeprint(os, c_friendly);
+ }
+
void ASTNode::MarkAlreadyPrinted() const {
// FIXME: Fetching BeevMgr is annoying. Can we put this in lispprinter class?
BeevMgr &bm = GetBeevMgr();
}
} //end of PL_Print1()
-
- // copied from Presentation Langauge printer.
- ostream& ASTNode::SMTLIB_Print(ostream &os, int indentation) const {
- // Clear the PrintMap
- BeevMgr& bm = GetBeevMgr();
- bm.PLPrintNodeSet.clear();
- bm.NodeLetVarMap.clear();
- bm.NodeLetVarVec.clear();
- bm.NodeLetVarMap1.clear();
-
- //pass 1: letize the node
- LetizeNode();
-
- //pass 2:
- //
- //2. print all the let variables and their counterpart expressions
- //2. as follows (LET var1 = expr1, var2 = expr2, ...
- //
- //3. Then print the Node itself, replacing every occurence of
- //3. expr1 with var1, expr2 with var2, ...
- //os << "(";
- if(0 < bm.NodeLetVarMap.size()) {
- //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin();
- //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end();
- std::vector<pair<ASTNode,ASTNode> >::iterator it = bm.NodeLetVarVec.begin();
- std::vector<pair<ASTNode,ASTNode> >::iterator itend = bm.NodeLetVarVec.end();
-
- os << "(LET ";
- //print the let var first
- it->first.SMTLIB_Print1(os,indentation,false);
- os << " = ";
- //print the expr
- it->second.SMTLIB_Print1(os,indentation,false);
-
- //update the second map for proper printing of LET
- bm.NodeLetVarMap1[it->second] = it->first;
-
- for(it++;it!=itend;it++) {
- os << "," << endl;
- //print the let var first
- it->first.SMTLIB_Print1(os,indentation,false);
- os << " = ";
- //print the expr
- it->second.SMTLIB_Print1(os,indentation,false);
-
- //update the second map for proper printing of LET
- bm.NodeLetVarMap1[it->second] = it->first;
- }
-
- os << " IN " << endl;
- SMTLIB_Print1(os,indentation, true);
- os << ") ";
- }
- else
- SMTLIB_Print1(os,indentation, false);
- return os;
- }
-
-
-
-
-
-void ASTNode::SMTLIB_Print1(ostream& os,
- int indentation,
- bool letize) const
-{
- //os << spaces(indentation);
- //os << endl << spaces(indentation);
- if (!IsDefined()) {
- os << "<undefined>";
- return;
- }
-
- //if this node is present in the letvar Map, then print the letvar
- BeevMgr &bm = GetBeevMgr();
-
- //this is to print letvars for shared subterms inside the printing
- //of "(LET v0 = term1, v1=term1@term2,...
- if((bm.NodeLetVarMap1.find(*this) != bm.NodeLetVarMap1.end()) && !letize) {
- (bm.NodeLetVarMap1[*this]).SMTLIB_Print1(os,indentation,letize);
- return;
- }
-
- //this is to print letvars for shared subterms inside the actual
- //term to be printed
- if((bm.NodeLetVarMap.find(*this) != bm.NodeLetVarMap.end()) && letize) {
- (bm.NodeLetVarMap[*this]).SMTLIB_Print1(os,indentation,letize);
- return;
- }
-
- //otherwise print it normally
- Kind kind = GetKind();
- const ASTVec &c = GetChildren();
- switch(kind)
- {
- case BITVECTOR: // Not sure how this is differen to a BVCONST??
- {os << "bv";
- unsigned char * str;
- str = CONSTANTBV::BitVector_to_Dec(c[0].GetBVConst());
- os << str << "[" << c[0].GetValueWidth() << "]";
- CONSTANTBV::BitVector_Dispose(str);
- }
- break;
- case BVCONST:
- {
- os << "bv";
- unsigned char * str;
- str = CONSTANTBV::BitVector_to_Dec(GetBVConst());
- os << str << "[" << GetValueWidth() << "]";
- CONSTANTBV::BitVector_Dispose(str);
- }
- break;
- case SYMBOL:
- _int_node_ptr->nodeprint(os);
- break;
- case FALSE:
- os << "false";
- break;
- case TRUE:
- os << "true";
- break;
- case BVEXTRACT:
- {
- unsigned int upper = GetUnsignedConst(c[1]);
- unsigned int lower = GetUnsignedConst(c[2]);
- assert(upper > lower);
- os << "(extract[" << upper << ":" << lower << "] ";
- c[0].SMTLIB_Print1(os,indentation,letize);
- os << ")";
- }
- default:
- {
- os << "(" << functionToSMTLIBName(kind);
-
- ASTVec::const_iterator iend = c.end();
- for (ASTVec::const_iterator i = c.begin(); i != iend; i++)
- {
- os << " ";
- i->SMTLIB_Print1(os,0,letize);
- }
-
- os << ")";
- }
- }
-}
-
-string ASTNode::functionToSMTLIBName(const Kind k) const
-{
- switch(k)
- {
- case AND:
- case OR:
- case NAND:
- case NOR:
- case XOR:
- case BVAND:
- case BVNEG:
- case ITE:
- case BVOR:
- case NOT:
- return _kind_names[k];
-
- case BVMULT: return "bvmul";
- case WRITE: return "store";
- case EQ: return "=";
- case BVCONCAT: return "concat";
-
- default:
- FatalError(_kind_names[k]);
- }
-}
-
- // printer for C code (copied from PL_Print())
- // TODO: this does not fully implement printing of all of the STP
- // language - FatalError calls inserted for unimplemented
- // functionality, e.g.,:
- // FatalError("C_Print1: printing not implemented for this kind: ",*this);
-
- //two pass algorithm:
- //
- //1. In the first pass, letize this Node, N: i.e. if a node
- //1. appears more than once in N, then record this fact.
- //
- //2. In the second pass print a "global let" and then print N
- //2. as follows: Every occurence of a node occuring more than
- //2. once is replaced with the corresponding let variable.
- ostream& ASTNode::C_Print(ostream &os,
- int indentation) const {
- // Clear the PrintMap
- BeevMgr& bm = GetBeevMgr();
- bm.PLPrintNodeSet.clear();
- bm.NodeLetVarMap.clear();
- bm.NodeLetVarVec.clear();
- bm.NodeLetVarMap1.clear();
-
- //pass 1: letize the node
- LetizeNode();
-
- unsigned int lower, upper, num_bytes = 0;
-
- //pass 2:
- //
- //2. print all the let variables and their counterpart expressions
- //2. as follows (LET var1 = expr1, var2 = expr2, ...
- //
- //3. Then print the Node itself, replacing every occurence of
- //3. expr1 with var1, expr2 with var2, ...
- //os << "(";
- if(0 < bm.NodeLetVarMap.size()) {
- //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin();
- //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end();
- std::vector<pair<ASTNode,ASTNode> >::iterator it = bm.NodeLetVarVec.begin();
- std::vector<pair<ASTNode,ASTNode> >::iterator itend = bm.NodeLetVarVec.end();
-
- // start a new block to create new static scope
- os << "{" << endl;
-
- for(;it!=itend;it++) {
-
- // see if it's a BVEXTRACT, and if so, whether it's multi-byte
- if (it->second.GetKind() == BVEXTRACT) {
- upper = GetUnsignedConst(it->second.GetChildren()[1]);
- lower = GetUnsignedConst(it->second.GetChildren()[2]);
- num_bytes = (upper - lower + 1) / 8;
- assert(num_bytes > 0);
- }
-
- //print the let var first
- if (num_bytes > 1) {
- // for multi-byte assignment, use 'memcpy' and array notation
- os << "unsigned char ";
- it->first.C_Print1(os,indentation,false);
- os << "[" << num_bytes << "]; ";
- os << "memcpy(";
- it->first.C_Print1(os,indentation,false);
- os << ", ";
- //print the expr
- it->second.C_Print1(os,indentation,false);
- os << ", " << num_bytes << ");";
- }
- else {
- // for single-byte assignment, use '='
- os << "unsigned char ";
- it->first.C_Print1(os,indentation,false);
- os << " = ";
- //print the expr
- it->second.C_Print1(os,indentation,false);
- os << ";" << endl;
- }
-
- //update the second map for proper printing of LET
- bm.NodeLetVarMap1[it->second] = it->first;
- }
-
- os << endl << "stp_assert ";
- C_Print1(os,indentation, true);
-
- os << ";" << endl << "}";
- }
- else {
- os << "stp_assert ";
- C_Print1(os,indentation, false);
- os << ";";
- }
- //os << " )";
- //os << " ";
-
- return os;
- } //end of C_Print()
-
- // helper function for printing C code (copied from PL_Print1())
- void ASTNode::C_Print1(ostream& os,
- int indentation,
- bool letize) const {
-
- unsigned int upper, lower, num_bytes;
- Kind LHSkind, RHSkind;
-
- //os << spaces(indentation);
- //os << endl << spaces(indentation);
- if (!IsDefined()) {
- os << "<undefined>";
- return;
- }
-
- //if this node is present in the letvar Map, then print the letvar
- BeevMgr &bm = GetBeevMgr();
-
- //this is to print letvars for shared subterms inside the printing
- //of "(LET v0 = term1, v1=term1@term2,...
- if((bm.NodeLetVarMap1.find(*this) != bm.NodeLetVarMap1.end()) && !letize) {
- (bm.NodeLetVarMap1[*this]).C_Print1(os,indentation,letize);
- return;
- }
-
- //this is to print letvars for shared subterms inside the actual
- //term to be printed
- if((bm.NodeLetVarMap.find(*this) != bm.NodeLetVarMap.end()) && letize) {
- (bm.NodeLetVarMap[*this]).C_Print1(os,indentation,letize);
- return;
- }
-
- //otherwise print it normally
- Kind kind = GetKind();
- const ASTVec &c = GetChildren();
- switch(kind) {
- case BVGETBIT:
- FatalError("C_Print1: printing not implemented for this kind: ",*this);
- c[0].C_Print1(os,indentation,letize);
- os << "{";
- c[1].C_Print1(os,indentation,letize);
- os << "}";
- break;
- case BITVECTOR:
- FatalError("C_Print1: printing not implemented for this kind: ",*this);
- os << "BITVECTOR(";
- unsigned char * str;
- str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst());
- os << str << ")";
- CONSTANTBV::BitVector_Dispose(str);
- break;
- case BOOLEAN:
- FatalError("C_Print1: printing not implemented for this kind: ",*this);
- os << "BOOLEAN";
- break;
- case FALSE:
- os << "0";
- break;
- case TRUE:
- os << "1";
- break;
- case BVCONST:
- case SYMBOL:
- // print in C friendly format:
- _int_node_ptr->nodeprint(os, true);
- break;
- case READ:
- c[0].C_Print1(os, indentation,letize);
- os << "[";
- c[1].C_Print1(os,indentation,letize);
- os << "]";
- break;
- case WRITE:
- os << "(";
- c[0].C_Print1(os,indentation,letize);
- os << " WITH [";
- c[1].C_Print1(os,indentation,letize);
- os << "] := ";
- c[2].C_Print1(os,indentation,letize);
- os << ")";
- os << endl;
- break;
- case BVUMINUS:
- os << kind << "( ";
- c[0].C_Print1(os,indentation,letize);
- os << ")";
- break;
- case NOT:
- os << "!(";
- c[0].C_Print1(os,indentation,letize);
- os << ") " << endl;
- break;
- case BVNEG:
- os << " ~(";
- c[0].C_Print1(os,indentation,letize);
- os << ")";
- break;
- case BVCONCAT:
- FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features
- os << "(";
- c[0].C_Print1(os,indentation,letize);
- os << " @ ";
- c[1].C_Print1(os,indentation,letize);
- os << ")" << endl;
- break;
- case BVOR:
- os << "(";
- c[0].C_Print1(os,indentation,letize);
- os << " | ";
- c[1].C_Print1(os,indentation,letize);
- os << ")";
- break;
- case BVAND:
- os << "(";
- c[0].C_Print1(os,indentation,letize);
- os << " & ";
- c[1].C_Print1(os,indentation,letize);
- os << ")";
- break;
- case BVEXTRACT:
-
- // we only accept indices that are byte-aligned
- // (e.g., [15:8], [23:16])
- // and round down to byte indices rather than bit indices
- upper = GetUnsignedConst(c[1]);
- lower = GetUnsignedConst(c[2]);
- assert(upper > lower);
- assert(lower % 8 == 0);
- assert((upper + 1) % 8 == 0);
- num_bytes = (upper - lower + 1) / 8;
- assert (num_bytes > 0);
-
- // for multi-byte extraction, use the ADDRESS
- if (num_bytes > 1) {
- os << "&";
- c[0].C_Print1(os,indentation,letize);
- os << "[" << lower / 8 << "]";
- }
- // for single-byte extraction, use the VALUE
- else {
- c[0].C_Print1(os,indentation,letize);
- os << "[" << lower / 8 << "]";
- }
-
- break;
- case BVLEFTSHIFT:
- FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features
- os << "(";
- c[0].C_Print1(os,indentation,letize);
- os << " << ";
- os << GetUnsignedConst(c[1]);
- os << ")";
- break;
- case BVRIGHTSHIFT:
- FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features
- os << "(";
- c[0].C_Print1(os,indentation,letize);
- os << " >> ";
- os << GetUnsignedConst(c[1]);
- os << ")";
- break;
- case BVMULT:
- case BVSUB:
- case BVPLUS:
- case SBVDIV:
- case SBVREM:
- case BVDIV:
- case BVMOD:
- os << kind << "(";
- os << this->GetValueWidth();
- for(ASTVec::const_iterator it=c.begin(),itend=c.end();it!=itend;it++) {
- os << ", " << endl;
- it->C_Print1(os,indentation,letize);
- }
- os << ")" << endl;
- break;
- case ITE:
- os << "if (";
- c[0].C_Print1(os,indentation,letize);
- os << ")" << endl;
- os << "{";
- c[1].C_Print1(os,indentation,letize);
- os << endl << "} else {";
- c[2].C_Print1(os,indentation,letize);
- os << endl << "}";
- break;
- case BVLT:
- // convert to UNSIGNED before doing comparison!
- os << "((unsigned char)";
- c[0].C_Print1(os,indentation,letize);
- os << " < ";
- os << "(unsigned char)";
- c[1].C_Print1(os,indentation,letize);
- os << ")";
- break;
- case BVLE:
- // convert to UNSIGNED before doing comparison!
- os << "((unsigned char)";
- c[0].C_Print1(os,indentation,letize);
- os << " <= ";
- os << "(unsigned char)";
- c[1].C_Print1(os,indentation,letize);
- os << ")";
- break;
- case BVGT:
- // convert to UNSIGNED before doing comparison!
- os << "((unsigned char)";
- c[0].C_Print1(os,indentation,letize);
- os << " > ";
- os << "(unsigned char)";
- c[1].C_Print1(os,indentation,letize);
- os << ")";
- break;
- case BVGE:
- // convert to UNSIGNED before doing comparison!
- os << "((unsigned char)";
- c[0].C_Print1(os,indentation,letize);
- os << " >= ";
- os << "(unsigned char)";
- c[1].C_Print1(os,indentation,letize);
- os << ")";
- break;
- case BVXOR:
- case BVNAND:
- case BVNOR:
- case BVXNOR:
- FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features
- break;
- case BVSLT:
- // convert to SIGNED before doing comparison!
- os << "((signed char)";
- c[0].C_Print1(os,indentation,letize);
- os << " < ";
- os << "(signed char)";
- c[1].C_Print1(os,indentation,letize);
- os << ")";
- break;
- case BVSLE:
- // convert to SIGNED before doing comparison!
- os << "((signed char)";
- c[0].C_Print1(os,indentation,letize);
- os << " <= ";
- os << "(signed char)";
- c[1].C_Print1(os,indentation,letize);
- os << ")";
- break;
- case BVSGT:
- // convert to SIGNED before doing comparison!
- os << "((signed char)";
- c[0].C_Print1(os,indentation,letize);
- os << " > ";
- os << "(signed char)";
- c[1].C_Print1(os,indentation,letize);
- os << ")";
- break;
- case BVSGE:
- // convert to SIGNED before doing comparison!
- os << "((signed char)";
- c[0].C_Print1(os,indentation,letize);
- os << " >= ";
- os << "(signed char)";
- c[1].C_Print1(os,indentation,letize);
- os << ")";
- break;
- case EQ:
- // tricky tricky ... if it's a single-byte comparison,
- // simply do ==, but if it's multi-byte, must do memcmp
- LHSkind = c[0].GetKind();
- RHSkind = c[1].GetKind();
-
- num_bytes = 0;
-
- // try to figure out whether it's a single-byte or multi-byte
- // comparison
- if (LHSkind == BVEXTRACT) {
- upper = GetUnsignedConst(c[0].GetChildren()[1]);
- lower = GetUnsignedConst(c[0].GetChildren()[2]);
- num_bytes = (upper - lower + 1) / 8;
- }
- else if (RHSkind == BVEXTRACT) {
- upper = GetUnsignedConst(c[1].GetChildren()[1]);
- lower = GetUnsignedConst(c[1].GetChildren()[2]);
- num_bytes = (upper - lower + 1) / 8;
- }
-
- if (num_bytes > 1) {
- os << "(memcmp(";
- c[0].C_Print1(os,indentation,letize);
- os << ", ";
- c[1].C_Print1(os,indentation,letize);
- os << ", ";
- os << num_bytes;
- os << ") == 0)";
- }
- else if (num_bytes == 1) {
- os << "(";
- c[0].C_Print1(os,indentation,letize);
- os << " == ";
- c[1].C_Print1(os,indentation,letize);
- os << ")";
- }
- else {
- FatalError("C_Print1: ugh problem in implementing ==");
- }
-
- break;
- case NEQ:
- c[0].C_Print1(os,indentation,letize);
- os << " != ";
- c[1].C_Print1(os,indentation,letize);
- os << endl;
- break;
- case AND:
- case OR:
- case NAND:
- case NOR:
- case XOR: {
- os << "(";
- c[0].C_Print1(os,indentation,letize);
- ASTVec::const_iterator it=c.begin();
- ASTVec::const_iterator itend=c.end();
-
- it++;
- for(;it!=itend;it++) {
- switch (kind) {
- case AND:
- os << " && ";
- break;
- case OR:
- os << " || ";
- break;
- case NAND:
- FatalError("unsupported boolean type in C_Print1");
- break;
- case NOR:
- FatalError("unsupported boolean type in C_Print1");
- break;
- case XOR:
- FatalError("unsupported boolean type in C_Print1");
- break;
- default:
- FatalError("unsupported boolean type in C_Print1");
- }
- it->C_Print1(os,indentation,letize);
- }
- os << ")";
- break;
- }
- case IFF:
- FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features
- os << "(";
- os << "(";
- c[0].C_Print1(os,indentation,letize);
- os << ")";
- os << " <=> ";
- os << "(";
- c[1].C_Print1(os,indentation,letize);
- os << ")";
- os << ")";
- os << endl;
- break;
- case IMPLIES:
- FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features
- os << "(";
- os << "(";
- c[0].C_Print1(os,indentation,letize);
- os << ")";
- os << " => ";
- os << "(";
- c[1].C_Print1(os,indentation,letize);
- os << ")";
- os << ")";
- os << endl;
- break;
- case BVSX:
- FatalError("C_Print1: printing not implemented for this kind: ",*this); // stopgap for un-implemented features
-
- os << kind << "(";
- c[0].C_Print1(os,indentation,letize);
- os << ",";
- os << this->GetValueWidth();
- os << ")" << endl;
- break;
- default:
- //remember to use LispPrinter here. Otherwise this function will
- //go into an infinite loop. Recall that "<<" is overloaded to
- //the lisp printer. FatalError uses lispprinter
- FatalError("C_Print1: printing not implemented for this kind: ",*this);
- break;
- }
- } //end of C_Print1()
-
-
////////////////////////////////////////////////////////////////
// BeevMgr members
////////////////////////////////////////////////////////////////
return ((size_t) node1._int_node_ptr) < ((size_t) node2._int_node_ptr);
}
- string functionToSMTLIBName(const Kind k) const;
-
public:
//Check if it points to a null node
bool IsNull () const { return _int_node_ptr == NULL; }
bool IsAlreadyPrinted() const;
void MarkAlreadyPrinted() const;
+ // delegates to the ASTInternal node.
+ void nodeprint(ostream& os, bool c_friendly = false) const;
+
+
public:
// Default constructor. This gets used when declaring an ASTVec
// of a given size, in the hash table, etc. For faster
void PL_Print1(ostream &os, int indentation = 0, bool b = false) const;
- // C code printer
- ostream& C_Print(ostream &os, int indentation = 0) const;
- void C_Print1(ostream &os, int indentation = 0, bool b = false) const;
-
- ostream& SMTLIB_Print(ostream &os, int indentation) const;
- void SMTLIB_Print1(ostream& os, int indentation, bool letize) const;
-
-
//Construct let variables for shared subterms
void LetizeNode(void) const;
include ../Makefile.common
#SRCS = AST.cpp ASTKind.cpp ASTUtil.cpp BitBlast.cpp SimpBool.cpp ToCNF.cpp DPLLMgr.cpp ToSAT.cpp Transform.cpp
-SRCS = AST.cpp ASTKind.cpp ASTUtil.cpp BitBlast.cpp SimpBool.cpp ToCNF.cpp ToSAT.cpp Transform.cpp
+SRCS = AST.cpp ASTKind.cpp ASTUtil.cpp BitBlast.cpp SimpBool.cpp ToCNF.cpp ToSAT.cpp Transform.cpp printer/SMTLIBPrinter.cpp printer/dotPrinter.cpp printer/CPrinter.cpp
OBJS = $(SRCS:.cpp=.o)
CFLAGS += -I../sat/mtl -I../sat/core
clean:
rm -rf *.o *~ bbtest asttest cnftest *.a ASTKind.h ASTKind.cpp .#*
+ rm -rf outputer/*.o
depend:
makedepend -Y -- $(CFLAGS) -- $(SRCS)
--- /dev/null
+#include "printers.h"
+
+namespace printer {
+
+using std::string;
+using namespace BEEV;
+
+
+// printer for C code (copied from PL_Print())
+// TODO: this does not fully implement printing of all of the STP
+// language - FatalError calls inserted for unimplemented
+// functionality, e.g.,:
+// FatalError("C_Print1: printing not implemented for this kind: ",*this);
+
+// helper function for printing C code (copied from PL_Print1())
+void C_Print1(ostream& os, const ASTNode n, int indentation, bool letize) {
+
+ unsigned int upper, lower, num_bytes;
+ Kind LHSkind, RHSkind;
+
+ //os << spaces(indentation);
+ //os << endl << spaces(indentation);
+ if (!n.IsDefined()) {
+ os << "<undefined>";
+ return;
+ }
+
+ //if this node is present in the letvar Map, then print the letvar
+ BeevMgr &bm = n.GetBeevMgr();
+
+ //this is to print letvars for shared subterms inside the printing
+ //of "(LET v0 = term1, v1=term1@term2,...
+ if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize) {
+ C_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize);
+ return;
+ }
+
+ //this is to print letvars for shared subterms inside the actual
+ //term to be printed
+ if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize) {
+ C_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize);
+ return;
+ }
+
+ //otherwise print it normally
+ Kind kind = n.GetKind();
+ const ASTVec &c = n.GetChildren();
+ switch (kind) {
+ case BVGETBIT:
+ FatalError("C_Print1: printing not implemented for this kind: ", n);
+ C_Print1(os, c[0], indentation, letize);
+ os << "{";
+ C_Print1(os, c[1], indentation, letize);
+ os << "}";
+ break;
+ case BITVECTOR:
+ FatalError("C_Print1: printing not implemented for this kind: ", n);
+ os << "BITVECTOR(";
+ unsigned char * str;
+ str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst());
+ os << str << ")";
+ CONSTANTBV::BitVector_Dispose(str);
+ break;
+ case BOOLEAN:
+ FatalError("C_Print1: printing not implemented for this kind: ", n);
+ os << "BOOLEAN";
+ break;
+ case FALSE:
+ os << "0";
+ break;
+ case TRUE:
+ os << "1";
+ break;
+ case BVCONST:
+ case SYMBOL:
+ // print in C friendly format:
+ n.nodeprint(os, true);
+ break;
+ case READ:
+ C_Print1(os, c[0], indentation, letize);
+ os << "[";
+ C_Print1(os, c[1], indentation, letize);
+ os << "]";
+ break;
+ case WRITE:
+ os << "(";
+ C_Print1(os, c[0], indentation, letize);
+ os << " WITH [";
+ C_Print1(os, c[1], indentation, letize);
+ os << "] := ";
+ C_Print1(os, c[2], indentation, letize);
+ os << ")";
+ os << endl;
+ break;
+ case BVUMINUS:
+ os << kind << "( ";
+ C_Print1(os, c[0], indentation, letize);
+ os << ")";
+ break;
+ case NOT:
+ os << "!(";
+ C_Print1(os, c[0], indentation, letize);
+ os << ") " << endl;
+ break;
+ case BVNEG:
+ os << " ~(";
+ C_Print1(os, c[0], indentation, letize);
+ os << ")";
+ break;
+ case BVCONCAT:
+ FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
+ os << "(";
+ C_Print1(os,c[0], indentation, letize);
+ os << " @ ";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")" << endl;
+ break;
+ case BVOR:
+ os << "(";
+ C_Print1(os, c[0], indentation, letize);
+ os << " | ";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVAND:
+ os << "(";
+ C_Print1(os, c[0], indentation, letize);
+ os << " & ";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVEXTRACT:
+
+ // we only accept indices that are byte-aligned
+ // (e.g., [15:8], [23:16])
+ // and round down to byte indices rather than bit indices
+ upper = GetUnsignedConst(c[1]);
+ lower = GetUnsignedConst(c[2]);
+ assert(upper > lower);
+ assert(lower % 8 == 0);
+ assert((upper + 1) % 8 == 0);
+ num_bytes = (upper - lower + 1) / 8;
+ assert (num_bytes > 0);
+
+ // for multi-byte extraction, use the ADDRESS
+ if (num_bytes > 1) {
+ os << "&";
+ C_Print1(os, c[0], indentation, letize);
+ os << "[" << lower / 8 << "]";
+ }
+ // for single-byte extraction, use the VALUE
+ else {
+ C_Print1(os, c[0], indentation, letize);
+ os << "[" << lower / 8 << "]";
+ }
+
+ break;
+ case BVLEFTSHIFT:
+ FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
+ os << "(";
+ C_Print1(os, c[0], indentation, letize);
+ os << " << ";
+ os << GetUnsignedConst(c[1]);
+ os << ")";
+ break;
+ case BVRIGHTSHIFT:
+ FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
+ os << "(";
+ C_Print1(os,c[0], indentation, letize);
+ os << " >> ";
+ os << GetUnsignedConst(c[1]);
+ os << ")";
+ break;
+ case BVMULT:
+ case BVSUB:
+ case BVPLUS:
+ case SBVDIV:
+ case SBVREM:
+ case BVDIV:
+ case BVMOD:
+ os << kind << "(";
+ os << n.GetValueWidth();
+ for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) {
+ os << ", " << endl;
+ C_Print1(os, *it, indentation, letize);
+ }
+ os << ")" << endl;
+ break;
+ case ITE:
+ os << "if (";
+ C_Print1(os, c[0], indentation, letize);
+ os << ")" << endl;
+ os << "{";
+ C_Print1(os, c[1], indentation, letize);
+ os << endl << "} else {";
+ C_Print1(os, c[2], indentation, letize);
+ os << endl << "}";
+ break;
+ case BVLT:
+ // convert to UNSIGNED before doing comparison!
+ os << "((unsigned char)";
+ C_Print1(os, c[0], indentation, letize);
+ os << " < ";
+ os << "(unsigned char)";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVLE:
+ // convert to UNSIGNED before doing comparison!
+ os << "((unsigned char)";
+ C_Print1(os, c[0], indentation, letize);
+ os << " <= ";
+ os << "(unsigned char)";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVGT:
+ // convert to UNSIGNED before doing comparison!
+ os << "((unsigned char)";
+ C_Print1(os, c[0], indentation, letize);
+ os << " > ";
+ os << "(unsigned char)";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVGE:
+ // convert to UNSIGNED before doing comparison!
+ os << "((unsigned char)";
+ C_Print1(os, c[0], indentation, letize);
+ os << " >= ";
+ os << "(unsigned char)";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVXOR:
+ case BVNAND:
+ case BVNOR:
+ case BVXNOR:
+ FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
+ break;
+ case BVSLT:
+ // convert to SIGNED before doing comparison!
+ os << "((signed char)";
+ C_Print1(os, c[0], indentation, letize);
+ os << " < ";
+ os << "(signed char)";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVSLE:
+ // convert to SIGNED before doing comparison!
+ os << "((signed char)";
+ C_Print1(os, c[0], indentation, letize);
+ os << " <= ";
+ os << "(signed char)";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVSGT:
+ // convert to SIGNED before doing comparison!
+ os << "((signed char)";
+ C_Print1(os, c[0], indentation, letize);
+ os << " > ";
+ os << "(signed char)";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case BVSGE:
+ // convert to SIGNED before doing comparison!
+ os << "((signed char)";
+ C_Print1(os, c[0], indentation, letize);
+ os << " >= ";
+ os << "(signed char)";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ break;
+ case EQ:
+ // tricky tricky ... if it's a single-byte comparison,
+ // simply do ==, but if it's multi-byte, must do memcmp
+ LHSkind = c[0].GetKind();
+ RHSkind = c[1].GetKind();
+
+ num_bytes = 0;
+
+ // try to figure out whether it's a single-byte or multi-byte
+ // comparison
+ if (LHSkind == BVEXTRACT) {
+ upper = GetUnsignedConst(c[0].GetChildren()[1]);
+ lower = GetUnsignedConst(c[0].GetChildren()[2]);
+ num_bytes = (upper - lower + 1) / 8;
+ }
+ else if (RHSkind == BVEXTRACT) {
+ upper = GetUnsignedConst(c[1].GetChildren()[1]);
+ lower = GetUnsignedConst(c[1].GetChildren()[2]);
+ num_bytes = (upper - lower + 1) / 8;
+ }
+
+ if (num_bytes > 1) {
+ os << "(memcmp(";
+ C_Print1(os,c[0], indentation, letize);
+ os << ", ";
+ C_Print1(os, c[1], indentation, letize);
+ os << ", ";
+ os << num_bytes;
+ os << ") == 0)";
+ }
+ else if (num_bytes == 1) {
+ os << "(";
+ C_Print1(os, c[0], indentation, letize);
+ os << " == ";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ }
+ else {
+ FatalError("C_Print1: ugh problem in implementing ==");
+ }
+
+ break;
+ case NEQ:
+ C_Print1(os, c[0], indentation, letize);
+ os << " != ";
+ C_Print1(os, c[1], indentation, letize);
+ os << endl;
+ break;
+ case AND:
+ case OR:
+ case NAND:
+ case NOR:
+ case XOR: {
+ os << "(";
+ C_Print1(os, c[0], indentation, letize);
+ ASTVec::const_iterator it = c.begin();
+ ASTVec::const_iterator itend = c.end();
+
+ it++;
+ for (; it != itend; it++) {
+ switch (kind) {
+ case AND:
+ os << " && ";
+ break;
+ case OR:
+ os << " || ";
+ break;
+ case NAND:
+ FatalError("unsupported boolean type in C_Print1");
+ break;
+ case NOR:
+ FatalError("unsupported boolean type in C_Print1");
+ break;
+ case XOR:
+ FatalError("unsupported boolean type in C_Print1");
+ break;
+ default:
+ FatalError("unsupported boolean type in C_Print1");
+ }
+ C_Print1(os, *it, indentation, letize);
+ }
+ os << ")";
+ break;
+ }
+ case IFF:
+ FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
+ os << "(";
+ os << "(";
+ C_Print1(os,c[0], indentation, letize);
+ os << ")";
+ os << " <=> ";
+ os << "(";
+ C_Print1(os,c[1], indentation, letize);
+ os << ")";
+ os << ")";
+ os << endl;
+ break;
+ case IMPLIES:
+ FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
+ os << "(";
+ os << "(";
+ C_Print1(os, c[0],indentation, letize);
+ os << ")";
+ os << " => ";
+ os << "(";
+ C_Print1(os, c[1], indentation, letize);
+ os << ")";
+ os << ")";
+ os << endl;
+ break;
+ case BVSX:
+ FatalError("C_Print1: printing not implemented for this kind: ", n); // stopgap for un-implemented features
+
+ os << kind << "(";
+ C_Print1(os, c[0],indentation, letize);
+ os << ",";
+ os << n.GetValueWidth();
+ os << ")" << endl;
+ break;
+ default:
+ //remember to use LispPrinter here. Otherwise this function will
+ //go into an infinite loop. Recall that "<<" is overloaded to
+ //the lisp printer. FatalError uses lispprinter
+ FatalError("C_Print1: printing not implemented for this kind: ", n);
+ break;
+ }
+} //end of C_Print1()
+
+
+//two pass algorithm:
+//
+//1. In the first pass, letize this Node, N: i.e. if a node
+//1. appears more than once in N, then record this fact.
+//
+//2. In the second pass print a "global let" and then print N
+//2. as follows: Every occurence of a node occuring more than
+//2. once is replaced with the corresponding let variable.
+ostream& C_Print(ostream &os, const ASTNode n, int indentation) {
+ // Clear the PrintMap
+ BeevMgr& bm = n.GetBeevMgr();
+ bm.PLPrintNodeSet.clear();
+ bm.NodeLetVarMap.clear();
+ bm.NodeLetVarVec.clear();
+ bm.NodeLetVarMap1.clear();
+
+ //pass 1: letize the node
+ n.LetizeNode();
+
+ unsigned int lower, upper, num_bytes = 0;
+
+ //pass 2:
+ //
+ //2. print all the let variables and their counterpart expressions
+ //2. as follows (LET var1 = expr1, var2 = expr2, ...
+ //
+ //3. Then print the Node itself, replacing every occurence of
+ //3. expr1 with var1, expr2 with var2, ...
+ //os << "(";
+ if (0 < bm.NodeLetVarMap.size()) {
+ //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin();
+ //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end();
+ std::vector<pair<ASTNode, ASTNode> >::iterator it = bm.NodeLetVarVec.begin();
+ std::vector<pair<ASTNode, ASTNode> >::iterator itend = bm.NodeLetVarVec.end();
+
+ // start a new block to create new static scope
+ os << "{" << endl;
+
+ for (; it != itend; it++) {
+
+ // see if it's a BVEXTRACT, and if so, whether it's multi-byte
+ if (it->second.GetKind() == BVEXTRACT) {
+ upper = GetUnsignedConst(it->second.GetChildren()[1]);
+ lower = GetUnsignedConst(it->second.GetChildren()[2]);
+ num_bytes = (upper - lower + 1) / 8;
+ assert(num_bytes > 0);
+ }
+
+ //print the let var first
+ if (num_bytes > 1) {
+ // for multi-byte assignment, use 'memcpy' and array notation
+ os << "unsigned char ";
+ C_Print1(os, it->first,indentation, false);
+ os << "[" << num_bytes << "]; ";
+ os << "memcpy(";
+ C_Print1(os,it->first, indentation, false);
+ os << ", ";
+ //print the expr
+ C_Print1(os,it->second, indentation, false);
+ os << ", " << num_bytes << ");";
+ }
+ else {
+ // for single-byte assignment, use '='
+ os << "unsigned char ";
+ C_Print1(os, it->first,indentation, false);
+ os << " = ";
+ //print the expr
+ C_Print1(os, it->second,indentation, false);
+ os << ";" << endl;
+ }
+
+ //update the second map for proper printing of LET
+ bm.NodeLetVarMap1[it->second] = it->first;
+ }
+
+ os << endl << "stp_assert ";
+ C_Print1(os, n, indentation, true);
+
+ os << ";" << endl << "}";
+ }
+ else {
+ os << "stp_assert ";
+ C_Print1(os, n, indentation, false);
+ os << ";";
+ }
+ //os << " )";
+ //os << " ";
+
+ return os;
+} //end of C_Print()
+}
--- /dev/null
+#include "printers.h"
+
+namespace printer {
+
+using std::string;
+using namespace BEEV;
+
+string functionToSMTLIBName(const BEEV::Kind k);
+void SMTLIB_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize);
+
+void outputBitVec(const ASTNode n, ostream& os) {
+ Kind k = n.GetKind();
+ const ASTVec &c = n.GetChildren();
+ ASTNode op;
+
+ if (BITVECTOR == k) {
+ op = c[0];
+ }
+ else if (BVCONST == k) {
+ op = n;
+ }
+ else
+ FatalError("nsadfsdaf");
+
+ // CONSTANTBV::BitVector_to_Dec returns a signed representation by default.
+ // Prepend with zero to convert to unsigned.
+
+ os << "bv";
+ CBV unsign = CONSTANTBV::BitVector_Concat(n.GetBeevMgr().CreateZeroConst(1).GetBVConst(), op.GetBVConst());
+ unsigned char * str = CONSTANTBV::BitVector_to_Dec(unsign);
+ CONSTANTBV::BitVector_Destroy(unsign);
+ os << str << "[" << op.GetValueWidth() << "]";
+ CONSTANTBV::BitVector_Dispose(str);
+}
+
+void SMTLIB_Print1(ostream& os, const ASTNode n, int indentation, bool letize) {
+ //os << spaces(indentation);
+ //os << endl << spaces(indentation);
+ if (!n.IsDefined()) {
+ os << "<undefined>";
+ return;
+ }
+
+ //if this node is present in the letvar Map, then print the letvar
+ BeevMgr &bm = n.GetBeevMgr();
+
+ //this is to print letvars for shared subterms inside the printing
+ //of "(LET v0 = term1, v1=term1@term2,...
+ if ((bm.NodeLetVarMap1.find(n) != bm.NodeLetVarMap1.end()) && !letize) {
+ SMTLIB_Print1(os, (bm.NodeLetVarMap1[n]), indentation, letize);
+ return;
+ }
+
+ //this is to print letvars for shared subterms inside the actual
+ //term to be printed
+ if ((bm.NodeLetVarMap.find(n) != bm.NodeLetVarMap.end()) && letize) {
+ SMTLIB_Print1(os, (bm.NodeLetVarMap[n]), indentation, letize);
+ return;
+ }
+
+ //otherwise print it normally
+ Kind kind = n.GetKind();
+ const ASTVec &c = n.GetChildren();
+ switch (kind) {
+ case BITVECTOR:
+ case BVCONST:
+ outputBitVec(n, os);
+ break;
+
+ case SYMBOL:
+ n.nodeprint(os);
+ break;
+ case FALSE:
+ os << "false";
+ break;
+ case TRUE:
+ os << "true";
+ break;
+
+ case BVSX:
+ case BVZX: {
+ unsigned int amount = GetUnsignedConst(c[1]);
+ if (BVZX == kind)
+ os << "(zero_extend[";
+ else
+ os << "(sign_extend[";
+
+ os << amount << "]";
+ SMTLIB_Print1(os, c[0], indentation, letize);
+ os << ")";
+ }
+ break;
+ case BVEXTRACT: {
+ unsigned int upper = GetUnsignedConst(c[1]);
+ unsigned int lower = GetUnsignedConst(c[2]);
+ assert(upper >= lower);
+ os << "(extract[" << upper << ":" << lower << "] ";
+ SMTLIB_Print1(os, c[0], indentation, letize);
+ os << ")";
+ }
+ break;
+ default: {
+ os << "(" << functionToSMTLIBName(kind);
+
+ ASTVec::const_iterator iend = c.end();
+ for (ASTVec::const_iterator i = c.begin(); i != iend; i++) {
+ os << " ";
+ SMTLIB_Print1(os, *i, 0, letize);
+ }
+
+ os << ")";
+ }
+ }
+}
+
+// copied from Presentation Langauge printer.
+ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation) {
+ // Clear the PrintMap
+ BeevMgr& bm = n.GetBeevMgr();
+ bm.PLPrintNodeSet.clear();
+ bm.NodeLetVarMap.clear();
+ bm.NodeLetVarVec.clear();
+ bm.NodeLetVarMap1.clear();
+
+ //pass 1: letize the node
+ n.LetizeNode();
+
+ //pass 2:
+ //
+ //2. print all the let variables and their counterpart expressions
+ //2. as follows (LET var1 = expr1, var2 = expr2, ...
+ //
+ //3. Then print the Node itself, replacing every occurence of
+ //3. expr1 with var1, expr2 with var2, ...
+ //os << "(";
+ if (0 < bm.NodeLetVarMap.size()) {
+ //ASTNodeMap::iterator it=bm.NodeLetVarMap.begin();
+ //ASTNodeMap::iterator itend=bm.NodeLetVarMap.end();
+ std::vector<pair<ASTNode, ASTNode> >::iterator it = bm.NodeLetVarVec.begin();
+ std::vector<pair<ASTNode, ASTNode> >::iterator itend = bm.NodeLetVarVec.end();
+
+ os << "(LET ";
+ //print the let var first
+ SMTLIB_Print1(os, it->first, indentation, false);
+ os << " = ";
+ //print the expr
+ SMTLIB_Print1(os, it->second, indentation, false);
+
+ //update the second map for proper printing of LET
+ bm.NodeLetVarMap1[it->second] = it->first;
+
+ for (it++; it != itend; it++) {
+ os << "," << endl;
+ //print the let var first
+ SMTLIB_Print1(os, it->first, indentation, false);
+ os << " = ";
+ //print the expr
+ SMTLIB_Print1(os, it->second, indentation, false);
+
+ //update the second map for proper printing of LET
+ bm.NodeLetVarMap1[it->second] = it->first;
+ }
+
+ os << " IN " << endl;
+ SMTLIB_Print1(os, n, indentation, true);
+ os << ") ";
+ }
+ else
+ SMTLIB_Print1(os, n, indentation, false);
+
+ os << endl;
+ return os;
+}
+
+string functionToSMTLIBName(const Kind k) {
+ switch (k) {
+ case AND:
+ case BVAND:
+ case BVNAND:
+ case BVNOR:
+ case BVOR:
+ case BVSGE:
+ case BVSGT:
+ case BVSLE:
+ case BVSLT:
+ case BVSUB:
+ case BVXOR:
+ case ITE:
+ case NAND:
+ case NOR:
+ case NOT:
+ case OR:
+ case XOR:
+ case IFF:
+ return _kind_names[k];
+
+ case BVCONCAT:
+ return "concat";
+ case BVDIV:
+ return "bvudiv";
+ case BVGT:
+ return "bvugt";
+ case BVGE:
+ return "bvuge";
+ case BVLE:
+ return "bvule";
+ case BVLEFTSHIFT:
+ return "bvshl";
+ case BVLT:
+ return "bvult";
+ case BVMOD:
+ return "bvurem";
+ case BVMULT:
+ return "bvmul";
+ case BVNEG:
+ return "bvnot"; // CONFUSSSSINNG. (1/2)
+ case BVPLUS:
+ return "bvadd";
+ case BVRIGHTSHIFT:
+ return "bvlshr"; // logical
+ case BVSRSHIFT:
+ return "bvashr"; // arithmetic.
+ case BVUMINUS:
+ return "bvneg"; // CONFUSSSSINNG. (2/2)
+ case EQ:
+ return "=";
+ case READ:
+ return "select";
+ case WRITE:
+ return "store";
+ case SBVDIV:
+ return "bvsdiv";
+ case SBVREM:
+ return "bvsrem";
+
+ default: {
+ cerr << "Unknown name when outputting:";
+ FatalError(_kind_names[k]);
+ return ""; // to quieten compiler/
+ }
+ }
+}
+
+}
--- /dev/null
+#include "printers.h"
+
+/*
+ * Outputs in DOT graph format. Can be layed out by the dotty/neato tools.
+ */
+
+namespace printer {
+
+using std::string;
+using namespace BEEV;
+
+void outputBitVec(const ASTNode n, ostream& os);
+
+void Dot_Print1(ostream &os, const ASTNode n, hash_set<int> *alreadyOutput) {
+
+ // check if this node has already been printed. If so return.
+ if (alreadyOutput->find(n.GetNodeNum()) != alreadyOutput->end())
+ return;
+
+ alreadyOutput->insert(n.GetNodeNum());
+
+ os << "n" << n.GetNodeNum() << "[label =\"";
+ switch(n.GetKind())
+ {
+ case SYMBOL:
+ n.nodeprint(os);
+ break;
+
+ case BITVECTOR:
+ case BVCONST:
+ outputBitVec(n, os);
+ break;
+
+ default:
+ os << _kind_names[n.GetKind()];
+ }
+
+
+ os << "\"];" << endl;
+
+
+ // print the edges to each child.
+ ASTVec ch = n.GetChildren();
+ ASTVec::iterator itend = ch.end();
+ int i =0;
+ for(ASTVec::iterator it = ch.begin(); it < itend; it++)
+ {
+ os << "n" << n.GetNodeNum() << " -> " << "n" << it->GetNodeNum() << "[label=" << i++ << "];" << endl;
+ }
+
+ // print each of the children.
+ for(ASTVec::iterator it = ch.begin(); it < itend; it++)
+ {
+ Dot_Print1(os, *it, alreadyOutput);
+ }
+}
+
+ostream& Dot_Print(ostream &os, const ASTNode n) {
+
+ os << "digraph G{" << endl;
+
+ // create hashmap to hold integers (node numbers).
+ hash_set<int> alreadyOutput;
+
+ Dot_Print1(os, n, &alreadyOutput);
+
+ os << "}" << endl;
+
+ return os;
+}
+
+}
--- /dev/null
+#ifndef PRINTERS_H_
+#define PRINTERS_H_
+
+#include "../AST.h"
+#include "../ASTUtil.h"
+#include "../ASTKind.h"
+
+
+namespace printer
+{
+
+ ostream& Dot_Print(ostream &os, const BEEV::ASTNode n);
+ ostream& SMTLIB_Print(ostream &os, const BEEV::ASTNode n, const int indentation=0);
+ ostream& C_Print(ostream &os, const BEEV::ASTNode n, const int indentation=0);
+}
+
+#endif /* PRINTERS_H_ */
CFLAGS = $(CFLAGS_BASE)
endif
-CXXFLAGS = $(CFLAGS) -Wall -DEXT_HASH_MAP -Wno-deprecated
+CXXFLAGS = $(CFLAGS) -Wall -Wextra -DEXT_HASH_MAP -Wno-deprecated
#CXXFLAGS = $(CFLAGS) -Wall -DTR1_UNORDERED_MAP
#CXXFLAGS = $(CFLAGS) -Wall
#LDFLAGS= -lstdc++
#include <assert.h>
#include "fdstream.h"
#include "../AST/AST.h"
+#include "../AST/printer/printers.h"
//These typedefs lower the effort of using the keyboard to type (too
//many overloaded meanings of the word type)
char * vc_printSMTLIB(VC vc, Expr e)
{
stringstream ss;
- ((nodestar)e)->SMTLIB_Print(ss,0);
+ printer::SMTLIB_Print(ss,*((nodestar)e), 0);
string s = ss.str();
char *copy = strdup(s.c_str());
return copy;
cout << endl;
// print constraints and assert
- q.C_Print(cout);
+ printer::C_Print(cout,q);
}
projects / francis / stp.git / commitdiff