Add the ability to tell the SMTLIB2 printer whether it contains arrays or not. The...

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

diff --git a/src/printer/SMTLIB2Printer.cpp b/src/printer/SMTLIB2Printer.cpp
index dc15389946ef9bb9d475311824f79735ae77d90a..351f0005a7caaa218c711567c6b455d3ede613ed 100644 (file)
--- a/src/printer/SMTLIB2Printer.cpp
+++ b/src/printer/SMTLIB2Printer.cpp
@@ -24,32 +24,32 @@ namespace printer
   void SMTLIB2_Print1(ostream& os, const BEEV::ASTNode n, int indentation,     bool letize);
   void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os);
 
-void SMTLIB2_PrintBack(ostream &os, const ASTNode& n)
+void SMTLIB2_PrintBack(ostream &os, const ASTNode& n, const bool definately_bv)
 {
-       if (containsArrayOps(n))
-               os << "(set-logic QF_ABV)" << endl;
+       if (!definately_bv && containsArrayOps(n))
+               os << "(set-logic QF_ABV)\n";
        else
-               os << "(set-logic QF_BV)"<< endl;
+               os << "(set-logic QF_BV)\n";
 
-       os << "(set-info :smt-lib-version 2.0)"<< endl;
+       os << "(set-info :smt-lib-version 2.0)\n";
 
 
        if (input_status == TO_BE_SATISFIABLE) {
-               os << "(set-info :status sat)"<< endl;
+               os << "(set-info :status sat)\n";
        }
        else if (input_status == TO_BE_UNSATISFIABLE) {
-               os << "(set-info :status unsat)"<< endl;
+               os << "(set-info :status unsat)\n";
        } else
-               os << "(set-info :status unknown)"<< endl;
+               os << "(set-info :status unknown)\n";
 
        ASTNodeSet visited, symbols;
        buildListOfSymbols(n, visited, symbols);
        printVarDeclsToStream(symbols, os);
        os << "(assert ";
     SMTLIB_Print(os, n, 0, &SMTLIB2_Print1, false);
-    os << ")" << endl;
-    os << "(check-sat)" << endl;
-    os << "(exit)" << endl;
+    os << ")\n";
+    // os << "(check-sat)" << endl;
+    // os << "(exit)\n";
   }
 
 void printVarDeclsToStream(ASTNodeSet& symbols, ostream& os)

diff --git a/src/printer/printers.h b/src/printer/printers.h
index da15251e0aa01149f4b41cb782f01050ce606254..f70f31497384777ef0709143d37f49884d7a4b25 100644 (file)
--- a/src/printer/printers.h
+++ b/src/printer/printers.h
@@ -38,9 +38,7 @@ namespace printer
   void SMTLIB1_PrintBack(ostream &os,
                         const BEEV::ASTNode& n );
 
-  void SMTLIB2_PrintBack(ostream &os,
-                        const BEEV::ASTNode& n );
-
+  void SMTLIB2_PrintBack(ostream &os, const ASTNode& n, bool definately_bv=false);
 
   ostream& GDL_Print(ostream &os, const BEEV::ASTNode n);
   ostream& GDL_Print(ostream &os, const ASTNode n, string (*annotate)(const ASTNode&));