* \todo document this file
*/
-#include "expr/metakind.h"
-
#include <iostream>
+#include "expr/metakind.h"
+#include "expr/node_value.h"
+
// clang-format off
${metakind_includes}
// clang-format off
namespace cvc5 {
+namespace expr {
+
+// clang-format off
+${metakind_constantMaps}
+// clang-format on
+
+} // namespace expr
+
namespace kind {
/**
return metaKinds[k + 1];
} /* metaKindOf(k) */
-} // namespace kind
-
-namespace expr {
+namespace metakind {
-// clang-format off
-${metakind_constantMaps}
-// clang-format on
+/**
+ * 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, class T, bool pool>
+struct NodeValueConstCompare
+{
+ static bool compare(const ::cvc5::expr::NodeValue* x,
+ const ::cvc5::expr::NodeValue* y)
+ {
+ if (pool)
+ {
+ if (x->d_nchildren == 1)
+ {
+ Assert(y->d_nchildren == 0);
+ return compare(y, x);
+ }
+ else if (y->d_nchildren == 1)
+ {
+ Assert(x->d_nchildren == 0);
+ return x->getConst<T>() == *reinterpret_cast<T*>(y->d_children[0]);
+ }
+ }
-} // namespace expr
+ Assert(x->d_nchildren == 0);
+ Assert(y->d_nchildren == 0);
+ return x->getConst<T>() == y->getConst<T>();
+ }
-namespace kind {
-namespace metakind {
+ static size_t constHash(const ::cvc5::expr::NodeValue* nv)
+ {
+ return nv->getConst<T>().hash();
+ }
+};
size_t NodeValueCompare::constHash(const ::cvc5::expr::NodeValue* nv)
{
template bool NodeValueCompare::compare<false>(
const ::cvc5::expr::NodeValue* nv1, const ::cvc5::expr::NodeValue* nv2);
-void NodeValueConstPrinter::toStream(std::ostream& out,
- const ::cvc5::expr::NodeValue* nv)
+void nodeValueConstantToStream(std::ostream& out,
+ const ::cvc5::expr::NodeValue* nv)
{
Assert(nv->getMetaKind() == kind::metakind::CONSTANT);
}
}
-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"
template <class T>
struct ConstantMap;
-/**
- * Static, compile-time information about kinds k and what type their
- * corresponding cvc5 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 ::cvc5::expr::NodeValue* x,
- const ::cvc5::expr::NodeValue* y);
- inline static size_t constHash(const ::cvc5::expr::NodeValue* nv);
-};/* NodeValueConstCompare<k, pool> */
-
struct NodeValueCompare {
template <bool pool>
static bool compare(const ::cvc5::expr::NodeValue* nv1,
NULLARY_OPERATOR /**< nullary operator */
};/* enum MetaKind_t */
+/**
+ * Write the string representation of a payload of a constant node to an output
+ * stream.
+ *
+ * @param out the stream to write to
+ * @param nv the node value representing a constant node
+ */
+void nodeValueConstantToStream(std::ostream& out,
+ const ::cvc5::expr::NodeValue* nv);
+
+/**
+ * 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(::cvc5::expr::NodeValue* nv);
+
+/** Return the minimum arity of the given kind. */
+uint32_t getMinArityForKind(::cvc5::Kind k);
+/** Return the maximum arity of the given kind. */
+uint32_t getMaxArityForKind(::cvc5::Kind k);
+
} // namespace metakind
// import MetaKind into the "cvc5::kind" namespace but keep the
* Get the metakind for a particular kind.
*/
MetaKind metaKindOf(Kind k);
+
+/**
+ * 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(::cvc5::expr::NodeValue* nv);
+
} // namespace kind
namespace expr {
// Comparison predicate
struct NodeValuePoolEq {
- inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
+ bool operator()(const NodeValue* nv1, const NodeValue* nv2) const
+ {
return ::cvc5::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2);
}
};
} // namespace expr
} // namespace cvc5
-#include "expr/node_value.h"
-
#endif /* CVC5__KIND__METAKIND_H */
#ifdef CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP
${metakind_fwd_decls}
// clang-format on
-namespace expr {
-// clang-format off
-${metakind_getConst_decls}
-// clang-format on
-} // namespace expr
-
namespace kind {
namespace metakind {
-template <Kind k, bool pool>
-inline bool NodeValueConstCompare<k, pool>::compare(
- const ::cvc5::expr::NodeValue* x, const ::cvc5::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);
- } 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 ::cvc5::expr::NodeValue* nv)
-{
- typedef typename ConstantMapReverse<k>::T T;
- return nv->getConst<T>().hash();
-}
-
// clang-format off
${metakind_constantMaps_decls}
// clang-format on
-struct NodeValueConstPrinter
-{
- static void toStream(std::ostream& out, const ::cvc5::expr::NodeValue* nv);
- static void toStream(std::ostream& out, TNode n);
-};
-
-/**
- * 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(::cvc5::expr::NodeValue* nv);
-
-/** Return the minimum arity of the given kind. */
-uint32_t getMinArityForKind(::cvc5::Kind k);
-/** Return the maximum arity of the given kind. */
-uint32_t getMaxArityForKind(::cvc5::Kind k);
-
} // namespace metakind
-
-/**
- * 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(::cvc5::expr::NodeValue* nv);
-
} // namespace kind
-
} // namespace cvc5
#endif /* CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP */
register_metakind CONSTANT "$1" 0
if [[ "${payload_seen}" != true ]]; then
- metakind_getConst_decls="${metakind_getConst_decls}
-template <>
-${class} const& NodeValue::getConst< ${class} >() const;
-"
-
metakind_constantMaps="${metakind_constantMaps}
// The reinterpret_cast of d_children to \"${class} const*\"
// flags a \"strict aliasing\" warning; it's okay, because we never access
"
fi
- metakind_constantMaps_decls="${metakind_constantMaps_decls}
-template <>
-struct ConstantMapReverse< ::cvc5::kind::$1 > {
- using T = ${class};
-};/* ConstantMapReverse< ::cvc5::kind::$1 > */
-"
-
metakind_compares="${metakind_compares}
case kind::$1:
- return NodeValueConstCompare< kind::$1, pool >::compare(nv1, nv2);
+ return NodeValueConstCompare<kind::$1, ${class}, pool>::compare(nv1, nv2);
"
metakind_constHashes="${metakind_constHashes}
case kind::$1:
metakind_kinds \
metakind_constantMaps \
metakind_constantMaps_decls \
- metakind_getConst_decls \
metakind_compares \
metakind_constHashes \
metakind_constPrinters \
class ExprSetDepth;
} // namespace expr
-namespace kind {
- namespace metakind {
- struct NodeValueConstPrinter;
- } // namespace metakind
- } // namespace kind
-
/**
* Encapsulation of an NodeValue pointer. The reference count is
* maintained in the NodeValue if ref_count is true.
friend class ::cvc5::expr::attr::AttributeManager;
friend struct ::cvc5::expr::attr::SmtAttributes;
- friend struct ::cvc5::kind::metakind::NodeValueConstPrinter;
-
/**
* Assigns the expression value and does reference counting. No assumptions
* are made on the expression, and should only be used if we know what we
d_nv->toStream(out, toDepth, dagThreshold, language);
}
+ void constToStream(std::ostream& out) const
+ {
+ kind::metakind::nodeValueConstantToStream(out, d_nv);
+ }
+
/**
* IOStream manipulator to set the maximum depth of Nodes when
* pretty-printing. -1 means print to any depth. E.g.:
out << ' ' << getId();
} else if (getMetaKind() == kind::metakind::CONSTANT) {
out << ' ';
- kind::metakind::NodeValueConstPrinter::toStream(out, this);
+ kind::metakind::nodeValueConstantToStream(out, this);
} else {
if (nv_begin() != nv_end()) {
for (const_nv_iterator child = nv_begin(); child != nv_end(); ++child) {
#include "cvc5_private.h"
-// circular dependency
-#include "expr/metakind.h"
-
#ifndef CVC5__EXPR__NODE_VALUE_H
#define CVC5__EXPR__NODE_VALUE_H
#include <string>
#include "expr/kind.h"
+#include "expr/metakind.h"
#include "options/language.h"
namespace cvc5 {
namespace kind {
namespace metakind {
- template < ::cvc5::Kind k, bool pool>
+
+ template < ::cvc5::Kind k, class T, bool pool>
struct NodeValueConstCompare;
struct NodeValueCompare;
- struct NodeValueConstPrinter;
- void deleteNodeValueConstant(::cvc5::expr::NodeValue* nv);
} // namespace metakind
} // namespace kind
friend class ::cvc5::NodeBuilder;
friend class ::cvc5::NodeManager;
- template <Kind k, bool pool>
- friend struct ::cvc5::kind::metakind::NodeValueConstCompare;
+ template <Kind k, class T, bool pool>
+ friend struct kind::metakind::NodeValueConstCompare;
- friend struct ::cvc5::kind::metakind::NodeValueCompare;
- friend struct ::cvc5::kind::metakind::NodeValueConstPrinter;
+ friend struct kind::metakind::NodeValueCompare;
- friend void ::cvc5::kind::metakind::deleteNodeValueConstant(NodeValue* nv);
+ friend void kind::metakind::nodeValueConstantToStream(std::ostream& out,
+ const NodeValue* nv);
+ friend void kind::metakind::deleteNodeValueConstant(NodeValue* nv);
friend class RefCountGuard;
/** If this is a CONST_* Node, extract the constant from it. */
template <class T>
- inline const T& getConst() const;
+ const T& getConst() const;
static inline NodeValue& null()
{
if(n.getMetaKind() == kind::metakind::CONSTANT) {
// constant
out << ' ';
- kind::metakind::NodeValueConstPrinter::toStream(out, n);
+ n.constToStream(out);
}
else if (n.isClosure())
{
default:
// fall back on whatever operator<< does on underlying type; we
// might luck out and be SMT-LIB v2 compliant
- kind::metakind::NodeValueConstPrinter::toStream(out, n);
+ n.constToStream(out);
}
break;
case kind::BITVECTOR_TYPE:
default:
// fall back on whatever operator<< does on underlying type; we
// might luck out and be SMT-LIB v2 compliant
- kind::metakind::NodeValueConstPrinter::toStream(out, n);
+ n.constToStream(out);
}
return;
projects / cvc5.git / commitdiff