summaryrefslogtreecommitdiff
path: root/src/expr/kind_template.h
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2017-08-14 18:34:18 -0700
committerGitHub <noreply@github.com>2017-08-14 18:34:18 -0700
commitc577a90f58374e64d293fe02293dc31c693704ef (patch)
tree4f7be8f45f105aac39947ecd713026993b575f73 /src/expr/kind_template.h
parent7b8531e83dd4c95a5b0eaa4927da5228c6942b7c (diff)
Move function definitions from kind.h to kind.cpp (#217)
Diffstat (limited to 'src/expr/kind_template.h')
-rw-r--r--src/expr/kind_template.h91
1 files changed, 10 insertions, 81 deletions
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index d8c96ffa1..4f5b1eecd 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -20,7 +20,6 @@
#define __CVC4__KIND_H
#include <iosfwd>
-#include <sstream>
#include "base/exception.h"
@@ -43,47 +42,16 @@ typedef ::CVC4::kind::Kind_t Kind;
namespace kind {
-inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
-inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
- using namespace CVC4::kind;
+std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
- switch(k) {
-
- /* special cases */
- case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
- case NULL_EXPR: out << "NULL"; break;
-${kind_printers}
- case LAST_KIND: out << "LAST_KIND"; break;
- default: out << "UNKNOWNKIND!" << int(k); break;
- }
-
- return out;
-}
-
-#line 64 "${template}"
+#line 48 "${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
* the arguments. */
/* TODO: This could be generated. */
-inline bool isAssociative(::CVC4::Kind k) {
- switch(k) {
- case kind::AND:
- case kind::OR:
- case kind::MULT:
- case kind::PLUS:
- return true;
-
- default:
- return false;
- }
-}
-
-inline std::string kindToString(::CVC4::Kind k) {
- std::stringstream ss;
- ss << k;
- return ss.str();
-}
+bool isAssociative(::CVC4::Kind k) CVC4_PUBLIC;
+std::string kindToString(::CVC4::Kind k) CVC4_PUBLIC;
struct KindHashFunction {
inline size_t operator()(::CVC4::Kind k) const {
@@ -98,7 +66,7 @@ struct KindHashFunction {
*/
enum TypeConstant {
${type_constant_list}
-#line 102 "${template}"
+#line 70 "${template}"
LAST_TYPE
};/* enum TypeConstant */
@@ -111,22 +79,13 @@ struct TypeConstantHashFunction {
}
};/* struct TypeConstantHashFunction */
-inline std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) {
- switch(typeConstant) {
-${type_constant_descriptions}
-#line 118 "${template}"
- default:
- out << "UNKNOWN_TYPE_CONSTANT";
- break;
- }
- return out;
-}
+std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant);
namespace theory {
enum TheoryId {
${theory_enum}
-#line 130 "${template}"
+#line 89 "${template}"
THEORY_LAST
};/* enum TheoryId */
@@ -137,39 +96,9 @@ inline TheoryId& operator ++ (TheoryId& id) {
return id = static_cast<TheoryId>(((int)id) + 1);
}
-inline std::ostream& operator<<(std::ostream& out, TheoryId theoryId) {
- switch(theoryId) {
-${theory_descriptions}
-#line 144 "${template}"
- default:
- out << "UNKNOWN_THEORY";
- break;
- }
- return out;
-}
-
-inline TheoryId kindToTheoryId(::CVC4::Kind k) {
- switch(k) {
- case kind::UNDEFINED_KIND:
- case kind::NULL_EXPR:
- break;
-${kind_to_theory_id}
-#line 158 "${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}
-#line 168 "${template}"
- case LAST_TYPE:
- break;
- }
- throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant");
-}
+std::ostream& operator<<(std::ostream& out, TheoryId theoryId);
+TheoryId kindToTheoryId(::CVC4::Kind k) CVC4_PUBLIC;
+TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant);
}/* CVC4::theory namespace */
}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback