From: trevor_hansen Date: Thu, 27 Aug 2009 05:15:44 +0000 (+0000) Subject: Moving the Lisp & Presentation Language (PL) printers to the "printer" namespace. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=6170d517086ed5ed1ea03509a60965476880872b;p=francis%2Fstp.git Moving the Lisp & Presentation Language (PL) printers to the "printer" namespace. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@146 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/AST/AST.cpp b/src/AST/AST.cpp index e3a52a6..af22539 100644 --- a/src/AST/AST.cpp +++ b/src/AST/AST.cpp @@ -10,6 +10,7 @@ #include "AST.h" #include +#include "printer/printers.h" namespace BEEV { @@ -221,165 +222,7 @@ void ASTNode::NFASTPrint(int l, int max, int prefix) const } } -// Print in lisp format -ostream &ASTNode::LispPrint(ostream &os, int indentation) const -{ - // Clear the PrintMap - BeevMgr& bm = GetBeevMgr(); - bm.AlreadyPrintedSet.clear(); - LispPrint_indent(os, indentation); - printf("\n"); - return os; -} - -// Print newline and indentation, then print the thing. -ostream &ASTNode::LispPrint_indent(ostream &os, int indentation) const -{ - os << endl << spaces(indentation); - LispPrint1(os, indentation); - return os; -} - -/** Internal function to print in lisp format. Assume newline - and indentation printed already before first line. Recursive - calls will have newline & indent, though */ -ostream &ASTNode::LispPrint1(ostream &os, int indentation) const -{ - if (!IsDefined()) - { - os << ""; - return os; - } - Kind kind = GetKind(); - // FIXME: figure out how to avoid symbols with same names as kinds. - // if (kind == READ) { - // const ASTVec &children = GetChildren(); - // children[0].LispPrint1(os, indentation); - // os << "[" << children[1] << "]"; - // } else - if (kind == BVGETBIT) - { - const ASTVec &children = GetChildren(); - // child 0 is a symbol. Print without the NodeNum. - os << GetNodeNum() << ":"; - - children[0]._int_node_ptr->nodeprint(os); - //os << "{" << children[1].GetBVConst() << "}"; - os << "{"; - children[1]._int_node_ptr->nodeprint(os); - os << "}"; - } - else if (kind == NOT) - { - const ASTVec &children = GetChildren(); - os << GetNodeNum() << ":"; - os << "(NOT "; - children[0].LispPrint1(os, indentation); - os << ")"; - } - else if (Degree() == 0) - { - // Symbol or a kind with no children print as index:NAME if shared, - // even if they have been printed before. - os << GetNodeNum() << ":"; - _int_node_ptr->nodeprint(os); - // os << "(" << _int_node_ptr->_ref_count << ")"; - // os << "{" << GetValueWidth() << "}"; - } - else if (IsAlreadyPrinted()) - { - // print non-symbols as "[index]" if seen before. - os << "[" << GetNodeNum() << "]"; - // << "(" << _int_node_ptr->_ref_count << ")"; - } - else - { - MarkAlreadyPrinted(); - const ASTVec &children = GetChildren(); - os << GetNodeNum() << ":" - //<< "(" << _int_node_ptr->_ref_count << ")" - << "(" << kind << " "; - // os << "{" << GetValueWidth() << "}"; - ASTVec::const_iterator iend = children.end(); - for (ASTVec::const_iterator i = children.begin(); i != iend; i++) - { - i->LispPrint_indent(os, indentation + 2); - } - os << ")"; - } - return os; -} - -//print in PRESENTATION LANGUAGE -// -//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::PL_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 >::iterator it = bm.NodeLetVarVec.begin(); - std::vector >::iterator itend = bm.NodeLetVarVec.end(); - - os << "(LET "; - //print the let var first - it->first.PL_Print1(os, indentation, false); - os << " = "; - //print the expr - it->second.PL_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.PL_Print1(os, indentation, false); - os << " = "; - //print the expr - it->second.PL_Print1(os, indentation, false); - - //update the second map for proper printing of LET - bm.NodeLetVarMap1[it->second] = it->first; - } - os << " IN " << endl; - PL_Print1(os, indentation, true); - os << ") "; - } - else - PL_Print1(os, indentation, false); - //os << " )"; - os << " "; - return os; -} //end of PL_Print() //traverse "*this", and construct "let variables" for terms that //occur more than once in "*this". @@ -449,279 +292,7 @@ void ASTNode::LetizeNode(void) const } } //end of LetizeNode() -void ASTNode::PL_Print1(ostream& os, int indentation, bool letize) const -{ - //os << spaces(indentation); - //os << endl << spaces(indentation); - if (!IsDefined()) - { - os << ""; - 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]).PL_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]).PL_Print1(os, indentation, letize); - return; - } - - //otherwise print it normally - Kind kind = GetKind(); - const ASTVec &c = GetChildren(); - switch (kind) - { - case BVGETBIT: - c[0].PL_Print1(os, indentation, letize); - os << "{"; - c[1].PL_Print1(os, indentation, letize); - os << "}"; - break; - case BITVECTOR: - os << "BITVECTOR("; - unsigned char * str; - str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst()); - os << str << ")"; - CONSTANTBV::BitVector_Dispose(str); - break; - case BOOLEAN: - os << "BOOLEAN"; - break; - case FALSE: - case TRUE: - os << kind; - break; - case BVCONST: - case SYMBOL: - _int_node_ptr->nodeprint(os); - break; - case READ: - c[0].PL_Print1(os, indentation, letize); - os << "["; - c[1].PL_Print1(os, indentation, letize); - os << "]"; - break; - case WRITE: - os << "("; - c[0].PL_Print1(os, indentation, letize); - os << " WITH ["; - c[1].PL_Print1(os, indentation, letize); - os << "] := "; - c[2].PL_Print1(os, indentation, letize); - os << ")"; - os << endl; - break; - case BVUMINUS: - os << kind << "( "; - c[0].PL_Print1(os, indentation, letize); - os << ")"; - break; - case NOT: - os << "NOT("; - c[0].PL_Print1(os, indentation, letize); - os << ") " << endl; - break; - case BVNEG: - os << " ~("; - c[0].PL_Print1(os, indentation, letize); - os << ")"; - break; - case BVCONCAT: - os << "("; - c[0].PL_Print1(os, indentation, letize); - os << " @ "; - c[1].PL_Print1(os, indentation, letize); - os << ")" << endl; - break; - case BVOR: - os << "("; - c[0].PL_Print1(os, indentation, letize); - os << " | "; - c[1].PL_Print1(os, indentation, letize); - os << ")"; - break; - case BVAND: - os << "("; - c[0].PL_Print1(os, indentation, letize); - os << " & "; - c[1].PL_Print1(os, indentation, letize); - os << ")"; - break; - case BVEXTRACT: - c[0].PL_Print1(os, indentation, letize); - os << "["; - os << GetUnsignedConst(c[1]); - os << ":"; - os << GetUnsignedConst(c[2]); - os << "]"; - break; - case BVLEFTSHIFT: - os << "("; - c[0].PL_Print1(os, indentation, letize); - os << " << "; - os << GetUnsignedConst(c[1]); - os << ")"; - break; - case BVRIGHTSHIFT: - os << "("; - c[0].PL_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->PL_Print1(os, indentation, letize); - } - os << ")" << endl; - break; - case ITE: - os << "IF("; - c[0].PL_Print1(os, indentation, letize); - os << ")" << endl; - os << "THEN "; - c[1].PL_Print1(os, indentation, letize); - os << endl << "ELSE "; - c[2].PL_Print1(os, indentation, letize); - os << endl << "ENDIF"; - break; - case BVLT: - case BVLE: - case BVGT: - case BVGE: - case BVXOR: - case BVNAND: - case BVNOR: - case BVXNOR: - os << kind << "("; - c[0].PL_Print1(os, indentation, letize); - os << ","; - c[1].PL_Print1(os, indentation, letize); - os << ")" << endl; - break; - case BVSLT: - os << "SBVLT" << "("; - c[0].PL_Print1(os, indentation, letize); - os << ","; - c[1].PL_Print1(os, indentation, letize); - os << ")" << endl; - break; - case BVSLE: - os << "SBVLE" << "("; - c[0].PL_Print1(os, indentation, letize); - os << ","; - c[1].PL_Print1(os, indentation, letize); - os << ")" << endl; - break; - case BVSGT: - os << "SBVGT" << "("; - c[0].PL_Print1(os, indentation, letize); - os << ","; - c[1].PL_Print1(os, indentation, letize); - os << ")" << endl; - break; - case BVSGE: - os << "SBVGE" << "("; - c[0].PL_Print1(os, indentation, letize); - os << ","; - c[1].PL_Print1(os, indentation, letize); - os << ")" << endl; - break; - case EQ: - c[0].PL_Print1(os, indentation, letize); - os << " = "; - c[1].PL_Print1(os, indentation, letize); - os << endl; - break; - case NEQ: - c[0].PL_Print1(os, indentation, letize); - os << " /= "; - c[1].PL_Print1(os, indentation, letize); - os << endl; - break; - case AND: - case OR: - case NAND: - case NOR: - case XOR: - { - os << "("; - c[0].PL_Print1(os, indentation, letize); - ASTVec::const_iterator it = c.begin(); - ASTVec::const_iterator itend = c.end(); - it++; - for (; it != itend; it++) - { - os << " " << kind << " "; - it->PL_Print1(os, indentation, letize); - os << endl; - } - os << ")"; - break; - } - case IFF: - os << "("; - os << "("; - c[0].PL_Print1(os, indentation, letize); - os << ")"; - os << " <=> "; - os << "("; - c[1].PL_Print1(os, indentation, letize); - os << ")"; - os << ")"; - os << endl; - break; - case IMPLIES: - os << "("; - os << "("; - c[0].PL_Print1(os, indentation, letize); - os << ")"; - os << " => "; - os << "("; - c[1].PL_Print1(os, indentation, letize); - os << ")"; - os << ")"; - os << endl; - break; - case BVSX: - case BVZX: - os << kind << "("; - c[0].PL_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("PL_Print1: printing not implemented for this kind: ", *this); - break; - } -} //end of PL_Print1() //////////////////////////////////////////////////////////////// // BeevMgr members @@ -1616,6 +1187,21 @@ void BeevMgr::ASTNodeStats(const char * c, const ASTNode& a) cout << NodeSize(a) << endl << endl; } +ostream &ASTNode::LispPrint(ostream &os, int indentation) const +{ + printer::Lisp_Print(os, *this, indentation); +} + +ostream &ASTNode::LispPrint_indent(ostream &os, int indentation) const +{ + printer::Lisp_Print_indent(os, *this, indentation); +} + +ostream& ASTNode::PL_Print(ostream &os, int indentation) const +{ + printer::PL_Print(os, *this, indentation); +} + unsigned int BeevMgr::NodeSize(const ASTNode& a, bool clearStatInfo) { if (clearStatInfo) @@ -1799,7 +1385,7 @@ void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, int decision_level, in { cout << "!"; } - vv.PL_Print(cout, 0); + printer::PL_Print(cout,vv, 0); cout << endl; } diff --git a/src/AST/AST.h b/src/AST/AST.h index 773406c..3274657 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -184,9 +184,7 @@ public: } //end of arithless // Internal lisp-form printer that does not clear _node_print_table - ostream &LispPrint1(ostream &os, int indentation) const; - - ostream &LispPrint_indent(ostream &os, int indentation) const; + //ostream &LispPrint1(ostream &os, int indentation) const; // For lisp DAG printing. Has it been printed already, so we can // just print the node number? @@ -317,12 +315,12 @@ public: // lisp-form printer ostream& LispPrint(ostream &os, int indentation = 0) const; + ostream &LispPrint_indent(ostream &os, int indentation) const; + //Presentation Language Printer ostream& PL_Print(ostream &os, int indentation = 0) const; - void PL_Print1(ostream &os, int indentation = 0, bool b = false) const; - //Construct let variables for shared subterms void LetizeNode(void) const; diff --git a/src/AST/Makefile b/src/AST/Makefile index c25326d..76575cd 100644 --- a/src/AST/Makefile +++ b/src/AST/Makefile @@ -1,7 +1,7 @@ include ../../scripts/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 printer/SMTLIBPrinter.cpp printer/dotPrinter.cpp printer/CPrinter.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 printer/PLPrinter.cpp printer/LispPrinter.cpp OBJS = $(SRCS:.cpp=.o) CFLAGS += -I../sat/mtl -I../sat/core diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp index bbc0218..94eaa58 100644 --- a/src/AST/ToSAT.cpp +++ b/src/AST/ToSAT.cpp @@ -143,7 +143,7 @@ void BeevMgr::PrintStats(MINISAT::Solver& s) reportf("decisions : %llu (%.0f /sec)\n", s.decisions , s.decisions /cpu_time); reportf("propagations : %llu (%.0f /sec)\n", s.propagations, s.propagations/cpu_time); reportf("conflict literals : %llu (%4.2f %% deleted)\n", s.tot_literals, - (s.max_literals - s.tot_literals)*100 / (double)s.max_literals); + (s.max_literals - s.tot_literals)*100 / (double)s.max_literals); if (mem_used != 0) reportf("Memory used : %.2f MB\n", mem_used / 1048576.0); reportf("CPU time : %g s\n", cpu_time); @@ -977,7 +977,7 @@ void BeevMgr::PrintCounterExample(bool t, std::ostream& os) if (f.GetKind() == SYMBOL || (f.GetKind() == READ && f[0].GetKind() == SYMBOL && f[1].GetKind() == BVCONST)) { os << "ASSERT( "; - f.PL_Print(os, 0); + f.PL_Print(os,0); os << " = "; if (BITVECTOR_TYPE == se.GetType()) { diff --git a/src/AST/printer/LispPrinter.cpp b/src/AST/printer/LispPrinter.cpp new file mode 100644 index 0000000..8716be6 --- /dev/null +++ b/src/AST/printer/LispPrinter.cpp @@ -0,0 +1,100 @@ +#include "printers.h" + +namespace printer +{ + +using std::string; +using namespace BEEV; + +ostream &Lisp_Print_indent(ostream &os, const ASTNode& n,int indentation); + + +/** Internal function to print in lisp format. Assume newline + and indentation printed already before first line. Recursive + calls will have newline & indent, though */ +ostream &Lisp_Print1(ostream &os, const ASTNode& n, int indentation) +{ + if (!n.IsDefined()) + { + os << ""; + return os; + } + Kind kind = n.GetKind(); + // FIXME: figure out how to avoid symbols with same names as kinds. + // if (kind == READ) { + // const ASTVec &children = GetChildren(); + // children[0].LispPrint1(os, indentation); + // os << "[" << children[1] << "]"; + // } else + if (kind == BVGETBIT) + { + const ASTVec &children = n.GetChildren(); + // child 0 is a symbol. Print without the NodeNum. + os << n.GetNodeNum() << ":"; + + children[0].nodeprint(os,true); + os << "{"; + children[1].nodeprint(os,true); + os << "}"; + } + else if (kind == NOT) + { + const ASTVec &children = n.GetChildren(); + os << n.GetNodeNum() << ":"; + os << "(NOT "; + Lisp_Print1(os,children[0], indentation); + os << ")"; + } + else if (n.Degree() == 0) + { + // Symbol or a kind with no children print as index:NAME if shared, + // even if they have been printed before. + os << n.GetNodeNum() << ":"; + n.nodeprint(os,true); + // os << "(" << _int_node_ptr->_ref_count << ")"; + // os << "{" << GetValueWidth() << "}"; + } + else if (n.IsAlreadyPrinted()) + { + // print non-symbols as "[index]" if seen before. + os << "[" << n.GetNodeNum() << "]"; + // << "(" << _int_node_ptr->_ref_count << ")"; + } + else + { + n.MarkAlreadyPrinted(); + const ASTVec &children = n.GetChildren(); + os << n.GetNodeNum() << ":" + //<< "(" << _int_node_ptr->_ref_count << ")" + << "(" << kind << " "; + // os << "{" << GetValueWidth() << "}"; + ASTVec::const_iterator iend = children.end(); + for (ASTVec::const_iterator i = children.begin(); i != iend; i++) + { + Lisp_Print_indent(os, *i, indentation + 2); + } + os << ")"; + } + return os; +} + +// Print in lisp format +ostream &Lisp_Print(ostream &os, const ASTNode& n, int indentation) +{ + // Clear the PrintMap + BeevMgr& bm = n.GetBeevMgr(); + bm.AlreadyPrintedSet.clear(); + Lisp_Print_indent(os, n, indentation); + printf("\n"); + return os; +} + +// Print newline and indentation, then print the thing. +ostream &Lisp_Print_indent(ostream &os, const ASTNode& n,int indentation) +{ + os << endl << spaces(indentation); + Lisp_Print1(os, n, indentation); + return os; +} + +} diff --git a/src/AST/printer/PLPrinter.cpp b/src/AST/printer/PLPrinter.cpp new file mode 100644 index 0000000..28d23cb --- /dev/null +++ b/src/AST/printer/PLPrinter.cpp @@ -0,0 +1,354 @@ +#include "printers.h" + +namespace printer +{ + +using std::string; +using namespace BEEV; + +void PL_Print1(ostream& os, const ASTNode& n,int indentation, bool letize) +{ + //os << spaces(indentation); + //os << endl << spaces(indentation); + if (!n.IsDefined()) + { + os << ""; + 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) + { + PL_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) + { + PL_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: + PL_Print1(os, c[0], indentation, letize); + os << "{"; + PL_Print1(os, c[1],indentation, letize); + os << "}"; + break; + case BITVECTOR: + os << "BITVECTOR("; + unsigned char * str; + str = CONSTANTBV::BitVector_to_Hex(c[0].GetBVConst()); + os << str << ")"; + CONSTANTBV::BitVector_Dispose(str); + break; + case BOOLEAN: + os << "BOOLEAN"; + break; + case FALSE: + case TRUE: + os << kind; + break; + case BVCONST: + case SYMBOL: + n.nodeprint(os, true); + break; + case READ: + PL_Print1(os, c[0], indentation, letize); + os << "["; + PL_Print1(os, c[1], indentation, letize); + os << "]"; + break; + case WRITE: + os << "("; + PL_Print1(os, c[0], indentation, letize); + os << " WITH ["; + PL_Print1(os, c[1], indentation, letize); + os << "] := "; + PL_Print1(os, c[2], indentation, letize); + os << ")"; + os << endl; + break; + case BVUMINUS: + os << kind << "( "; + PL_Print1(os, c[0], indentation, letize); + os << ")"; + break; + case NOT: + os << "NOT("; + PL_Print1(os, c[0], indentation, letize); + os << ") " << endl; + break; + case BVNEG: + os << " ~("; + PL_Print1(os, c[0], indentation, letize); + os << ")"; + break; + case BVCONCAT: + os << "("; + PL_Print1(os, c[0], indentation, letize); + os << " @ "; + PL_Print1(os, c[1], indentation, letize); + os << ")" << endl; + break; + case BVOR: + os << "("; + PL_Print1(os, c[0], indentation, letize); + os << " | "; + PL_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVAND: + os << "("; + PL_Print1(os, c[0], indentation, letize); + os << " & "; + PL_Print1(os, c[1], indentation, letize); + os << ")"; + break; + case BVEXTRACT: + PL_Print1(os, c[0], indentation, letize); + os << "["; + os << GetUnsignedConst(c[1]); + os << ":"; + os << GetUnsignedConst(c[2]); + os << "]"; + break; + case BVLEFTSHIFT: + os << "("; + PL_Print1(os, c[0], indentation, letize); + os << " << "; + os << GetUnsignedConst(c[1]); + os << ")"; + break; + case BVRIGHTSHIFT: + os << "("; + PL_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; + PL_Print1(os, *it, indentation, letize); + } + os << ")" << endl; + break; + case ITE: + os << "IF("; + PL_Print1(os, c[0], indentation, letize); + os << ")" << endl; + os << "THEN "; + PL_Print1(os, c[1], indentation, letize); + os << endl << "ELSE "; + PL_Print1(os, c[2], indentation, letize); + os << endl << "ENDIF"; + break; + case BVLT: + case BVLE: + case BVGT: + case BVGE: + case BVXOR: + case BVNAND: + case BVNOR: + case BVXNOR: + os << kind << "("; + PL_Print1(os, c[0], indentation, letize); + os << ","; + PL_Print1(os, c[1], indentation, letize); + os << ")" << endl; + break; + case BVSLT: + os << "SBVLT" << "("; + PL_Print1(os, c[0], indentation, letize); + os << ","; + PL_Print1(os, c[1], indentation, letize); + os << ")" << endl; + break; + case BVSLE: + os << "SBVLE" << "("; + PL_Print1(os, c[0], indentation, letize); + os << ","; + PL_Print1(os, c[1], indentation, letize); + os << ")" << endl; + break; + case BVSGT: + os << "SBVGT" << "("; + PL_Print1(os, c[0], indentation, letize); + os << ","; + PL_Print1(os, c[1], indentation, letize); + os << ")" << endl; + break; + case BVSGE: + os << "SBVGE" << "("; + PL_Print1(os, c[0], indentation, letize); + os << ","; + PL_Print1(os, c[1], indentation, letize); + os << ")" << endl; + break; + case EQ: + PL_Print1(os,c[0], indentation, letize); + os << " = "; + PL_Print1(os, c[1], indentation, letize); + os << endl; + break; + case NEQ: + PL_Print1(os, c[0], indentation, letize); + os << " /= "; + PL_Print1(os, c[1], indentation, letize); + os << endl; + break; + case AND: + case OR: + case NAND: + case NOR: + case XOR: + { + os << "("; + PL_Print1(os, c[0], indentation, letize); + ASTVec::const_iterator it = c.begin(); + ASTVec::const_iterator itend = c.end(); + + it++; + for (; it != itend; it++) + { + os << " " << kind << " "; + PL_Print1(os, *it, indentation, letize); + os << endl; + } + os << ")"; + break; + } + case IFF: + os << "("; + os << "("; + PL_Print1(os, c[0], indentation, letize); + os << ")"; + os << " <=> "; + os << "("; + PL_Print1(os,c[1], indentation, letize); + os << ")"; + os << ")"; + os << endl; + break; + case IMPLIES: + os << "("; + os << "("; + PL_Print1(os, c[0], indentation, letize); + os << ")"; + os << " => "; + os << "("; + PL_Print1(os, c[1], indentation, letize); + os << ")"; + os << ")"; + os << endl; + break; + case BVSX: + case BVZX: + os << kind << "("; + PL_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("PL_Print1: printing not implemented for this kind: ", n); + break; + } +} //end of PL_Print1() + + +//print in PRESENTATION LANGUAGE +// +//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& PL_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(); + + //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 >::iterator it = bm.NodeLetVarVec.begin(); + std::vector >::iterator itend = bm.NodeLetVarVec.end(); + + os << "(LET "; + //print the let var first + PL_Print1(os, it->first, indentation, false); + os << " = "; + //print the expr + PL_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 + PL_Print1(os, it->first, indentation, false); + os << " = "; + //print the expr + PL_Print1(os, it->second, indentation, false); + + //update the second map for proper printing of LET + bm.NodeLetVarMap1[it->second] = it->first; + } + + os << " IN " << endl; + PL_Print1(os, n, indentation, true); + os << ") "; + } + else + PL_Print1(os,n, indentation, false); + //os << " )"; + os << " "; + return os; +} //end of PL_Print() +} diff --git a/src/AST/printer/printers.h b/src/AST/printer/printers.h index ae38669..a6c7d90 100644 --- a/src/AST/printer/printers.h +++ b/src/AST/printer/printers.h @@ -9,8 +9,13 @@ 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); +ostream& PL_Print(ostream &os, const BEEV::ASTNode& n, int indentation=0); + +ostream& Lisp_Print(ostream &os, const BEEV::ASTNode& n, int indentation=0); +ostream& Lisp_Print_indent(ostream &os, const BEEV::ASTNode& n,int indentation=0); } #endif /* PRINTERS_H_ */