The SMT-LIB2 format changes names from "implies" to "=>", and "IFF" to "=".

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

diff --git a/src/printer/SMTLIB1Printer.cpp b/src/printer/SMTLIB1Printer.cpp
index 9a91d5039a5b7055e7f47a45a9284d63f6b6331d..b458ba2d89186839f8d20a152bde44053a269da7 100644 (file)
--- a/src/printer/SMTLIB1Printer.cpp
+++ b/src/printer/SMTLIB1Printer.cpp
@@ -203,7 +203,7 @@ void printSMTLIB1VarDeclsToStream(ASTNodeSet& symbols, ostream& os)
 
                        for (int i =0; i < c.size()-1; i++)
                        {
-                               os << "(" << functionToSMTLIBName(kind);
+                               os << "(" << functionToSMTLIBName(kind,true);
                                os << " ";
                                SMTLIB1_Print1(os, c[i], 0, letize);
                                os << " ";
@@ -214,7 +214,7 @@ void printSMTLIB1VarDeclsToStream(ASTNodeSet& symbols, ostream& os)
                }
                else
                {
-                       os << "(" << functionToSMTLIBName(kind);
+                       os << "(" << functionToSMTLIBName(kind,true);
 
                        ASTVec::const_iterator iend = c.end();
                        for (ASTVec::const_iterator i = c.begin(); i != iend; i++)

diff --git a/src/printer/SMTLIB2Printer.cpp b/src/printer/SMTLIB2Printer.cpp
index aa3975722934c862286fa6e3b606b323286cb0d8..58fd1a2cd41ff8714b7eb7f41f62bb890d7f7cc2 100644 (file)
--- a/src/printer/SMTLIB2Printer.cpp
+++ b/src/printer/SMTLIB2Printer.cpp
@@ -197,7 +197,7 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)
 
                        for (int i =0; i < c.size()-1; i++)
                        {
-                               os << "(" << functionToSMTLIBName(kind);
+                               os << "(" << functionToSMTLIBName(kind,false);
                                os << " ";
                                SMTLIB2_Print1(os, c[i], 0, letize);
                                os << " ";
@@ -208,7 +208,7 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)
                }
                else
                {
-                       os << "(" << functionToSMTLIBName(kind);
+                       os << "(" << functionToSMTLIBName(kind,false);
 
                        ASTVec::const_iterator iend = c.end();
                        for (ASTVec::const_iterator i = c.begin(); i != iend; i++)

diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp
index 88c9dc3ad2eb0f2d7d5d76114842167db6562f78..d98e3253525315fda7654c08cbd5fe5f6859f995 100644 (file)
--- a/src/printer/SMTLIBPrinter.cpp
+++ b/src/printer/SMTLIBPrinter.cpp
@@ -164,10 +164,20 @@ using namespace BEEV;
                }
        } //end of LetizeNode()
 
-  string functionToSMTLIBName(const Kind k)
+  string functionToSMTLIBName(const Kind k, bool smtlib1)
   {
     switch (k)
       {
+    case IFF:
+       if (smtlib1)
+                       return "iff";
+       else
+               return "=";
+    case IMPLIES:
+       if (smtlib1)
+               return "implies";
+        else
+           return "=>";
       case AND:
       case BVAND:
       case BVNAND:
@@ -185,8 +195,6 @@ using namespace BEEV;
       case NOT:
       case OR:
       case XOR:
-      case IFF:
-      case IMPLIES:
        {
         return tolower(_kind_names[k]);
        }

diff --git a/src/printer/SMTLIBPrinter.h b/src/printer/SMTLIBPrinter.h
index 182cf909e50e22a568a7f3edc3e7b9e7175ff257..476e0ebe7be3c1834e3d3af18a7f751ac00a90e4 100644 (file)
--- a/src/printer/SMTLIBPrinter.h
+++ b/src/printer/SMTLIBPrinter.h
@@ -17,7 +17,7 @@ namespace printer
        //correctly print shared subterms inside the LET itself
        extern BEEV::ASTNodeMap NodeLetVarMap1;
 
-       string functionToSMTLIBName(const Kind k);
+       string functionToSMTLIBName(const Kind k, bool smtlib1);
 
        void LetizeNode(const ASTNode& n, BEEV::ASTNodeSet& PLPrintNodeSet);