When outputting to SMTLIB format handle properly some cases when the number of argume...

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

diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp
index bc5ba0097e0140725e05cff1eb98280c72a20088..cfe345afeaff3ceb11471184214a4a53416dbfb4 100644 (file)
--- a/src/printer/SMTLIBPrinter.cpp
+++ b/src/printer/SMTLIBPrinter.cpp
@@ -167,10 +167,14 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)
       case FALSE:
         os << "false";
         break;
-      case NAND: // No NAND in smtlib format.
+      case NAND: // No NAND, NOR in smtlib format.
+      case NOR:
          assert(c.size() ==2);
          os << "(" << "not ";
-         os << "(" << "and ";
+         if (NAND == kind )
+                 os << "(" << "and ";
+         else
+                 os << "(" << "or ";
          SMTLIB_Print1(os, c[0], 0, letize);
          os << " " ;
          SMTLIB_Print1(os, c[1], 0, letize);
@@ -205,8 +209,8 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)
         break;
        default:
        {
-               // SMT-LIB only allows arithmetic functions to have two parameters.
-               if (BVPLUS == kind && n.Degree() > 2)
+               // SMT-LIB only allows these functions to have two parameters.
+               if ((BVPLUS == kind || kind == BVOR || kind == BVAND)  && n.Degree() > 2)
                {
                        string close = "";