* 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

diff --git a/src/printer/SMTLIB1Printer.cpp b/src/printer/SMTLIB1Printer.cpp
index 7ff2097f0bf3a634e56b1e2d5fecb1de212e0244..d56f3b7cab9617c4e5bbf902c3ce4cef1c581f34 100644 (file)
--- 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 2494c51e9b5ce246796ff1008d02c9bdbf9632ee..9f437c15bda7785caf1fecc87ad501dc8bd2875d 100644 (file)
--- 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 6245a048fbc5e22bfb486cf79186c673bd285de7..8681b35feabc8ec81bcd2fda312912c4ab015843 100644 (file)
--- 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 546821feb8d5ca6cd6a52520fb87ecc254515572..4373f75df8ec6b50fc7913aa8043385244237384 100644 (file)
--- 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);