Public interface review items:

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

diff --git a/src/context/cdhashmap_forward.h b/src/context/cdhashmap_forward.h
index 593807f5c55c308fa6d5fe532e0a118a045b826b..3f1ed6b3230c56b4562c2240d40fe7ef69f9d903 100644 (file)
--- 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 01482ed341e097db599863e58b3b7915b6d7ee07..5d02d734f0a62648e32e42cba08c914cf872d6d7 100644 (file)
--- 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 78557afd2dbadb9932c63745b1897ce93ef4bda3..62c0b80f661ac34bdcf28eaf4d1d35dabf9fd074 100644 (file)
--- 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 a4d5e1986a388fb538133f3eaf2c1dce4a346fcc..bc9f5a5afc447ae0ee0faffe461bb798b1208322 100644 (file)
--- 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 76cebbdd17b995fb63f120d0101e1c9244fe8e9d..9bfc9680a1877e4d4af7b41031c32a86fe0c8288 100644 (file)
--- 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 (file)
index 615f6ab..0000000
--- 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 (file)
index 0c67ad0..0000000
--- 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 c113546574ffde991481d4b778a34b5f6782e907..90b9ac7748d5a92535978ba602519a346f851845 100644 (file)
--- 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 505a2d8d895da9a1a475ddb5d73b089b9f6c62db..43a7ee58df012864200d6fb26d6d24f9ec9d91a5 100644 (file)
--- 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"