* (define-fun...) now has proper type checking in non-debug builds

  (resolves bug #212)

* also closed some other type checking loopholes in SmtEngine

* small fixes to define-sort (resolves bug #214)

* infrastructural support for printing expressions in languages
  other than the internal representation language using an IO
  manipulator, e.g.:

    cout << Expr::setlanguage(language::output::LANG_SMTLIB_V2) << expr;

  main() sets the output language for all streams to correspond to
  the input language

* support delaying type checking in debug builds, so that one can debug
  the type checker itself (before it was difficult, because debug builds did
  all the type checking on Node creation!): new command-line flag
  --no-early-type-checking (only makes sense for debug builds)

* disallowed copy-construction of ExprManager and NodeManager, and made other
  constructors explicit; previously it was easy to unintentionally create
  duplicate managers, with really weird results (i.e., disappearing
  attributes!)

1 files changed, 83 insertions, 14 deletions

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 29164ffa5..2eac4ab62 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -26,6 +26,7 @@
 #include <stdint.h>
 
 #include "util/exception.h"
+#include "util/language.h"
 
 ${includes}
 
@@ -33,7 +34,7 @@ ${includes}
 // compiler directs the user to the template file instead of the
 // generated one.  We don't want the user to modify the generated one,
 // since it'll get overwritten on a later build.
-#line 37 "${template}"
+#line 38 "${template}"
 
 namespace CVC4 {
 
@@ -45,6 +46,8 @@ class Expr;
 class ExprManager;
 class SmtEngine;
 class Type;
+class TypeCheckingException;
+class TypeCheckingExceptionPrivate;
 
 namespace smt {
   class SmtEnginePrivate;
@@ -53,6 +56,7 @@ namespace smt {
 namespace expr {
   class CVC4_PUBLIC ExprSetDepth;
   class CVC4_PUBLIC ExprPrintTypes;
+  class CVC4_PUBLIC ExprSetLanguage;
 }/* CVC4::expr namespace */
 
 /**
@@ -61,6 +65,7 @@ namespace expr {
 class CVC4_PUBLIC TypeCheckingException : public Exception {
 
   friend class SmtEngine;
+  friend class smt::SmtEnginePrivate;
 
 private:
 
@@ -69,8 +74,10 @@ private:
 
 protected:
 
-  TypeCheckingException(): Exception() {}
+  TypeCheckingException() : Exception() {}
   TypeCheckingException(const Expr& expr, std::string message);
+  TypeCheckingException(ExprManager* em,
+                        const TypeCheckingExceptionPrivate* exc);
 
 public:
 
@@ -97,6 +104,14 @@ std::ostream& operator<<(std::ostream& out,
                          const TypeCheckingException& e) CVC4_PUBLIC;
 
 /**
+ * Output operator for expressions
+ * @param out the stream to output to
+ * @param e the expression to output
+ * @return the stream
+ */
+std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
+
+/**
  * Class encapsulating CVC4 expressions and methods for constructing new
  * expressions.
  */
@@ -281,7 +296,7 @@ public:
    * type checking is not requested, getType() will do the minimum
    * amount of checking required to return a valid result.
    *
-   * @param check whether we should check the type as we compute it 
+   * @param check whether we should check the type as we compute it
    * (default: false)
    */
   Type getType(bool check = false) const throw (TypeCheckingException);
@@ -296,7 +311,8 @@ public:
    * Outputs the string representation of the expression to the stream.
    * @param out the output stream
    */
-  void toStream(std::ostream& out, int depth = -1, bool types = false) const;
+  void toStream(std::ostream& out, int depth = -1, bool types = false,
+                OutputLanguage lang = language::output::LANG_AST) const;
 
   /**
    * Check if this is a null expression.
@@ -367,6 +383,11 @@ public:
   typedef expr::ExprPrintTypes printtypes;
 
   /**
+   * IOStream manipulator to set the output language for Exprs.
+   */
+  typedef expr::ExprSetLanguage setlanguage;
+
+  /**
    * Very basic pretty printer for Expr.
    * This is equivalent to calling e.getNode().printAst(...)
    * @param out output stream to print to.
@@ -402,15 +423,10 @@ protected:
   friend class SmtEngine;
   friend class smt::SmtEnginePrivate;
   friend class ExprManager;
-};
+  friend class TypeCheckingException;
+  friend std::ostream& operator<<(std::ostream& out, const Expr& e);
 
-/**
- * Output operator for expressions
- * @param out the stream to output to
- * @param e the expression to output
- * @return the stream
- */
-std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;
+};/* class Expr */
 
 /**
  * Extending the expression with the capability to construct Boolean
@@ -551,7 +567,7 @@ public:
   static inline void setDepth(std::ostream& out, long depth) {
     out.iword(s_iosIndex) = depth;
   }
-};
+};/* class ExprSetDepth */
 
 /**
  * IOStream manipulator to print type ascriptions or not.
@@ -598,11 +614,50 @@ public:
   }
 };/* class ExprPrintTypes */
 
+/**
+ * IOStream manipulator to set the output language for Exprs.
+ */
+class CVC4_PUBLIC ExprSetLanguage {
+  /**
+   * The allocated index in ios_base for our depth setting.
+   */
+  static const int s_iosIndex;
+
+  /**
+   * The default language to use, for ostreams that haven't yet had a
+   * setlanguage() applied to them.
+   */
+  static const int s_defaultLanguage = language::output::LANG_AST;
+
+  /**
+   * When this manipulator is used, the setting is stored here.
+   */
+  OutputLanguage d_language;
+
+public:
+  /**
+   * Construct a ExprSetLanguage with the given setting.
+   */
+  ExprSetLanguage(OutputLanguage l) : d_language(l) {}
+
+  inline void applyLanguage(std::ostream& out) {
+    out.iword(s_iosIndex) = int(d_language);
+  }
+
+  static inline OutputLanguage getLanguage(std::ostream& out) {
+    return OutputLanguage(out.iword(s_iosIndex));
+  }
+
+  static inline void setLanguage(std::ostream& out, OutputLanguage l) {
+    out.iword(s_iosIndex) = int(l);
+  }
+};/* class ExprSetLanguage */
+
 }/* CVC4::expr namespace */
 
 ${getConst_instantiations}
 
-#line 566 "${template}"
+#line 659 "${template}"
 
 namespace expr {
 
@@ -634,6 +689,20 @@ inline std::ostream& operator<<(std::ostream& out, ExprPrintTypes pt) {
   return out;
 }
 
+/**
+ * Sets the output language when pretty-printing a Expr to an ostream.
+ * Use like this:
+ *
+ *   // let out be an ostream, e an Expr
+ *   out << Expr::setlanguage(LANG_SMTLIB_V2) << e << endl;
+ *
+ * The setting stays permanently (until set again) with the stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, ExprSetLanguage l) {
+  l.applyLanguage(out);
+  return out;
+}
+
 }/* CVC4::expr namespace */
 
 // for hash_maps, hash_sets..