Output language "cvc3" (as opposed to "cvc" or "cvc4") produces output for CVC3:

1. no decimals used for rational literals
2. queries/check-sats wrapped with PUSH/POP

diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 39deb285a906bbdaecaa18a3f822ee59af7bd515..8a5cdd8d5b56cad909f2fbbf3d8a88ce6166b682 100644 (file)
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -259,6 +259,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\
 Languages currently supported as arguments to the --output-lang option:\n\
   auto                           match output language to input language\n\
   cvc4 | presentation | pl       CVC4 presentation language\n\
+  cvc3                           CVC3 presentation language\n\
   smt1 | smtlib1                 SMT-LIB format 1.2\n\
   smt | smtlib | smt2 | smtlib2  SMT-LIB format 2.0\n\
   z3str                          SMT-LIB 2.0 with Z3-str string constraints\n\

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 16f5f5c51c362daf8ab6eae67971e7e6fa2d5036..8412ecc2cd3b0f6603e3b23c4c58285c220b4e09 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -780,7 +780,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
 }/* CvcPrinter::toStream(TNode) */
 
 template <class T>
-static bool tryToStream(std::ostream& out, const Command* c) throw();
+static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode) throw();
 
 void CvcPrinter::toStream(std::ostream& out, const Command* c,
                            int toDepth, bool types, size_t dag) const throw() {
@@ -788,35 +788,35 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c,
   expr::ExprPrintTypes::Scope ptScope(out, types);
   expr::ExprDag::Scope dagScope(out, dag);
 
-  if(tryToStream<AssertCommand>(out, c) ||
-     tryToStream<PushCommand>(out, c) ||
-     tryToStream<PopCommand>(out, c) ||
-     tryToStream<CheckSatCommand>(out, c) ||
-     tryToStream<QueryCommand>(out, c) ||
-     tryToStream<QuitCommand>(out, c) ||
-     tryToStream<DeclarationSequence>(out, c) ||
-     tryToStream<CommandSequence>(out, c) ||
-     tryToStream<DeclareFunctionCommand>(out, c) ||
-     tryToStream<DeclareTypeCommand>(out, c) ||
-     tryToStream<DefineTypeCommand>(out, c) ||
-     tryToStream<DefineNamedFunctionCommand>(out, c) ||
-     tryToStream<DefineFunctionCommand>(out, c) ||
-     tryToStream<SimplifyCommand>(out, c) ||
-     tryToStream<GetValueCommand>(out, c) ||
-     tryToStream<GetModelCommand>(out, c) ||
-     tryToStream<GetAssignmentCommand>(out, c) ||
-     tryToStream<GetAssertionsCommand>(out, c) ||
-     tryToStream<GetProofCommand>(out, c) ||
-     tryToStream<SetBenchmarkStatusCommand>(out, c) ||
-     tryToStream<SetBenchmarkLogicCommand>(out, c) ||
-     tryToStream<SetInfoCommand>(out, c) ||
-     tryToStream<GetInfoCommand>(out, c) ||
-     tryToStream<SetOptionCommand>(out, c) ||
-     tryToStream<GetOptionCommand>(out, c) ||
-     tryToStream<DatatypeDeclarationCommand>(out, c) ||
-     tryToStream<CommentCommand>(out, c) ||
-     tryToStream<EmptyCommand>(out, c) ||
-     tryToStream<EchoCommand>(out, c)) {
+  if(tryToStream<AssertCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<PushCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<PopCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<CheckSatCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<QueryCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<QuitCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<DeclarationSequence>(out, c, d_cvc3Mode) ||
+     tryToStream<CommandSequence>(out, c, d_cvc3Mode) ||
+     tryToStream<DeclareFunctionCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<DeclareTypeCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<DefineTypeCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<DefineNamedFunctionCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<DefineFunctionCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<SimplifyCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<GetValueCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<GetModelCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<GetAssignmentCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<GetAssertionsCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<GetProofCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<SetBenchmarkStatusCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<SetBenchmarkLogicCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<SetInfoCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<GetInfoCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<SetOptionCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<GetOptionCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<DatatypeDeclarationCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<CommentCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<EmptyCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<EchoCommand>(out, c, d_cvc3Mode)) {
     return;
   }
 
@@ -830,13 +830,13 @@ static inline void toStream(std::ostream& out, const SExpr& sexpr) throw() {
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const CommandStatus* s) throw();
+static bool tryToStream(std::ostream& out, const CommandStatus* s, bool cvc3Mode) throw();
 
 void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
 
-  if(tryToStream<CommandSuccess>(out, s) ||
-     tryToStream<CommandFailure>(out, s) ||
-     tryToStream<CommandUnsupported>(out, s)) {
+  if(tryToStream<CommandSuccess>(out, s, d_cvc3Mode) ||
+     tryToStream<CommandFailure>(out, s, d_cvc3Mode) ||
+     tryToStream<CommandUnsupported>(out, s, d_cvc3Mode)) {
     return;
   }
 
@@ -937,41 +937,53 @@ void CvcPrinter::toStream(std::ostream& out, const Model& m, const Command* c) c
   }
 }
 
-static void toStream(std::ostream& out, const AssertCommand* c) throw() {
+static void toStream(std::ostream& out, const AssertCommand* c, bool cvc3Mode) throw() {
   out << "ASSERT " << c->getExpr() << ";";
 }
 
-static void toStream(std::ostream& out, const PushCommand* c) throw() {
+static void toStream(std::ostream& out, const PushCommand* c, bool cvc3Mode) throw() {
   out << "PUSH;";
 }
 
-static void toStream(std::ostream& out, const PopCommand* c) throw() {
+static void toStream(std::ostream& out, const PopCommand* c, bool cvc3Mode) throw() {
   out << "POP;";
 }
 
-static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
+static void toStream(std::ostream& out, const CheckSatCommand* c, bool cvc3Mode) throw() {
   Expr e = c->getExpr();
+  if(cvc3Mode) {
+    out << "PUSH; ";
+  }
   if(!e.isNull()) {
     out << "CHECKSAT " << e << ";";
   } else {
     out << "CHECKSAT;";
   }
+  if(cvc3Mode) {
+    out << " POP;";
+  }
 }
 
-static void toStream(std::ostream& out, const QueryCommand* c) throw() {
+static void toStream(std::ostream& out, const QueryCommand* c, bool cvc3Mode) throw() {
   Expr e = c->getExpr();
+  if(cvc3Mode) {
+    out << "PUSH; ";
+  }
   if(!e.isNull()) {
     out << "QUERY " << e << ";";
   } else {
     out << "QUERY TRUE;";
   }
+  if(cvc3Mode) {
+    out << " POP;";
+  }
 }
 
-static void toStream(std::ostream& out, const QuitCommand* c) throw() {
+static void toStream(std::ostream& out, const QuitCommand* c, bool cvc3Mode) throw() {
   //out << "EXIT;";
 }
 
-static void toStream(std::ostream& out, const CommandSequence* c) throw() {
+static void toStream(std::ostream& out, const CommandSequence* c, bool cvc3Mode) throw() {
   for(CommandSequence::const_iterator i = c->begin();
       i != c->end();
       ++i) {
@@ -979,7 +991,7 @@ static void toStream(std::ostream& out, const CommandSequence* c) throw() {
   }
 }
 
-static void toStream(std::ostream& out, const DeclarationSequence* c) throw() {
+static void toStream(std::ostream& out, const DeclarationSequence* c, bool cvc3Mode) throw() {
   DeclarationSequence::const_iterator i = c->begin();
   for(;;) {
     DeclarationDefinitionCommand* dd =
@@ -993,11 +1005,11 @@ static void toStream(std::ostream& out, const DeclarationSequence* c) throw() {
   }
 }
 
-static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() {
+static void toStream(std::ostream& out, const DeclareFunctionCommand* c, bool cvc3Mode) throw() {
   out << c->getSymbol() << " : " << c->getType() << ";";
 }
 
-static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() {
+static void toStream(std::ostream& out, const DefineFunctionCommand* c, bool cvc3Mode) throw() {
   Expr func = c->getFunction();
   const vector<Expr>& formals = c->getFormals();
   Expr formula = c->getFormula();
@@ -1016,7 +1028,7 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw()
   out << formula << ";";
 }
 
-static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() {
+static void toStream(std::ostream& out, const DeclareTypeCommand* c, bool cvc3Mode) throw() {
   if(c->getArity() > 0) {
     out << "ERROR: Don't know how to print parameterized type declaration "
            "in CVC language:" << endl << c->toString() << endl;
@@ -1025,7 +1037,7 @@ static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() {
   }
 }
 
-static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() {
+static void toStream(std::ostream& out, const DefineTypeCommand* c, bool cvc3Mode) throw() {
   if(c->getParameters().size() > 0) {
     out << "ERROR: Don't know how to print parameterized type definition "
            "in CVC language:" << endl << c->toString() << endl;
@@ -1034,15 +1046,15 @@ static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() {
   }
 }
 
-static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) throw() {
-  toStream(out, static_cast<const DefineFunctionCommand*>(c));
+static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c, bool cvc3Mode) throw() {
+  toStream(out, static_cast<const DefineFunctionCommand*>(c), cvc3Mode);
 }
 
-static void toStream(std::ostream& out, const SimplifyCommand* c) throw() {
+static void toStream(std::ostream& out, const SimplifyCommand* c, bool cvc3Mode) throw() {
   out << "TRANSFORM " << c->getTerm() << ";";
 }
 
-static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
+static void toStream(std::ostream& out, const GetValueCommand* c, bool cvc3Mode) throw() {
   const vector<Expr>& terms = c->getTerms();
   Assert(!terms.empty());
   out << "GET_VALUE ";
@@ -1050,51 +1062,51 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
   out << terms.back() << ";";
 }
 
-static void toStream(std::ostream& out, const GetModelCommand* c) throw() {
+static void toStream(std::ostream& out, const GetModelCommand* c, bool cvc3Mode) throw() {
   out << "COUNTERMODEL;";
 }
 
-static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {
+static void toStream(std::ostream& out, const GetAssignmentCommand* c, bool cvc3Mode) throw() {
   out << "% (get-assignment)";
 }
 
-static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() {
+static void toStream(std::ostream& out, const GetAssertionsCommand* c, bool cvc3Mode) throw() {
   out << "WHERE;";
 }
 
-static void toStream(std::ostream& out, const GetProofCommand* c) throw() {
+static void toStream(std::ostream& out, const GetProofCommand* c, bool cvc3Mode) throw() {
   out << "DUMP_PROOF;";
 }
 
-static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() {
+static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c, bool cvc3Mode) throw() {
   out << "% (set-info :status " << c->getStatus() << ")";
 }
 
-static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw() {
+static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c, bool cvc3Mode) throw() {
   out << "OPTION \"logic\" \"" << c->getLogic() << "\";";
 }
 
-static void toStream(std::ostream& out, const SetInfoCommand* c) throw() {
+static void toStream(std::ostream& out, const SetInfoCommand* c, bool cvc3Mode) throw() {
   out << "% (set-info " << c->getFlag() << " ";
   toStream(out, c->getSExpr());
   out << ")";
 }
 
-static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
+static void toStream(std::ostream& out, const GetInfoCommand* c, bool cvc3Mode) throw() {
   out << "% (get-info " << c->getFlag() << ")";
 }
 
-static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
+static void toStream(std::ostream& out, const SetOptionCommand* c, bool cvc3Mode) throw() {
   out << "OPTION \"" << c->getFlag() << "\" ";
   toStream(out, c->getSExpr());
   out << ";";
 }
 
-static void toStream(std::ostream& out, const GetOptionCommand* c) throw() {
+static void toStream(std::ostream& out, const GetOptionCommand* c, bool cvc3Mode) throw() {
   out << "% (get-option " << c->getFlag() << ")";
 }
 
-static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() {
+static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, bool cvc3Mode) throw() {
   const vector<DatatypeType>& datatypes = c->getDatatypes();
   out << "DATATYPE" << endl;
   bool firstDatatype = true;
@@ -1144,44 +1156,44 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr
   out << endl << "END;";
 }
 
-static void toStream(std::ostream& out, const CommentCommand* c) throw() {
+static void toStream(std::ostream& out, const CommentCommand* c, bool cvc3Mode) throw() {
   out << "% " << c->getComment();
 }
 
-static void toStream(std::ostream& out, const EmptyCommand* c) throw() {
+static void toStream(std::ostream& out, const EmptyCommand* c, bool cvc3Mode) throw() {
 }
 
-static void toStream(std::ostream& out, const EchoCommand* c) throw() {
+static void toStream(std::ostream& out, const EchoCommand* c, bool cvc3Mode) throw() {
   out << "ECHO \"" << c->getOutput() << "\";";
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const Command* c) throw() {
+static bool tryToStream(std::ostream& out, const Command* c, bool cvc3Mode) throw() {
   if(typeid(*c) == typeid(T)) {
-    toStream(out, dynamic_cast<const T*>(c));
+    toStream(out, dynamic_cast<const T*>(c), cvc3Mode);
     return true;
   }
   return false;
 }
 
-static void toStream(std::ostream& out, const CommandSuccess* s) throw() {
+static void toStream(std::ostream& out, const CommandSuccess* s, bool cvc3Mode) throw() {
   if(Command::printsuccess::getPrintSuccess(out)) {
     out << "OK" << endl;
   }
 }
 
-static void toStream(std::ostream& out, const CommandUnsupported* s) throw() {
+static void toStream(std::ostream& out, const CommandUnsupported* s, bool cvc3Mode) throw() {
   out << "UNSUPPORTED" << endl;
 }
 
-static void toStream(std::ostream& out, const CommandFailure* s) throw() {
+static void toStream(std::ostream& out, const CommandFailure* s, bool cvc3Mode) throw() {
   out << s->getMessage() << endl;
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() {
+static bool tryToStream(std::ostream& out, const CommandStatus* s, bool cvc3Mode) throw() {
   if(typeid(*s) == typeid(T)) {
-    toStream(out, dynamic_cast<const T*>(s));
+    toStream(out, dynamic_cast<const T*>(s), cvc3Mode);
     return true;
   }
   return false;

diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index 15b04488d21d36d2363d1f0420c892d9d1566090..ec08b36b1e80b963010b2b85f61556fb58363bfa 100644 (file)
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -28,10 +28,13 @@ namespace printer {
 namespace cvc {
 
 class CvcPrinter : public CVC4::Printer {
+  bool d_cvc3Mode;
+
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const throw();
   void toStream(std::ostream& out, const Model& m, const Command* c) const throw();
 public:
   using CVC4::Printer::toStream;
+  CvcPrinter(bool cvc3Mode = false) : d_cvc3Mode(cvc3Mode) { }
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 4fb2ff12ca91f15c8aa9c9e4b0a050f053f5f167..24b9f274d9b43af14e8362e86971e85ab64808b4 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -55,6 +55,9 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() {
   case LANG_AST:
     return new printer::ast::AstPrinter();
 
+  case LANG_CVC3:
+    return new printer::cvc::CvcPrinter(/* cvc3-mode = */ true);
+
   default:
     Unhandled(lang);
   }

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index a903b257648595d3556517f7ce4c6fa603edb5b4..15101b0e4fe9b8e3559bb65b56c2a6018983734e 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -767,9 +767,9 @@ void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const thro
 
 
 void Smt2Printer::toStream(std::ostream& out, const Model& m) const throw() {
-  out << "(model" << std::endl;
+  out << "(model" << endl;
   this->Printer::toStream(out, m);
-  out << ")" << std::endl;
+  out << ")" << endl;
 }
 
 
@@ -783,23 +783,23 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
       for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
         out << "(" << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << ")";
       }
-      out << ")))" << std::endl;
+      out << ")))" << endl;
     } else {
       if( tn.isSort() ){
         //print the cardinality
         if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
-          out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << std::endl;
+          out << "; cardinality of " << tn << " is " << (*tm.d_rep_set.d_type_reps.find(tn)).second.size() << endl;
         }
       }
-      out << c << std::endl;
+      out << c << endl;
       if( tn.isSort() ){
         //print the representatives
         if( tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
           for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
             if( (*tm.d_rep_set.d_type_reps.find(tn)).second[i].isVar() ){
-              out << "(declare-fun " << quoteSymbol((*tm.d_rep_set.d_type_reps.find(tn)).second[i]) << " () " << tn << ")" << std::endl;
+              out << "(declare-fun " << quoteSymbol((*tm.d_rep_set.d_type_reps.find(tn)).second[i]) << " () " << tn << ")" << endl;
             }else{
-              out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << std::endl;
+              out << "; rep: " << (*tm.d_rep_set.d_type_reps.find(tn)).second[i] << endl;
             }
           }
         }
@@ -820,7 +820,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
     if(val.getKind() == kind::LAMBDA) {
       out << "(define-fun " << n << " " << val[0]
           << " " << n.getType().getRangeType()
-          << " " << val[1] << ")" << std::endl;
+          << " " << val[1] << ")" << endl;
     } else {
       if( options::modelUninterpDtEnum() && val.getKind() == kind::STORE ) {
         TypeNode tn = val[1].getType();
@@ -830,7 +830,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
         }
       }
       out << "(define-fun " << n << " () "
-          << n.getType() << " " << val << ")" << std::endl;
+          << n.getType() << " " << val << ")" << endl;
     }
 /*
     //for table format (work in progress)
@@ -856,7 +856,7 @@ void Smt2Printer::toStream(std::ostream& out, const Model& m, const Command* c)
     }
 */
   }else{
-    out << c << std::endl;
+    out << c << endl;
   }
 }
 
@@ -886,7 +886,7 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
     out << PushCommand() << endl
         << AssertCommand(e) << endl
         << CheckSatCommand() << endl
-        << PopCommand() << endl;
+        << PopCommand();
   } else {
     out << "(check-sat)";
   }
@@ -898,7 +898,7 @@ static void toStream(std::ostream& out, const QueryCommand* c) throw() {
     out << PushCommand() << endl
         << AssertCommand(BooleanSimplification::negate(e)) << endl
         << CheckSatCommand() << endl
-        << PopCommand() << endl;
+        << PopCommand();
   } else {
     out << "(check-sat)";
   }
@@ -909,10 +909,16 @@ static void toStream(std::ostream& out, const QuitCommand* c) throw() {
 }
 
 static void toStream(std::ostream& out, const CommandSequence* c) throw() {
-  for(CommandSequence::const_iterator i = c->begin();
-      i != c->end();
-      ++i) {
-    out << *i << endl;
+  CommandSequence::const_iterator i = c->begin();
+  if(i != c->end()) {
+    for(;;) {
+      out << *i;
+      if(++i != c->end()) {
+        out << endl;
+      } else {
+        break;
+      }
+    }
   }
 }
 
@@ -996,7 +1002,7 @@ static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
   out << "(get-value ( ";
   const vector<Expr>& terms = c->getTerms();
   copy(terms.begin(), terms.end(), ostream_iterator<Expr>(out, " "));
-  out << " ))";
+  out << "))";
 }
 
 static void toStream(std::ostream& out, const GetModelCommand* c) throw() {

diff --git a/src/util/language.cpp b/src/util/language.cpp
index 8a1ab26af07042cf988b554b33b5828935bf77b3..1a184e64865c1d51d1b1b0b424dc1c4552a4e968 100644 (file)
--- a/src/util/language.cpp
+++ b/src/util/language.cpp
@@ -68,6 +68,8 @@ OutputLanguage toOutputLanguage(std::string language) {
      language == "presentation" || language == "native" ||
      language == "LANG_CVC4") {
     return output::LANG_CVC4;
+  } else if(language == "cvc3" || language == "LANG_CVC3") {
+    return output::LANG_CVC3;
   } else if(language == "smtlib1" || language == "smt1" ||
             language == "LANG_SMTLIB_V1") {
     return output::LANG_SMTLIB_V1;

diff --git a/src/util/language.h b/src/util/language.h
index c79c4d9aa11103795babf9e067f30b992c7a58a4..0d1c5486ae550120eb27025d63168b84b59fe463 100644 (file)
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -121,6 +121,8 @@ enum CVC4_PUBLIC Language {
 
   /** The AST output language */
   LANG_AST = 10,
+  /** The CVC3-compatibility output language */
+  LANG_CVC3,
 
   /** LANG_MAX is > any valid OutputLanguage id */
   LANG_MAX
@@ -147,6 +149,9 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_AST:
     out << "LANG_AST";
     break;
+  case LANG_CVC3:
+    out << "LANG_CVC3";
+    break;
   default:
     out << "undefined_output_language";
   }