From 51bd813c179e8c286362c5951b4db8a6d7b6c962 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 18 May 2010 13:44:32 +0000 Subject: [PATCH] A first attempt at an SMT-LIB2 output printer. I haven't tried to parse this so I'm not sure it's right. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@769 e59a4935-1847-0410-ae03-e826735625c1 --- src/STPManager/UserDefinedFlags.h | 2 + src/c_interface/c_interface.cpp | 2 +- src/main/main.cpp | 18 +- src/printer/SMTLIB1Printer.cpp | 231 ++++++++++++++ src/printer/SMTLIB2Printer.cpp | 225 ++++++++++++++ src/printer/SMTLIBPrinter.cpp | 489 +++++++++--------------------- src/printer/SMTLIBPrinter.h | 28 ++ src/printer/printers.h | 15 +- 8 files changed, 650 insertions(+), 360 deletions(-) create mode 100644 src/printer/SMTLIB1Printer.cpp create mode 100644 src/printer/SMTLIB2Printer.cpp create mode 100644 src/printer/SMTLIBPrinter.h diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h index d68a877..672759e 100644 --- a/src/STPManager/UserDefinedFlags.h +++ b/src/STPManager/UserDefinedFlags.h @@ -89,6 +89,7 @@ namespace BEEV bool print_STPinput_back_flag; bool print_STPinput_back_C_flag; bool print_STPinput_back_SMTLIB_flag; + bool print_STPinput_back_SMTLIB1_flag; bool print_STPinput_back_CVC_flag; bool print_STPinput_back_dot_flag; bool print_STPinput_back_GDL_flag; @@ -193,6 +194,7 @@ namespace BEEV print_STPinput_back_flag = false; print_STPinput_back_C_flag = false; print_STPinput_back_SMTLIB_flag = false; + print_STPinput_back_SMTLIB1_flag = false; print_STPinput_back_CVC_flag = false; print_STPinput_back_GDL_flag = false; print_STPinput_back_dot_flag = false; diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index ed18987..f1bc9f7 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -195,7 +195,7 @@ void vc_printExpr(VC vc, Expr e) { char * vc_printSMTLIB(VC vc, Expr e) { stringstream ss; - printer::SMTLIB_Print(ss,*((nodestar)e), 0); + printer::SMTLIB1_PrintBack(ss,*((nodestar)e)); string s = ss.str(); char *copy = strdup(s.c_str()); return copy; diff --git a/src/main/main.cpp b/src/main/main.cpp index b4fd069..b1f73f3 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -49,7 +49,7 @@ static const intptr_t INITIAL_MEMORY_PREALLOCATION_SIZE = 4000000; * step 5. Call SAT to determine if input is SAT or UNSAT ********************************************************************/ -typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER} OptionType; +typedef enum {PRINT_BACK_C=1, PRINT_BACK_CVC, PRINT_BACK_SMTLIB,PRINT_BACK_SMTLIB1, PRINT_BACK_GDL, PRINT_BACK_DOT, OUTPUT_BENCH, OUTPUT_CNF, USE_SIMPLIFYING_SOLVER} OptionType; int main(int argc, char ** argv) { char * infile; @@ -119,7 +119,9 @@ int main(int argc, char ** argv) { helpstring += "--print-back-CVC : print input in CVC format, then exit\n"; helpstring += - "--print-back-SMTLIB : print input in SMT-LIB format, then exit\n"; + "--print-back-SMTLIB : print input in SMT-LIB2 format, then exit\n"; + helpstring += + "--print-back-SMTLIB1 : print input in SMT-LIB1 format, then exit\n"; helpstring += "--print-back-GDL : print AiSee's graph format, then exit\n"; helpstring += @@ -156,6 +158,7 @@ int main(int argc, char ** argv) { lookup.insert(make_pair("--print-back-C",PRINT_BACK_C)); lookup.insert(make_pair("--print-back-CVC",PRINT_BACK_CVC)); lookup.insert(make_pair("--print-back-SMTLIB",PRINT_BACK_SMTLIB)); + lookup.insert(make_pair("--print-back-SMTLIB1",PRINT_BACK_SMTLIB1)); lookup.insert(make_pair("--print-back-GDL",PRINT_BACK_GDL)); lookup.insert(make_pair("--print-back-dot",PRINT_BACK_DOT)); lookup.insert(make_pair("--output-CNF",OUTPUT_CNF)); @@ -177,6 +180,10 @@ int main(int argc, char ** argv) { bm->UserFlags.print_STPinput_back_SMTLIB_flag = true; onePrintBack = true; break; + case PRINT_BACK_SMTLIB1: + bm->UserFlags.print_STPinput_back_SMTLIB1_flag = true; + onePrintBack = true; + break; case PRINT_BACK_GDL: bm->UserFlags.print_STPinput_back_GDL_flag = true; onePrintBack = true; @@ -404,9 +411,14 @@ int main(int argc, char ** argv) { print_STPInput_Back(query); } + if (bm->UserFlags.print_STPinput_back_SMTLIB1_flag) + { + printer::SMTLIB1_PrintBack(cout, original_input); + } + if (bm->UserFlags.print_STPinput_back_SMTLIB_flag) { - printer::SMTLIB_PrintBack(cout, original_input); + printer::SMTLIB2_PrintBack(cout, original_input); } if (bm->UserFlags.print_STPinput_back_C_flag) diff --git a/src/printer/SMTLIB1Printer.cpp b/src/printer/SMTLIB1Printer.cpp new file mode 100644 index 0000000..9a91d50 --- /dev/null +++ b/src/printer/SMTLIB1Printer.cpp @@ -0,0 +1,231 @@ +/******************************************************************** + * AUTHORS: Trevor Hansen, Vijay Ganesh + * + * BEGIN DATE: July, 2009 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- + +#include "printers.h" +#include +#include +#include "SMTLIBPrinter.h" + +// Outputs in the SMTLIB1 format. If you want something that can be parsed by other tools call +// SMTLIB_PrintBack(). SMTLIB_Print() prints just an expression. +// Wierdly is seems that only terms, not formulas can be LETized. + +// NB: This code doesn't include the substitution map. So if you've already simplified +// the graph, then solving what this prints out wont necessarily give you a model. + + +namespace printer +{ + using std::string; + using namespace BEEV; + + void SMTLIB1_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize); + void printSMTLIB1VarDeclsToStream(ASTNodeSet& symbols, ostream& os); + + void SMTLIB1_PrintBack(ostream &os, const ASTNode& n) +{ + os << "(" << endl; + os << "benchmark blah" << endl; + if (containsAnyArrayOps(n)) + os << ":logic QF_AUFBV" << endl; + else + os << ":logic QF_BV" << endl; + + + ASTNodeSet visited, symbols; + buildListOfSymbols(n, visited, symbols); + printSMTLIB1VarDeclsToStream(symbols, os); + os << ":formula "; + SMTLIB_Print(os, n, 0, &SMTLIB1_Print1); + os << ")" << endl; + } + +void printSMTLIB1VarDeclsToStream(ASTNodeSet& symbols, ostream& os) +{ + for (ASTNodeSet::const_iterator i = symbols.begin(), iend = symbols.end(); i + != iend; i++) + { + const BEEV::ASTNode& a = *i; + + // Should be a symbol. + assert(a.GetKind()== SYMBOL); + + switch (a.GetType()) + { + case BEEV::BITVECTOR_TYPE: + + os << ":extrafuns (( "; + a.nodeprint(os); + os << " BitVec[" << a.GetValueWidth() << "]"; + os << " ))" << endl; + break; + case BEEV::ARRAY_TYPE: + os << ":extrafuns (( "; + a.nodeprint(os); + os << " Array[" << a.GetIndexWidth(); + os << ":" << a.GetValueWidth() << "] ))" << endl; + break; + case BEEV::BOOLEAN_TYPE: + os << ":extrapreds (( "; + a.nodeprint(os); + os << "))" << endl; + break; + default: + BEEV::FatalError("printVarDeclsToStream: Unsupported type",a); + break; + } + } + } //printVarDeclsToStream + + void outputBitVec(const ASTNode n, ostream& os) + { + const 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.GetSTPMgr()->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 SMTLIB1_Print1(ostream& os, const ASTNode n, int indentation, bool letize) + { + //os << spaces(indentation); + //os << endl << spaces(indentation); + if (!n.IsDefined()) + { + FatalError(""); + return; + } + + //if this node is present in the letvar Map, then print the letvar + //this is to print letvars for shared subterms inside the printing + //of "(LET v0 = term1, v1=term1@term2,... + if ((NodeLetVarMap1.find(n) != NodeLetVarMap1.end()) && !letize) + { + SMTLIB1_Print1(os, (NodeLetVarMap1[n]), indentation, letize); + return; + } + + //this is to print letvars for shared subterms inside the actual + //term to be printed + if ((NodeLetVarMap.find(n) != NodeLetVarMap.end()) && letize) + { + SMTLIB1_Print1(os, (NodeLetVarMap[n]), indentation, letize); + return; + } + + //otherwise print it normally + const 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 NAND: // No NAND, NOR in smtlib format. + case NOR: + assert(c.size() ==2); + os << "(" << "not "; + if (NAND == kind ) + os << "(" << "and "; + else + os << "(" << "or "; + SMTLIB1_Print1(os, c[0], 0, letize); + os << " " ; + SMTLIB1_Print1(os, c[1], 0, letize); + os << "))"; + 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 - c[0].GetValueWidth()) << "]"; + SMTLIB1_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 << "] "; + SMTLIB1_Print1(os, c[0], indentation, letize); + os << ")"; + } + break; + default: + { + // SMT-LIB only allows these functions to have two parameters. + if ((BVPLUS == kind || kind == BVOR || kind == BVAND) && n.Degree() > 2) + { + string close = ""; + + for (int i =0; i < c.size()-1; i++) + { + os << "(" << functionToSMTLIBName(kind); + os << " "; + SMTLIB1_Print1(os, c[i], 0, letize); + os << " "; + close += ")"; + } + SMTLIB1_Print1(os, c[c.size()-1], 0, letize); + os << close; + } + else + { + os << "(" << functionToSMTLIBName(kind); + + ASTVec::const_iterator iend = c.end(); + for (ASTVec::const_iterator i = c.begin(); i != iend; i++) + { + os << " "; + SMTLIB1_Print1(os, *i, 0, letize); + } + + os << ")"; + } + } + } + } +} diff --git a/src/printer/SMTLIB2Printer.cpp b/src/printer/SMTLIB2Printer.cpp new file mode 100644 index 0000000..aa39757 --- /dev/null +++ b/src/printer/SMTLIB2Printer.cpp @@ -0,0 +1,225 @@ +/******************************************************************** + * AUTHORS: Trevor Hansen, Vijay Ganesh + * + * BEGIN DATE: July, 2009 + * + * LICENSE: Please view LICENSE file in the home dir of this Program + ********************************************************************/ +// -*- c++ -*- + +#include "printers.h" +#include +#include +#include "SMTLIBPrinter.h" + +// Outputs in the SMTLIB format. If you want something that can be parsed by other tools call +// SMTLIB_PrintBack(). SMTLIB_Print() prints just an expression. +// Wierdly is seems that only terms, not formulas can be LETized. + +namespace printer +{ + + using std::string; + using namespace BEEV; + + void SMTLIB2_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize); + void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os); + +void SMTLIB2_PrintBack(ostream &os, const ASTNode& n) +{ + if (containsAnyArrayOps(n)) + os << "(set-logic QF_AUFBV)" << endl; + else + os << "(set-logic QF_BV)"<< endl; + + os << "(set-info :smt-lib-version 2.0)"<< endl; + os << "(set-info :status unknown)"<< endl; + + ASTNodeSet visited, symbols; + buildListOfSymbols(n, visited, symbols); + printVarDeclsToStream(symbols, os); + os << "(assert "; + SMTLIB_Print(os, n, 0, &SMTLIB2_Print1); + os << ")" << endl; + os << "(check-sat)" << endl; + os << "(exit)" << endl; + } + +void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os) +{ + for (ASTNodeSet::const_iterator i = symbols.begin(), iend = symbols.end(); i + != iend; i++) + { + const BEEV::ASTNode& a = *i; + os << "(declare-fun "; + + // Should be a symbol. + assert(a.GetKind()== SYMBOL); + a.nodeprint(os); + os << " () ("; + + switch (a.GetType()) + { + case BEEV::BITVECTOR_TYPE: + os << "_ BitVec " << a.GetValueWidth() << ")"; + break; + case BEEV::ARRAY_TYPE: + os << "Array (_ BitVec " << a.GetIndexWidth() << ") (_BitVec " << a.GetValueWidth() << ") )"; + break; + case BEEV::BOOLEAN_TYPE: + os << " Bool "; + break; + default: + BEEV::FatalError("printVarDeclsToStream: Unsupported type",a); + break; + } + os << ")\n"; + } + } //printVarDeclsToStream + + void outputBitVecSMTLIB2(const ASTNode n, ostream& os) + { + const 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.GetSTPMgr()->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 SMTLIB2_Print1(ostream& os, const ASTNode n, int indentation, bool letize) + { + //os << spaces(indentation); + //os << endl << spaces(indentation); + if (!n.IsDefined()) + { + FatalError(""); + return; + } + + //if this node is present in the letvar Map, then print the letvar + //this is to print letvars for shared subterms inside the printing + //of "(LET v0 = term1, v1=term1@term2,... + if ((NodeLetVarMap1.find(n) != NodeLetVarMap1.end()) && !letize) + { + SMTLIB2_Print1(os, (NodeLetVarMap1[n]), indentation, letize); + return; + } + + //this is to print letvars for shared subterms inside the actual + //term to be printed + if ((NodeLetVarMap.find(n) != NodeLetVarMap.end()) && letize) + { + SMTLIB2_Print1(os, (NodeLetVarMap[n]), indentation, letize); + return; + } + + //otherwise print it normally + const Kind kind = n.GetKind(); + const ASTVec &c = n.GetChildren(); + switch (kind) + { + case BITVECTOR: + case BVCONST: + outputBitVecSMTLIB2(n, os); + break; + case SYMBOL: + n.nodeprint(os); + break; + case FALSE: + os << "false"; + break; + case NAND: // No NAND, NOR in smtlib format. + case NOR: + assert(c.size() ==2); + os << "(" << "not "; + if (NAND == kind ) + os << "(" << "and "; + else + os << "(" << "or "; + SMTLIB2_Print1(os, c[0], 0, letize); + os << " " ; + SMTLIB2_Print1(os, c[1], 0, letize); + os << "))"; + 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 - c[0].GetValueWidth()) << ") "; + SMTLIB2_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 << ") "; + SMTLIB2_Print1(os, c[0], indentation, letize); + os << ")"; + } + break; + default: + { + // SMT-LIB only allows these functions to have two parameters. + if ((BVPLUS == kind || kind == BVOR || kind == BVAND) && n.Degree() > 2) + { + string close = ""; + + for (int i =0; i < c.size()-1; i++) + { + os << "(" << functionToSMTLIBName(kind); + os << " "; + SMTLIB2_Print1(os, c[i], 0, letize); + os << " "; + close += ")"; + } + SMTLIB2_Print1(os, c[c.size()-1], 0, letize); + os << close; + } + else + { + os << "(" << functionToSMTLIBName(kind); + + ASTVec::const_iterator iend = c.end(); + for (ASTVec::const_iterator i = c.begin(); i != iend; i++) + { + os << " "; + SMTLIB2_Print1(os, *i, 0, letize); + } + + os << ")"; + } + } + } + } +} diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp index cfe345a..88c9dc3 100644 --- a/src/printer/SMTLIBPrinter.cpp +++ b/src/printer/SMTLIBPrinter.cpp @@ -1,378 +1,168 @@ -/******************************************************************** - * AUTHORS: Trevor Hansen, Vijay Ganesh - * - * BEGIN DATE: July, 2009 - * - * LICENSE: Please view LICENSE file in the home dir of this Program - ********************************************************************/ -// -*- c++ -*- - #include "printers.h" -#include -#include +#include "SMTLIBPrinter.h" -// Outputs in the SMTLIB format. If you want something that can be parsed by other tools call -// SMTLIB_PrintBack(). SMTLIB_Print() prints just an expression. -// Wierdly is seems that only terms, not formulas can be LETized. +// Functions used by both the version1 and version2 STMLIB printers. namespace printer { +using namespace BEEV; - 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 printVarDeclsToStream(ASTNodeSet& symbols, ostream& os); - + //Map from ASTNodes to LetVars + BEEV::ASTNodeMap NodeLetVarMap; - static string tolower(const char * name) - { - string s(name); - for (size_t i = 0; i < s.size(); ++i) - s[i] = ::tolower(s[i]); - return s; - } - -//Map from ASTNodes to LetVars -ASTNodeMap NodeLetVarMap; + //This is a vector which stores the Node to LetVars pairs. It + //allows for sorted printing, as opposed to NodeLetVarMap + std::vector > NodeLetVarVec; -//This is a vector which stores the Node to LetVars pairs. It -//allows for sorted printing, as opposed to NodeLetVarMap -std::vector > NodeLetVarVec; + //a partial Map from ASTNodes to LetVars. Needed in order to + //correctly print shared subterms inside the LET itself + BEEV::ASTNodeMap NodeLetVarMap1; -//a partial Map from ASTNodes to LetVars. Needed in order to -//correctly print shared subterms inside the LET itself -ASTNodeMap NodeLetVarMap1; + bool containsAnyArrayOps(const ASTNode& n) + { + return true; + } - // Initial version intended to print the whole thing back. -void SMTLIB_PrintBack(ostream &os, const ASTNode& n) -{ - os << "(" << endl; - os << "benchmark blah" << endl; - os << ":logic QF_AUFBV" << endl; - ASTNodeSet visited, symbols; - buildListOfSymbols(n, visited, symbols); - printVarDeclsToStream(symbols, os); - os << ":formula "; - SMTLIB_Print(os, n, 0); - os << ")" << endl; - } -void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os) -{ - for (ASTNodeSet::const_iterator i = symbols.begin(), iend = symbols.end(); i - != iend; i++) + static string tolower(const char * name) { - const BEEV::ASTNode& a = *i; + string s(name); + for (size_t i = 0; i < s.size(); ++i) + s[i] = ::tolower(s[i]); + return s; + } - // Should be a symbol. - assert(a.GetKind()== SYMBOL); + // copied from Presentation Langauge printer. + ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation, void (*SMTLIB1_Print1)(ostream&, const ASTNode , int , bool )) + { + // Clear the maps + NodeLetVarMap.clear(); + NodeLetVarVec.clear(); + NodeLetVarMap1.clear(); - switch (a.GetType()) + //pass 1: letize the node { - case BEEV::BITVECTOR_TYPE: - - os << ":extrafuns (( "; - a.nodeprint(os); - os << " BitVec[" << a.GetValueWidth() << "]"; - os << " ))" << endl; - break; - case BEEV::ARRAY_TYPE: - os << ":extrafuns (( "; - a.nodeprint(os); - os << " Array[" << a.GetIndexWidth(); - os << ":" << a.GetValueWidth() << "] ))" << endl; - break; - case BEEV::BOOLEAN_TYPE: - os << ":extrapreds (( "; - a.nodeprint(os); - os << "))" << endl; - break; - default: - BEEV::FatalError("printVarDeclsToStream: Unsupported type",a); - break; - } - } - } //printVarDeclsToStream - - void outputBitVec(const ASTNode n, ostream& os) - { - const 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.GetSTPMgr()->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 << ""; - return; - } - - //if this node is present in the letvar Map, then print the letvar - //this is to print letvars for shared subterms inside the printing - //of "(LET v0 = term1, v1=term1@term2,... - if ((NodeLetVarMap1.find(n) != NodeLetVarMap1.end()) && !letize) - { - SMTLIB_Print1(os, (NodeLetVarMap1[n]), indentation, letize); - return; - } - - //this is to print letvars for shared subterms inside the actual - //term to be printed - if ((NodeLetVarMap.find(n) != NodeLetVarMap.end()) && letize) - { - SMTLIB_Print1(os, (NodeLetVarMap[n]), indentation, letize); - return; - } - - //otherwise print it normally - const 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 NAND: // No NAND, NOR in smtlib format. - case NOR: - assert(c.size() ==2); - os << "(" << "not "; - if (NAND == kind ) - os << "(" << "and "; - else - os << "(" << "or "; - SMTLIB_Print1(os, c[0], 0, letize); - os << " " ; - SMTLIB_Print1(os, c[1], 0, letize); - os << "))"; - 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 - c[0].GetValueWidth()) << "]"; - 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: - { - // SMT-LIB only allows these functions to have two parameters. - if ((BVPLUS == kind || kind == BVOR || kind == BVAND) && n.Degree() > 2) - { - string close = ""; - - for (int i =0; i < c.size()-1; i++) - { - os << "(" << functionToSMTLIBName(kind); - os << " "; - SMTLIB_Print1(os, c[i], 0, letize); - os << " "; - close += ")"; - } - SMTLIB_Print1(os, c[c.size()-1], 0, letize); - os << close; - } - else - { - 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); - } + ASTNodeSet PLPrintNodeSet; + LetizeNode(n, PLPrintNodeSet); + } - os << ")"; - } - } - } - } + //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 < NodeLetVarMap.size()) + { + std::vector >::iterator it = + NodeLetVarVec.begin(); + const std::vector >::iterator itend = + NodeLetVarVec.end(); -void LetizeNode(const ASTNode& n, ASTNodeSet& PLPrintNodeSet) -{ - const Kind kind = n.GetKind(); + os << "(let ("; + //print the let var first + SMTLIB1_Print1(os, it->first, indentation, false); + os << " "; + //print the expr + SMTLIB1_Print1(os, it->second, indentation, false); + os << " )"; - if (kind == SYMBOL || kind == BVCONST || kind == FALSE || kind == TRUE) - return; + //update the second map for proper printing of LET + NodeLetVarMap1[it->second] = it->first; - const ASTVec &c = n.GetChildren(); - for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) + string closing = ""; + for (it++; it != itend; it++) + { + os << " " << endl; + os << "(let ("; + //print the let var first + SMTLIB1_Print1(os, it->first, indentation, false); + os << " "; + //print the expr + SMTLIB1_Print1(os, it->second, indentation, false); + os << ")"; + //update the second map for proper printing of LET + NodeLetVarMap1[it->second] = it->first; + closing += ")"; + } + + os << " ( " << endl; + SMTLIB1_Print1(os, n, indentation, true); + os << closing; + os << " ) ) "; + + } + else + SMTLIB1_Print1(os, n, indentation, false); + + os << endl; + return os; + } + + void LetizeNode(const ASTNode& n, ASTNodeSet& PLPrintNodeSet) { - const ASTNode& ccc = *it; + const Kind kind = n.GetKind(); - const Kind k = ccc.GetKind(); - if (k == SYMBOL || k == BVCONST || k == FALSE || k == TRUE) - continue; + if (kind == SYMBOL || kind == BVCONST || kind == FALSE || kind == TRUE) + return; - if (PLPrintNodeSet.find(ccc) == PLPrintNodeSet.end()) + const ASTVec &c = n.GetChildren(); + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) { - //If branch: if *it is not in NodeSet then, - // - //1. add it to NodeSet - // - //2. Letize its childNodes - PLPrintNodeSet.insert(ccc); - LetizeNode(ccc, PLPrintNodeSet); - } - else - { - //0. Else branch: Node has been seen before - // - //1. Check if the node has a corresponding letvar in the - //1. NodeLetVarMap. - // - //2. if no, then create a new var and add it to the - //2. NodeLetVarMap - if (ccc.GetType() == BITVECTOR_TYPE && NodeLetVarMap.find(ccc) - == NodeLetVarMap.end()) - { - //Create a new symbol. Get some name. if it conflicts with a - //declared name, too bad. - int sz = NodeLetVarMap.size(); - ostringstream oss; - oss << "?let_k_" << sz; + const ASTNode& ccc = *it; - ASTNode CurrentSymbol = n.GetSTPMgr()->CreateSymbol( - oss.str().c_str()); - CurrentSymbol.SetValueWidth(n.GetValueWidth()); - CurrentSymbol.SetIndexWidth(n.GetIndexWidth()); - /* If for some reason the variable being created here is - * already declared by the user then the printed output will - * not be a legal input to the system. too bad. I refuse to - * check for this. [Vijay is the author of this comment.] - */ + const Kind k = ccc.GetKind(); + if (k == SYMBOL || k == BVCONST || k == FALSE || k == TRUE) + continue; - NodeLetVarMap[ccc] = CurrentSymbol; - std::pair - node_letvar_pair(CurrentSymbol, ccc); - NodeLetVarVec.push_back(node_letvar_pair); + if (PLPrintNodeSet.find(ccc) == PLPrintNodeSet.end()) + { + //If branch: if *it is not in NodeSet then, + // + //1. add it to NodeSet + // + //2. Letize its childNodes + PLPrintNodeSet.insert(ccc); + LetizeNode(ccc, PLPrintNodeSet); + } + else + { + //0. Else branch: Node has been seen before + // + //1. Check if the node has a corresponding letvar in the + //1. NodeLetVarMap. + // + //2. if no, then create a new var and add it to the + //2. NodeLetVarMap + if (ccc.GetType() == BITVECTOR_TYPE && NodeLetVarMap.find(ccc) + == NodeLetVarMap.end()) + { + //Create a new symbol. Get some name. if it conflicts with a + //declared name, too bad. + int sz = NodeLetVarMap.size(); + ostringstream oss; + oss << "?let_k_" << sz; + + ASTNode CurrentSymbol = n.GetSTPMgr()->CreateSymbol( + oss.str().c_str()); + CurrentSymbol.SetValueWidth(n.GetValueWidth()); + CurrentSymbol.SetIndexWidth(n.GetIndexWidth()); + /* If for some reason the variable being created here is + * already declared by the user then the printed output will + * not be a legal input to the system. too bad. I refuse to + * check for this. [Vijay is the author of this comment.] + */ + + NodeLetVarMap[ccc] = CurrentSymbol; + std::pair + node_letvar_pair(CurrentSymbol, ccc); + NodeLetVarVec.push_back(node_letvar_pair); + } } } - } -} //end of LetizeNode() - - // copied from Presentation Langauge printer. - ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation) - { - // Clear the maps - NodeLetVarMap.clear(); - NodeLetVarVec.clear(); - NodeLetVarMap1.clear(); - - //pass 1: letize the node - { - ASTNodeSet PLPrintNodeSet; - LetizeNode(n, PLPrintNodeSet); - } - - //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 < NodeLetVarMap.size()) - { - std::vector >::iterator it = - NodeLetVarVec.begin(); - const std::vector >::iterator itend = - 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); - os << " )"; - - //update the second map for proper printing of LET - NodeLetVarMap1[it->second] = it->first; - - string closing = ""; - for (it++; it != itend; it++) - { - os << " " << endl; - 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); - os << ")"; - //update the second map for proper printing of LET - NodeLetVarMap1[it->second] = it->first; - closing += ")"; - } - - os << " ( " << endl; - SMTLIB_Print1(os, n, indentation, true); - os << closing; - os << " ) ) "; - - } - else - SMTLIB_Print1(os, n, indentation, false); - - os << endl; - return os; - } + } //end of LetizeNode() string functionToSMTLIBName(const Kind k) { @@ -448,5 +238,4 @@ void LetizeNode(const ASTNode& n, ASTNodeSet& PLPrintNodeSet) } } } - -} +}; diff --git a/src/printer/SMTLIBPrinter.h b/src/printer/SMTLIBPrinter.h new file mode 100644 index 0000000..182cf90 --- /dev/null +++ b/src/printer/SMTLIBPrinter.h @@ -0,0 +1,28 @@ +#ifndef SMTLIBPRINTERS_H_ +#define SMTLIBPRINTERS_H_ + +#include "printers.h" + +namespace printer +{ + + //Map from ASTNodes to LetVars + extern BEEV::ASTNodeMap NodeLetVarMap; + + //This is a vector which stores the Node to LetVars pairs. It + //allows for sorted printing, as opposed to NodeLetVarMap + extern std::vector > NodeLetVarVec; + + //a partial Map from ASTNodes to LetVars. Needed in order to + //correctly print shared subterms inside the LET itself + extern BEEV::ASTNodeMap NodeLetVarMap1; + + string functionToSMTLIBName(const Kind k); + + void LetizeNode(const ASTNode& n, BEEV::ASTNodeSet& PLPrintNodeSet); + + ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation, void (*SMTLIB_Print1)(ostream&, const ASTNode , int , bool )); + + bool containsAnyArrayOps(const ASTNode& n); +}; +#endif diff --git a/src/printer/printers.h b/src/printer/printers.h index d51e5f4..cd66294 100644 --- a/src/printer/printers.h +++ b/src/printer/printers.h @@ -1,5 +1,5 @@ /******************************************************************** - * AUTHORS: Vijay Ganesh + * AUTHORS: Vijay Ganesh, Trevor Hansen * * BEGIN DATE: November, 2005 * @@ -17,14 +17,11 @@ #include "../AST/ASTKind.h" #include "../STPManager/STP.h" -//using namespace std; 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, + 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); @@ -33,9 +30,15 @@ namespace printer const BEEV::ASTNode& n, int indentation=0); ostream& Lisp_Print_indent(ostream &os, const BEEV::ASTNode& n,int indentation=0); - void SMTLIB_PrintBack(ostream &os, + + // The "PrintBack" functions also define all the variables that are used. + void SMTLIB1_PrintBack(ostream &os, + const BEEV::ASTNode& n ); + + void SMTLIB2_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&)); -- 2.47.3