type checking for define-fun in production builds; related to (and might resolve) bug 212

11 files changed, 93 insertions, 43 deletions

diff --git a/configure.ac b/configure.ac
index d2033ac1f..ced90d56f 100644
--- a/configure.ac
+++ b/configure.ac
@@ -228,10 +228,10 @@ if test $cvc4_use_cln = 1; then
     [cvc4_use_cln=1],
     [if test $cvc4_use_cln = 0; then
        # fall back to GMP
-       AC_MSG_NOTICE([CLN not installed (or too old), will use gmp])
+       AC_MSG_NOTICE([CLN not installed (or too old) or pkgconfig missing, will use gmp])
      else
        # fail
-       AC_MSG_ERROR([CLN not installed (or too old)])
+       AC_MSG_ERROR([CLN not installed (or too old) or pkgconfig missing])
      fi
     ]
   )
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index bb227f92f..29164ffa5 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -60,6 +60,8 @@ namespace expr {
  */
 class CVC4_PUBLIC TypeCheckingException : public Exception {
 
+  friend class SmtEngine;
+
 private:
 
   /** The expression responsible for the error */
diff --git a/src/expr/node.h b/src/expr/node.h
index bd6b53522..871f1e0d7 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -53,7 +53,7 @@ class TypeCheckingExceptionPrivate : public Exception {
 
 private:
 
-  /** The node repsonsible for the failure */
+  /** The node responsible for the failure */
   NodeTemplate<true>* d_node;
 
 protected:
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index c0f489d7a..0860365bc 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -789,15 +789,11 @@ inline TypeNode NodeManager::mkSort(TypeNode constructor,
          constructor.getNumChildren() == 0,
          "expected a sort constructor");
   Assert(children.size() > 0, "expected non-zero # of children");
-  uint64_t arity;
-  std::string name;
-  bool hasArityAttribute =
-    getAttribute(constructor.d_nv, expr::SortArityAttr(), arity);
-  Assert(hasArityAttribute, "expected a sort constructor");
-  bool hasNameAttribute =
-    getAttribute(constructor.d_nv, expr::VarNameAttr(), name);
-  Assert(hasNameAttribute, "expected a sort constructor");
-  Assert(arity == children.size(),
+  Assert( hasAttribute(constructor.d_nv, expr::SortArityAttr()) &&
+          hasAttribute(constructor.d_nv, expr::VarNameAttr()),
+          "expected a sort constructor" );
+  std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr());
+  Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) == children.size(),
          "arity mismatch in application of sort constructor");
   NodeBuilder<> nb(this, kind::SORT_TYPE);
   Node sortTag = Node(constructor.d_nv->d_children[0]);
diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index 82214bed3..113b8a5f7 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -73,7 +73,9 @@ enum OptionValue {
   UF_THEORY,
   LAZY_DEFINITION_EXPANSION,
   INTERACTIVE,
-  NO_INTERACTIVE
+  NO_INTERACTIVE,
+  PRODUCE_MODELS,
+  PRODUCE_ASSIGNMENTS
 };/* enum OptionValue */
 
 /**
@@ -123,6 +125,8 @@ static struct option cmdlineOptions[] = {
   { "lazy-definition-expansion", no_argument, NULL, LAZY_DEFINITION_EXPANSION },
   { "interactive", no_argument      , NULL, INTERACTIVE },
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
+  { "produce-models", no_argument   , NULL, PRODUCE_MODELS},
+  { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS},
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -288,6 +292,14 @@ throw(OptionException) {
       opts->interactiveSetByUser = true;
       break;
 
+    case PRODUCE_MODELS:
+      opts->produceModels = true;
+      break;
+
+    case PRODUCE_ASSIGNMENTS:
+      opts->produceAssignments = true;
+      break;
+
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");
diff --git a/src/main/usage.h b/src/main/usage.h
index 2be5f092e..15a30a426 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -46,8 +46,12 @@ CVC4 options:\n\
    --stats                give statistics on exit\n\
    --default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
    --print-expr-types     print types with variables when printing exprs\n\
-   --uf=morgan|tim        select uninterpreted function theory implementation\n"
-;
+   --uf=morgan|tim        select uninterpreted function theory implementation\n\
+   --interactive          run interactively\n\
+   --no-interactive       do not run interactively\n\
+   --produce-models       support the get-value command\n\
+   --produce-assignments  support the get-assignment command\n\
+   --lazy-definition-expansion expand define-fun lazily\n";
 
 }/* CVC4::main namespace */
 }/* CVC4 namespace */
