From 779ca55f2802b2c77ea39d1c94a097a9761f544c Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 14 Aug 2017 20:10:55 -0700 Subject: [PATCH] Move function definitions from metakind.h to cpp (#218) --- src/expr/Makefile.am | 12 +++ src/expr/metakind_template.cpp | 176 +++++++++++++++++++++++++++++++++ src/expr/metakind_template.h | 159 ++++------------------------- src/expr/mkmetakind | 44 ++++----- 4 files changed, 227 insertions(+), 164 deletions(-) create mode 100644 src/expr/metakind_template.cpp diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 06a252b3c..bf4ad9acd 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -69,6 +69,7 @@ nodist_libexpr_la_SOURCES = \ kind.h \ kind.cpp \ metakind.h \ + metakind.cpp \ type_properties.h \ expr.h \ expr.cpp \ @@ -86,6 +87,7 @@ EXTRA_DIST = \ kind_template.h \ kind_template.cpp \ metakind_template.h \ + metakind_template.cpp \ type_properties_template.h \ expr_manager_template.h \ expr_manager_template.cpp \ @@ -109,6 +111,7 @@ BUILT_SOURCES = \ kind.h \ kind.cpp \ metakind.h \ + metakind.cpp \ type_properties.h \ expr.h \ expr.cpp \ @@ -121,6 +124,7 @@ CLEANFILES = \ kind.h \ kind.cpp \ metakind.h \ + metakind.cpp \ expr.h \ expr.cpp \ expr_manager.h \ @@ -162,6 +166,14 @@ metakind.h: metakind_template.h mkmetakind @top_builddir@/src/expr/.subdirs $(if `cat @top_builddir@/src/expr/.subdirs` \ > $@) || (rm -f $@ && exit 1) +metakind.cpp: metakind_template.cpp 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 + $(AM_V_GEN)(@srcdir@/mkmetakind \ + $< \ + `cat @top_builddir@/src/expr/.subdirs` \ + > $@) || (rm -f $@ && exit 1) + type_properties.h: type_properties_template.h 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 diff --git a/src/expr/metakind_template.cpp b/src/expr/metakind_template.cpp new file mode 100644 index 000000000..3e262db8c --- /dev/null +++ b/src/expr/metakind_template.cpp @@ -0,0 +1,176 @@ +#include "expr/metakind.h" + +#include + +namespace CVC4 { +namespace kind { + +/** + * Get the metakind for a particular kind. + */ +MetaKind metaKindOf(Kind k) { + static const MetaKind metaKinds[] = { + metakind::INVALID, /* UNDEFINED_KIND */ + metakind::INVALID, /* NULL_EXPR */ +${metakind_kinds} + metakind::INVALID /* LAST_KIND */ + };/* metaKinds[] */ + + Assert(k >= kind::NULL_EXPR && k < kind::LAST_KIND); + + // We've asserted that k >= NULL_EXPR (which is 0), but we still + // handle the UNDEFINED_KIND (-1) case. If we don't, the compiler + // emits warnings for non-assertion builds, since the check isn't done. + return metaKinds[k + 1]; +}/* metaKindOf(k) */ + +}/* CVC4::kind namespace */ + +namespace expr { + +${metakind_constantMaps} + +}/* CVC4::expr namespace */ + +namespace kind { +namespace metakind { + +size_t NodeValueCompare::constHash(const ::CVC4::expr::NodeValue* nv) { + Assert(nv->getMetaKind() == kind::metakind::CONSTANT); + + switch(nv->d_kind) { +${metakind_constHashes} + default: + Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind)); + } +} + +template +bool NodeValueCompare::compare(const ::CVC4::expr::NodeValue* nv1, + const ::CVC4::expr::NodeValue* nv2) { + if(nv1->d_kind != nv2->d_kind) { + return false; + } + + if(nv1->getMetaKind() == kind::metakind::CONSTANT) { + switch(nv1->d_kind) { +${metakind_compares} + default: + Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv1->d_kind)); + } + } + + if(nv1->d_nchildren != nv2->d_nchildren) { + return false; + } + + ::CVC4::expr::NodeValue::const_nv_iterator i = nv1->nv_begin(); + ::CVC4::expr::NodeValue::const_nv_iterator j = nv2->nv_begin(); + ::CVC4::expr::NodeValue::const_nv_iterator i_end = nv1->nv_end(); + + while(i != i_end) { + if((*i) != (*j)) { + return false; + } + ++i; + ++j; + } + + return true; +} + +template bool NodeValueCompare::compare(const ::CVC4::expr::NodeValue* nv1, + const ::CVC4::expr::NodeValue* nv2); +template bool NodeValueCompare::compare(const ::CVC4::expr::NodeValue* nv1, + const ::CVC4::expr::NodeValue* nv2); + +void NodeValueConstPrinter::toStream(std::ostream& out, + const ::CVC4::expr::NodeValue* nv) { + Assert(nv->getMetaKind() == kind::metakind::CONSTANT); + + switch(nv->d_kind) { +${metakind_constPrinters} + default: + Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind)); + } +} + +void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) { + toStream(out, n.d_nv); +} + +// The reinterpret_cast of d_children to various constant payload types +// in deleteNodeValueConstant(), below, can flag a "strict aliasing" +// warning; it should actually be okay, because we never access the +// embedded constant as a NodeValue* child, and never access an embedded +// NodeValue* child as a constant. +#pragma GCC diagnostic ignored "-Wstrict-aliasing" + +/** + * Cleanup to be performed when a NodeValue zombie is collected, and + * it has CONSTANT metakind. This calls the destructor for the underlying + * C++ type representing the constant value. See + * NodeManager::reclaimZombies() for more information. + * + * This doesn't support "non-inlined" NodeValues, which shouldn't need this + * kind of cleanup. + */ +void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv) { + Assert(nv->getMetaKind() == kind::metakind::CONSTANT); + + switch(nv->d_kind) { +${metakind_constDeleters} + default: + Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind)); + } +} + +// re-enable the strict-aliasing warning +# pragma GCC diagnostic warning "-Wstrict-aliasing" + +unsigned getLowerBoundForKind(::CVC4::Kind k) { + static const unsigned lbs[] = { + 0, /* NULL_EXPR */ +${metakind_lbchildren} + + 0 /* LAST_KIND */ + }; + + return lbs[k]; +} + +unsigned getUpperBoundForKind(::CVC4::Kind k) { + static const unsigned ubs[] = { + 0, /* NULL_EXPR */ +${metakind_ubchildren} + + 0, /* LAST_KIND */ + }; + + return ubs[k]; +} + +}/* CVC4::metakind namespace */ + +/** + * Map a kind of the operator to the kind of the enclosing expression. For + * example, since the kind of functions is just VARIABLE, it should map + * VARIABLE to APPLY_UF. + */ +Kind operatorToKind(::CVC4::expr::NodeValue* nv) { + if(nv->getKind() == kind::BUILTIN) { + return nv->getConst(); + } else if(nv->getKind() == kind::LAMBDA) { + return kind::APPLY_UF; + } + + switch(Kind k CVC4_UNUSED = nv->getKind()) { +${metakind_operatorKinds} + + default: + return kind::UNDEFINED_KIND; /* LAST_KIND */ + }; +} + +}/* CVC4::kind namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index b2e88c1ff..6f7aef5ed 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -19,7 +19,7 @@ #ifndef __CVC4__KIND__METAKIND_H #define __CVC4__KIND__METAKIND_H -#include +#include #include "base/cvc4_assert.h" #include "expr/kind.h" @@ -81,9 +81,9 @@ struct NodeValueConstCompare { struct NodeValueCompare { template - inline static bool compare(const ::CVC4::expr::NodeValue* nv1, - const ::CVC4::expr::NodeValue* nv2); - inline static size_t constHash(const ::CVC4::expr::NodeValue* nv); + static bool compare(const ::CVC4::expr::NodeValue* nv1, + const ::CVC4::expr::NodeValue* nv2); + static size_t constHash(const ::CVC4::expr::NodeValue* nv); };/* struct NodeValueCompare */ /** @@ -111,28 +111,9 @@ typedef ::CVC4::kind::metakind::MetaKind_t MetaKind; /** * Get the metakind for a particular kind. */ -static inline MetaKind metaKindOf(Kind k) { - static const MetaKind metaKinds[] = { - metakind::INVALID, /* UNDEFINED_KIND */ - metakind::INVALID, /* NULL_EXPR */ -${metakind_kinds} - metakind::INVALID /* LAST_KIND */ - };/* metaKinds[] */ - - Assert(k >= kind::NULL_EXPR && k < kind::LAST_KIND); - - // We've asserted that k >= NULL_EXPR (which is 0), but we still - // handle the UNDEFINED_KIND (-1) case. If we don't, the compiler - // emits warnings for non-assertion builds, since the check isn't done. - return metaKinds[k + 1]; -}/* metaKindOf(k) */ - +MetaKind metaKindOf(Kind k); }/* CVC4::kind namespace */ -namespace expr { - class NodeValue; -}/* CVC4::expr namespace */ - namespace kind { namespace metakind { @@ -169,6 +150,11 @@ ${metakind_includes} #ifdef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP namespace CVC4 { + +namespace expr { +${metakind_getConst_decls} +}/* CVC4::expr namespace */ + namespace kind { namespace metakind { @@ -197,80 +183,14 @@ inline size_t NodeValueConstCompare::constHash(const ::CVC4::expr::Node return nv->getConst().hash(); } -${metakind_constantMaps} - -template -inline bool NodeValueCompare::compare(const ::CVC4::expr::NodeValue* nv1, - const ::CVC4::expr::NodeValue* nv2) { - if(nv1->d_kind != nv2->d_kind) { - return false; - } - - if(nv1->getMetaKind() == kind::metakind::CONSTANT) { - switch(nv1->d_kind) { -${metakind_compares} - default: - Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv1->d_kind)); - } - } - - if(nv1->d_nchildren != nv2->d_nchildren) { - return false; - } - - ::CVC4::expr::NodeValue::const_nv_iterator i = nv1->nv_begin(); - ::CVC4::expr::NodeValue::const_nv_iterator j = nv2->nv_begin(); - ::CVC4::expr::NodeValue::const_nv_iterator i_end = nv1->nv_end(); - - while(i != i_end) { - if((*i) != (*j)) { - return false; - } - ++i; - ++j; - } - - return true; -} - -inline size_t NodeValueCompare::constHash(const ::CVC4::expr::NodeValue* nv) { - Assert(nv->getMetaKind() == kind::metakind::CONSTANT); - - switch(nv->d_kind) { -${metakind_constHashes} - default: - Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind)); - } -} +${metakind_constantMaps_decls} struct NodeValueConstPrinter { - inline static void toStream(std::ostream& out, + static void toStream(std::ostream& out, const ::CVC4::expr::NodeValue* nv); - inline static void toStream(std::ostream& out, TNode n); + static void toStream(std::ostream& out, TNode n); }; -inline void NodeValueConstPrinter::toStream(std::ostream& out, - const ::CVC4::expr::NodeValue* nv) { - Assert(nv->getMetaKind() == kind::metakind::CONSTANT); - - switch(nv->d_kind) { -${metakind_constPrinters} - default: - Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind)); - } -} - -inline void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) { - toStream(out, n.d_nv); -} - -// The reinterpret_cast of d_children to various constant payload types -// in deleteNodeValueConstant(), below, can flag a "strict aliasing" -// warning; it should actually be okay, because we never access the -// embedded constant as a NodeValue* child, and never access an embedded -// NodeValue* child as a constant. -#pragma GCC diagnostic ignored "-Wstrict-aliasing" - /** * Cleanup to be performed when a NodeValue zombie is collected, and * it has CONSTANT metakind. This calls the destructor for the underlying @@ -280,40 +200,10 @@ inline void NodeValueConstPrinter::toStream(std::ostream& out, TNode n) { * This doesn't support "non-inlined" NodeValues, which shouldn't need this * kind of cleanup. */ -inline void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv) { - Assert(nv->getMetaKind() == kind::metakind::CONSTANT); - - switch(nv->d_kind) { -${metakind_constDeleters} - default: - Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind)); - } -} +void deleteNodeValueConstant(::CVC4::expr::NodeValue* nv); -// re-enable the strict-aliasing warning -# pragma GCC diagnostic warning "-Wstrict-aliasing" - -inline unsigned getLowerBoundForKind(::CVC4::Kind k) { - static const unsigned lbs[] = { - 0, /* NULL_EXPR */ -${metakind_lbchildren} - - 0 /* LAST_KIND */ - }; - - return lbs[k]; -} - -inline unsigned getUpperBoundForKind(::CVC4::Kind k) { - static const unsigned ubs[] = { - 0, /* NULL_EXPR */ -${metakind_ubchildren} - - 0, /* LAST_KIND */ - }; - - return ubs[k]; -} +unsigned getLowerBoundForKind(::CVC4::Kind k); +unsigned getUpperBoundForKind(::CVC4::Kind k); }/* CVC4::kind::metakind namespace */ @@ -322,24 +212,11 @@ ${metakind_ubchildren} * example, since the kind of functions is just VARIABLE, it should map * VARIABLE to APPLY_UF. */ -static inline Kind operatorToKind(::CVC4::expr::NodeValue* nv) { - if(nv->getKind() == kind::BUILTIN) { - return nv->getConst(); - } else if(nv->getKind() == kind::LAMBDA) { - return kind::APPLY_UF; - } - - switch(Kind k CVC4_UNUSED = nv->getKind()) { -${metakind_operatorKinds} - - default: - return kind::UNDEFINED_KIND; /* LAST_KIND */ - }; -} +Kind operatorToKind(::CVC4::expr::NodeValue* nv); }/* CVC4::kind namespace */ -#line 343 "${template}" +#line 220 "${template}" namespace theory { diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 19e6e2244..1cfcf253a 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -229,17 +229,29 @@ function constant { echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC4::RationalHashFunction)" >&2 fi - if [ -n "$4" ]; then + # Avoid including the same header multiple times + if [ -n "$4" ] && [[ "${metakind_includes}" != *"#include \"$4\""* ]]; then metakind_includes="${metakind_includes} #include \"$4\"" fi register_metakind CONSTANT "$1" 0 - metakind_constantMaps="${metakind_constantMaps} -}/* CVC4::kind::metakind namespace */ -}/* CVC4::kind namespace */ - -namespace expr { + metakind_getConst_decls="${metakind_getConst_decls} +template <> +$2 const& NodeValue::getConst< $2 >() const; +" + metakind_constantMaps_decls="${metakind_constantMaps_decls} +template <> +struct ConstantMap< $2 > { + // typedef $theory_class OwningTheory; + enum { kind = ::CVC4::kind::$1 }; +};/* ConstantMap< $2 > */ +template <> +struct ConstantMapReverse< ::CVC4::kind::$1 > { + typedef $2 T; +};/* ConstantMapReverse< ::CVC4::kind::$1 > */ + " + metakind_constantMaps="${metakind_constantMaps} // The reinterpret_cast of d_children to \"$2 const*\" // flags a \"strict aliasing\" warning; it's okay, because we never access // the embedded constant as a NodeValue* child, and never access an embedded @@ -247,7 +259,7 @@ namespace expr { #pragma GCC diagnostic ignored \"-Wstrict-aliasing\" template <> -inline $2 const& NodeValue::getConst< $2 >() const { +$2 const& NodeValue::getConst< $2 >() const { AssertArgument(getKind() == ::CVC4::kind::$1, *this, \"Improper kind for getConst<$2>()\"); // To support non-inlined CONSTANT-kinded NodeValues (those that are @@ -261,22 +273,6 @@ inline $2 const& NodeValue::getConst< $2 >() const { // re-enable the warning #pragma GCC diagnostic warning \"-Wstrict-aliasing\" -}/* CVC4::expr namespace */ - -namespace kind { -namespace metakind { - -template <> -struct ConstantMap< $2 > { - // typedef $theory_class OwningTheory; - enum { kind = ::CVC4::kind::$1 }; -};/* ConstantMap< $2 > */ - -template <> -struct ConstantMapReverse< ::CVC4::kind::$1 > { - typedef $2 T; -};/* ConstantMapReverse< ::CVC4::kind::$1 > */ - " metakind_compares="${metakind_compares} case kind::$1: @@ -423,6 +419,8 @@ for var in \ metakind_includes \ metakind_kinds \ metakind_constantMaps \ + metakind_constantMaps_decls \ + metakind_getConst_decls \ metakind_compares \ metakind_constHashes \ metakind_constPrinters \ -- 2.30.2