From abb4b2fac339de9aac626cf023b1026ec9be0fdb Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 22 Feb 2010 11:49:47 +0000 Subject: [PATCH] * The bench printer prints out bitblasted formula which can be loaded by the ABC logic synthesis tool. * The GDL printer prints out graphs which can be laid out by aiSee3. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@616 e59a4935-1847-0410-ae03-e826735625c1 --- src/printer/BenchPrinter.cpp | 180 +++++++++++++++++++++++++++++++++++ src/printer/GDLPrinter.cpp | 126 ++++++++++++++++++++++++ src/printer/printers.h | 4 + 3 files changed, 310 insertions(+) create mode 100644 src/printer/BenchPrinter.cpp create mode 100644 src/printer/GDLPrinter.cpp diff --git a/src/printer/BenchPrinter.cpp b/src/printer/BenchPrinter.cpp new file mode 100644 index 0000000..098d6dc --- /dev/null +++ b/src/printer/BenchPrinter.cpp @@ -0,0 +1,180 @@ +#include "printers.h" +#include +#include "ASTKind.h" + +/* + * Bench format which the ABC logic synthesis tool can read. + * No more than 2-arity seem to be accepted. + */ + +namespace printer +{ +using std::string; +using namespace BEEV; + +string name(const Kind k) +{ + return _kind_names[k]; +} + +string bvconstToString(const ASTNode& n) +{ + assert (n.GetKind() == BVCONST); + std::stringstream output; + output << *n.GetBVConst(); + return output.str(); +} + +// ABC doesn't like spaces, nor brackets. in variable names. +// TODO CHECK that this doesn't cause duplicate names +string symbolToString(const ASTNode &n) +{ + assert(n.GetKind() == SYMBOL); + std::stringstream output; + n.nodeprint(output); + + string result = output.str(); + replace(result.begin(), result.end(), ' ', '_'); + replace(result.begin(), result.end(), '(', '_'); + replace(result.begin(), result.end(), ')', '_'); + + return result; + +} + +string Bench_Print1(ostream &os, const ASTNode& n, hash_set *alreadyOutput) +{ + if (n.GetValueWidth() > 1 && (n.GetKind() != SYMBOL)) + { + // some of the nodes have a width of zero (oddly), but they are probably ok. + cerr << "width" << n.GetValueWidth(); + cerr << n; + assert(n.GetValueWidth() == 1); + } + + assert(!n.IsNull()); + + std::stringstream output; + if (n.GetKind() == BVCONST) + return bvconstToString(n); + + if (n.GetKind() == SYMBOL) + return symbolToString(n); + + if (n.GetKind() == BVGETBIT) + { + assert(n[1].GetKind() == BVCONST); + std::stringstream nn; + nn << Bench_Print1(os, n[0], alreadyOutput) << "_" << bvconstToString( + n[1]); + return nn.str(); + } + + std::stringstream thisNode; + thisNode << "n" << n.GetNodeNum(); + + if (alreadyOutput->find(n.GetNodeNum()) != alreadyOutput->end()) + return thisNode.str(); + + alreadyOutput->insert(n.GetNodeNum()); + + assert(n.Degree() > 0); + + // The bench format doesn't accept propositional ITEs. + if (n.GetKind() == ITE) + { + assert(n.Degree() == 3); + string p = Bench_Print1(os, n[0], alreadyOutput); + string p1 = Bench_Print1(os, n[1], alreadyOutput); + string p2 = Bench_Print1(os, n[2], alreadyOutput); + + os << thisNode.str() << "_1 = AND(" << p << "," << p1 << ")" << endl; + os << thisNode.str() << "_2" << " = NOT(" << p << ")," << endl; + os << thisNode.str() << "_3" << " = AND(" << thisNode.str() << "_2" + << "," << p2 << ")" << endl; + os << thisNode.str() << "=" << "OR(," << thisNode.str() << "_1" << "," + << thisNode.str() << "_3)" << endl; + } + else + { + if (n.Degree() > 2) + { + if(n.GetKind() != AND && n.GetKind() != XOR && n.GetKind() != OR) // must be associative. + { + cerr << name(n.GetKind()); + } + + output << thisNode.str() << "_1" << "=" << name(n.GetKind()) << "(" << Bench_Print1(os, n[0], alreadyOutput) + << "," << Bench_Print1(os, n[1], alreadyOutput) << ")" << endl; + + + for (unsigned i = 2; i < n.Degree()-1/*note minus one.*/; i++) + { + output << thisNode.str() << "_" << i << "=" << name(n.GetKind()) << "(" << Bench_Print1(os, n[i], alreadyOutput) + << "," << thisNode.str() << "_" << (i-1) << ")" << endl; + } + + output << thisNode.str() << "=" << name(n.GetKind()) << "(" << Bench_Print1(os, n[n.Degree()-1], alreadyOutput) + << "," << thisNode.str() << "_" << (n.Degree()-2) << ")" << endl; + + os << output.str(); + } + else + { + output << thisNode.str() << "=" << name(n.GetKind()) << "("; + for (unsigned i = 0; i < n.Degree(); i++) + { + if (i >= 1) + output << " , "; + output << Bench_Print1(os, n[i], alreadyOutput); + + } + os << output.str() << ")" << endl; + } + } + return thisNode.str(); +} + +void OutputInputs(ostream &os, const ASTNode& n, hash_set *alreadyOutput) +{ + if (alreadyOutput->find(n.GetNodeNum()) != alreadyOutput->end()) + return; + + alreadyOutput->insert(n.GetNodeNum()); + + if (n.GetKind() == BVGETBIT) + { + assert(n[1].GetKind() == BVCONST); + std::stringstream nn; + n[0].nodeprint(nn); + nn << "_" << bvconstToString(n[1]); + os << "INPUT(" << nn.str() << ")" << endl; + return; + } + + // A boolean symbol. + if (n.GetKind() == SYMBOL) + { + os << "INPUT(" << symbolToString(n) << ")" << endl; + return; + } + + for (unsigned i = 0; i < n.Degree(); i++) + { + OutputInputs(os, n[i], alreadyOutput); + } +} + +ostream& Bench_Print(ostream &os, const ASTNode n) +{ + hash_set alreadyOutput; + + OutputInputs(os, n, &alreadyOutput); + alreadyOutput.clear(); + + os << "OUTPUT(" << "n" << n.GetNodeNum() << ")" << endl; + string top = Bench_Print1(os, n, &alreadyOutput); + return os; +} +} +; diff --git a/src/printer/GDLPrinter.cpp b/src/printer/GDLPrinter.cpp new file mode 100644 index 0000000..f84d963 --- /dev/null +++ b/src/printer/GDLPrinter.cpp @@ -0,0 +1,126 @@ +// Outputs in the Graph Description Langauge format (GDL) +// can be laid out by the graph layout tool: aiSee. + +// todo: this contains only small differences to the dotprinter.cpp. they should be merged. + +/******************************************************************** + * AUTHORS: Trevor Hansen + * + * BEGIN DATE: November, 2005 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- + +#include "printers.h" +#include + +namespace printer +{ + + using std::string; + using namespace BEEV; + + void outputBitVec(const ASTNode n, ostream& os); + + void GDL_Print1(ostream &os, const ASTNode& n, hash_set *alreadyOutput, string (*annotate)(const ASTNode&)) + { + // check if this node has already been printed. If so return. + if (alreadyOutput->find(n.GetNodeNum()) != alreadyOutput->end()) + return; + + alreadyOutput->insert(n.GetNodeNum()); + + os << "node: { title:\"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 << annotate(n); + 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++) + { + std::stringstream label; + + if (!isCommutative(n.GetKind())) + label << " label:\"" << i << "\""; + + + if (it->isConstant()) + { + std::stringstream ss; + os << "node: { title:\"n"; + ss << n.GetNodeNum() << "_" << it->GetNodeNum(); + + os << ss.str() << "\" label: \""; + if (it->GetType() == BEEV::BOOLEAN_TYPE) + os << _kind_names[it->GetKind()]; + else + outputBitVec(*it, os); + os << "\"}" << endl; + + os << "edge: { source:\"n" << n.GetNodeNum() << "\" target: \"" << "n" << ss.str() << "\"" << label.str() << "}" << endl; + } + else + os << "edge: { source:\"n" << n.GetNodeNum() << "\" target: \"" << "n" << it->GetNodeNum() << "\"" << label.str() << "}" << endl; + i++; + } + + // print each of the children. + for (ASTVec::iterator it = ch.begin(); it < itend; it++) + { + if (!it->isConstant()) + GDL_Print1(os, *it, alreadyOutput,annotate); + } + } + + + string empty(const ASTNode& n) + { + return ""; + } + + + + ostream& GDL_Print(ostream &os, const ASTNode n, string (*annotate)(const ASTNode&)) + { + + os << "graph: {" << endl; + os << "splines: yes" << endl; + os << "layoutalgorithm: dfs" << endl; + os << "display_edge_labels: yes" << endl; + + + // create hashmap to hold integers (node numbers). + hash_set alreadyOutput; + + GDL_Print1(os, n, &alreadyOutput,annotate);; + + os << "}" << endl; + + return os; + } + + ostream& GDL_Print(ostream &os, const ASTNode n) + { + return GDL_Print(os,n,empty); + } + +} diff --git a/src/printer/printers.h b/src/printer/printers.h index 8230bef..d51e5f4 100644 --- a/src/printer/printers.h +++ b/src/printer/printers.h @@ -36,6 +36,10 @@ namespace printer void SMTLIB_PrintBack(ostream &os, const BEEV::ASTNode& n ); + ostream& GDL_Print(ostream &os, const BEEV::ASTNode n); + ostream& GDL_Print(ostream &os, const ASTNode n, string (*annotate)(const ASTNode&)); + + ostream& Bench_Print(ostream &os, const ASTNode n); } #endif /* PRINTERS_H_ */ -- 2.47.3