summaryrefslogtreecommitdiff
path: root/src/expr/metakind_template.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/metakind_template.h')
-rw-r--r--src/expr/metakind_template.h285
1 files changed, 285 insertions, 0 deletions
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
new file mode 100644
index 000000000..95e107313
--- /dev/null
+++ b/src/expr/metakind_template.h
@@ -0,0 +1,285 @@
+/********************* */
+/** metakind_template.h
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Template for the metakind header.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__KIND__METAKIND_H
+#define __CVC4__KIND__METAKIND_H
+
+#include <iostream>
+
+#include "expr/kind.h"
+#include "util/Assert.h"
+
+${metakind_includes}
+
+namespace CVC4 {
+
+namespace expr {
+ class NodeValue;
+}/* CVC4::expr namespace */
+
+namespace kind {
+namespace metakind {
+
+/**
+ * Static, compile-time information about types T representing CVC4
+ * constants:
+ *
+ * typename ConstantMap<T>::OwningTheory
+ *
+ * The theory in charge of constructing T when constructing Nodes
+ * with NodeManager::mkConst(T).
+ *
+ * typename ConstantMap<T>::kind
+ *
+ * The kind to use when constructing Nodes with
+ * NodeManager::mkConst(T).
+ */
+template <class T>
+struct ConstantMap;
+
+/**
+ * Static, compile-time information about kinds k and what type their
+ * corresponding CVC4 constants are:
+ *
+ * typename ConstantMapReverse<k>::T
+ *
+ * Constant type for kind k.
+ */
+template <Kind k>
+struct ConstantMapReverse;
+
+/**
+ * Static, compile-time mapping from CONSTANT kinds to comparison
+ * functors on NodeValue*. The single element of this structure is:
+ *
+ * static bool NodeValueCompare<K, pool>::compare(NodeValue* x, NodeValue* y)
+ *
+ * Compares x and y, given that they are both K-kinded (and the
+ * meta-kind of K is CONSTANT). If pool == true, one of x and y
+ * (but not both) may be a "non-inlined" NodeValue. If pool ==
+ * false, neither x nor y may be a "non-inlined" NodeValue.
+ */
+template <Kind k, bool pool>
+struct NodeValueConstCompare {
+ inline static bool compare(const ::CVC4::expr::NodeValue* x,
+ const ::CVC4::expr::NodeValue* y);
+ inline static size_t constHash(const ::CVC4::expr::NodeValue* nv);
+};/* NodeValueConstCompare<k, pool> */
+
+struct NodeValueCompare {
+ template <bool pool>
+ inline static bool compare(const ::CVC4::expr::NodeValue* nv1,
+ const ::CVC4::expr::NodeValue* nv2);
+ inline static size_t constHash(const ::CVC4::expr::NodeValue* nv);
+};/* struct NodeValueCompare */
+
+struct NodeValueConstPrinter {
+ inline static void toStream(std::ostream& out,
+ const ::CVC4::expr::NodeValue* nv);
+};
+
+/**
+ * "metakinds" represent the "kinds" of kinds at the meta-level.
+ * "metakind" is an ugly name but it's not used by client code, just
+ * by the expr package, and the intent here is to keep it from
+ * polluting the kind namespace. For more documentation on what these
+ * mean, see src/expr/builtin_kinds.
+ */
+enum MetaKind_t {
+ INVALID = -1, /*! special node non-kinds like NULL_EXPR or LAST_KIND */
+ VARIABLE, /*! special node kinds: no operator */
+ OPERATOR, /*! operators that get "inlined" */
+ PARAMETERIZED, /*! parameterized ops (like APPLYs) that carry extra data */
+ CONSTANT /*! constants */
+};/* enum MetaKind_t */
+
+}/* CVC4::kind::metakind namespace */
+
+// import MetaKind into the "CVC4::kind" namespace but keep the
+// individual MetaKind constants under kind::metakind::
+typedef ::CVC4::kind::metakind::MetaKind_t MetaKind;
+
+static inline MetaKind metaKindOf(Kind k) {
+ static const MetaKind metaKinds[] = {
+ metakind::INVALID, /* NULL_EXPR */
+${metakind_kinds}
+ metakind::INVALID /* LAST_KIND */
+ };/* metaKinds[] */
+
+ return metaKinds[k];
+}/* metaKindOf(k) */
+
+}/* CVC4::kind namespace */
+
+namespace expr {
+ class NodeValue;
+}/* CVC4::expr namespace */
+
+namespace kind {
+namespace metakind {
+
+/* these are #defines so their sum can be #if-checked in node_value.h */
+#define __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT 8
+#define __CVC4__EXPR__NODE_VALUE__NBITS__KIND 8
+#define __CVC4__EXPR__NODE_VALUE__NBITS__ID 32
+#define __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN 16
+
+static const unsigned MAX_CHILDREN =
+ (1u << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1;
+
+}/* CVC4::kind::metakind namespace */
+}/* CVC4::kind namespace */
+
+namespace expr {
+
+// Comparison predicate
+struct NodeValueEq {
+ inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
+ return ::CVC4::kind::metakind::NodeValueCompare::compare<false>(nv1, nv2);
+ }
+};
+
+// Comparison predicate
+struct NodeValuePoolEq {
+ inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
+ return ::CVC4::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2);
+ }
+};
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#include "expr/node_value.h"
+
+#endif /* __CVC4__KIND__METAKIND_H */
+
+#ifdef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
+
+namespace CVC4 {
+namespace kind {
+namespace metakind {
+
+template <Kind k, bool pool>
+inline bool NodeValueConstCompare<k, pool>::compare(const ::CVC4::expr::NodeValue* x,
+ const ::CVC4::expr::NodeValue* y) {
+ typedef typename ConstantMapReverse<k>::T T;
+ if(pool) {
+ if(x->d_nchildren == 1) {
+ Assert(y->d_nchildren == 0);
+ return compare(y, x);
+ return *reinterpret_cast<T*>(x->d_children[0]) == y->getConst<T>();
+ } else if(y->d_nchildren == 1) {
+ Assert(x->d_nchildren == 0);
+ return x->getConst<T>() == *reinterpret_cast<T*>(y->d_children[0]);
+ }
+ }
+
+ Assert(x->d_nchildren == 0);
+ Assert(y->d_nchildren == 0);
+ return x->getConst<T>() == y->getConst<T>();
+}
+
+template <Kind k, bool pool>
+inline size_t NodeValueConstCompare<k, pool>::constHash(const ::CVC4::expr::NodeValue* nv) {
+ typedef typename ConstantMapReverse<k>::T T;
+ return nv->getConst<T>().hash();
+}
+
+${metakind_constantMaps}
+
+template <bool pool>
+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));
+ }
+}
+
+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 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];
+}
+
+}/* CVC4::kind::metakind namespace */
+}/* CVC4::kind namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback