From cdfe5983777460fada2fbc257174e55e63e3d75f Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 14 Mar 2010 03:04:56 +0000 Subject: [PATCH] * When printing in CVC format, traverse the nodes looking for symbols rather than using just the symbols that were parsed in. This makes it easier when converting from one format to another. * Fix the SMTLIB printer, convert NAND to NOT(AND(.., typo on extrapred, convert pluses with >2 arguments into nested 2 argument pluses. * Bugfix. Call print-back with the correct input function. Note. GDL print-back isn't printing out the entire input expression. I'm not sure why. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@642 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/AST.h | 3 +- src/AST/ASTmisc.cpp | 16 +++++++ src/STPManager/STPManager.h | 2 +- src/main/main.cpp | 14 ++++-- src/printer/AssortedPrinters.cpp | 17 +++++--- src/printer/GDLPrinter.cpp | 8 ++-- src/printer/SMTLIBPrinter.cpp | 73 ++++++++++++++++++-------------- 7 files changed, 87 insertions(+), 46 deletions(-) diff --git a/src/AST/AST.h b/src/AST/AST.h index 09e5446..ac9e829 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -27,7 +27,6 @@ namespace BEEV bool isAtomic(Kind k); bool isCommutative(const Kind k); - // If (a > b) in the termorder, then return 1 elseif (a < b) in the // termorder, then return -1 else return 0 int TermOrder(const ASTNode& a, const ASTNode& b); @@ -104,5 +103,7 @@ namespace BEEV // Function to dump contents of ASTNodeMap ostream &operator<<(ostream &os, const ASTNodeMap &nmap); + + void buildListOfSymbols(const ASTNode& n, ASTNodeSet& visited,ASTNodeSet& symbols); }; // end namespace BEEV #endif diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp index 1f6b9af..b700eb5 100644 --- a/src/AST/ASTmisc.cpp +++ b/src/AST/ASTmisc.cpp @@ -112,6 +112,22 @@ namespace BEEV return true; } + void buildListOfSymbols(const ASTNode& n, ASTNodeSet& visited, + ASTNodeSet& symbols) + { + if (visited.find(n) != visited.end()) + return; // already visited. + + visited.insert(n); + + if (n.GetKind() == SYMBOL) + { + symbols.insert(n); + } + + for (unsigned i = 0; i < n.GetChildren().size(); i++) + buildListOfSymbols(n[i], visited, symbols); + } /* FUNCTION: Typechecker for terms and formulas diff --git a/src/STPManager/STPManager.h b/src/STPManager/STPManager.h index c5a53b1..dc34c20 100644 --- a/src/STPManager/STPManager.h +++ b/src/STPManager/STPManager.h @@ -371,7 +371,7 @@ namespace BEEV void ASTNodeStats(const char * c, const ASTNode& a); // Print variable to the input stream - void printVarDeclsToStream(ostream &os); + void printVarDeclsToStream(ostream &os, ASTNodeSet& symbols); // Print assertions to the input stream void printAssertsToStream(ostream &os, int simplify); diff --git a/src/main/main.cpp b/src/main/main.cpp index d1615b6..251add5 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -344,6 +344,11 @@ int main(int argc, char ** argv) { if (onePrintBack) { + ASTNode original_input = bm->CreateNode(AND, + bm->CreateNode(NOT, query), + asserts); + + if(bm->UserFlags.print_STPinput_back_flag) { if(bm->UserFlags.smtlib_parser_flag) @@ -354,27 +359,28 @@ int main(int argc, char ** argv) { if (bm->UserFlags.print_STPinput_back_CVC_flag) { + //needs just the query. Reads the asserts out of the data structure. print_STPInput_Back(query); } if (bm->UserFlags.print_STPinput_back_SMTLIB_flag) { - printer::SMTLIB_PrintBack(cout, asserts); + printer::SMTLIB_PrintBack(cout, original_input); } if (bm->UserFlags.print_STPinput_back_C_flag) { - printer::C_Print(cout, asserts); + printer::C_Print(cout, original_input); } if (bm->UserFlags.print_STPinput_back_GDL_flag) { - printer::GDL_Print(cout, asserts); + printer::GDL_Print(cout, original_input); } if (bm->UserFlags.print_STPinput_back_dot_flag) { - printer::Dot_Print(cout, asserts); + printer::Dot_Print(cout, original_input); } return 0; diff --git a/src/printer/AssortedPrinters.cpp b/src/printer/AssortedPrinters.cpp index d332bbf..4bd690a 100644 --- a/src/printer/AssortedPrinters.cpp +++ b/src/printer/AssortedPrinters.cpp @@ -86,8 +86,8 @@ namespace BEEV // cout << endl; // } //end of Convert_MINISATVar_To_ASTNode_Print() - void STPMgr::printVarDeclsToStream(ostream &os) { - for(ASTVec::iterator + void STPMgr::printVarDeclsToStream(ostream &os, ASTNodeSet& ListOfDeclaredVars) { + for(ASTNodeSet::iterator i = ListOfDeclaredVars.begin(),iend=ListOfDeclaredVars.end(); i!=iend;i++) { @@ -113,8 +113,6 @@ namespace BEEV } } //printVarDeclsToStream - - void STPMgr::printAssertsToStream(ostream &os, int simplify_print) { ASTVec v = GetAsserts(); for(ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++) { @@ -130,7 +128,16 @@ namespace BEEV } void print_STPInput_Back(const ASTNode& query) { - (BEEV::GlobalSTP->bm)->printVarDeclsToStream(cout); + + // Determine the symbols in the query and asserts. + ASTNodeSet visited; + ASTNodeSet symbols; + buildListOfSymbols(query, visited, symbols); + ASTVec v = (BEEV::GlobalSTP->bm)->GetAsserts(); + for(ASTVec::iterator i=v.begin(),iend=v.end();i!=iend;i++) + buildListOfSymbols(*i, visited, symbols); + + (BEEV::GlobalSTP->bm)->printVarDeclsToStream(cout, symbols); (BEEV::GlobalSTP->bm)->printAssertsToStream(cout,0); cout << "QUERY("; query.PL_Print(cout); diff --git a/src/printer/GDLPrinter.cpp b/src/printer/GDLPrinter.cpp index 4ec51f3..89e4c3e 100644 --- a/src/printer/GDLPrinter.cpp +++ b/src/printer/GDLPrinter.cpp @@ -51,14 +51,14 @@ namespace printer os << "\"}" << endl; // print the edges to each child. - ASTVec ch = n.GetChildren(); - ASTVec::iterator itend = ch.end(); + const ASTVec ch = n.GetChildren(); + const ASTVec::const_iterator itend = ch.end(); //If a node has the child 'TRUE' twice, we only want to output one TRUE node. ASTNodeSet constantOutput; int i =0; - for (ASTVec::iterator it = ch.begin(); it < itend; it++) + for (ASTVec::const_iterator it = ch.begin(); it < itend; it++) { std::stringstream label; @@ -91,7 +91,7 @@ namespace printer } // print each of the children. - for (ASTVec::iterator it = ch.begin(); it < itend; it++) + for (ASTVec::const_iterator it = ch.begin(); it < itend; it++) { if (!it->isConstant()) GDL_Print1(os, *it, alreadyOutput,annotate); diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp index 9296111..bc5ba00 100644 --- a/src/printer/SMTLIBPrinter.cpp +++ b/src/printer/SMTLIBPrinter.cpp @@ -45,23 +45,6 @@ std::vector > NodeLetVarVec; //correctly print shared subterms inside the LET itself ASTNodeMap NodeLetVarMap1; -void buildListOfSymbols(const ASTNode& n, ASTNodeSet& visited, - ASTNodeSet& symbols) -{ - if (visited.find(n) != visited.end()) - return; // already visited. - - visited.insert(n); - - if (n.GetKind() == SYMBOL) - { - symbols.insert(n); - } - - for (unsigned i = 0; i < n.GetChildren().size(); i++) - buildListOfSymbols(n[i], visited, symbols); -} - // Initial version intended to print the whole thing back. void SMTLIB_PrintBack(ostream &os, const ASTNode& n) { @@ -102,7 +85,7 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os) os << ":" << a.GetValueWidth() << "] ))" << endl; break; case BEEV::BOOLEAN_TYPE: - os << ":extrapred (( "; + os << ":extrapreds (( "; a.nodeprint(os); os << "))" << endl; break; @@ -184,6 +167,15 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os) case FALSE: os << "false"; break; + case NAND: // No NAND in smtlib format. + assert(c.size() ==2); + os << "(" << "not "; + os << "(" << "and "; + SMTLIB_Print1(os, c[0], 0, letize); + os << " " ; + SMTLIB_Print1(os, c[1], 0, letize); + os << "))"; + break; case TRUE: os << "true"; break; @@ -211,19 +203,38 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os) 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 << ")"; - } + default: + { + // SMT-LIB only allows arithmetic functions to have two parameters. + if (BVPLUS == kind && 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); + } + + os << ")"; + } + } } } -- 2.47.3