From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 19 May 2010 14:09:45 +0000 (+0000)
Subject: Fix: lets, types, extends and extracts in the SMTLIB2 format.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=ceb88bd56038c99ccc54a948aa5e3ebf731f7ae8;p=francis%2Fstp.git

Fix: lets, types, extends and extracts in the SMTLIB2 format.



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

diff --git a/src/printer/SMTLIB1Printer.cpp b/src/printer/SMTLIB1Printer.cpp
index b458ba2..a8875df 100644
--- a/src/printer/SMTLIB1Printer.cpp
+++ b/src/printer/SMTLIB1Printer.cpp
@@ -42,7 +42,7 @@ namespace printer
 	buildListOfSymbols(n, visited, symbols);
 	printSMTLIB1VarDeclsToStream(symbols, os);
 	os << ":formula ";
-    SMTLIB_Print(os, n, 0, &SMTLIB1_Print1);
+    SMTLIB_Print(os, n, 0, &SMTLIB1_Print1,true);
     os << ")" << endl;
   }
 
diff --git a/src/printer/SMTLIB2Printer.cpp b/src/printer/SMTLIB2Printer.cpp
index 58fd1a2..1d983e6 100644
--- a/src/printer/SMTLIB2Printer.cpp
+++ b/src/printer/SMTLIB2Printer.cpp
@@ -39,7 +39,7 @@ void SMTLIB2_PrintBack(ostream &os, const ASTNode& n)
 	buildListOfSymbols(n, visited, symbols);
 	printVarDeclsToStream(symbols, os);
 	os << "(assert ";
-    SMTLIB_Print(os, n, 0, &SMTLIB2_Print1);
+    SMTLIB_Print(os, n, 0, &SMTLIB2_Print1, false);
     os << ")" << endl;
     os << "(check-sat)" << endl;
     os << "(exit)" << endl;
@@ -56,24 +56,27 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)
       // Should be a symbol.
       assert(a.GetKind()== SYMBOL);
       a.nodeprint(os);
-      os << " () (";
+
 
 		switch (a.GetType())
 		{
       case BEEV::BITVECTOR_TYPE:
-        os << "_ BitVec " << a.GetValueWidth() << ")";
+    	  os << " () (";
+    	  os << "_ BitVec " << a.GetValueWidth() << ")";
+
         break;
       case BEEV::ARRAY_TYPE:
-        os << "Array (_ BitVec " << a.GetIndexWidth()  << ") (_BitVec " << a.GetValueWidth() << ") )";
+    	  os << " () (";
+    	  os << "Array (_ BitVec " << a.GetIndexWidth()  << ") (_ BitVec " << a.GetValueWidth() << ") )";
         break;
       case BEEV::BOOLEAN_TYPE:
-        os << " Bool ";
+        os << " () Bool ";
         break;
       default:
         BEEV::FatalError("printVarDeclsToStream: Unsupported type",a);
         break;
       }
-		os << ")\n";
+  	  os << ")\n";
     }
   } //printVarDeclsToStream
 
@@ -169,9 +172,9 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)
         {
           unsigned int amount = GetUnsignedConst(c[1]);
           if (BVZX == kind)
-            os << "(_ zero_extend ";
+            os << "((_ zero_extend ";
           else
-            os << "(_ sign_extend ";
+            os << "((_ sign_extend ";
 
           os << (amount - c[0].GetValueWidth()) << ") ";
           SMTLIB2_Print1(os, c[0], indentation, letize);
@@ -183,7 +186,7 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)
           unsigned int upper = GetUnsignedConst(c[1]);
           unsigned int lower = GetUnsignedConst(c[2]);
           assert(upper >= lower);
-          os << "((_ extract" << upper << " " << lower << ") ";
+          os << "((_ extract " << upper << " " << lower << ") ";
           SMTLIB2_Print1(os, c[0], indentation, letize);
           os << ")";
         }
diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp
index d98e325..c995e81 100644
--- a/src/printer/SMTLIBPrinter.cpp
+++ b/src/printer/SMTLIBPrinter.cpp
@@ -23,17 +23,8 @@ using namespace BEEV;
 		return true;
 	}
 
-
-	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;
-	}
-
 	  // copied from Presentation Langauge printer.
-	  ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation, void (*SMTLIB1_Print1)(ostream&, const ASTNode , int , bool ))
+	  ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation, void (*SMTLIB1_Print1)(ostream&, const ASTNode , int , bool ), bool smtlib1)
 	  {
 	    // Clear the maps
 		NodeLetVarMap.clear();
@@ -62,12 +53,17 @@ using namespace BEEV;
 					NodeLetVarVec.end();
 
 			os << "(let (";
+			if (!smtlib1)
+				os << "(";
 	        //print the let var first
 	        SMTLIB1_Print1(os, it->first, indentation, false);
 			os << " ";
 	        //print the expr
 	        SMTLIB1_Print1(os, it->second, indentation, false);
 			os << " )";
+			if (!smtlib1)
+				os << ")";
+
 
 	        //update the second map for proper printing of LET
 			NodeLetVarMap1[it->second] = it->first;
@@ -77,12 +73,17 @@ using namespace BEEV;
 	          {
 				os << " " << endl;
 				os << "(let (";
+				if (!smtlib1)
+						os << "(";
 	            //print the let var first
 	            SMTLIB1_Print1(os, it->first, indentation, false);
 				os << " ";
 	            //print the expr
 	            SMTLIB1_Print1(os, it->second, indentation, false);
 				os << ")";
+				if (!smtlib1)
+						os << ")";
+
 	            //update the second map for proper printing of LET
 				NodeLetVarMap1[it->second] = it->first;
 				closing += ")";
diff --git a/src/printer/SMTLIBPrinter.h b/src/printer/SMTLIBPrinter.h
index 476e0eb..9c5cfe9 100644
--- a/src/printer/SMTLIBPrinter.h
+++ b/src/printer/SMTLIBPrinter.h
@@ -21,7 +21,7 @@ namespace printer
 
 	void LetizeNode(const ASTNode& n, BEEV::ASTNodeSet& PLPrintNodeSet);
 
-	ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation, void (*SMTLIB_Print1)(ostream&, const ASTNode , int , bool ));
+	ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation, void (*SMTLIB_Print1)(ostream&, const ASTNode , int , bool ), bool smtlib1);
 
 	bool containsAnyArrayOps(const ASTNode& n);
 };