Public interface review items:

* don't document internal-only stuff (like DefaultCleanup for CDLists)
* NoSuchFunctionException -> TypeCheckingException

9 files changed, 19 insertions, 61 deletions

diff --git a/src/context/cdhashmap_forward.h b/src/context/cdhashmap_forward.h
index 593807f5c..3f1ed6b32 100644
--- a/src/context/cdhashmap_forward.h
+++ b/src/context/cdhashmap_forward.h
@@ -28,6 +28,8 @@
 #ifndef __CVC4__CONTEXT__CDMAP_FORWARD_H
 #define __CVC4__CONTEXT__CDMAP_FORWARD_H
 
+/// \cond internals
+
 namespace __gnu_cxx {
   template <class Key> struct hash;
 }/* __gnu_cxx namespace */
@@ -39,4 +41,6 @@ namespace CVC4 {
   }/* CVC4::context namespace */
 }/* CVC4 namespace */
 
+/// \endcond
+
 #endif /* __CVC4__CONTEXT__CDMAP_FORWARD_H */
diff --git a/src/context/cdhashset_forward.h b/src/context/cdhashset_forward.h
index 01482ed34..5d02d734f 100644
--- a/src/context/cdhashset_forward.h
+++ b/src/context/cdhashset_forward.h
@@ -28,6 +28,8 @@
 #ifndef __CVC4__CONTEXT__CDSET_FORWARD_H
 #define __CVC4__CONTEXT__CDSET_FORWARD_H
 
+/// \cond internals
+
 namespace __gnu_cxx {
   template <class Key> struct hash;
 }/* __gnu_cxx namespace */
@@ -39,4 +41,6 @@ namespace CVC4 {
   }/* CVC4::context namespace */
 }/* CVC4 namespace */
 
+/// \endcond
+
 #endif /* __CVC4__CONTEXT__CDSET_FORWARD_H */
diff --git a/src/context/cdlist_forward.h b/src/context/cdlist_forward.h
index 78557afd2..62c0b80f6 100644
--- a/src/context/cdlist_forward.h
+++ b/src/context/cdlist_forward.h
@@ -36,6 +36,8 @@
 
 #include <memory>
 
+/// \cond internals
+
 namespace __gnu_cxx {
   template <class Key> struct hash;
 }/* __gnu_cxx namespace */
@@ -52,6 +54,8 @@ public:
 template <class T, class CleanUp = DefaultCleanUp<T>, class Allocator = std::allocator<T> >
 class CDList;
 
+/// \endcond
+
 }/* CVC4::context namespace */
 }/* CVC4 namespace */
 
diff --git a/src/cvc4.i b/src/cvc4.i
index a4d5e1986..bc9f5a5af 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -117,7 +117,6 @@ using namespace CVC4;
 %include "expr/expr_stream.i"
 
 %include "smt/smt_engine.i"
-%include "smt/no_such_function_exception.i"
 %include "smt/modal_exception.i"
 
 %include "options/options.i"
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 76cebbdd1..9bfc9680a 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -11,7 +11,6 @@ libsmt_la_SOURCES = \
 	smt_engine_scope.cpp \
 	smt_engine_scope.h \
 	modal_exception.h \
-	no_such_function_exception.h \
 	simplification_mode.h \
 	simplification_mode.cpp
 
@@ -21,6 +20,5 @@ nodist_libsmt_la_SOURCES = \
 EXTRA_DIST = \
 	options_handlers.h \
 	smt_options_template.cpp \
-	no_such_function_exception.i \
 	modal_exception.i \
 	smt_engine.i
