From 02fb5a3a3219158e8c1b31a737c0a17182e8d91e Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 8 Aug 2012 05:13:53 +0000 Subject: [PATCH] Public interface review items: * don't document internal-only stuff (like DefaultCleanup for CDLists) * NoSuchFunctionException -> TypeCheckingException --- src/context/cdhashmap_forward.h | 4 +++ src/context/cdhashset_forward.h | 4 +++ src/context/cdlist_forward.h | 4 +++ src/cvc4.i | 1 - src/smt/Makefile.am | 2 -- src/smt/no_such_function_exception.h | 44 ---------------------------- src/smt/no_such_function_exception.i | 5 ---- src/smt/smt_engine.cpp | 15 +++++----- src/smt/smt_engine.h | 1 - 9 files changed, 19 insertions(+), 61 deletions(-) delete mode 100644 src/smt/no_such_function_exception.h delete mode 100644 src/smt/no_such_function_exception.i 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 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 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 +/// \cond internals + namespace __gnu_cxx { template struct hash; }/* __gnu_cxx namespace */ @@ -52,6 +54,8 @@ public: template , class Allocator = std::allocator > 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& 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& 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_mapend()) { - 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& 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" -- 2.30.2