added fix so that STP can read back its SMTLIB printout

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

diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp
index 2fb0e25ac6e065a86750d53be871b92c65fbac18..674409f3a14f82b1b55fe307361b527fec3b7cf7 100644 (file)
--- a/src/printer/SMTLIBPrinter.cpp
+++ b/src/printer/SMTLIBPrinter.cpp
@@ -21,6 +21,14 @@ namespace printer
   using std::string;
   using namespace BEEV;
 
+  static string tolower(const char * name)
+  {
+       string s(name);
+       for (size_t i = 0; i < s.size(); ++i)
+         s[i] = ::tolower(s[i]);
+       return s;
+  }
+  
   string functionToSMTLIBName(const BEEV::Kind k);
   void SMTLIB_Print1(ostream& os, 
                      const BEEV::ASTNode n, 
@@ -32,7 +40,9 @@ namespace printer
     // need to add fake headers into here.
     os << "(" << endl;
     os << "benchmark blah" << endl;
+    os << ":logic QF_BV" << endl;
     printVarDeclsToStream(n.GetSTPMgr(),os);
+    os << ":formula" << endl;
     SMTLIB_Print(os, n, 0);
     os << ")" << endl;
   }
@@ -50,7 +60,8 @@ namespace printer
 
         os << ":extrafuns (( ";
         a.nodeprint(os);
-        os << " bv[" << a.GetValueWidth() << "]";
+        //os << " bv[" << a.GetValueWidth() << "]";
+        os << " BitVec[" << a.GetValueWidth() << "]";
         os << " ))" << endl;
         break;
 
@@ -278,7 +289,8 @@ namespace printer
       case OR:
       case XOR:
       case IFF:
-        return _kind_names[k];
+        //return _kind_names[k];
+        return tolower(_kind_names[k]);
 
       case BVCONCAT:
         return "concat";

diff --git a/src/to-sat/BitBlast.cpp b/src/to-sat/BitBlast.cpp
index d6ebc21227b88586e885dd839cd76090c9bd1d97..78d156adf9ddf40eaadf73995e7660523c392060 100644 (file)
--- a/src/to-sat/BitBlast.cpp
+++ b/src/to-sat/BitBlast.cpp
@@ -31,7 +31,6 @@ namespace BEEV
 
   const ASTNode BitBlaster::BBTerm(const ASTNode& term)
   {
-
     //CHANGED TermMemo is now an ASTNodeMap. Based on BBFormMemo
     ASTNodeMap::iterator it = BBTermMemo.find(term);
     if (it != BBTermMemo.end())