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 b458ba2d89186839f8d20a152bde44053a269da7..a8875df82d097cdec8ed64259f0b6bb0c0d2226e 100644 (file)
--- 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 58fd1a2cd41ff8714b7eb7f41f62bb890d7f7cc2..1d983e655c7d5408087a93b9fbfcf4ab23755ed9 100644 (file)
--- 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 d98e3253525315fda7654c08cbd5fe5f6859f995..c995e81cad3510198e1e284e04351759fe2d6a67 100644 (file)
--- 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 476e0ebe7be3c1834e3d3af18a7f751ac00a90e4..9c5cfe96635621e34e28f4ddd4030de018faedfc 100644 (file)
--- 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);
 };