Rough version of smtlib print back. The output version is form information only,...

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@216 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/AST/printer/SMTLIBPrinter.cpp b/src/AST/printer/SMTLIBPrinter.cpp
index 1839e58b08825aa84c08a0cb8022b16054140e6a..40519c22bbfa88081767a73a44fbcde2be5bc4b8 100644 (file)
--- a/src/AST/printer/SMTLIBPrinter.cpp
+++ b/src/AST/printer/SMTLIBPrinter.cpp
@@ -10,6 +10,11 @@
 #include "printers.h"
 #include <cassert>
 
+// 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 06815f285d0918a4968e9fb0e8ae9cd15078e108..9b15a6d4180635975c107faceb10bc4fe8e9def5 100644 (file)
--- 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 808b717614dfd0e36750381bde9371c555a93539..5a99df4802fa3750a2ff61c65500ffa527a20b0a 100644 (file)
--- 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 1903ac00ffee0b2b605533ba12a8d283385b3b78..cd432f2c40f67c27247f697e7bced6b11918e397 100644 (file)
--- 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);
     }
 ;