diff --git a/src/smt/noninteractive_exception.h b/src/smt/modal_exception.h
index 4cf97ab3e..c5c0f6ab2 100644
--- a/src/smt/noninteractive_exception.h
+++ b/src/smt/modal_exception.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file noninteractive_exception.h
+/*! \file modal_exception.h
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
@@ -21,29 +21,29 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H
-#define __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H
+#ifndef __CVC4__SMT__MODAL_EXCEPTION_H
+#define __CVC4__SMT__MODAL_EXCEPTION_H
 
 #include "util/exception.h"
 
 namespace CVC4 {
 
-class CVC4_PUBLIC NoninteractiveException : public CVC4::Exception {
+class CVC4_PUBLIC ModalException : public CVC4::Exception {
 public:
-  NoninteractiveException() :
-    Exception("Interactive feature used while operating in "
-              "non-interactive mode") {
+  ModalException() :
+    Exception("Feature used while operating in "
+              "incorrect state") {
   }
 
-  NoninteractiveException(const std::string& msg) :
+  ModalException(const std::string& msg) :
     Exception(msg) {
   }
 
-  NoninteractiveException(const char* msg) :
+  ModalException(const char* msg) :
     Exception(msg) {
   }
-};/* class NoninteractiveException */
+};/* class ModalException */
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__SMT__NONINTERACTIVE_EXCEPTION_H */
+#endif /* __CVC4__SMT__MODAL_EXCEPTION_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c41737028..5bf5ebd69 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -20,7 +20,7 @@
 #include <string>
 
 #include "smt/smt_engine.h"
-#include "smt/noninteractive_exception.h"
+#include "smt/modal_exception.h"
 #include "smt/bad_option_exception.h"
 #include "smt/no_such_function_exception.h"
 #include "context/context.h"
