* (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!)

2 files changed, 30 insertions, 5 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index fc2c8550e..de2fa4ebc 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -199,11 +199,12 @@ void SmtEngine::defineFunction(Expr func,
   Type formulaType = formula.getType(true);// type check body
   if(formulaType != FunctionType(func.getType()).getRangeType()) {
     stringstream ss;
-    ss << "Defined function's declared type does not match type of body\n"
-       << "The function: " << func << "\n"
-       << "Its type    : " << func.getType() << "\n"
-       << "The body    : " << formula << "\n"
-       << "Body type   : " << formulaType << "\n";
+    ss << "Defined function's declared type does not match that of body\n"
+       << "The function  : " << func << "\n"
+       << "Its range type: "
+       << FunctionType(func.getType()).getRangeType() << "\n"
+       << "The body      : " << formula << "\n"
+       << "Body type     : " << formulaType;
     throw TypeCheckingException(func, ss.str());
   }
   TNode funcNode = func.getTNode();
@@ -305,9 +306,22 @@ void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n)
   smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, n));
 }
 
+void SmtEngine::ensureBoolean(const BoolExpr& e) {
+  Type type = e.getType(true);
+  Type boolType = d_exprManager->booleanType();
+  if(type != boolType) {
+    stringstream ss;
+    ss << "Expected " << boolType << "\n"
+       << "The assertion : " << e << "\n"
+       << "Its type      : " << type;
+    throw TypeCheckingException(e, ss.str());
+  }
+}
+
 Result SmtEngine::checkSat(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT checkSat(" << e << ")" << endl;
+  ensureBoolean(e);// ensure expr is type-checked at this point
   SmtEnginePrivate::addFormula(*this, e.getNode());
   Result r = check().asSatisfiabilityResult();
   Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << endl;
@@ -317,6 +331,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
 Result SmtEngine::query(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT query(" << e << ")" << endl;
+  ensureBoolean(e);// ensure expr is type-checked at this point
   SmtEnginePrivate::addFormula(*this, e.getNode().notNode());
   Result r = check().asValidityResult();
   Debug("smt") << "SMT query(" << e << ") ==> " << r << endl;
@@ -326,12 +341,14 @@ Result SmtEngine::query(const BoolExpr& e) {
 Result SmtEngine::assertFormula(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT assertFormula(" << e << ")" << endl;
+  ensureBoolean(e);// type check node
   SmtEnginePrivate::addFormula(*this, e.getNode());
   return quickCheck().asValidityResult();
 }
 
 Expr SmtEngine::simplify(const Expr& e) {
   NodeManagerScope nms(d_nodeManager);
+  e.getType(true);// ensure expr is type-checked at this point
   Debug("smt") << "SMT simplify(" << e << ")" << endl;
   Unimplemented();
 }
@@ -352,6 +369,8 @@ Expr SmtEngine::getValue(Expr term)
   // assertions
 
   NodeManagerScope nms(d_nodeManager);
+  Type type = term.getType(true);// ensure expr is type-checked at this point
+  SmtEnginePrivate::preprocess(*this, term.getNode());
 
   Unimplemented();
 }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index fd132a0c6..1fd68d2a5 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -132,6 +132,12 @@ class CVC4_PUBLIC SmtEngine {
    */
   Result quickCheck();
 
+  /**
+   * Fully type-check the argument, and also type-check that it's
+   * actually Boolean.
+   */
+  void ensureBoolean(const BoolExpr& e);
+
   friend class ::CVC4::smt::SmtEnginePrivate;
 
 public: