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.cpp | |
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.cpp')
-rw-r--r-- | src/expr/symbol_table.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index e3bd898ef..71745f649 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -50,7 +50,7 @@ SymbolTable::~SymbolTable() { } void SymbolTable::bind(const std::string& name, Expr obj, - bool levelZero) throw(AssertionException) { + bool levelZero) throw() { CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr"); ExprManagerScope ems(obj); if(levelZero) d_exprMap->insertAtContextLevelZero(name, obj); @@ -58,7 +58,7 @@ void SymbolTable::bind(const std::string& name, Expr obj, } void SymbolTable::bindDefinedFunction(const std::string& name, Expr obj, - bool levelZero) throw(AssertionException) { + bool levelZero) throw() { CheckArgument(!obj.isNull(), obj, "cannot bind to a null Expr"); ExprManagerScope ems(obj); if(levelZero){ @@ -84,7 +84,7 @@ bool SymbolTable::isBoundDefinedFunction(Expr func) const throw() { return d_functions->contains(func); } -Expr SymbolTable::lookup(const std::string& name) const throw(AssertionException) { +Expr SymbolTable::lookup(const std::string& name) const throw() { return (*d_exprMap->find(name)).second; } @@ -121,7 +121,7 @@ bool SymbolTable::isBoundType(const std::string& name) const throw() { return d_typeMap->find(name) != d_typeMap->end(); } -Type SymbolTable::lookupType(const std::string& name) const throw(AssertionException) { +Type SymbolTable::lookupType(const std::string& name) const throw() { pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second; Assert(p.first.size() == 0, "type constructor arity is wrong: " @@ -131,7 +131,7 @@ Type SymbolTable::lookupType(const std::string& name) const throw(AssertionExcep } Type SymbolTable::lookupType(const std::string& name, - const std::vector<Type>& params) const throw(AssertionException) { + const std::vector<Type>& params) const throw() { pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second; Assert(p.first.size() == params.size(), "type constructor arity is wrong: " |