From c577a90f58374e64d293fe02293dc31c693704ef Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 14 Aug 2017 18:34:18 -0700 Subject: Move function definitions from kind.h to kind.cpp (#217) --- src/expr/Makefile.am | 12 ++++++ src/expr/kind_template.cpp | 95 ++++++++++++++++++++++++++++++++++++++++++++++ src/expr/kind_template.h | 91 +++++--------------------------------------- 3 files changed, 117 insertions(+), 81 deletions(-) create mode 100644 src/expr/kind_template.cpp (limited to 'src/expr') diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 2400468a2..06a252b3c 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -67,6 +67,7 @@ libexpr_la_SOURCES = \ nodist_libexpr_la_SOURCES = \ kind.h \ + kind.cpp \ metakind.h \ type_properties.h \ expr.h \ @@ -83,6 +84,7 @@ EXTRA_DIST = \ datatype.i \ emptyset.i \ kind_template.h \ + kind_template.cpp \ metakind_template.h \ type_properties_template.h \ expr_manager_template.h \ @@ -105,6 +107,7 @@ EXTRA_DIST = \ BUILT_SOURCES = \ kind.h \ + kind.cpp \ metakind.h \ type_properties.h \ expr.h \ @@ -116,6 +119,7 @@ BUILT_SOURCES = \ CLEANFILES = \ kind.h \ + kind.cpp \ metakind.h \ expr.h \ expr.cpp \ @@ -142,6 +146,14 @@ kind.h: kind_template.h mkkind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ `cat @top_builddir@/src/expr/.subdirs` \ > $@) || (rm -f $@ && exit 1) +kind.cpp: kind_template.cpp mkkind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds + $(AM_V_at)chmod +x @srcdir@/mkkind + $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true + $(AM_V_GEN)(@srcdir@/mkkind \ + $< \ + `cat @top_builddir@/src/expr/.subdirs` \ + > $@) || (rm -f $@ && exit 1) + metakind.h: metakind_template.h mkmetakind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds $(AM_V_at)chmod +x @srcdir@/mkmetakind $(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp new file mode 100644 index 000000000..5f92af622 --- /dev/null +++ b/src/expr/kind_template.cpp @@ -0,0 +1,95 @@ +#include "expr/kind.h" + +namespace CVC4 { +namespace kind { + +std::ostream& operator<<(std::ostream& out, CVC4::Kind k) { + using namespace CVC4::kind; + + 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; +} + +/** 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. */ +bool isAssociative(::CVC4::Kind k) { + switch(k) { + case kind::AND: + case kind::OR: + case kind::MULT: + case kind::PLUS: + return true; + + default: + return false; + } +} + +std::string kindToString(::CVC4::Kind k) { + std::stringstream ss; + ss << k; + return ss.str(); +} + +}/* CVC4::kind namespace */ + +std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant) { + switch(typeConstant) { +${type_constant_descriptions} +#line 51 "${template}" + default: + out << "UNKNOWN_TYPE_CONSTANT"; + break; + } + return out; +} + +namespace theory { + +std::ostream& operator<<(std::ostream& out, TheoryId theoryId) { + switch(theoryId) { +${theory_descriptions} +#line 64 "${template}" + default: + out << "UNKNOWN_THEORY"; + break; + } + return out; +} + +TheoryId kindToTheoryId(::CVC4::Kind k) { + switch(k) { + case kind::UNDEFINED_KIND: + case kind::NULL_EXPR: + break; +${kind_to_theory_id} +#line 78 "${template}" + case kind::LAST_KIND: + break; + } + throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind"); +} + +TheoryId typeConstantToTheoryId(::CVC4::TypeConstant typeConstant) { + switch(typeConstant) { +${type_constant_to_theory_id} +#line 88 "${template}" + case LAST_TYPE: + break; + } + throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad type constant"); +} + +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ 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 -#include #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(((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 */ -- cgit v1.2.3