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/kind_template.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/kind_template.h')
-rw-r--r-- | src/expr/kind_template.h | 27 |
1 files changed, 18 insertions, 9 deletions
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index fc7d838a1..2857dc5d8 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -24,7 +24,7 @@ #include <iostream> #include <sstream> -#include "util/Assert.h" +#include "util/exception.h" namespace CVC4 { namespace kind { @@ -100,6 +100,7 @@ struct KindHashFunction { */ enum TypeConstant { ${type_constant_list} +#line 104 "${template}" LAST_TYPE };/* enum TypeConstant */ @@ -115,6 +116,7 @@ struct TypeConstantHashFunction { inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) { switch(typeConstant) { ${type_constant_descriptions} +#line 120 "${template}" default: out << "UNKNOWN_TYPE_CONSTANT"; break; @@ -126,8 +128,9 @@ namespace theory { enum TheoryId { ${theory_enum} +#line 132 "${template}" THEORY_LAST -}; +};/* enum TheoryId */ const TheoryId THEORY_FIRST = static_cast<TheoryId>(0); const TheoryId THEORY_SAT_SOLVER = THEORY_LAST; @@ -139,6 +142,7 @@ inline TheoryId& operator ++ (TheoryId& id) { inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) { switch(theoryId) { ${theory_descriptions} +#line 146 "${template}" default: out << "UNKNOWN_THEORY"; break; @@ -148,23 +152,28 @@ ${theory_descriptions} inline TheoryId kindToTheoryId(::CVC4::Kind k) { switch(k) { + case kind::UNDEFINED_KIND: + case kind::NULL_EXPR: + break; ${kind_to_theory_id} - default: - Unhandled(k); +#line 160 "${template}" + case kind::LAST_KIND: + break; } + throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind"); } inline TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) { switch(typeConstant) { ${type_constant_to_theory_id} - default: - Unhandled(typeConstant); +#line 170 "${template}" + case LAST_TYPE: + break; } + throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant"); } -}/* theory namespace */ - - +}/* CVC4::theory namespace */ }/* CVC4 namespace */ #endif /* __CVC4__KIND_H */ |