* The bvsmod operation can now be output by the printers.

* Output the status i.e. sat, unsat if known.

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

diff --git a/src/printer/SMTLIB1Printer.cpp b/src/printer/SMTLIB1Printer.cpp
index a8875df82d097cdec8ed64259f0b6bb0c0d2226e..7ff2097f0bf3a634e56b1e2d5fecb1de212e0244 100644 (file)
--- a/src/printer/SMTLIB1Printer.cpp
+++ b/src/printer/SMTLIB1Printer.cpp
@@ -37,6 +37,14 @@ namespace printer
        else
                os << ":logic QF_BV" << endl;
 
+       if (input_status == TO_BE_SATISFIABLE) {
+               os << ":status sat" << endl;
+       }
+       else if (input_status == TO_BE_UNSATISFIABLE) {
+               os << ":status unsat" << endl;
+       }
+       else
+               os << ":status unknown" << endl;
 
        ASTNodeSet visited, symbols;
        buildListOfSymbols(n, visited, symbols);
@@ -196,6 +204,11 @@ void printSMTLIB1VarDeclsToStream(ASTNodeSet& symbols, ostream& os)
         break;
        default:
        {
+           if ((kind == AND  || kind == OR|| kind == XOR) && n.Degree() != 2)
+           {
+               FatalError("Wrong number of arguments to operation (must be two).", n);
+           }
+
                // SMT-LIB only allows these functions to have two parameters.
                if ((BVPLUS == kind || kind == BVOR || kind == BVAND)  && n.Degree() > 2)
                {

diff --git a/src/printer/SMTLIB2Printer.cpp b/src/printer/SMTLIB2Printer.cpp
index 1d983e655c7d5408087a93b9fbfcf4ab23755ed9..2494c51e9b5ce246796ff1008d02c9bdbf9632ee 100644 (file)
--- a/src/printer/SMTLIB2Printer.cpp
+++ b/src/printer/SMTLIB2Printer.cpp
@@ -33,7 +33,15 @@ void SMTLIB2_PrintBack(ostream &os, const ASTNode& n)
                os << "(set-logic QF_BV)"<< endl;
 
        os << "(set-info :smt-lib-version 2.0)"<< endl;
-       os << "(set-info :status unknown)"<< endl;
+
+
+       if (input_status == TO_BE_SATISFIABLE) {
+               os << "(set-info :status sat)"<< endl;
+       }
+       else if (input_status == TO_BE_UNSATISFIABLE) {
+               os << "(set-info :status unsat)"<< endl;
+       } else
+               os << "(set-info :status unknown)"<< endl;
 
        ASTNodeSet visited, symbols;
        buildListOfSymbols(n, visited, symbols);
@@ -193,6 +201,11 @@ void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)
         break;
        default:
        {
+           if ((kind == AND  || kind == OR|| kind == XOR) && n.Degree() != 2)
+           {
+               FatalError("Wrong number of arguments to operation (must be two).", n);
+           }
+
                // SMT-LIB only allows these functions to have two parameters.
                if ((BVPLUS == kind || kind == BVOR || kind == BVAND)  && n.Degree() > 2)
                {

diff --git a/src/printer/SMTLIBPrinter.cpp b/src/printer/SMTLIBPrinter.cpp
index a3b7bcb2e0fdb6198d427d6d5152f798520a24a5..6245a048fbc5e22bfb486cf79186c673bd285de7 100644 (file)
--- a/src/printer/SMTLIBPrinter.cpp
+++ b/src/printer/SMTLIBPrinter.cpp
@@ -247,6 +247,8 @@ static string tolower(const char * name)
         return "bvsdiv";
       case SBVREM:
         return "bvsrem";
+      case SBVMOD:
+        return "bvsmod";
 
       default:
         {