diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
| commit | 65f720aac2d497c6e829d9c76638073a10060e7d (patch) | |
| tree | 357035797e31f96a37dce30cb97ddb0aaf8f3bb7 /src/expr/symbol_table.h | |
| parent | c0c351a89871e0a6881668fa1a8d87349ab8af8e (diff) | |
Public interface review items:
* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
or a public exception type.
* auto-generated documentation for Smt options and internal options
Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
Diffstat (limited to 'src/expr/symbol_table.h')
| -rw-r--r-- | src/expr/symbol_table.h | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index 3f24d10f8..6db335ded 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -79,7 +79,7 @@ public: * @param obj the expression to bind to <code>name</code> * @param levelZero set if the binding must be done at level 0 */ - void bind(const std::string& name, Expr obj, bool levelZero = false) throw(AssertionException); + void bind(const std::string& name, Expr obj, bool levelZero = false) throw(); /** * Bind a function body to a name in the current scope. If @@ -93,7 +93,7 @@ public: * @param obj the expression to bind to <code>name</code> * @param levelZero set if the binding must be done at level 0 */ - void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) throw(AssertionException); + void bindDefinedFunction(const std::string& name, Expr obj, bool levelZero = false) throw(); /** * Bind a type to a name in the current scope. If <code>name</code> @@ -159,7 +159,7 @@ public: * @param name the identifier to lookup * @returns the expression bound to <code>name</code> in the current scope. */ - Expr lookup(const std::string& name) const throw(AssertionException); + Expr lookup(const std::string& name) const throw(); /** * Lookup a bound type. @@ -167,7 +167,7 @@ public: * @param name the type identifier to lookup * @returns the type bound to <code>name</code> in the current scope. */ - Type lookupType(const std::string& name) const throw(AssertionException); + Type lookupType(const std::string& name) const throw(); /** * Lookup a bound parameterized type. @@ -178,7 +178,7 @@ public: * the current scope. */ Type lookupType(const std::string& name, - const std::vector<Type>& params) const throw(AssertionException); + const std::vector<Type>& params) const throw(); /** * Lookup the arity of a bound parameterized type. |