From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 3 Nov 2009 19:57:29 +0000 (+0000)
Subject: added fix so that STP can read back its SMTLIB printout
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=1b735b1f451a3821203815d198c6d9b96df8418e;p=francis%2Fstp.git

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 2fb0e25..674409f 100644
--- 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 d6ebc21..78d156a 100644
--- 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())