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.)

8 files changed, 21 insertions, 30 deletions

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 83bbb25a7..e848cf9a9 100644
--- 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 a7c792692..93885d75f 100755
--- 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 4f7e2a692..3b7900878 100644
--- 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 f8e754868..4ae66f510 100644
--- 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 6791b6c51..6dbf4ed03 100644
--- 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 28ecc11c4..842325869 100644
--- 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 b99eda5ca..0734dec6c 100644
--- 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 99f197ff7..dba8a0f29 100644
--- 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"