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

diff --git a/src/AST/AST.h b/src/AST/AST.h
index dd44d27ebb8bf18f2d5ddecb84f63b32d2e271c4..cfad329c4baefa912b59ab0e8d39179b6be7ac5a 100644 (file)
--- 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 a705cc1da51e33ec03ed509187994c859cf0796a..6a8c94a5b0f96ff50099d2d4f3d8a695910aed2d 100644 (file)
--- 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 b384a8a89f3f1018608beffcc47ac5b569c20712..1594b057b2c3c772f47bc29eb0219763a864fe4b 100644 (file)
--- 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<int> 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 c8871280d1ba36690f76751211a5dcbc623d0665..f921db56d250e18870dfbc6e5b2c294ee23bd3ba 100644 (file)
--- 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 21cd30f73539a9e3782b023bf3efd3907dea29e5..3418008fe315b66b893989c1bb5eb662ca059dc7 100644 (file)
--- 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 364d4bef0afec240acef65016ac7fba36b921b44..81201d5b9bb1de43bd55036b4c25a46b8be59216 100644 (file)
--- 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 bc9a176cc76f6d2c8c4af7b63e1b9d384530ae39..548bb6dc4e4e6721a191720c8f83136ecdca5ae6 100644 (file)
--- 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 251fbf4a5b00749bb7f816b4cd15e4e405dc1ff8..af3439ace5a0700a43126f766dc321231ce11c77 100644 (file)
--- 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;
                       }