From 8c276aba43446d15014b9a6f4faef10c9f05dedc Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Sun, 6 Sep 2009 21:50:09 +0000 Subject: [PATCH] Added capability to print back CVC-language input to STP git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@194 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/AST.h | 13 ++-------- src/AST/ASTUtil.h | 5 ---- src/AST/printer/AssortedPrinters.cpp | 36 +++++++++++++++++++++++++++- src/AST/printer/AssortedPrinters.h | 7 ++++++ src/c_interface/c_interface.cpp | 4 ++-- src/main/main.cpp | 18 +++++++------- src/parser/CVC.lex | 1 + src/parser/CVC.y | 2 +- 8 files changed, 57 insertions(+), 29 deletions(-) diff --git a/src/AST/AST.h b/src/AST/AST.h index dd44d27..cfad329 100644 --- a/src/AST/AST.h +++ b/src/AST/AST.h @@ -1572,17 +1572,8 @@ namespace BEEV bool UpdateSolverMap(const ASTNode& e0, const ASTNode& e1); public: - //FIXME: HACK_ATTACK. this vector was hacked into the code to - //support a special request by Dawson' group. They want the - //counterexample to be printed in the order of variables declared. - //TO BE COMMENTED LATER (say by 1st week of march,2006) - ASTVec _special_print_set; - - //prints the initial activity levels of variables - //void PrintActivityLevels_Of_SATVars(char * init_msg, MINISAT::Solver& newS); - - //this function biases the activity levels of MINISAT variables. - //void ChangeActivityLevels_Of_SATVars(MINISAT::Solver& n); + ASTVec ListOfDeclaredVars; + void printVarDeclsToStream(ostream &os); // Constructor BeevMgr() : diff --git a/src/AST/ASTUtil.h b/src/AST/ASTUtil.h index a705cc1..6a8c94a 100644 --- a/src/AST/ASTUtil.h +++ b/src/AST/ASTUtil.h @@ -63,10 +63,5 @@ namespace BEEV { #endif void CountersAndStats(const char * functionname); - - //global function which accepts an integer and looks up the - //corresponding ASTNode and prints a string of that ASTNode - void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, - int decision, int polarity=0); }; // end namespace. #endif diff --git a/src/AST/printer/AssortedPrinters.cpp b/src/AST/printer/AssortedPrinters.cpp index b384a8a..1594b05 100644 --- a/src/AST/printer/AssortedPrinters.cpp +++ b/src/AST/printer/AssortedPrinters.cpp @@ -232,7 +232,7 @@ namespace BEEV //vector to store the integer values std::vector out_int; cout << "% "; - for (ASTVec::iterator it = _special_print_set.begin(), itend = _special_print_set.end(); it != itend; it++) + for (ASTVec::iterator it = ListOfDeclaredVars.begin(), itend = ListOfDeclaredVars.end(); it != itend; it++) { if (ARRAY_TYPE == it->GetType()) { @@ -358,4 +358,38 @@ namespace BEEV printer::PL_Print(cout,vv, 0); cout << endl; } //end of Convert_MINISATVar_To_ASTNode_Print() + + void BeevMgr::printVarDeclsToStream(ostream &os) { + for(ASTVec::iterator i = ListOfDeclaredVars.begin(),iend=ListOfDeclaredVars.end();i!=iend;i++) { + BEEV::ASTNode a = *i; + switch(a.GetType()) { + case BEEV::BITVECTOR_TYPE: + a.PL_Print(os); + os << " : BITVECTOR(" << a.GetValueWidth() << ");" << endl; + break; + case BEEV::ARRAY_TYPE: + a.PL_Print(os); + os << " : ARRAY " << "BITVECTOR(" << a.GetIndexWidth() << ") OF "; + os << "BITVECTOR(" << a.GetValueWidth() << ");" << endl; + break; + case BEEV::BOOLEAN_TYPE: + a.PL_Print(os); + os << " : BOOLEAN;" << endl; + break; + default: + BEEV::FatalError("vc_printDeclsToStream: Unsupported type",a); + break; + } + } + } //printVarDeclsToStream + + void print_STPInput_Back(const ASTNode& asserts, const ASTNode& query) { + BEEV::GlobalBeevMgr->printVarDeclsToStream(cout); + cout << "ASSERT("; + asserts.PL_Print(cout); + cout << ");\n\n"; + cout << "QUERY("; + query.PL_Print(cout); + cout << ");\n"; + } //end of print_STPInput_Back() };//end of namespace BEEV diff --git a/src/AST/printer/AssortedPrinters.h b/src/AST/printer/AssortedPrinters.h index c887128..f921db5 100644 --- a/src/AST/printer/AssortedPrinters.h +++ b/src/AST/printer/AssortedPrinters.h @@ -70,5 +70,12 @@ namespace BEEV } ; }; //End of Class ListVecPrinter + + //global function which accepts an integer and looks up the + //corresponding ASTNode and prints a string of that ASTNode + void Convert_MINISATVar_To_ASTNode_Print(int minisat_var, + int decision, int polarity=0); + + void print_STPInput_Back(const ASTNode& asserts, const ASTNode& query); };// end of namespace BEEV #endif diff --git a/src/c_interface/c_interface.cpp b/src/c_interface/c_interface.cpp index 21cd30f..3418008 100644 --- a/src/c_interface/c_interface.cpp +++ b/src/c_interface/c_interface.cpp @@ -40,7 +40,7 @@ void vc_setFlags(char c) { helpstring += "-d : check counterexample\n"; helpstring += "-p : print counterexample\n"; helpstring += "-y : print counterexample in binary\n"; - helpstring += "-b : STP input read back\n"; + helpstring += "-b : print STP input back to cout\n"; helpstring += "-x : flatten nested XORs\n"; helpstring += "-h : help\n"; helpstring += "-m : use the SMTLIB parser\n"; @@ -142,7 +142,7 @@ void vc_printExprCCode(VC vc, Expr e) { BEEV::ASTNode q = (*(nodestar)e); // print variable declarations - BEEV::ASTVec declsFromParser = (nodelist)BEEV::GlobalBeevMgr->_special_print_set; + BEEV::ASTVec declsFromParser = (nodelist)BEEV::GlobalBeevMgr->ListOfDeclaredVars; for(BEEV::ASTVec::iterator it=declsFromParser.begin(),itend=declsFromParser.end(); it!=itend;it++) { if(BEEV::BITVECTOR_TYPE == it->GetType()) { diff --git a/src/main/main.cpp b/src/main/main.cpp index 364d4be..81201d5 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -9,6 +9,7 @@ #include "../AST/AST.h" #include "../sat/core/Solver.h" #include "../sat/core/SolverTypes.h" +#include "../AST/printer/AssortedPrinters.h" #ifdef EXT_HASH_MAP using namespace __gnu_cxx; @@ -55,7 +56,7 @@ int main(int argc, char ** argv) { helpstring += "-d : check counterexample\n"; helpstring += "-p : print counterexample\n"; helpstring += "-y : print counterexample in binary\n"; - helpstring += "-b : STP input read back\n"; + helpstring += "-b : print STP input back to cout\n"; helpstring += "-x : flatten nested XORs\n"; helpstring += "-h : help\n"; helpstring += "-m : use the SMTLIB parser\n"; @@ -181,15 +182,14 @@ int main(int argc, char ** argv) { { cvcparse((void*)AssertsQuery); } - + ASTNode asserts = (*(ASTVec*)AssertsQuery)[0]; - ASTNode query = (*(ASTVec*)AssertsQuery)[1]; - GlobalBeevMgr->TopLevelSAT(asserts, query); - - // if(print_STPinput_back_flag) { - // asserts.PL_Print(cout); - // query.PL_Print(cout); - // } + ASTNode query = (*(ASTVec*)AssertsQuery)[1]; + if(print_STPinput_back_flag) { + print_STPInput_Back(asserts, query); + return 0; + } + GlobalBeevMgr->TopLevelSAT(asserts, query); return 0; }//end of Main diff --git a/src/parser/CVC.lex b/src/parser/CVC.lex index bc9a176..548bb6d 100644 --- a/src/parser/CVC.lex +++ b/src/parser/CVC.lex @@ -39,6 +39,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) [ \t\r\f] { /* skip whitespace */ } 0b{BITS}+ { cvclval.node = new BEEV::ASTNode(BEEV::GlobalBeevMgr->CreateBVConst(yytext+2, 2)); return BVCONST_TOK;} 0bin{BITS}+ { cvclval.node = new BEEV::ASTNode(BEEV::GlobalBeevMgr->CreateBVConst(yytext+4, 2)); return BVCONST_TOK;} +0x{HEX}+ { cvclval.node = new BEEV::ASTNode(BEEV::GlobalBeevMgr->CreateBVConst(yytext+2, 16)); return BVCONST_TOK;} 0h{HEX}+ { cvclval.node = new BEEV::ASTNode(BEEV::GlobalBeevMgr->CreateBVConst(yytext+2, 16)); return BVCONST_TOK;} 0hex{HEX}+ { cvclval.node = new BEEV::ASTNode(BEEV::GlobalBeevMgr->CreateBVConst(yytext+4, 16)); return BVCONST_TOK;} {DIGIT}+ { cvclval.uintval = strtoul(yytext, NULL, 10); return NUMERAL_TOK;} diff --git a/src/parser/CVC.y b/src/parser/CVC.y index 251fbf4..af3439a 100644 --- a/src/parser/CVC.y +++ b/src/parser/CVC.y @@ -275,7 +275,7 @@ VarDecl : FORM_IDs ':' Type //FIXME: HACK_ATTACK. this vector was hacked into the code to //support a special request by Dawson' group. They want the //counterexample to be printed in the order of variables declared. - GlobalBeevMgr->_special_print_set.push_back(*i); + GlobalBeevMgr->ListOfDeclaredVars.push_back(*i); } delete $1; } -- 2.47.3