diff --git a/src/smt/no_such_function_exception.h b/src/smt/no_such_function_exception.h
deleted file mode 100644
index 615f6ab2b..000000000
--- a/src/smt/no_such_function_exception.h
+++ /dev/null
@@ -1,44 +0,0 @@
-/*********************                                                        */
-/*! \file no_such_function_exception.h
- ** \verbatim
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief An exception that is thrown when an option setting is not
- ** understood.
- **
- ** An exception that is thrown when an interactive-only feature while
- ** CVC4 is being used in a non-interactive setting (for example, the
- ** "(get-assertions)" command in an SMT-LIBv2 script).
- **/
-
-#include "cvc4_public.h"
-
-#ifndef __CVC4__SMT__NO_SUCH_FUNCTION_EXCEPTION_H
-#define __CVC4__SMT__NO_SUCH_FUNCTION_EXCEPTION_H
-
-#include "util/exception.h"
-
-namespace CVC4 {
-
-class CVC4_PUBLIC NoSuchFunctionException : public CVC4::Exception {
-public:
-  NoSuchFunctionException(Expr name) :
-    Exception(std::string("Undefined function: `") + name.toString() + "': ") {
-  }
-
-  NoSuchFunctionException(Expr name, const std::string& msg) :
-    Exception(std::string("Undefined function: `") + name.toString() + "': " + msg) {
-  }
-};/* class NoSuchFunctionException */
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__SMT__NO_SUCH_FUNCTION_EXCEPTION_H */
diff --git a/src/smt/no_such_function_exception.i b/src/smt/no_such_function_exception.i
deleted file mode 100644
index 0c67ad0d3..000000000
--- a/src/smt/no_such_function_exception.i
+++ /dev/null
@@ -1,5 +0,0 @@
-%{
-#include "smt/no_such_function_exception.h"
-%}
-
-%include "smt/no_such_function_exception.h"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index c11354657..90b9ac774 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -39,7 +39,6 @@
 #include "expr/node_builder.h"
 #include "prop/prop_engine.h"
 #include "smt/modal_exception.h"
-#include "smt/no_such_function_exception.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/theory_engine.h"
@@ -186,7 +185,7 @@ class SmtEnginePrivate {
    *
    * Returns false if the formula simplifies to "false"
    */
-  bool simplifyAssertions() throw(NoSuchFunctionException, AssertionException);
+  bool simplifyAssertions() throw(TypeCheckingException, AssertionException);
 
 public:
 
@@ -226,13 +225,13 @@ public:
    * even be simplified.
    */
   void addFormula(TNode n)
-    throw(NoSuchFunctionException, AssertionException);
+    throw(TypeCheckingException, AssertionException);
 
   /**
    * Expand definitions in n.
    */
   Node expandDefinitions(TNode n, hash_map<TNode, Node, TNodeHashFunction>& cache)
-    throw(NoSuchFunctionException, AssertionException);
+    throw(TypeCheckingException, AssertionException);
 
 };/* class SmtEnginePrivate */
 
@@ -785,7 +784,7 @@ void SmtEngine::defineFunction(Expr func,
 }
 
 Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<TNode, Node, TNodeHashFunction>& cache)
-  throw(NoSuchFunctionException, AssertionException) {
+  throw(TypeCheckingException, AssertionException) {
 
   if(n.getKind() != kind::APPLY && n.getNumChildren() == 0) {
     // don't bother putting in the cache
@@ -814,7 +813,7 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<TNode, Node, TNodeHas
       Debug("expand") << "     : \"" << name << "\"" << endl;
     }
     if(i == d_smt.d_definedFunctions->end()) {
-      throw NoSuchFunctionException(Expr(d_smt.d_exprManager, new Node(func)));
+      throw TypeCheckingException(n.toExpr(), std::string("Undefined function: `") + func.toString() + "'");
     }
     if(Debug.isOn("expand")) {
       Debug("expand") << " defn: " << def.getFunction() << endl
@@ -1234,7 +1233,7 @@ void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertion
 
 // returns false if simpflication led to "false"
 bool SmtEnginePrivate::simplifyAssertions()
-  throw(NoSuchFunctionException, AssertionException) {
+  throw(TypeCheckingException, AssertionException) {
   try {
 
     Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
@@ -1508,7 +1507,7 @@ void SmtEnginePrivate::processAssertions() {
 }
 
 void SmtEnginePrivate::addFormula(TNode n)
-  throw(NoSuchFunctionException, AssertionException) {
+  throw(TypeCheckingException, AssertionException) {
 
   Trace("smt") << "SmtEnginePrivate::addFormula(" << n << ")" << endl;
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 505a2d8d8..43a7ee58d 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -31,7 +31,6 @@
 #include "util/proof.h"
 #include "util/model.h"
 #include "smt/modal_exception.h"
-#include "smt/no_such_function_exception.h"
 #include "util/hash.h"
 #include "options/options.h"
 #include "util/result.h"