From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 19 May 2010 04:35:26 +0000 (+0000)
Subject: The SMT-LIB2 format changes names from "implies" to "=>", and "IFF" to "=".
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=ff6f643820e4d455522200a9fbf5cd077bb7624d;p=francis%2Fstp.git

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 9a91d50..b458ba2 100644
--- 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 aa39757..58fd1a2 100644
--- 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 88c9dc3..d98e325 100644
--- 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 182cf90..476e0eb 100644
--- 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);