some bugfixes that come as a result of debugging some CASCADE/C stuff..

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 83bbb25a78d2028c2a3b0db85480bf62f4f90064..e848cf9a93a4f564307aee7a466b5020ebcb7aeb 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -375,7 +375,13 @@ public:
    * @return the string representation of this type.
    */
   inline std::string toString() const {
-    return d_nv->toString();
+    std::stringstream ss;
+    OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AST : options::outputLanguage();
+    d_nv->toStream(ss, -1, false, 0,
+                   outlang == language::output::LANG_AUTO ?
+                     language::output::LANG_AST :
+                     outlang);
+    return ss.str();
   }
 
   /**
@@ -383,15 +389,10 @@ public:
    * given stream
    *
    * @param out the stream to serialize this node to
-   * @param toDepth the depth to which to print this expression, or -1 to
-   * print it fully
-   * @param types set to true to ascribe types to the output expressions
-   * (might break language compliance, but good for debugging expressions)
    * @param language the language in which to output
    */
-  inline void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
-                       OutputLanguage language = language::output::LANG_AST) const {
-    d_nv->toStream(out, toDepth, types, dag, language);
+  inline void toStream(std::ostream& out, OutputLanguage language = language::output::LANG_AST) const {
+    d_nv->toStream(out, -1, false, 0, language);
   }
 
   /**
@@ -634,11 +635,7 @@ private:
  * @return the stream
  */
 inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
-  n.toStream(out,
-             Node::setdepth::getDepth(out),
-             Node::printtypes::getPrintTypes(out),
-             Node::dag::getDag(out),
-             Node::setlanguage::getLanguage(out));
+  n.toStream(out, Node::setlanguage::getLanguage(out));
   return out;
 }
 

diff --git a/src/options/mkoptions b/src/options/mkoptions
index a7c792692f3e427c598a34b0791ddde9eaa59668..93885d75f6227c7c38c57d8beb2608a3d038267a 100755 (executable)
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -1134,8 +1134,7 @@ function output_module {
 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
 /* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
 
-/* Edit the template file instead:                     */
-/* $1 */
+/* Edit the template file instead.                     */
 
 EOF
   fi

diff --git a/src/options/options.h b/src/options/options.h
index 4f7e2a69208fbef85622c8bfc61b5c059c35aafe..3b79008780e0f11921ddc38e9d3b2dfcdf60dc0f 100644 (file)
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -126,16 +126,6 @@ public:
    */
   std::vector<std::string> parseOptions(int argc, char* argv[]) throw(OptionException);
 
-  /**
-   * Set the output language based on the given string.
-   */
-  void setOutputLanguage(const char* str) throw(OptionException);
-
-  /**
-   * Set the input language based on the given string.
-   */
-  void setInputLanguage(const char* str) throw(OptionException);
-
 };/* class Options */
 
 }/* CVC4 namespace */

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index f8e7548687977fd075b647446978bbff6dd07716..4ae66f51054ec5a4f2b37d7c67111840b08f819d 100644 (file)
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -89,7 +89,7 @@ void AstPrinter::toStream(std::ostream& out, TNode n,
     if(types) {
       // print the whole type, but not *its* type
       out << ":";
-      n.getType().toStream(out, -1, false, 0, language::output::LANG_AST);
+      n.getType().toStream(out, language::output::LANG_AST);
     }
 
     return;

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 6791b6c51cd465a99b0d75e936bb20e47e935ceb..6dbf4ed030bab7b1b1fd8051821cacd9b7d5f267 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -98,7 +98,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
     if(types) {
       // print the whole type, but not *its* type
       out << ":";
-      n.getType().toStream(out, -1, false, false, language::output::LANG_CVC4);
+      n.getType().toStream(out, language::output::LANG_CVC4);
     }
     return;
   }

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 28ecc11c4e89a4abe682608bec79c461ec764cfe..8423258693f3154e10365f815aa03e77d9a23f33 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -97,7 +97,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     if(types) {
       // print the whole type, but not *its* type
       out << ":";
-      n.getType().toStream(out, -1, false, 0, language::output::LANG_SMTLIB_V2);
+      n.getType().toStream(out, language::output::LANG_SMTLIB_V2);
     }
 
     return;

diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index b99eda5ca816bea841b57aa981d2e5f208000d31..0734dec6c72cd4cb0e6d7ba5a2e1dcdb5d0de93f 100644 (file)
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -58,11 +58,11 @@ class CVC4_PUBLIC SExpr {
 
 public:
 
-  class Keyword : protected std::string {
+  class CVC4_PUBLIC Keyword : protected std::string {
   public:
     Keyword(const std::string& s) : std::string(s) {}
     const std::string& getString() const { return *this; }
-  };/* class Keyword */
+  };/* class SExpr::Keyword */
 
   SExpr() :
     d_sexprType(SEXPR_STRING),

diff --git a/src/util/sexpr.i b/src/util/sexpr.i
index 99f197ff7627b89f372f3d6ec63f59ed41cc57a4..dba8a0f2921c1f75a811a081aae1a8b7352b29b6 100644 (file)
--- a/src/util/sexpr.i
+++ b/src/util/sexpr.i
@@ -5,4 +5,9 @@
 %ignore CVC4::operator<<(std::ostream&, const SExpr&);
 %ignore CVC4::operator<<(std::ostream&, SExpr::SexprTypes);
 
+// for Java and the like
+%extend CVC4::SExpr {
+  std::string toString() const { return self->getValue(); }
+};/* CVC4::SExpr */
+
 %include "util/sexpr.h"