From 23fca2683f80d55983eb91c8c66486b59c8b5c24 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 10 Sep 2009 13:36:22 +0000 Subject: [PATCH] Rough version of smtlib print back. The output version is form information only, it won't parse back in. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@216 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/printer/SMTLIBPrinter.cpp | 50 +++++++++++++++++++++++++++++++ src/AST/printer/printers.h | 2 ++ src/main/main.cpp | 30 ++++++++++--------- src/parser/smtlib.y | 4 +++ 4 files changed, 72 insertions(+), 14 deletions(-) diff --git a/src/AST/printer/SMTLIBPrinter.cpp b/src/AST/printer/SMTLIBPrinter.cpp index 1839e58..40519c2 100644 --- a/src/AST/printer/SMTLIBPrinter.cpp +++ b/src/AST/printer/SMTLIBPrinter.cpp @@ -10,6 +10,11 @@ #include "printers.h" #include +// todo : fix lets. +// : Finish mapping function names from internal names to SMTLIB names. +// : build proper headers for PrintBack +// : Letize code for each printer should be merged. + namespace printer { @@ -18,6 +23,51 @@ namespace printer string functionToSMTLIBName(const BEEV::Kind k); void SMTLIB_Print1(ostream& os, const BEEV::ASTNode n, int indentation, bool letize); + void printVarDeclsToStream( const BeevMgr mgr, ostream &os); + + // Initial version intended to print the whole thing back. + void SMTLIB_PrintBack(ostream &os, const ASTNode& n) { + // need to add fake headers into here. + os << "(" << endl; + os << "benchmark blah" << endl; + printVarDeclsToStream(n.GetBeevMgr(),os); + SMTLIB_Print(os, n, 0); + os << ")" << endl; + } + + void printVarDeclsToStream( const BeevMgr mgr, ostream &os) { + for(ASTVec::const_iterator i = mgr.ListOfDeclaredVars.begin(),iend=mgr.ListOfDeclaredVars.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 << " bv[" << 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 << ":extrapred (( "; + a.nodeprint(os); + os << "))" << endl; + break; + default: + BEEV::FatalError("printVarDeclsToStream: Unsupported type",a); + break; + } + } + } //printVarDeclsToStream void outputBitVec(const ASTNode n, ostream& os) { diff --git a/src/AST/printer/printers.h b/src/AST/printer/printers.h index 06815f2..9b15a6d 100644 --- a/src/AST/printer/printers.h +++ b/src/AST/printer/printers.h @@ -26,6 +26,8 @@ namespace printer 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); + void SMTLIB_PrintBack(ostream &os, const BEEV::ASTNode& n ); + } #endif /* PRINTERS_H_ */ diff --git a/src/main/main.cpp b/src/main/main.cpp index 808b717..5a99df4 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -8,6 +8,7 @@ // -*- c++ -*- #include "../AST/AST.h" #include "../AST/printer/AssortedPrinters.h" +#include "../AST/printer/printers.h" #ifdef EXT_HASH_MAP using namespace __gnu_cxx; @@ -36,7 +37,7 @@ int main(int argc, char ** argv) { // Grab some memory from the OS upfront to reduce system time when // individual hash tables are being allocated - if (sbrk(INITIAL_MEMORY_PREALLOCATION_SIZE) == ((void *) -1)) + if (sbrk(INITIAL_MEMORY_PREALLOCATION_SIZE) == ((void *) -1)) { // FIXME: figure out how to get and print the real error // message. @@ -60,11 +61,11 @@ int main(int argc, char ** argv) { helpstring += "-x : flatten nested XORs\n"; helpstring += "-y : print counterexample in binary\n"; - for(int i=1; i < argc;i++) + for(int i=1; i < argc;i++) { - if(argv[i][0] == '-') + if(argv[i][0] == '-') { - switch(argv[i][1]) + switch(argv[i][1]) { case 'a' : optimize_flag = false; @@ -174,30 +175,31 @@ int main(int argc, char ** argv) { GlobalBeevMgr = new BeevMgr(); ASTVec * AssertsQuery = new ASTVec; - if (smtlib_parser_flag) + if (smtlib_parser_flag) { smtparse((void*)AssertsQuery); } - else + else { - cvcparse((void*)AssertsQuery); + cvcparse((void*)AssertsQuery); } - + ASTNode asserts = (*(ASTVec*)AssertsQuery)[0]; - ASTNode query = (*(ASTVec*)AssertsQuery)[1]; - if(print_STPinput_back_flag) + ASTNode query = (*(ASTVec*)AssertsQuery)[1]; + if(print_STPinput_back_flag) { - if(smtlib_parser_flag) + if(smtlib_parser_flag) { - FatalError("Print back feature for SMT format not yet implemented\n"); + // don't pass the query. It's not returned by the smtlib parser. + printer::SMTLIB_PrintBack(cout, asserts); } - else + else { print_STPInput_Back(asserts, query); } return 0; } //end of PrintBack if - GlobalBeevMgr->TopLevelSAT(asserts, query); + GlobalBeevMgr->TopLevelSAT(asserts, query); return 0; }//end of Main diff --git a/src/parser/smtlib.y b/src/parser/smtlib.y index 1903ac0..cd432f2 100644 --- a/src/parser/smtlib.y +++ b/src/parser/smtlib.y @@ -416,6 +416,8 @@ var_decl: //var $2->SetIndexWidth($3.indexwidth); $2->SetValueWidth($3.valuewidth); + if(print_STPinput_back_flag) + GlobalBeevMgr->ListOfDeclaredVars.push_back(*$2); } | LPAREN_TOK FORMID_TOK RPAREN_TOK { @@ -424,6 +426,8 @@ var_decl: //var $2->SetIndexWidth(0); $2->SetValueWidth(0); + if(print_STPinput_back_flag) + GlobalBeevMgr->ListOfDeclaredVars.push_back(*$2); } ; -- 2.47.3