From 205d2215f4a89970dfa3692bf019377d4bdc4f92 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 24 May 2010 02:03:46 +0000
Subject: [PATCH] * Letize booleans when printing back smb2lib format. * Print
 back in smtlib/smtlib2 format arity > 2 and, xor, or.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@783 e59a4935-1847-0410-ae03-e826735625c1
---
 src/printer/SMTLIB1Printer.cpp | 6 +++---
 src/printer/SMTLIB2Printer.cpp | 7 +++----
 src/printer/SMTLIBPrinter.cpp  | 8 ++++----
 src/printer/SMTLIBPrinter.h    | 2 +-
 4 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/src/printer/SMTLIB1Printer.cpp b/src/printer/SMTLIB1Printer.cpp
index 7ff2097..d56f3b7 100644
--- a/src/printer/SMTLIB1Printer.cpp
+++ b/src/printer/SMTLIB1Printer.cpp
@@ -204,13 +204,13 @@ void printSMTLIB1VarDeclsToStream(ASTNodeSet& symbols, ostream& os)
         break;
   	default:
   	{
-  	    if ((kind == AND  || kind == OR|| kind == XOR) && n.Degree() != 2)
+  	    if ((kind == AND  || kind == OR|| kind == XOR) && n.Degree() == 1)
   	    {
-  	    	FatalError("Wrong number of arguments to operation (must be two).", n);
+  	    	FatalError("Wrong number of arguments to operation (must be >1).", n);
   	    }
 
   		// SMT-LIB only allows these functions to have two parameters.
-  		if ((BVPLUS == kind || kind == BVOR || kind == BVAND)  && n.Degree() > 2)
+  	    if ((kind == AND  || kind == OR|| kind == XOR || BVPLUS == kind || kind == BVOR || kind == BVAND)  && n.Degree() > 2)
   		{
   			string close = "";
 
diff --git a/src/printer/SMTLIB2Printer.cpp b/src/printer/SMTLIB2Printer.cpp
index 2494c51..9f437c1 100644
--- a/src/printer/SMTLIB2Printer.cpp
+++ b/src/printer/SMTLIB2Printer.cpp
@@ -14,7 +14,6 @@
 
 // Outputs in the SMTLIB format. If you want something that can be parsed by other tools call
 // SMTLIB_PrintBack(). SMTLIB_Print() prints just an expression.
-// Wierdly is seems that only terms, not formulas can be LETized.
 
 namespace printer
 {
@@ -201,13 +200,13 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)
         break;
   	default:
   	{
-  	    if ((kind == AND  || kind == OR|| kind == XOR) && n.Degree() != 2)
+  	    if ((kind == AND  || kind == OR|| kind == XOR) && n.Degree() == 1)
   	    {
-  	    	FatalError("Wrong number of arguments to operation (must be two).", n);
+  	    	FatalError("Wrong number of arguments to operation (must be >1).", n);
   	    }
 
   		// SMT-LIB only allows these functions to have two parameters.
-  		if ((BVPLUS == kind || kind == BVOR || kind == BVAND)  && n.Degree() > 2)
+  		if ((kind == AND  || kind == OR|| kind == XOR || BVPLUS == kind || kind == BVOR || kind == BVAND)  && n.Degree() > 2)
   		{
   			string close = "";
 
diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp
index 6245a04..8681b35 100644
--- a/src/printer/SMTLIBPrinter.cpp
+++ b/src/printer/SMTLIBPrinter.cpp
@@ -43,7 +43,7 @@ static string tolower(const char * name)
 	    //pass 1: letize the node
 		{
 			ASTNodeSet PLPrintNodeSet;
-			LetizeNode(n, PLPrintNodeSet);
+			LetizeNode(n, PLPrintNodeSet, smtlib1);
 		}
 
 	    //pass 2:
@@ -111,7 +111,7 @@ static string tolower(const char * name)
 	    return os;
 	  }
 
-	void LetizeNode(const ASTNode& n, ASTNodeSet& PLPrintNodeSet)
+	void LetizeNode(const ASTNode& n, ASTNodeSet& PLPrintNodeSet, bool smtlib1)
 	{
 		const Kind kind = n.GetKind();
 
@@ -135,7 +135,7 @@ static string tolower(const char * name)
 				//
 				//2. Letize its childNodes
 				PLPrintNodeSet.insert(ccc);
-				LetizeNode(ccc, PLPrintNodeSet);
+				LetizeNode(ccc, PLPrintNodeSet, smtlib1);
 			}
 			else
 			{
@@ -146,7 +146,7 @@ static string tolower(const char * name)
 				//
 				//2. if no, then create a new var and add it to the
 				//2. NodeLetVarMap
-				if (ccc.GetType() == BITVECTOR_TYPE && NodeLetVarMap.find(ccc)
+				if ((!smtlib1 || ccc.GetType() == BITVECTOR_TYPE) && NodeLetVarMap.find(ccc)
 						== NodeLetVarMap.end())
 				{
 					//Create a new symbol. Get some name. if it conflicts with a
diff --git a/src/printer/SMTLIBPrinter.h b/src/printer/SMTLIBPrinter.h
index 546821f..4373f75 100644
--- a/src/printer/SMTLIBPrinter.h
+++ b/src/printer/SMTLIBPrinter.h
@@ -19,7 +19,7 @@ namespace printer
 
 	string functionToSMTLIBName(const Kind k, bool smtlib1);
 
-	void LetizeNode(const ASTNode& n, BEEV::ASTNodeSet& PLPrintNodeSet);
+	void LetizeNode(const ASTNode& n, BEEV::ASTNodeSet& PLPrintNodeSet, bool smtlib1);
 
 	ostream& SMTLIB_Print(ostream &os, const ASTNode n, const int indentation, void (*SMTLIB_Print1)(ostream&, const ASTNode , int , bool ), bool smtlib1);
 
-- 
2.47.3