@@ -191,6 +191,16 @@ void SmtEngine::defineFunction(Expr func,
                                const vector<Expr>& formals,
                                Expr formula) {
   NodeManagerScope nms(d_nodeManager);
+  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";
+    throw TypeCheckingException(func, ss.str());
+  }
   TNode funcNode = func.getTNode();
   vector<Node> formalsNodes;
   for(vector<Expr>::const_iterator i = formals.begin(),
@@ -321,29 +331,45 @@ Expr SmtEngine::simplify(const Expr& e) {
   Unimplemented();
 }
 
-Model SmtEngine::getModel() {
+Expr SmtEngine::getValue(Expr term)
+  throw(ModalException, AssertionException) {
+  if(!d_options->interactive) {
+    const char* msg =
+      "Cannot get value when not in interactive mode.";
+    throw ModalException(msg);
+  }
+  if(!d_options->produceModels) {
+    const char* msg =
+      "Cannot get value when produce-models options is off.";
+    throw ModalException(msg);
+  }
+  // TODO also check that the last query was sat/unknown, without intervening
+  // assertions
+
   NodeManagerScope nms(d_nodeManager);
+
   Unimplemented();
 }
 
-Expr SmtEngine::getValue(Expr term)
-  throw(NoninteractiveException, AssertionException) {
-  if(!d_options->interactive) {
+SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
+  if(!d_options->produceAssignments) {
     const char* msg =
-      "Cannot query the current assertion list when not in interactive mode.";
-    throw NoninteractiveException(msg);
+      "Cannot get the current assignment when produce-assignments option is off.";
+    throw ModalException(msg);
   }
+  // TODO also check that the last query was sat/unknown, without intervening
+  // assertions
 
   NodeManagerScope nms(d_nodeManager);
 
   Unimplemented();
 }
 
-vector<Expr> SmtEngine::getAssertions() throw(NoninteractiveException) {
+vector<Expr> SmtEngine::getAssertions() throw(ModalException, AssertionException) {
   if(!d_options->interactive) {
     const char* msg =
       "Cannot query the current assertion list when not in interactive mode.";
-    throw NoninteractiveException(msg);
+    throw ModalException(msg);
   }
   Assert(d_assertionList != NULL);
   return vector<Expr>(d_assertionList->begin(), d_assertionList->end());
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index c9bf321b9..fd132a0c6 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -30,7 +30,7 @@
 #include "util/model.h"
 #include "util/sexpr.h"
 #include "util/hash.h"
-#include "smt/noninteractive_exception.h"
+#include "smt/modal_exception.h"
 #include "smt/no_such_function_exception.h"
 #include "smt/bad_option_exception.h"
 
@@ -207,22 +207,24 @@ public:
   Expr simplify(const Expr& e);
 
   /**
-   * Get a (counter)model (only if preceded by a SAT or INVALID query).
+   * Get the assigned value of a term (only if preceded by a SAT or
+   * INVALID query).  Only permitted if the SmtEngine is set to
+   * operate interactively and produce-models is on.
    */
-  Model getModel();
+  Expr getValue(Expr term) throw(ModalException, AssertionException);
 
   /**
    * Get the assigned value of a term (only if preceded by a SAT or
    * INVALID query).  Only permitted if the SmtEngine is set to
-   * operate interactively.
+   * operate interactively and produce-assignments is on.
    */
-  Expr getValue(Expr term) throw(NoninteractiveException, AssertionException);
+  SExpr getAssignment() throw(ModalException, AssertionException);
 
   /**
    * Get the current set of assertions.  Only permitted if the
    * SmtEngine is set to operate interactively.
    */
-  std::vector<Expr> getAssertions() throw(NoninteractiveException);
+  std::vector<Expr> getAssertions() throw(ModalException, AssertionException);
 
   /**
    * Push a user-level context.
diff --git a/src/util/options.h b/src/util/options.h
index 9bb0b0a38..08de590d8 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -77,6 +77,12 @@ struct CVC4_PUBLIC Options {
    */
   bool interactiveSetByUser;
 
+  /** Whether we support SmtEngine::getValue() for this run. */
+  bool produceModels;
+
+  /** Whether we support SmtEngine::getAssignment() for this run. */
+  bool produceAssignments;
+
   Options() :
     binary_name(),
     statistics(false),
@@ -91,7 +97,9 @@ struct CVC4_PUBLIC Options {
     strictParsing(false),
     lazyDefinitionExpansion(false),
     interactive(false),
-    interactiveSetByUser(false) {
+    interactiveSetByUser(false),
+    produceModels(false),
+    produceAssignments(false) {
   }
 };/* struct Options */
 
diff --git a/test/regress/regress0/simple-rdl-definefun.smt2 b/test/regress/regress0/simple-rdl-definefun.smt2
index 08e99867a..c04a1ed64 100644
--- a/test/regress/regress0/simple-rdl-definefun.smt2
+++ b/test/regress/regress0/simple-rdl-definefun.smt2
@@ -7,7 +7,7 @@
 (define-sort F (x) (A Real Real))
 (declare-fun x2 () (F Real))
 (define-fun minus ((x Real) (z Real)) Real (- x z))
-(define-fun less ((x Real) (z Real)) Bool (< x z))
+(define-fun less ((x Real) (z Real)) Real (< x z))
 (define-fun foo ((x Real) (z Real)) Bool (less x z))
 (assert (not (=> (foo (minus x y) 0) (less x y))))
 (check-sat)