diff options
Diffstat (limited to 'src/expr/kind_template.h')
-rw-r--r-- | src/expr/kind_template.h | 32 |
1 files changed, 10 insertions, 22 deletions
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 93c37f6cc..0168363d4 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -22,6 +22,7 @@ #include <iosfwd> #include "base/exception.h" +#include "theory/theory_id.h" namespace CVC4 { namespace kind { @@ -44,7 +45,7 @@ namespace kind { std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC; -#line 48 "${template}" +#line 49 "${template}" /** Returns true if the given kind is associative. This is used by ExprManager to * decide whether it's safe to modify big expressions by changing the grouping of @@ -64,11 +65,12 @@ struct KindHashFunction { /** * The enumeration for the built-in atomic types. */ -enum CVC4_PUBLIC TypeConstant { -${type_constant_list} -#line 70 "${template}" +enum CVC4_PUBLIC TypeConstant +{ + ${type_constant_list} +#line 71 "${template}" LAST_TYPE -};/* enum TypeConstant */ +}; /* enum TypeConstant */ /** * We hash the constants with their values. @@ -83,23 +85,9 @@ std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant); namespace theory { -enum TheoryId { -${theory_enum} -#line 89 "${template}" - THEORY_LAST -};/* enum TheoryId */ - -const TheoryId THEORY_FIRST = static_cast<TheoryId>(0); -const TheoryId THEORY_SAT_SOLVER = THEORY_LAST; - -CVC4_PUBLIC inline TheoryId& operator++(TheoryId& id) { - return id = static_cast<TheoryId>(static_cast<int>(id) + 1); -} - -std::ostream& operator<<(std::ostream& out, TheoryId theoryId); -TheoryId kindToTheoryId(::CVC4::Kind k) CVC4_PUBLIC; -TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) CVC4_PUBLIC; -std::string getStatsPrefix(TheoryId theoryId) CVC4_PUBLIC; +::CVC4::theory::TheoryId kindToTheoryId(::CVC4::Kind k) CVC4_PUBLIC; +::CVC4::theory::TheoryId typeConstantToTheoryId( + ::CVC4::TypeConstant typeConstant) CVC4_PUBLIC; }/* CVC4::theory namespace */ }/* CVC4 namespace */ |