fi
# Checks for libraries.
-AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])])
-AC_CHECK_LIB(gmpxx, __gmpz_init, , AC_MSG_ERROR(libgmpxx.a is not found))
+AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])])
+AC_CHECK_LIB(gmpxx, __gmpz_init, , [AC_MSG_ERROR([GNU MP C++ library (libgmpxx) not found, see http://gmplib.org/])])
# Check for antlr C++ runtime (defined in config/antlr.m4)
AC_LIB_ANTLR
attribute.h \
attribute.cpp \
@srcdir@/kind.h \
- node_builder.cpp \
+ @srcdir@/metakind.h \
node_manager.cpp \
expr_manager.cpp \
node_value.cpp \
EXTRA_DIST = \
@srcdir@/kind.h \
- kind_prologue.h \
- kind_middle.h \
- kind_epilogue.h
+ @srcdir@/metakind.h \
+ kind_template.h \
+ metakind_template.h
-@srcdir@/kind.h: mkkind kind_prologue.h kind_middle.h kind_epilogue.h builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+@srcdir@/kind.h: mkkind kind_template.h builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mkkind
$(AM_V_GEN)(@srcdir@/mkkind \
- @srcdir@/kind_prologue.h \
- @srcdir@/kind_middle.h \
- @srcdir@/kind_epilogue.h \
+ @srcdir@/kind_template.h \
@srcdir@/builtin_kinds \
`grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
> @srcdir@/kind.h) || (rm -f @srcdir@/kind.h && exit 1)
-BUILT_SOURCES = @srcdir@/kind.h
-dist-hook: @srcdir@/kind.h
-MAINTAINERCLEANFILES = @srcdir@/kind.h
+@srcdir@/metakind.h: mkmetakind metakind_template.h builtin_kinds @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+ $(AM_V_at)chmod +x @srcdir@/mkmetakind
+ $(AM_V_GEN)(@srcdir@/mkmetakind \
+ @srcdir@/metakind_template.h \
+ @srcdir@/builtin_kinds \
+ `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
+ > @srcdir@/metakind.h) || (rm -f @srcdir@/metakind.h && exit 1)
+
+BUILT_SOURCES = @srcdir@/kind.h @srcdir@/metakind.h
+dist-hook: @srcdir@/kind.h @srcdir@/metakind.h
+MAINTAINERCLEANFILES = @srcdir@/kind.h @srcdir@/metakind.h
#
# This "kinds" file is written in a domain-specific language for
# declaring CVC4 kinds. Comments are marked with #, as this line is.
-# There are four basic commands:
-#
-# special K ["comment"]
-# operator K ["comment"]
-# parameterized K ["comment"]
-# constant K T ["comment"]
-#
-# special K (with an optional comment) declares a kind K that has no
-# operator (it's not conceptually an APPLY of an operator to
-# operands). This is appropriate for special built-ins,
-# e.g. VARIABLE.
-#
-# operator K (with an optional comment) declares a "built-in"
-# operator. Really this is the same as "special" except that it has
-# an operator (automatically generated by NodeManager).
-#
-# parameterized K (with an optional comment) declares a "built-in"
-# parameterized operator. This is a theory-specific APPLY, e.g.,
-# APPLY_UF, which applies its first parameter (say, "f"), to its
-# operands (say, "x" and "y", making the full application "f(x,y)").
-# Nodes with such a kind will have an operator (Node::hasOperator()
-# returns true, and Node::getOperator() returns the Node of functional
-# type representing "f" here), and the "children" are defined to be
-# this operator's parameters, and don't include the operator itself
-# (here, there are only two children "x" and "y"). For consistency
-# these should probably start with "APPLY_", but this is not enforced.
-#
-# constant K T (with an optional comment) declares a constant kind. T
-# is the C++ type representing the constant internally. For
-# consistency, these should probably start with "CONST_", but this is
-# not enforced.
-#
-# This file is actually an executable Bourne shell script (sourced by
-# the processing scripts after defining functions called "special,"
-# "operator," "parameterized," and "constant"). So if you need a
-# multi-line comment string, do it the Bourne-like way. Please don't
-# do anything else in this file than using these commands though.
#
+# The first non-blank, non-comment line in this file must be a theory
+# declaration:
+#
+# theory T header
+#
+# There are four basic commands for declaring kinds:
+#
+# variable K ["comment"]
+#
+# This declares a kind K that has no operator (it's conceptually a
+# VARIABLE). This is appropriate for things like VARIABLE and
+# SKOLEM.
+#
+# operator K #children ["comment"]
+#
+# Declares a "built-in" operator kind K. Really this is the same
+# as "variable" except that it has an operator (automatically
+# generated by NodeManager).
+#
+# You can specify an exact # of children required as the second
+# argument to the operator command. In debug mode, assertions are
+# automatically included to ensure that no Nodes can ever be
+# created violating this. (FIXME: the public Expr stuff should
+# enforce them regardless of whether debugging or not.) For
+# example, a binary operator could be specified as:
+#
+# operator LESS_THAN 2 "arithmetic comparison, x < y"
+#
+# Alternatively, a range can be specified for #children as
+# "LB:[UB]", LB and UB representing lower and upper bounds on the
+# number of children (inclusive). If there is no lower bound, put
+# a "0". If there is no upper bound, leave the colon after LB,
+# but omit UB. For example, an N-ary operator might be defined
+# as:
+#
+# operator PLUS 2: "addition on two or more arguments"
+#
+# parameterized K #children ["comment"]
+#
+# Declares a "built-in" parameterized operator kind K. This is a
+# theory-specific APPLY, e.g., APPLY_UF, which applies its first
+# parameter (say, "f"), to its operands (say, "x" and "y", making
+# the full application "f(x,y)"). Nodes with such a kind will
+# have an operator (Node::hasOperator() returns true, and
+# Node::getOperator() returns the Node of functional type
+# representing "f" here), and the "children" are defined to be
+# this operator's parameters, and don't include the operator
+# itself (here, there are only two children "x" and "y").
+#
+# LB and UB are the same as documented for the operator command.
+# The first parameter (the function being applied) does not count
+# as a child.
+#
+# For consistency these should start with "APPLY_", but this is
+# not enforced.
+#
+# constant K T Hasher header ["comment"]
+#
+# Declares a constant kind K. T is the C++ type representing the
+# constant internally (and it should be
+# ::fully::qualified::like::this), and header is the header needed
+# to define it. Hasher is a hash functor type defined like this:
+#
+# struct MyHashFcn {
+# static size_t hash(const T& val);
+# };
+#
+# For consistency, constants taking a non-void payload should
+# start with "CONST_", but this is not enforced.
+#
+# Lines may be broken with a backslash between arguments; for example:
+#
+# constant CONST_INT \
+# int IntHash \
+# "" \
+# "This is a constant representing an INT.
+# Its payload is the C++ int type.
+# It is used by the theory of arithmetic."
+#
+# As shown in the example, ["comment"] fields may be broken across
+# multiple lines too.
+#
+# The expr package guarantees that Nodes built with kinds have the
+# following constraints imposed on them. (The #children guarantee
+# only holds when assertions are turned on.)
+#
+# Node meta-kind has operator? # children
+# ================== ================= =======================
+# variable no zero
+# operator yes as documented above
+# parameterized yes as documented above
+# constant no zero
+#
+# NOTE THAT This file is actually an executable Bourne shell script
+# (sourced by the processing scripts after defining functions called
+# "theory," "variable," "operator," "parameterized," and "constant").
+# Please don't do anything else in this file other than using these
+# commands.
+#
+
+theory builtin
+
+# A kind representing "inlined" operators defined with OPERATOR
+# Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
+# not stored that way. If you ask for the operator of (EQUAL a b),
+# you'll get a special, singleton (BUILTIN EQUAL) Node.
+constant BUILTIN ::CVC4::Kind ::CVC4::kind::KindHashFcn \
+ "expr/kind.h" "The kind of nodes representing built-in operators"
-operator EQUAL "equality"
-operator ITE "if-then-else"
-special SKOLEM "skolem var"
-special VARIABLE "variable"
-operator TUPLE "a tuple"
+operator EQUAL 2 "equality"
+operator DISTINCT 2: "disequality"
+operator ITE 3 "if-then-else"
+variable SKOLEM "skolem var"
+variable VARIABLE "variable"
+operator TUPLE 2: "a tuple"
}
void Expr::printAst(std::ostream & o, int indent) const {
+ ExprManagerScope ems(*this);
getNode().printAst(o, indent);
}
+++ /dev/null
-/********************* */
-/** kind_epilogue.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.
- **
- ** Epilogue for the Node kind header. This file finishes off the
- ** pretty-printing function for the Kind enum.
- **/
-
- case LAST_KIND: out << "LAST_KIND"; break;
- default: out << "UNKNOWNKIND!" << int(k); break;
- }
-
- return out;
-}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__KIND_H */
+++ /dev/null
-/********************* */
-/** kind_middle.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.
- **
- ** Middle section of the Node kind header. This file finishes off the
- ** Kind enum and starts the pretty-printing function definition.
- **/
-
- LAST_KIND
-
-};/* enum Kind_t */
-
-}/* CVC4::kind namespace */
-
-// import Kind into the "CVC4" namespace but keep the individual kind
-// constants under kind::
-typedef ::CVC4::kind::Kind_t 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;
-
- switch(k) {
-
- /* special cases */
- case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
- case NULL_EXPR: out << "NULL"; break;
+++ /dev/null
-/********************* */
-/** kind_prologue.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.
- **
- ** Prologue of the Node kind header. This file starts the Kind enumeration.
- **/
-
-#ifndef __CVC4__KIND_H
-#define __CVC4__KIND_H
-
-#include "cvc4_config.h"
-#include <iostream>
-
-namespace CVC4 {
-namespace kind {
-
-enum Kind_t {
- /* undefined */
- UNDEFINED_KIND = -1,
- /** Null Kind */
- NULL_EXPR,
- /** The kind of nodes representing built-in operators */
- BUILTIN,
--- /dev/null
+/********************* */
+/** kind_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 Node kind header.
+ **/
+
+#ifndef __CVC4__KIND_H
+#define __CVC4__KIND_H
+
+#include "cvc4_config.h"
+#include <iostream>
+#include <sstream>
+
+namespace CVC4 {
+namespace kind {
+
+enum Kind_t {
+ UNDEFINED_KIND = -1, /*! undefined */
+ NULL_EXPR, /*! Null kind */
+${kind_decls}
+ LAST_KIND
+
+};/* enum Kind_t */
+
+}/* CVC4::kind namespace */
+
+// import Kind into the "CVC4" namespace but keep the individual kind
+// constants under kind::
+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;
+
+ 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;
+}
+
+inline std::string kindToString(::CVC4::Kind k) {
+ std::stringstream ss;
+ ss << k;
+ return ss.str();
+}
+
+struct KindHashFcn {
+ static inline size_t hash(::CVC4::Kind k) { return k; }
+};
+
+}/* CVC4::kind namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__KIND_H */
--- /dev/null
+/********************* */
+/** 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 */
# Copyright (c) 2010 The CVC4 Project
#
# The purpose of this script is to create kind.h from a prologue,
-# middle, epilogue, and a list of theory kinds.
+# middle section, epilogue, and a list of theory kinds.
#
# Invocation:
#
# Output is to standard out.
#
+copyright=2010
+
cat <<EOF
/********************* -*- C++ -*- */
/** kind.h
**
- ** Copyright 2010 The AcSys Group, New York University, and as below.
+ ** Copyright $copyright The AcSys Group, New York University, and as below.
**
** This header file automatically generated by:
**
EOF
-prologue=$1; shift
-middle=$1; shift
-epilogue=$1; shift
+me=$(basename "$0")
-cases=
+template=$1; shift
-function special {
- r=$1
- comment=$2
+kind_decls=
+kind_printers=
- echo " $r, /*! $comment */"
- cases="$cases case $r: out << \"$r\"; break;
-"
+seen_theory=false
+seen_theory_builtin=false
+
+function theory {
+ # theory T header
+
+ lineno=${BASH_LINENO[0]}
+
+ # this script doesn't care about the theory class information, but
+ # makes does make sure it's there
+ seen_theory=true
+ if [ "$1" = builtin ]; then
+ if $seen_theory_builtin; then
+ echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
+ exit 1
+ fi
+ seen_theory_builtin=true
+ elif [ -z "$1" -o -z "$2" ]; then
+ echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
+ exit 1
+ elif ! expr "$1" : '\(::*\)' >/dev/null; then
+ echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
+ elif ! expr "$1" : '\(::CVC4::theory::*\)' >/dev/null; then
+ echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
+ fi
+}
+
+function variable {
+ # variable K ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ check_theory_seen
+ register_kind "$1" 0 "$2"
}
function operator {
- special "$1" "$2"
+ # operator K #children ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ check_theory_seen
+ register_kind "$1" "$2" "$3"
}
function parameterized {
- special "$1" "$2"
+ # parameterized K #children ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ check_theory_seen
+ register_kind "$1" "$2" "$3"
}
function constant {
- special "$1" "$3"
+ # constant K T Hasher header ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ check_theory_seen
+ register_kind "$1" 0 "$5"
+}
+
+function register_kind {
+ r=$1
+ nc=$2
+ comment=$3
+
+ kind_decls="${kind_decls} $r, /*! $comment */
+"
+ kind_printers="${kind_printers} case $r: out << \"$r\"; break;
+"
+}
+
+function check_theory_seen {
+ if ! $seen_theory; then
+ echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
+ exit 1
+ fi
+}
+
+function check_builtin_theory_seen {
+ if ! $seen_theory_builtin; then
+ echo "$me: warning: no declaration for the builtin theory found" >&2
+ fi
}
-cat "$prologue"
while [ $# -gt 0 ]; do
- b=$(basename $(dirname "$1"))
- echo
- echo " /* from $b */"
- cases="$cases
+ kf=$1
+ seen_theory=false
+ b=$(basename $(dirname "$kf"))
+ kind_decls="${kind_decls}
+ /* from $b */
+"
+ kind_printers="${kind_printers}
/* from $b */
"
- source "$1"
+ source "$kf"
+ check_theory_seen
shift
done
-cat "$middle"
-echo "$cases"
-cat "$epilogue"
+check_builtin_theory_seen
+
+## output
+
+text=$(cat "$template")
+for var in kind_decls kind_printers; do
+ eval text="\${text//\\\$\\{$var\\}/\${$var}}"
+done
+error=`expr "$text" : '.*\${\([^}]*\)}.*'`
+if [ -n "$error" ]; then
+ echo "$template:0: error: undefined replacement \${$error}" >&2
+ exit 1
+fi
+echo "$text"
--- /dev/null
+#!/bin/bash
+#
+# mkmetakind
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+# Copyright (c) 2010 The CVC4 Project
+#
+# The purpose of this script is to create metakind.h from a prologue,
+# two middle sections, epilogue, and a list of theory kinds.
+#
+# This is kept distinct from kind.h because kind.h is a public header
+# and metakind.h is intended for the expr package only.
+#
+# Invocation:
+#
+# mkmetakind prologue-file middle1-file middle2-file epilogue-file theory-kind-files...
+#
+# Output is to standard out.
+#
+
+copyright=2010
+
+cat <<EOF
+/********************* -*- C++ -*- */
+/** metakind.h
+ **
+ ** Copyright $copyright The AcSys Group, New York University, and as below.
+ **
+ ** This header file automatically generated by:
+ **
+ ** $0 $@
+ **
+ ** for the CVC4 project.
+ **/
+
+EOF
+
+me=$(basename "$0")
+
+template=$1; shift
+
+metakind_includes=
+metakind_kinds=
+metakind_constantMaps=
+metakind_compares=
+metakind_constHashes=
+metakind_constPrinters=
+metakind_ubchildren=
+metakind_lbchildren=
+
+seen_theory=false
+seen_theory_builtin=false
+
+function theory {
+ # theory T header
+
+ lineno=${BASH_LINENO[0]}
+
+ # this script doesn't care about the theory class information, but
+ # makes does make sure it's there
+ seen_theory=true
+ if [ "$1" = builtin ]; then
+ if $seen_theory_builtin; then
+ echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
+ exit 1
+ fi
+ seen_theory_builtin=true
+ elif [ -z "$1" -o -z "$2" ]; then
+ echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
+ exit 1
+ elif ! expr "$1" : '\(::*\)' >/dev/null; then
+ echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
+ elif ! expr "$1" : '\(::CVC4::theory::*\)' >/dev/null; then
+ echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
+ fi
+
+ theory_class=$1
+ if [ "$1" != builtin ]; then
+ metakind_includes="${metakind_includes}
+// #include \"theory/$b/$2\""
+ fi
+}
+
+function variable {
+ # variable K ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ check_theory_seen
+ register_metakind VARIABLE "$1" 0
+}
+
+function operator {
+ # operator K #children ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ check_theory_seen
+ register_metakind OPERATOR "$1" "$2"
+}
+
+function parameterized {
+ # parameterized K #children ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ check_theory_seen
+ register_metakind PARAMETERIZED "$1" "$2"
+}
+
+function constant {
+ # constant K T Hasher header ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ check_theory_seen
+
+ if ! expr "$2" : '\(::*\)' >/dev/null; then
+ echo "$kf:$lineno: warning: constant $1 class \`$2' isn't fully-qualified (e.g., ::CVC4::Rational)" >&2
+ fi
+ if ! expr "$3" : '\(::*\)' >/dev/null; then
+ echo "$kf:$lineno: warning: constant $1 hasher \`$3' isn't fully-qualified (e.g., ::CVC4::RationalHashFcn)" >&2
+ fi
+
+ if [ -n "$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 {
+
+template <>
+inline const $2 & NodeValue::getConst< $2 >() const {
+ Assert(getKind() == ::CVC4::kind::$1);
+ // To support non-inlined CONSTANT-kinded NodeValues (those that are
+ // \"constructed\" when initially checking them against the NodeManager
+ // pool), we must check d_nchildren here.
+ return d_nchildren == 0
+ ? *reinterpret_cast< const $2 * >(d_children)
+ : *reinterpret_cast< const $2 * >(d_children[0]);
+}
+
+}/* 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:
+ return NodeValueConstCompare< kind::$1, pool >::compare(nv1, nv2);
+"
+ metakind_constHashes="${metakind_constHashes}
+ case kind::$1:
+ return $3::hash(nv->getConst< $2 >());
+"
+ metakind_constPrinters="${metakind_constPrinters}
+ case kind::$1:
+ out << nv->getConst< $2 >();
+ break;
+"
+}
+
+function register_metakind {
+ mk=$1
+ k=$2
+ nc=$3
+ metakind_kinds="${metakind_kinds} metakind::$mk, /* $k */
+";
+
+ # figure out the range given by $nc
+ if expr "$nc" : '^[0-9]\+$' >/dev/null; then
+ lb=$nc
+ ub=$nc
+ elif expr "$nc" : '^[0-9]\+:$' >/dev/null; then
+ let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1}'`
+ ub=MAX_CHILDREN
+ elif expr "$nc" : '^[0-9]\+:[0-9]\+$' >/dev/null; then
+ let `echo "$nc" | awk 'BEGIN{FS=":"}{print"lb="$1" ub="$2}'`
+ if [ $ub -lt $lb ]; then
+ echo "$kf:$lineno: error in range \`$nc': LB < UB (in definition of $k)" >&2
+ exit 1
+ fi
+ else
+ echo "$kf:$lineno: can't parse range \`$nc' in definition of $k" >&2
+ exit 1
+ fi
+
+ metakind_lbchildren="${metakind_lbchildren}
+ $lb, /* $k */"
+ metakind_ubchildren="${metakind_ubchildren}
+ $ub, /* $k */"
+}
+
+function check_theory_seen {
+ if ! $seen_theory; then
+ echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
+ exit 1
+ fi
+}
+
+function check_builtin_theory_seen {
+ if ! $seen_theory_builtin; then
+ echo "$me: warning: no declaration for the builtin theory found" >&2
+ fi
+}
+
+while [ $# -gt 0 ]; do
+ kf=$1
+ seen_theory=false
+ b=$(basename $(dirname "$kf"))
+ metakind_kinds="${metakind_kinds}
+ /* from $b */
+"
+ source "$kf"
+ check_theory_seen
+ shift
+done
+check_builtin_theory_seen
+
+## output
+
+text=$(cat "$template")
+for var in metakind_includes metakind_kinds metakind_constantMaps \
+ metakind_compares metakind_constHashes metakind_constPrinters \
+ metakind_ubchildren metakind_lbchildren; do
+ eval text="\${text//\\\$\\{$var\\}/\${$var}}"
+done
+error=`expr "$text" : '.*\${\([^}]*\)}.*'`
+if [ -n "$error" ]; then
+ echo "$template:0: error: undefined replacement \${$error}" >&2
+ exit 1
+fi
+echo "$text"
#include "expr/node.h"
#include "util/output.h"
+#include <iostream>
+
+using namespace std;
+
namespace CVC4 {
namespace expr {
-#ifdef CVC4_DEBUG
-#endif /* CVC4_DEBUG */
+const int NodeSetDepth::s_iosIndex = std::ios_base::xalloc();
}/* CVC4::expr namespace */
}/* CVC4 namespace */
class AttributeManager;
}/* CVC4::expr::attr namespace */
+ class NodeSetDepth;
}/* CVC4::expr namespace */
/**
* @return the node representing the i-th child
*/
NodeTemplate operator[](int i) const {
- Assert(i >= 0 && unsigned(i) < d_nv->d_nchildren);
- return NodeTemplate(d_nv->d_children[i]);
+ return NodeTemplate(d_nv->getChild(i));
}
/**
NodeTemplate<true> getOperator() const;
/** Returns true if the node has an operator (i.e., it's not a variable or a constant). */
- bool hasOperator() const;
+ inline bool hasOperator() const;
/**
* Returns the type of this node.
return Kind(d_nv->d_kind);
}
+ /**
+ * Returns the metakind of this node.
+ * @return the metakind
+ */
+ inline kind::MetaKind getMetaKind() const {
+ return kind::metaKindOf(getKind());
+ }
+
/**
* Returns the number of children this node has.
* @return the number of children
*/
inline size_t getNumChildren() const;
+ /**
+ * If this is a CONST_* Node, extract the constant from it.
+ */
+ template <class T>
+ inline const T& getConst() const;
+
/**
* Returns the value of the given attribute that this has been attached.
* @param attKind the kind of the attribute
* given stream
* @param out the sream to serialise this node to
*/
- inline void toStream(std::ostream& out) const {
- d_nv->toStream(out);
+ inline void toStream(std::ostream& out, int toDepth = -1) const {
+ d_nv->toStream(out, toDepth);
}
+ /**
+ * IOStream manipulator to set the maximum depth of Nodes when
+ * pretty-printing. -1 means print to any depth. E.g.:
+ *
+ * // let a, b, c, and d be VARIABLEs
+ * Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d)))
+ * out << setdepth(3) << n;
+ *
+ * gives "(OR a b (AND c (NOT d)))", but
+ *
+ * out << setdepth(1) << [same node as above]
+ *
+ * gives "(OR a b (...))"
+ */
+ typedef expr::NodeSetDepth setdepth;
+
/**
* Very basic pretty printer for Node.
* @param o output stream to print to.
}
}
-};/* class NodeTemplate */
+};/* class NodeTemplate<ref_count> */
+
+namespace expr {
+
+/**
+ * IOStream manipulator to set the maximum depth of Nodes when
+ * pretty-printing. -1 means print to any depth. E.g.:
+ *
+ * // let a, b, c, and d be VARIABLEs
+ * Node n = nm->mkNode(OR, a, b, nm->mkNode(AND, c, nm->mkNode(NOT, d)))
+ * out << setdepth(3) << n;
+ *
+ * gives "(OR a b (AND c (NOT d)))", but
+ *
+ * out << setdepth(1) << [same node as above]
+ *
+ * gives "(OR a b (...))".
+ *
+ * The implementation of this class serves two purposes; it holds
+ * information about the depth setting (such as the index of the
+ * allocated word in ios_base), and serves also as the manipulator
+ * itself (as above).
+ */
+class NodeSetDepth {
+ /**
+ * The allocated index in ios_base for our depth setting.
+ */
+ static const int s_iosIndex;
+
+ /**
+ * The default depth to print, for ostreams that haven't yet had a
+ * setdepth() applied to them.
+ */
+ static const int s_defaultPrintDepth = 3;
+
+ /**
+ * When this manipulator is
+ */
+ long d_depth;
+
+public:
+ /**
+ * Construct a NodeSetDepth with the given depth.
+ */
+ NodeSetDepth(long depth) : d_depth(depth) {}
+
+ inline void applyDepth(std::ostream& out) {
+ out.iword(s_iosIndex) = d_depth;
+ }
+
+ static inline long getDepth(std::ostream& out) {
+ long& l = out.iword(s_iosIndex);
+ if(l == 0) {
+ // set the default print depth on this ostream
+ l = s_defaultPrintDepth;
+ }
+ return l;
+ }
+
+ static inline void setDepth(std::ostream& out, long depth) {
+ out.iword(s_iosIndex) = depth;
+ }
+};
+
+/**
+ * Sets the default depth when pretty-printing a Node to an ostream.
+ * Use like this:
+ *
+ * // let out be an ostream, n a Node
+ * out << Node::setdepth(n) << n << endl;
+ *
+ * The depth stays permanently (until set again) with the stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, NodeSetDepth sd) {
+ sd.applyDepth(out);
+ return out;
+}
+
+}/* CVC4::expr namespace */
/**
* Serializes a given node to the given stream.
* @param node the node to output to the stream
* @return the changed stream.
*/
-inline std::ostream& operator<<(std::ostream& out, const Node& node) {
- node.toStream(out);
+inline std::ostream& operator<<(std::ostream& out, TNode n) {
+ n.toStream(out, Node::setdepth::getDepth(out));
return out;
}
template <bool ref_count>
inline size_t NodeTemplate<ref_count>::getNumChildren() const {
- return d_nv->d_nchildren;
+ return d_nv->getNumChildren();
+}
+
+template <bool ref_count>
+template <class T>
+inline const T& NodeTemplate<ref_count>::getConst() const {
+ return d_nv->getConst<T>();
}
template <bool ref_count>
Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
if(ref_count) {
d_nv->inc();
+ } else {
+ Assert(d_nv->d_rc > 0, "TNode constructed from NodeValue with rc == 0");
}
}
-// the code for these two "conversion/copy constructors" is identical, but
-// apparently we need both. see comment in the class.
+// the code for these two following constructors ("conversion/copy
+// constructors") is identical, but we need both. see comment in the
+// class.
+
template <bool ref_count>
NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<!ref_count>& e) {
Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
d_nv = e.d_nv;
if(ref_count) {
d_nv->inc();
+ } else {
+ // shouldn't ever happen
+ Assert(d_nv->d_rc > 0,
+ "INTERNAL ERROR: TNode constructed from Node with rc == 0");
}
}
d_nv = e.d_nv;
if(ref_count) {
d_nv->inc();
+ } else {
+ Assert(d_nv->d_rc > 0, "TNode constructed from TNode with rc == 0");
}
}
Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
if(ref_count) {
d_nv->dec();
+ } else {
+ Assert(d_nv->d_rc > 0 || d_nv->isBeingDeleted(),
+ "TNode pointing to an expired NodeValue at destruction time");
}
- Assert(ref_count ||
- d_nv->d_rc > 0 ||
- d_nv->isBeingDeleted(),
- "Temporary node pointing to an expired node");
}
template <bool ref_count>
d_nv = ev;
if(ref_count) {
d_nv->inc();
+ } else {
+ Assert(d_nv->d_rc > 0, "TNode assigned to NodeValue with rc == 0");
}
}
d_nv = e.d_nv;
if(ref_count) {
d_nv->inc();
+ } else {
+ Assert(d_nv->d_rc > 0, "TNode assigned from TNode with rc == 0");
}
}
return *this;
d_nv = e.d_nv;
if(ref_count) {
d_nv->inc();
+ } else {
+ // shouldn't ever happen
+ Assert(d_nv->d_rc > 0,
+ "INTERNAL ERROR: TNode assigned from Node with rc == 0");
}
}
return *this;
indent(out, ind);
out << '(';
out << getKind();
- if(getKind() == kind::VARIABLE) {
+ if(getMetaKind() == kind::metakind::VARIABLE) {
out << ' ' << getId();
-
- } else if(getNumChildren() >= 1) {
- for(const_iterator child = begin(); child != end(); ++child) {
+ } else if(getMetaKind() == kind::metakind::CONSTANT) {
+ out << ' ';
+ kind::metakind::NodeValueConstPrinter::toStream(out, d_nv);
+ } else {
+ if(hasOperator()) {
+ out << std::endl;
+ getOperator().printAst(out, ind + 1);
+ }
+ if(getNumChildren() >= 1) {
+ for(const_iterator child = begin(); child != end(); ++child) {
+ out << std::endl;
+ (*child).printAst(out, ind + 1);
+ }
out << std::endl;
- NodeTemplate((*child)).printAst(out, ind + 1);
+ indent(out, ind);
}
- out << std::endl;
- indent(out, ind);
}
out << ')';
}
*/
template <bool ref_count>
NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const {
- switch(Kind k = getKind()) {
- case kind::APPLY:
- /* The operator is the first child. */
- return NodeTemplate<true>(d_nv->d_children[0]);
-
- case kind::EQUAL:
- case kind::ITE:
- case kind::TUPLE:
- case kind::NOT:
- case kind::AND:
- case kind::IFF:
- case kind::IMPLIES:
- case kind::OR:
- case kind::XOR:
- case kind::PLUS: {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
+ switch(kind::MetaKind mk = getMetaKind()) {
+ case kind::metakind::INVALID:
+ IllegalArgument(*this, "getOperator() called on Node with INVALID-kinded kind");
+
+ case kind::metakind::VARIABLE:
+ IllegalArgument(*this, "getOperator() called on Node with VARIABLE-kinded kind");
+
+ case kind::metakind::OPERATOR: {
/* Returns a BUILTIN node. */
- /* TODO: construct a singleton at load-time? */
- /* TODO: maybe keep a table like the TheoryOfTable ? */
- NodeTemplate<true> n = NodeManager::currentNM()->mkNode(k);
- return NodeManager::currentNM()->mkNode(kind::BUILTIN, n);
+ return NodeManager::currentNM()->operatorOf(getKind());
}
- case kind::FALSE:
- case kind::TRUE:
- case kind::SKOLEM:
- case kind::VARIABLE:
- IllegalArgument(*this, "getOperator() called on kind with no operator");
+ case kind::metakind::PARAMETERIZED:
+ /* The operator is the first child. */
+ return Node(d_nv->d_children[0]);
+
+ case kind::metakind::CONSTANT:
+ IllegalArgument(*this, "getOperator() called on Node with CONSTANT-kinded kind");
default:
- Unhandled(getKind());
+ Unhandled(mk);
}
}
* or a constant).
*/
template <bool ref_count>
-bool NodeTemplate<ref_count>::hasOperator() const {
- switch(getKind()) {
- case kind::APPLY:
- case kind::EQUAL:
- case kind::ITE:
- case kind::TUPLE:
- case kind::FALSE:
- case kind::TRUE:
- case kind::NOT:
- case kind::AND:
- case kind::IFF:
- case kind::IMPLIES:
- case kind::OR:
- case kind::XOR:
- case kind::PLUS:
- return true;
-
- case kind::SKOLEM:
- case kind::VARIABLE:
- return false;
-
- default:
- Unhandled(getKind());
- }
+inline bool NodeTemplate<ref_count>::hasOperator() const {
+ return NodeManager::hasOperator(getKind());
}
template <bool ref_count>
+++ /dev/null
-/********************* */
-/** node_builder.cpp
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): dejan
- ** 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.
- **
- **/
-
}/* CVC4 namespace */
#include "expr/kind.h"
+#include "expr/metakind.h"
#include "util/Assert.h"
#include "expr/node_value.h"
#include "util/output.h"
}
Builder& collapseTo(Kind k) {
- AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR,
+ AssertArgument(k != kind::UNDEFINED_KIND &&
+ k != kind::NULL_EXPR &&
+ k < kind::LAST_KIND,
k, "illegal collapsing kind");
if(getKind() != k) {
return d_nv->getKind();
}
+ /** Get the kind of this Node-under-construction. */
+ inline kind::MetaKind getMetaKind() const {
+ Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+ return d_nv->getMetaKind();
+ }
+
/** Get the current number of children of this Node-under-construction. */
inline unsigned getNumChildren() const {
Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
/** Access to children of this Node-under-construction. */
inline Node operator[](int i) const {
Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
- Assert(i >= 0 && i < d_nv->getNumChildren(), "index out of range for NodeBuilder[]");
- return Node(d_nv->d_children[i]);
+ Assert(i >= 0 && unsigned(i) < d_nv->getNumChildren(),
+ "index out of range for NodeBuilder[]");
+ return Node(d_nv->getChild(i));
}
/**
Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
Assert(getKind() == kind::UNDEFINED_KIND,
"can't redefine the Kind of a NodeBuilder");
- Assert(k != kind::UNDEFINED_KIND,
- "can't define the Kind of a NodeBuilder to be UNDEFINED_KIND");
+ AssertArgument(k != kind::UNDEFINED_KIND &&
+ k != kind::NULL_EXPR &&
+ k < kind::LAST_KIND,
+ k, "illegal node-building kind");
d_nv->d_kind = expr::NodeValue::kindToDKind(k);
return static_cast<Builder&>(*this);
}
/** Append a child to this Node-under-construction. */
Builder& append(TNode n) {
Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
+ Assert(!n.isNull(), "Cannot use NULL Node as a child of a Node");
allocateNvIfNecessaryForAppend();
expr::NodeValue* nv = n.d_nv;
nv->inc();
operator Node();
operator Node() const;
- inline void toStream(std::ostream& out) const {
+ inline void toStream(std::ostream& out, int depth = -1) const {
Assert(!isUsed(), "NodeBuilder is one-shot only; attempt to access it after conversion");
- d_nv->toStream(out);
+ d_nv->toStream(out, depth);
}
Builder& operator&=(TNode);
NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
}
- inline BackedNodeBuilder(expr::NodeValue* buf, unsigned maxChildren, NodeManager* nm, Kind k) :
+ inline BackedNodeBuilder(expr::NodeValue* buf,
+ unsigned maxChildren,
+ NodeManager* nm,
+ Kind k) :
NodeBuilderBase<BackedNodeBuilder>(buf, maxChildren) {
}
return OrNodeBuilder(Node(d_eb), n);
}
-inline AndNodeBuilder& operator&&(AndNodeBuilder& a, const AndNodeBuilder& b) {
+inline AndNodeBuilder& operator&&(AndNodeBuilder& a,
+ const AndNodeBuilder& b) {
return a && Node(b.d_eb);
}
-inline AndNodeBuilder& operator&&(AndNodeBuilder& a, const OrNodeBuilder& b) {
+inline AndNodeBuilder& operator&&(AndNodeBuilder& a,
+ const OrNodeBuilder& b) {
return a && Node(b.d_eb);
}
-inline OrNodeBuilder operator||(AndNodeBuilder& a, const AndNodeBuilder& b) {
+inline OrNodeBuilder operator||(AndNodeBuilder& a,
+ const AndNodeBuilder& b) {
return a || Node(b.d_eb);
}
-inline OrNodeBuilder operator||(AndNodeBuilder& a, const OrNodeBuilder& b) {
+inline OrNodeBuilder operator||(AndNodeBuilder& a,
+ const OrNodeBuilder& b) {
return a || Node(b.d_eb);
}
return *this;
}
-inline AndNodeBuilder operator&&(OrNodeBuilder& a, const AndNodeBuilder& b) {
+inline AndNodeBuilder operator&&(OrNodeBuilder& a,
+ const AndNodeBuilder& b) {
return a && Node(b.d_eb);
}
-inline AndNodeBuilder operator&&(OrNodeBuilder& a, const OrNodeBuilder& b) {
+inline AndNodeBuilder operator&&(OrNodeBuilder& a,
+ const OrNodeBuilder& b) {
return a && Node(b.d_eb);
}
-inline OrNodeBuilder& operator||(OrNodeBuilder& a, const AndNodeBuilder& b) {
+inline OrNodeBuilder& operator||(OrNodeBuilder& a,
+ const AndNodeBuilder& b) {
return a || Node(b.d_eb);
}
-inline OrNodeBuilder& operator||(OrNodeBuilder& a, const OrNodeBuilder& b) {
+inline OrNodeBuilder& operator||(OrNodeBuilder& a,
+ const OrNodeBuilder& b) {
return a || Node(b.d_eb);
}
return MultNodeBuilder(Node(d_eb), n);
}
-inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, const PlusNodeBuilder& b) {
+inline PlusNodeBuilder& operator+(PlusNodeBuilder& a,
+ const PlusNodeBuilder& b) {
return a + Node(b.d_eb);
}
-inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, const MultNodeBuilder& b) {
+inline PlusNodeBuilder& operator+(PlusNodeBuilder& a,
+ const MultNodeBuilder& b) {
return a + Node(b.d_eb);
}
-inline PlusNodeBuilder& operator-(PlusNodeBuilder&a, const PlusNodeBuilder& b) {
+inline PlusNodeBuilder& operator-(PlusNodeBuilder&a,
+ const PlusNodeBuilder& b) {
return a - Node(b.d_eb);
}
-inline PlusNodeBuilder& operator-(PlusNodeBuilder& a, const MultNodeBuilder& b) {
+inline PlusNodeBuilder& operator-(PlusNodeBuilder& a,
+ const MultNodeBuilder& b) {
return a - Node(b.d_eb);
}
-inline MultNodeBuilder operator*(PlusNodeBuilder& a, const PlusNodeBuilder& b) {
+inline MultNodeBuilder operator*(PlusNodeBuilder& a,
+ const PlusNodeBuilder& b) {
return a * Node(b.d_eb);
}
-inline MultNodeBuilder operator*(PlusNodeBuilder& a, const MultNodeBuilder& b) {
+inline MultNodeBuilder operator*(PlusNodeBuilder& a,
+ const MultNodeBuilder& b) {
return a * Node(b.d_eb);
}
template <bool rc>
inline PlusNodeBuilder MultNodeBuilder::operator-(const NodeTemplate<rc>& n) {
- return PlusNodeBuilder(Node(d_eb), NodeManager::currentNM()->mkNode(kind::UMINUS, n));
+ return PlusNodeBuilder(Node(d_eb),
+ NodeManager::currentNM()->mkNode(kind::UMINUS, n));
}
template <bool rc>
return *this;
}
-inline PlusNodeBuilder operator+(MultNodeBuilder& a, const PlusNodeBuilder& b) {
+inline PlusNodeBuilder operator+(MultNodeBuilder& a,
+ const PlusNodeBuilder& b) {
return a + Node(b.d_eb);
}
-inline PlusNodeBuilder operator+(MultNodeBuilder& a, const MultNodeBuilder& b) {
+inline PlusNodeBuilder operator+(MultNodeBuilder& a,
+ const MultNodeBuilder& b) {
return a + Node(b.d_eb);
}
-inline PlusNodeBuilder operator-(MultNodeBuilder& a, const PlusNodeBuilder& b) {
+inline PlusNodeBuilder operator-(MultNodeBuilder& a,
+ const PlusNodeBuilder& b) {
return a - Node(b.d_eb);
}
-inline PlusNodeBuilder operator-(MultNodeBuilder& a, const MultNodeBuilder& b) {
+inline PlusNodeBuilder operator-(MultNodeBuilder& a,
+ const MultNodeBuilder& b) {
return a - Node(b.d_eb);
}
-inline MultNodeBuilder& operator*(MultNodeBuilder& a, const PlusNodeBuilder& b) {
+inline MultNodeBuilder& operator*(MultNodeBuilder& a,
+ const PlusNodeBuilder& b) {
return a * Node(b.d_eb);
}
-inline MultNodeBuilder& operator*(MultNodeBuilder& a, const MultNodeBuilder& b) {
+inline MultNodeBuilder& operator*(MultNodeBuilder& a,
+ const MultNodeBuilder& b) {
return a * Node(b.d_eb);
}
template <bool rc1, bool rc2>
-inline AndNodeBuilder operator&&(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& b) {
+inline AndNodeBuilder operator&&(const NodeTemplate<rc1>& a,
+ const NodeTemplate<rc2>& b) {
return AndNodeBuilder(a, b);
}
template <bool rc1, bool rc2>
-inline OrNodeBuilder operator||(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& b) {
+inline OrNodeBuilder operator||(const NodeTemplate<rc1>& a,
+ const NodeTemplate<rc2>& b) {
return OrNodeBuilder(a, b);
}
template <bool rc1, bool rc2>
-inline PlusNodeBuilder operator+(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& b) {
+inline PlusNodeBuilder operator+(const NodeTemplate<rc1>& a,
+ const NodeTemplate<rc2>& b) {
return PlusNodeBuilder(a, b);
}
template <bool rc1, bool rc2>
-inline PlusNodeBuilder operator-(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& b) {
+inline PlusNodeBuilder operator-(const NodeTemplate<rc1>& a,
+ const NodeTemplate<rc2>& b) {
return PlusNodeBuilder(a, NodeManager::currentNM()->mkNode(kind::UMINUS, b));
}
template <bool rc1, bool rc2>
-inline MultNodeBuilder operator*(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& b) {
+inline MultNodeBuilder operator*(const NodeTemplate<rc1>& a,
+ const NodeTemplate<rc2>& b) {
return MultNodeBuilder(a, b);
}
template <bool rc>
-inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a, const AndNodeBuilder& b) {
+inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a,
+ const AndNodeBuilder& b) {
return a && Node(b.d_eb);
}
template <bool rc>
-inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a, const OrNodeBuilder& b) {
+inline AndNodeBuilder operator&&(const NodeTemplate<rc>& a,
+ const OrNodeBuilder& b) {
return a && Node(b.d_eb);
}
template <bool rc>
-inline OrNodeBuilder operator||(const NodeTemplate<rc>& a, const AndNodeBuilder& b) {
+inline OrNodeBuilder operator||(const NodeTemplate<rc>& a,
+ const AndNodeBuilder& b) {
return a || Node(b.d_eb);
}
template <bool rc>
-inline OrNodeBuilder operator||(const NodeTemplate<rc>& a, const OrNodeBuilder& b) {
+inline OrNodeBuilder operator||(const NodeTemplate<rc>& a,
+ const OrNodeBuilder& b) {
return a || Node(b.d_eb);
}
template <bool rc>
-inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a, const PlusNodeBuilder& b) {
+inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a,
+ const PlusNodeBuilder& b) {
return a + Node(b.d_eb);
}
template <bool rc>
-inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a, const MultNodeBuilder& b) {
+inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a,
+ const MultNodeBuilder& b) {
return a + Node(b.d_eb);
}
template <bool rc>
-inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a, const PlusNodeBuilder& b) {
+inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a,
+ const PlusNodeBuilder& b) {
return a - Node(b.d_eb);
}
template <bool rc>
-inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a, const MultNodeBuilder& b) {
+inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a,
+ const MultNodeBuilder& b) {
return a - Node(b.d_eb);
}
template <bool rc>
-inline MultNodeBuilder operator*(const NodeTemplate<rc>& a, const PlusNodeBuilder& b) {
+inline MultNodeBuilder operator*(const NodeTemplate<rc>& a,
+ const PlusNodeBuilder& b) {
return a * Node(b.d_eb);
}
template <bool rc>
-inline MultNodeBuilder operator*(const NodeTemplate<rc>& a, const MultNodeBuilder& b) {
+inline MultNodeBuilder operator*(const NodeTemplate<rc>& a,
+ const MultNodeBuilder& b) {
return a * Node(b.d_eb);
}
namespace CVC4 {
template <class Builder>
-inline NodeBuilderBase<Builder>::NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren, Kind k) :
+inline NodeBuilderBase<Builder>::NodeBuilderBase(expr::NodeValue* buf,
+ unsigned maxChildren,
+ Kind k) :
d_inlineNv(*buf),
d_nv(&d_inlineNv),
d_nm(NodeManager::currentNM()),
d_inlineNvMaxChildren(maxChildren),
d_nvMaxChildren(maxChildren) {
+ Assert(k != kind::NULL_EXPR, "illegal Node-building kind");
+
d_inlineNv.d_id = 0;
d_inlineNv.d_rc = 0;
d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
}
template <class Builder>
-inline NodeBuilderBase<Builder>::NodeBuilderBase(expr::NodeValue* buf, unsigned maxChildren, NodeManager* nm, Kind k) :
+inline NodeBuilderBase<Builder>::NodeBuilderBase(expr::NodeValue* buf,
+ unsigned maxChildren,
+ NodeManager* nm,
+ Kind k) :
d_inlineNv(*buf),
d_nv(&d_inlineNv),
d_nm(nm),
d_inlineNvMaxChildren(maxChildren),
d_nvMaxChildren(maxChildren) {
+ Assert(k != kind::NULL_EXPR, "illegal Node-building kind");
+
d_inlineNv.d_id = 0;
d_inlineNv.d_rc = 0;
d_inlineNv.d_kind = expr::NodeValue::kindToDKind(k);
template <class Builder>
void NodeBuilderBase<Builder>::clear(Kind k) {
+ Assert(k != kind::NULL_EXPR, "illegal Node-building clear kind");
+
if(EXPECT_FALSE( nvIsAllocated() )) {
dealloc();
} else if(EXPECT_FALSE( !isUsed() )) {
// file comments at the top of this file.
// Case 0: If a VARIABLE
- if(getKind() == kind::VARIABLE) {
+ if(getMetaKind() == kind::metakind::VARIABLE) {
/* 0. If a VARIABLE, treat similarly to 1(b), except that we know
- * there are no children (no reference counts to reason about)
+ * there are no children (no reference counts to reason about),
* and we don't keep VARIABLE-kinded Nodes in the NodeManager
* pool. */
// there are no children, so we don't have to worry about
// reference counts in this case.
nv->d_nchildren = 0;
- nv->d_kind = expr::NodeValue::kindToDKind(kind::VARIABLE);
+ nv->d_kind = d_nv->d_kind;
nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
nv->d_rc = 0;
setUsed();
return Node(nv);
}
+ // check that there are the right # of children for this kind
+ Assert(getMetaKind() != kind::metakind::CONSTANT,
+ "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds");
+ Assert(d_nv->d_nchildren >= kind::metakind::getLowerBoundForKind(getKind()),
+ "Nodes with kind %s must have at least %u children (the one under "
+ "construction has %u)",
+ kind::kindToString(getKind()).c_str(),
+ kind::metakind::getLowerBoundForKind(getKind()),
+ getNumChildren());
+ Assert(d_nv->d_nchildren <= kind::metakind::getUpperBoundForKind(getKind()),
+ "Nodes with kind %s must have at most %u children (the one under "
+ "construction has %u)",
+ kind::kindToString(getKind()).c_str(),
+ kind::metakind::getUpperBoundForKind(getKind()),
+ getNumChildren());
+
// Implementation differs depending on whether the NodeValue was
// malloc'ed or not and whether or not it's in the already-been-seen
// NodeManager pool of Nodes. See implementation notes at the top
** supplied by the user (or derived class) **/
// Lookup the expression value in the pool we already have
- expr::NodeValue* nv = d_nm->poolLookup(&d_inlineNv);
- if(nv != NULL) {
+ expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv);
+ // If something else is there, we reuse it
+ if(poolNv != NULL) {
/* Subcase (a): The Node under construction already exists in
* the NodeManager's pool. */
decrRefCounts();
d_inlineNv.d_nchildren = 0;
setUsed();
- Debug("gc") << "creating node value " << nv
- << " [" << nv->d_id << "]: " << nv->toString() << "\n";
- return Node(nv);
+ return Node(poolNv);
} else {
/* Subcase (b): The Node under construction is NOT already in
* the NodeManager's pool. */
* reference count. */
// create the canonical expression value for this node
- nv = (expr::NodeValue*)
+ expr::NodeValue* nv = (expr::NodeValue*)
std::malloc(sizeof(expr::NodeValue) +
( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));
if(nv == NULL) {
d_inlineNv.d_nchildren = 0;
setUsed();
+ //poolNv = nv;
d_nm->poolInsert(nv);
Debug("gc") << "creating node value " << nv
- << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+ << " [" << nv->d_id << "]: " << *nv << "\n";
return Node(nv);
}
} else {
** buffer that was heap-allocated by this NodeBuilder. **/
// Lookup the expression value in the pool we already have (with insert)
- expr::NodeValue* nv = d_nm->poolLookup(d_nv);
+ expr::NodeValue* poolNv = d_nm->poolLookup(d_nv);
// If something else is there, we reuse it
- if(nv != NULL) {
- /* Subcase (a) The Node under construction already exists in the
- * NodeManager's pool. */
+ if(poolNv != NULL) {
+ /* Subcase (a): The Node under construction already exists in
+ * the NodeManager's pool. */
- /* 2(a). Reference counts for all children in d_nv must be
+ /* 2(a). Reference-counts for all children in d_nv must be
* decremented. The NodeBuilder is marked as "used" and the
* heap-allocated d_nv deleted. d_nv is repointed to d_inlineNv
* so that destruction of the NodeBuilder doesn't cause any
dealloc();
setUsed();
- Debug("gc") << "creating node value " << nv
- << " [" << nv->d_id << "]: " << nv->toString() << "\n";
- return Node(nv);
+ return Node(poolNv);
} else {
/* Subcase (b) The Node under construction is NOT already in the
* NodeManager's pool. */
* a Node wrapper. */
crop();
- nv = d_nv;
+ expr::NodeValue* nv = d_nv;
nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
d_nv = &d_inlineNv;
d_nvMaxChildren = d_inlineNvMaxChildren;
setUsed();
+
+ //poolNv = nv;
d_nm->poolInsert(nv);
Debug("gc") << "creating node value " << nv
- << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+ << " [" << nv->d_id << "]: " << *nv << "\n";
return Node(nv);
}
}
// file comments at the top of this file.
// Case 0: If a VARIABLE
- if(getKind() == kind::VARIABLE) {
+ if(getMetaKind() == kind::metakind::VARIABLE) {
/* 0. If a VARIABLE, treat similarly to 1(b), except that we know
- * there are no children, and we don't keep VARIABLE-kinded Nodes
- * in the NodeManager pool. */
+ * there are no children (no reference counts to reason about),
+ * and we don't keep VARIABLE-kinded Nodes in the NodeManager
+ * pool. */
Assert( ! nvIsAllocated(),
"internal NodeBuilder error: "
// there are no children, so we don't have to worry about
// reference counts in this case.
nv->d_nchildren = 0;
- nv->d_kind = expr::NodeValue::kindToDKind(kind::VARIABLE);
+ nv->d_kind = d_nv->d_kind;
nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
nv->d_rc = 0;
Debug("gc") << "creating node value " << nv
- << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+ << " [" << nv->d_id << "]: " << *nv << "\n";
return Node(nv);
}
+ // check that there are the right # of children for this kind
+ Assert(getMetaKind() != kind::metakind::CONSTANT,
+ "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds");
+ Assert(d_nv->d_nchildren >= kind::metakind::getLowerBoundForKind(getKind()),
+ "Nodes with kind %s must have at least %u children (the one under "
+ "construction has %u)",
+ kind::kindToString(getKind()).c_str(),
+ kind::metakind::getLowerBoundForKind(getKind()),
+ getNumChildren());
+ Assert(d_nv->d_nchildren <= kind::metakind::getUpperBoundForKind(getKind()),
+ "Nodes with kind %s must have at most %u children (the one under "
+ "construction has %u)",
+ kind::kindToString(getKind()).c_str(),
+ kind::metakind::getUpperBoundForKind(getKind()),
+ getNumChildren());
+
// Implementation differs depending on whether the NodeValue was
// malloc'ed or not and whether or not it's in the already-been-seen
// NodeManager pool of Nodes. See implementation notes at the top
** supplied by the user (or derived class) **/
// Lookup the expression value in the pool we already have
- expr::NodeValue* nv = d_nm->poolLookup(&d_inlineNv);
- if(nv != NULL) {
+ expr::NodeValue* poolNv = d_nm->poolLookup(&d_inlineNv);
+ // If something else is there, we reuse it
+ if(poolNv != NULL) {
/* Subcase (a): The Node under construction already exists in
* the NodeManager's pool. */
* leave child reference counts alone and get them at
* NodeBuilder destruction time. */
- Debug("gc") << "creating node value " << nv
- << " [" << nv->d_id << "]: " << nv->toString() << "\n";
- return Node(nv);
+ return Node(poolNv);
} else {
/* Subcase (b): The Node under construction is NOT already in
* the NodeManager's pool. */
* count. */
// create the canonical expression value for this node
- nv = (expr::NodeValue*)
+ expr::NodeValue* nv = (expr::NodeValue*)
std::malloc(sizeof(expr::NodeValue) +
( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));
if(nv == NULL) {
(*i)->inc();
}
+ //poolNv = nv;
d_nm->poolInsert(nv);
Debug("gc") << "creating node value " << nv
- << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+ << " [" << nv->d_id << "]: " << *nv << "\n";
return Node(nv);
}
} else {
** buffer that was heap-allocated by this NodeBuilder. **/
// Lookup the expression value in the pool we already have (with insert)
- expr::NodeValue* nv = d_nm->poolLookup(d_nv);
+ expr::NodeValue* poolNv = d_nm->poolLookup(d_nv);
// If something else is there, we reuse it
- if(nv != NULL) {
- /* Subcase (a) The Node under construction already exists in the
- * NodeManager's pool. */
+ if(poolNv != NULL) {
+ /* Subcase (a): The Node under construction already exists in
+ * the NodeManager's pool. */
/* 2(a). The existing NodeManager pool entry is returned; we
* leave child reference counts alone and get them at
* NodeBuilder destruction time. */
- Debug("gc") << "creating node value " << nv
- << " [" << nv->d_id << "]: " << nv->toString() << "\n";
- return Node(nv);
+ return Node(poolNv);
} else {
/* Subcase (b) The Node under construction is NOT already in the
* NodeManager's pool. */
* decremented to match at NodeBuilder destruction time. */
// create the canonical expression value for this node
- nv = (expr::NodeValue*)
+ expr::NodeValue* nv = (expr::NodeValue*)
std::malloc(sizeof(expr::NodeValue) +
( sizeof(expr::NodeValue*) * d_nv->d_nchildren ));
if(nv == NULL) {
(*i)->inc();
}
+ //poolNv = nv;
d_nm->poolInsert(nv);
Debug("gc") << "creating node value " << nv
- << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+ << " [" << nv->d_id << "]: " << *nv << "\n";
return Node(nv);
}
}
template <class Builder>
inline std::ostream& operator<<(std::ostream& out,
const NodeBuilderBase<Builder>& b) {
- b.toStream(out);
+ b.toStream(out, Node::setdepth::getDepth(out));
return out;
}
__thread NodeManager* NodeManager::s_current = 0;
+NodeManager::NodeManager(context::Context* ctxt) :
+ d_attrManager(ctxt),
+ d_nodeUnderDeletion(NULL),
+ d_reclaiming(false) {
+ poolInsert( &expr::NodeValue::s_null );
+
+ for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
+ Kind k = Kind(i);
+
+ if(hasOperator(k)) {
+ d_operators[i] = mkConst(Kind(k));
+ }
+ }
+}
+
NodeManager::~NodeManager() {
+ // have to ensure "this" is the current NodeManager during
+ // destruction of operators, because they get GCed.
+
NodeManagerScope nms(this);
+
+ for(unsigned i = 0; i < unsigned(kind::LAST_KIND); ++i) {
+ d_operators[i] = Node::null();
+ }
+
while(!d_zombies.empty()) {
reclaimZombies();
}
poolRemove( &expr::NodeValue::s_null );
}
-NodeValue* NodeManager::poolLookup(NodeValue* nv) const {
- NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
- if(find == d_nodeValuePool.end()) {
- return NULL;
- } else {
- return *find;
- }
-}
-
/**
* This class ensure that NodeManager::d_reclaiming gets set to false
* even on exceptional exit from NodeManager::reclaimZombies().
// during reclamation, reclaimZombies() is never supposed to be called
Assert(! d_reclaiming, "NodeManager::reclaimZombies() not re-entrant!");
+
+ // whether exit is normal or exceptional, the Reclaim dtor is called
+ // and ensures that d_reclaiming is set back to false.
Reclaim r(d_reclaiming);
// We copy the set away and clear the NodeManager's set of zombies.
// collect ONLY IF still zero
if(nv->d_rc == 0) {
Debug("gc") << "deleting node value " << nv
- << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+ << " [" << nv->d_id << "]: " << *nv << "\n";
// remove from the pool
if(nv->getKind() != kind::VARIABLE) {
poolRemove(nv);
}
- NVReclaim rc(d_underTheShotgun);
- d_underTheShotgun = nv;
+
+ // whether exit is normal or exceptional, the NVReclaim dtor is
+ // called and ensures that d_nodeUnderDeletion is set back to
+ // NULL.
+ NVReclaim rc(d_nodeUnderDeletion);
+ d_nodeUnderDeletion = nv;
// remove attributes
d_attrManager.deleteAllAttributes(nv);
#include <ext/hash_set>
#include "expr/kind.h"
+#include "expr/metakind.h"
#include "expr/expr.h"
#include "expr/node_value.h"
#include "context/context.h"
friend class expr::NodeValue;
typedef __gnu_cxx::hash_set<expr::NodeValue*,
- expr::NodeValueInternalHashFunction,
- expr::NodeValue::NodeValueEq> NodeValuePool;
+ expr::NodeValuePoolHashFcn,
+ expr::NodeValuePoolEq> NodeValuePool;
typedef __gnu_cxx::hash_set<expr::NodeValue*,
expr::NodeValueIDHashFunction,
- expr::NodeValue::NodeValueEq> ZombieSet;
+ expr::NodeValueEq> ZombieSet;
static __thread NodeManager* s_current;
NodeValuePool d_nodeValuePool;
expr::attr::AttributeManager d_attrManager;
- expr::NodeValue* d_underTheShotgun;
+ expr::NodeValue* d_nodeUnderDeletion;
bool d_reclaiming;
ZombieSet d_zombies;
- expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
+ inline expr::NodeValue* poolLookup(expr::NodeValue* nv) const;
void poolInsert(expr::NodeValue* nv);
- void poolRemove(expr::NodeValue* nv);
+ inline void poolRemove(expr::NodeValue* nv);
- bool isCurrentlyDeleting(const expr::NodeValue *nv) const{
- return d_underTheShotgun == nv;
+ bool isCurrentlyDeleting(const expr::NodeValue* nv) const{
+ return d_nodeUnderDeletion == nv;
}
+ Node d_operators[kind::LAST_KIND];
+
/**
* Register a NodeValue as a zombie.
*/
if(d_reclaiming) {// FIXME multithreading
// currently reclaiming zombies; just push onto the list
Debug("gc") << "zombifying node value " << nv
- << " [" << nv->d_id << "]: " << nv->toString()
+ << " [" << nv->d_id << "]: " << *nv
<< " [CURRENTLY-RECLAIMING]\n";
d_zombies.insert(nv);// FIXME multithreading
} else {
Debug("gc") << "zombifying node value " << nv
- << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+ << " [" << nv->d_id << "]: " << *nv << "\n";
d_zombies.insert(nv);// FIXME multithreading
// for now, collect eagerly. can add heuristic here later..
*/
void reclaimZombies();
-public:
-
- NodeManager(context::Context* ctxt) :
- d_attrManager(ctxt),
- d_underTheShotgun(NULL),
- d_reclaiming(false)
+ /**
+ * This template gives a mechanism to stack-allocate a NodeValue
+ * with enough space for N children (where N is a compile-time
+ * constant). You use it like this:
+ *
+ * NVStorage<4> nvStorage;
+ * NodeValue& nvStack = reinterpret_cast<NodeValue&>(nvStorage);
+ *
+ * ...and then you can use nvStack as a NodeValue that you know has
+ * room for 4 children.
+ */
+ template <size_t N>
+ struct NVStorage {
+ expr::NodeValue nv;
+ expr::NodeValue* child[N];
+ };/* struct NodeManager::NVStorage<N> */
- { // static initialization
- poolInsert( &expr::NodeValue::s_null );
- }
+public:
+ NodeManager(context::Context* ctxt);
~NodeManager();
/** The node manager in the current context. */
/** Create a variable of unknown type (?). */
Node mkVar();
+ /** Create a constant of type T */
+ template <class T>
+ Node mkConst(const T&);
+
+ /** Determine whether Nodes of a particular Kind have operators. */
+ static inline bool hasOperator(Kind mk);
+
+ /** Get the (singleton) operator of an OPERATOR-kinded kind. */
+ inline TNode operatorOf(Kind k) {
+ AssertArgument( kind::metaKindOf(k) == kind::metakind::OPERATOR, k,
+ "Kind is not an OPERATOR-kinded kind "
+ "in NodeManager::operatorOf()" );
+ return d_operators[k];
+ }
+
/** Retrieve an attribute for a node.
*
* @param nv the node value
inline typename AttrKind::value_type getAttribute(expr::NodeValue* nv,
const AttrKind& attr) const;
- /* NOTE: there are two, distinct hasAttribute() declarations for
- a reason (rather than using a pointer-valued argument with a
- default value): they permit more optimized code in the underlying
- hasAttribute() implementations. */
-
/** Check whether an attribute is set for a node.
*
* @param nv the node value
return getAttribute(n, CVC4::expr::TypeAttr());
}
+inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const {
+ NodeValuePool::const_iterator find = d_nodeValuePool.find(nv);
+ if(find == d_nodeValuePool.end()) {
+ return NULL;
+ } else {
+ return *find;
+ }
+}
+
inline void NodeManager::poolInsert(expr::NodeValue* nv) {
Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(),
"NodeValue already in the pool!");
}/* CVC4 namespace */
+#define __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
+#include "expr/metakind.h"
+#undef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP
+
#include "expr/node_builder.h"
namespace CVC4 {
// general expression-builders
+inline bool NodeManager::hasOperator(Kind k) {
+ switch(kind::MetaKind mk = kind::metaKindOf(k)) {
+
+ case kind::metakind::INVALID:
+ case kind::metakind::VARIABLE:
+ return false;
+
+ case kind::metakind::OPERATOR:
+ case kind::metakind::PARAMETERIZED:
+ return true;
+
+ case kind::metakind::CONSTANT:
+ return false;
+
+ default:
+ Unhandled(mk);
+ }
+}
+
inline Node NodeManager::mkNode(Kind kind) {
return NodeBuilder<>(this, kind);
}
return NodeBuilder<>(this, kind::VARIABLE);
}
+template <class T>
+Node NodeManager::mkConst(const T& val) {
+ // typedef typename kind::metakind::constantMap<T>::OwningTheory theory_t;
+
+ //
+ // TODO: construct a special NodeValue that points to this T but
+ // is == an inlined version (like exists in the hash_set).
+ //
+ // Something similar for (a, b) and (a, b, c) and (a, b, c, d)
+ // versions.
+ //
+ // ALSO TODO: make poolLookup() use hash_set<>::operator[] to auto-insert,
+ // and then set = value after to avoid double-hashing. fix in all places
+ // where poolLookup is called.
+ //
+ // THEN ALSO TODO: CDMap<> destruction in attribute.cpp to make valgrind
+ // happy
+ //
+ // THEN: reconsider CVC3 tracing mechanism, experiments..
+ //
+
+ NVStorage<1> nvStorage;
+ expr::NodeValue& nvStack = reinterpret_cast<expr::NodeValue&>(nvStorage);
+
+ nvStack.d_id = 0;
+ nvStack.d_kind = kind::metakind::ConstantMap<T>::kind;
+ nvStack.d_rc = 0;
+ nvStack.d_nchildren = 1;
+ nvStack.d_children[0] =
+ const_cast<expr::NodeValue*>(reinterpret_cast<const expr::NodeValue*>(&val));
+ expr::NodeValue* nv = poolLookup(&nvStack);
+
+ if(nv != NULL) {
+ return Node(nv);
+ }
+
+ nv = (expr::NodeValue*)
+ std::malloc(sizeof(expr::NodeValue) + sizeof(T));
+ if(nv == NULL) {
+ throw std::bad_alloc();
+ }
+
+ nv->d_nchildren = 0;
+ nv->d_kind = kind::metakind::ConstantMap<T>::kind;
+ nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading
+ nv->d_rc = 0;
+
+ //OwningTheory::mkConst(val);
+ new (&nv->d_children) T(val);
+
+ poolInsert(nv);
+ Debug("gc") << "creating node value " << nv
+ << " [" << nv->d_id << "]: " << *nv << "\n";
+
+ return Node(nv);
+}
+
}/* CVC4 namespace */
#endif /* __CVC4__EXPR_MANAGER_H */
#include "expr/node_value.h"
#include "expr/node.h"
+#include "expr/kind.h"
+#include "expr/metakind.h"
#include <sstream>
using namespace std;
return ss.str();
}
-void NodeValue::toStream(std::ostream& out) const {
- if(d_kind == kind::VARIABLE) {
+void NodeValue::toStream(std::ostream& out, int toDepth) const {
+ using namespace CVC4::kind;
+ using namespace CVC4;
+
+ if(getKind() == kind::NULL_EXPR) {
+ out << "null";
+ } else if(getMetaKind() == kind::metakind::VARIABLE) {
+ if(getKind() != kind::VARIABLE) {
+ out << getKind() << ':';
+ }
+
string s;
+
// conceptually "this" is const, and hasAttribute() doesn't change
// its argument, but it requires a non-const key arg (for now)
if(NodeManager::currentNM()->getAttribute(const_cast<NodeValue*>(this),
out << "var_" << d_id;
}
} else {
- out << "(" << Kind(d_kind);
- for(const_nv_iterator i = nv_begin(); i != nv_end(); ++i) {
- if(i != nv_end()) {
- out << " ";
+ out << '(' << Kind(d_kind);
+ if(getMetaKind() == kind::metakind::CONSTANT) {
+ out << ' ';
+ kind::metakind::NodeValueConstPrinter::toStream(out, this);
+ } else {
+ for(const_nv_iterator i = nv_begin(); i != nv_end(); ++i) {
+ if(i != nv_end()) {
+ out << ' ';
+ }
+ if(toDepth != 0) {
+ (*i)->toStream(out, toDepth < 0 ? toDepth : toDepth - 1);
+ } else {
+ out << "(...)";
+ }
}
- (*i)->toStream(out);
}
- out << ")";
+ out << ')';
}
}
#include "cvc4_private.h"
+// circular dependency
+#include "expr/metakind.h"
+
#ifndef __CVC4__EXPR__NODE_VALUE_H
#define __CVC4__EXPR__NODE_VALUE_H
#include "cvc4_config.h"
-#include <stdint.h>
#include "expr/kind.h"
+#include <stdint.h>
#include <string>
#include <iterator>
class MultNodeBuilder;
class NodeManager;
+namespace kind {
+ namespace metakind {
+ template < ::CVC4::Kind k, bool pool >
+ struct NodeValueConstCompare;
+
+ struct NodeValueCompare;
+ struct NodeValueConstPrinter;
+ }/* CVC4::kind::metakind namespace */
+}/* CVC4::kind namespace */
+
namespace expr {
+#if __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT + \
+ __CVC4__EXPR__NODE_VALUE__NBITS__KIND + \
+ __CVC4__EXPR__NODE_VALUE__NBITS__ID + \
+ __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN != 64
+# error NodeValue header bit assignment does not sum to 64 !
+#endif /* sum != 64 */
+
/**
* This is an NodeValue.
*/
/** A convenient null-valued expression value */
static NodeValue s_null;
+ static const unsigned NBITS_REFCOUNT = __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT;
+ static const unsigned NBITS_KIND = __CVC4__EXPR__NODE_VALUE__NBITS__KIND;
+ static const unsigned NBITS_ID = __CVC4__EXPR__NODE_VALUE__NBITS__ID;
+ static const unsigned NBITS_NCHILDREN = __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN;
+
/** Maximum reference count possible. Used for sticky
* reference-counting. Should be (1 << num_bits(d_rc)) - 1 */
- static const unsigned MAX_RC = 255;
-
- /** Number of bits assigned to the kind in the NodeValue header */
- static const unsigned KINDBITS = 8;
+ static const unsigned MAX_RC = (1u << NBITS_REFCOUNT) - 1;
/** A mask for d_kind */
- static const unsigned kindMask = (1u << KINDBITS) - 1;
+ static const unsigned kindMask = (1u << NBITS_KIND) - 1;
// this header fits into one 64-bit word
/** The ID (0 is reserved for the null value) */
- unsigned d_id : 32;
+ unsigned d_id : NBITS_ID;
/** The expression's reference count. @see cvc4::Node. */
- unsigned d_rc : 8;
+ unsigned d_rc : NBITS_REFCOUNT;
/** Kind of the expression */
- unsigned d_kind : KINDBITS;
+ unsigned d_kind : NBITS_KIND;
/** Number of children */
- unsigned d_nchildren : 16;
+ unsigned d_nchildren : NBITS_NCHILDREN;
/** Variable number of child nodes */
NodeValue* d_children[0];
// todo add exprMgr ref in debug case
- template <bool> friend class CVC4::NodeTemplate;
- template <class Builder> friend class CVC4::NodeBuilderBase;
- template <unsigned nchild_thresh> friend class CVC4::NodeBuilder;
- friend class CVC4::NodeManager;
+ template <bool> friend class ::CVC4::NodeTemplate;
+ template <class Builder> friend class ::CVC4::NodeBuilderBase;
+ template <unsigned nchild_thresh> friend class ::CVC4::NodeBuilder;
+ friend class ::CVC4::NodeManager;
+
+ template <Kind k, bool pool>
+ friend struct ::CVC4::kind::metakind::NodeValueConstCompare;
+
+ friend struct ::CVC4::kind::metakind::NodeValueCompare;
+ friend struct ::CVC4::kind::metakind::NodeValueConstPrinter;
void inc();
void dec();
public:
template <bool ref_count>
- iterator<ref_count> begin() const {
- return iterator<ref_count>(d_children);
- }
+ inline iterator<ref_count> begin() const;
template <bool ref_count>
- iterator<ref_count> end() const {
- return iterator<ref_count>(d_children + d_nchildren);
- }
+ inline iterator<ref_count> end() const;
/**
* Hash this NodeValue. For hash_maps, hash_sets, etc.. but this is
* collisions for all VARIABLEs.
* @return the hash value of this expression.
*/
- size_t internalHash() const {
+ size_t poolHash() const {
+ if(getMetaKind() == kind::metakind::CONSTANT) {
+ return kind::metakind::NodeValueCompare::constHash(this);
+ }
+
size_t hash = d_kind;
const_nv_iterator i = nv_begin();
const_nv_iterator i_end = nv_end();
return hash;
}
- inline bool compareTo(const NodeValue* nv) const {
- if(d_kind != nv->d_kind) {
- return false;
- }
-
- if(d_nchildren != nv->d_nchildren) {
- return false;
- }
-
- const_nv_iterator i = nv_begin();
- const_nv_iterator j = nv->nv_begin();
- const_nv_iterator i_end = nv_end();
-
- while(i != i_end) {
- if((*i) != (*j)) {
- return false;
- }
- ++i;
- ++j;
- }
-
- return true;
- }
-
- // Comparison predicate
- struct NodeValueEq {
- bool operator()(const NodeValue* nv1, const NodeValue* nv2) const {
- return nv1->compareTo(nv2);
- }
- };
-
unsigned getId() const { return d_id; }
Kind getKind() const { return dKindToKind(d_kind); }
- unsigned getNumChildren() const { return d_nchildren; }
+ kind::MetaKind getMetaKind() const { return kind::metaKindOf(getKind()); }
+ unsigned getNumChildren() const {
+ return (getMetaKind() == kind::metakind::PARAMETERIZED)
+ ? d_nchildren - 1
+ : d_nchildren;
+ }
std::string toString() const;
- void toStream(std::ostream& out) const;
+ void toStream(std::ostream& out, int toDepth = -1) const;
static inline unsigned kindToDKind(Kind k) {
return ((unsigned) k) & kindMask;
return s_null;
}
+ /**
+ * If this is a CONST_* Node, extract the constant from it.
+ */
+ template <class T>
+ inline const T& getConst() const;
+
+ NodeValue* getChild(int i) const;
+
};/* class NodeValue */
/**
* For hash_maps, hash_sets, etc.. but this is for expr package
* internal use only at present! This is likely to be POORLY
- * PERFORMING for other uses! NodeValue::internalHash() will lead to
+ * PERFORMING for other uses! NodeValue::poolHash() will lead to
* collisions for all VARIABLEs.
*/
-struct NodeValueInternalHashFunction {
+struct NodeValuePoolHashFcn {
inline size_t operator()(const NodeValue* nv) const {
- return (size_t) nv->internalHash();
+ return (size_t) nv->poolHash();
}
-};/* struct NodeValueInternalHashFunction */
+};/* struct NodeValuePoolHashFcn */
/**
* For hash_maps, hash_sets, etc.
inline size_t operator()(const NodeValue* nv) const {
return (size_t) nv->getId();
}
-};/* struct NodeValueHashFcn */
+};/* struct NodeValueIDHashFcn */
+
+inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv);
}/* CVC4::expr namespace */
}/* CVC4 namespace */
-#include "node_manager.h"
+#include "expr/node_manager.h"
namespace CVC4 {
namespace expr {
return d_children + d_nchildren;
}
+template <bool ref_count>
+inline NodeValue::iterator<ref_count> NodeValue::begin() const {
+ NodeValue* const* firstChild = d_children;
+ if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+ ++firstChild;
+ }
+ return iterator<ref_count>(firstChild);
+}
+
+template <bool ref_count>
+inline NodeValue::iterator<ref_count> NodeValue::end() const {
+ return iterator<ref_count>(d_children + d_nchildren);
+}
-inline bool NodeValue::isBeingDeleted() const
-{
+inline bool NodeValue::isBeingDeleted() const {
return NodeManager::currentNM() != NULL &&
NodeManager::currentNM()->isCurrentlyDeleting(this);
}
+inline NodeValue* NodeValue::getChild(int i) const {
+ if(getMetaKind() == kind::metakind::PARAMETERIZED) {
+ ++i;
+ }
+
+ Assert(i >= 0 && unsigned(i) < d_nchildren);
+ return d_children[i];
+}
+
}/* CVC4::expr namespace */
}/* CVC4 namespace */
return NodeTemplate<ref_count>(*d_i);
}
+inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
+ nv.toStream(out, Node::setdepth::getDepth(out));
+ return out;
+}
+
}/* CVC4::expr namespace */
}/* CVC4 namespace */
case OR:
return 1;
- case APPLY:
+ case APPLY_UF:
case EQUAL:
case IFF:
case IMPLIES:
return 3;
case AND:
- case APPLY:
+ case APPLY_UF:
case PLUS:
case OR:
return UINT_MAX;
LPAREN formulaList[args] RPAREN
// TODO: check arity
- { t = mkExpr(CVC4::kind::APPLY, args); }
+ { t = mkExpr(CVC4::kind::APPLY_UF, args); }
| /* if-then-else */
t = iteTerm
: /* a built-in operator application */
LPAREN kind = builtinOp annotatedFormulas[args] RPAREN
{ checkArity(kind, args.size());
- formula = mkExpr(kind,args); }
+ if((kind == kind::AND || kind == kind::OR) && args.size() == 1) {
+ formula = args[0];
+ } else {
+ formula = mkExpr(kind, args);
+ }
+ }
| /* a "distinct" expr */
/* TODO: Should there be a DISTINCT kind in the Expr package? */
LPAREN DISTINCT annotatedFormulas[args] RPAREN
- { std::vector<Expr> diseqs;
- for(unsigned i = 0; i < args.size(); ++i) {
- for(unsigned j = i+1; j < args.size(); ++j) {
- diseqs.push_back(mkExpr(CVC4::kind::NOT,
- mkExpr(CVC4::kind::EQUAL,args[i],args[j])));
- }
- }
- formula = mkExpr(CVC4::kind::AND, diseqs); }
+ { formula = mkExpr(CVC4::kind::DISTINCT, args); }
| /* An ite expression */
LPAREN (ITE | IF_THEN_ELSE)
{ args.push_back(f); }
annotatedFormulas[args] RPAREN
// TODO: check arity
- { formula = mkExpr(CVC4::kind::APPLY,args); }
+ { formula = mkExpr(CVC4::kind::APPLY_UF, args); }
| /* a variable */
{ std::string name; }
EXTRA_DIST = \
@srcdir@/theoryof_table.h \
- theoryof_table_prologue.h \
- theoryof_table_middle.h \
- theoryof_table_epilogue.h
+ theoryof_table_template.h
-@srcdir@/theoryof_table.h: @srcdir@/mktheoryof theoryof_table_prologue.h theoryof_table_middle.h theoryof_table_epilogue.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+@srcdir@/theoryof_table.h: @srcdir@/mktheoryof theoryof_table_template.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mktheoryof
$(AM_V_GEN)(@srcdir@/mktheoryof \
- @srcdir@/theoryof_table_prologue.h \
- @srcdir@/theoryof_table_middle.h \
- @srcdir@/theoryof_table_epilogue.h \
+ @srcdir@/theoryof_table_template.h \
`grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
> @srcdir@/theoryof_table.h) || (rm -f @srcdir@/theoryof_table.h && exit 1)
# src/expr/builtin_kinds.
#
-operator PLUS "arithmetic addition"
-operator MULT "arithmetic multiplication"
-operator UMINUS "arithmetic negation"
+theory ::CVC4::theory::arith::TheoryArith "theory_arith.h"
-constant CONST_RATIONAL ::CVC4::Rational "a multiple-precision rational constant"
-constant CONST_INTEGER ::CVC4::Integer "a multiple-precision integer constant"
+operator PLUS 2: "arithmetic addition"
+operator MULT 2: "arithmetic multiplication"
+operator UMINUS 1 "arithmetic negation"
+
+constant \
+ CONST_RATIONAL \
+ ::CVC4::Rational \
+ ::CVC4::RationalHashFcn \
+ "util/rational.h" \
+ "a multiple-precision rational constant"
+
+constant \
+ CONST_INTEGER \
+ ::CVC4::Integer \
+ ::CVC4::IntegerHashFcn \
+ "util/integer.h" \
+ "a multiple-precision integer constant"
+++ /dev/null
-/********************* */
-/** theory_def.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.
- **
- ** Definition for TheoryARITH (for purposes of linking to the
- ** theory-code-finding mechanisms in the parent directory).
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__ARITH__THEORY_DEF_H
-#define __CVC4__THEORY__ARITH__THEORY_DEF_H
-
-#include "theory/arith/theory_arith.h"
-
-namespace CVC4 {
- namespace theory {
- namespace arith {
- typedef TheoryArith TheoryARITH;
- }
- }
-}
-
-#endif /* __CVC4__THEORY__ARITH__THEORY_DEF_H */
# For documentation on this file format, please refer to
# src/expr/builtin_kinds.
#
+
+theory ::CVC4::theory::arrays::TheoryArrays "theory_arrays.h"
+++ /dev/null
-/********************* */
-/** theory_def.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.
- **
- ** Definition for TheoryARRAYS (for purposes of linking to the
- ** theory-code-finding mechanisms in the parent directory).
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__ARRAYS__THEORY_DEF_H
-#define __CVC4__THEORY__ARRAYS__THEORY_DEF_H
-
-#include "theory/arrays/theory_arrays.h"
-
-namespace CVC4 {
- namespace theory {
- namespace arrays {
- typedef TheoryArrays TheoryARRAYS;
- }
- }
-}
-
-#endif /* __CVC4__THEORY__ARRAYS__THEORY_DEF_H */
# src/expr/builtin_kinds.
#
-operator FALSE "falsity"
-operator TRUE "truth"
-operator NOT "logical not"
-operator AND "logical and"
-operator IFF "logical equivalence"
-operator IMPLIES "logical implication"
-operator OR "logical or"
-operator XOR "exclusive or"
+theory ::CVC4::theory::booleans::TheoryBool "theory_bool.h"
+
+operator FALSE 0 "falsity"
+operator TRUE 0 "truth"
+
+operator NOT 1 "logical not"
+operator AND 2: "logical and"
+operator IFF 2 "logical equivalence"
+operator IMPLIES 2 "logical implication"
+operator OR 2: "logical or"
+operator XOR 2: "exclusive or"
+++ /dev/null
-/********************* */
-/** theory_def.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.
- **
- ** Definition for TheoryBOOLEANS (for purposes of linking to the
- ** theory-code-finding mechanisms in the parent directory).
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__BOOLEANS__THEORY_DEF_H
-#define __CVC4__THEORY__BOOLEANS__THEORY_DEF_H
-
-#include "theory/booleans/theory_bool.h"
-
-namespace CVC4 {
- namespace theory {
- namespace booleans {
- typedef TheoryBool TheoryBOOLEANS;
- }
- }
-}
-
-#endif /* __CVC4__THEORY__BOOLEANS__THEORY_DEF_H */
# For documentation on this file format, please refer to
# src/expr/builtin_kinds.
#
+
+theory ::CVC4::theory::bv::TheoryBV "theory_bv.h"
+++ /dev/null
-/********************* */
-/** theory_def.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.
- **
- ** Definition for TheoryBV (for purposes of linking to the
- ** theory-code-finding mechanisms in the parent directory).
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__BV__THEORY_DEF_H
-#define __CVC4__THEORY__BV__THEORY_DEF_H
-
-#include "theory/bv/theory_bv.h"
-
-#endif /* __CVC4__THEORY__BV__THEORY_DEF_H */
# Output is to standard out.
#
+copyright=2010
+
cat <<EOF
/********************* -*- C++ -*- */
/** theoryof_table.h
**
- ** Copyright 2010 The AcSys Group, New York University, and as below.
+ ** Copyright $copyright The AcSys Group, New York University, and as below.
**
** This header file automatically generated by:
**
EOF
-prologue=$1; shift
-middle=$1; shift
-epilogue=$1; shift
+template=$1; shift
+
+theoryof_table_includes=
+theoryof_table_registers=
-registers=
+seen_theory=false
+seen_theory_builtin=false
-function special {
- r=$1
- comment=$2
+function theory {
+ lineno=${BASH_LINENO[0]}
- registers="$registers d_table[::CVC4::kind::$r] = th;
+ # this script doesn't care about the theory class information, but
+ # makes does make sure it's there
+ seen_theory=true
+ if [ "$1" = builtin ]; then
+ if $seen_theory_builtin; then
+ echo "$kf:$lineno: error: \"builtin\" theory redefined" >&2
+ exit 1
+ fi
+ seen_theory_builtin=true
+ elif [ -z "$1" -o -z "$2" ]; then
+ echo "$kf:$lineno: error: \"theory\" directive missing class or header argument" >&2
+ exit 1
+ elif ! expr "$1" : '\(::*\)' >/dev/null; then
+ echo "$kf:$lineno: warning: theory class \`$1' isn't fully-qualified (e.g., ::CVC4::theory::foo)" >&2
+ elif ! expr "$1" : '\(::CVC4::theory::*\)' >/dev/null; then
+ echo "$kf:$lineno: warning: theory class not under ::CVC4::theory namespace" >&2
+ fi
+
+ theoryof_table_includes="${theoryof_table_includes}#include \"theory/$b/$2\"
+"
+ theoryof_table_registers="${theoryof_table_registers}
+ /* from $b */
+ void registerTheory($1* th) {
"
}
+function variable {
+ # variable K ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ do_theoryof "$1"
+}
+
function operator {
- special "$1" "$2"
+ # operator K #children ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ do_theoryof "$1"
}
function parameterized {
- special "$1" "$2"
+ # parameterized K #children ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ do_theoryof "$1"
}
function constant {
- special "$1" "$3"
+ # constant K T Hasher header ["comment"]
+
+ lineno=${BASH_LINENO[0]}
+
+ do_theoryof "$1"
}
-cat "$prologue"
-while [ $# -gt 0 ]; do
- b=$(basename $(dirname "$1"))
- B=$(echo "$b" | tr 'a-z' 'A-Z')
- echo "#include \"theory/$b/theory_def.h\""
- registers="$registers
- /* from $b */
- void registerTheory(::CVC4::theory::$b::Theory$B* th) {
+function do_theoryof {
+ check_theory_seen
+ theoryof_table_registers="${theoryof_table_registers} d_table[::CVC4::kind::$1] = th;
"
- source "$1"
- registers="$registers }
+}
+
+function check_theory_seen {
+ if ! $seen_theory; then
+ echo "$kf:$lineno: error: no \"theory\" declaration found (it has to be first)" >&2
+ exit 1
+ fi
+}
+
+while [ $# -gt 0 ]; do
+ kf=$1
+ seen_theory=false
+ b=$(basename $(dirname "$kf"))
+ source "$kf"
+ check_theory_seen
+ theoryof_table_registers="${theoryof_table_registers} }
"
shift
done
-echo
-cat "$middle"
-echo "$registers"
-cat "$epilogue"
+
+## output
+
+text=$(cat "$template")
+for var in theoryof_table_includes theoryof_table_registers; do
+ eval text="\${text//\\\$\\{$var\\}/\${$var}}"
+done
+error=`expr "$text" : '.*\${\([^}]*\)}.*'`
+if [ -n "$error" ]; then
+ echo "$template:0: error: undefined replacement \${$error}" >&2
+ exit 1
+fi
+echo "$text"
TNode n = *workp;
+ if(n.hasOperator()) {
+ TNode c = n.getOperator();
+
+ if(! c.getAttribute(RegisteredAttr())) {
+ if(c.getNumChildren() == 0) {
+ c.setAttribute(RegisteredAttr(), true);
+ registerTerm(c);
+ } else {
+ toReg.push_back(c);
+ }
+ }
+ }
+
for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
TNode c = *i;
return getRewriteCache(in);
}
- if(in.getKind() == kind::VARIABLE ||
- in.getKind() == kind::SKOLEM) {
+ if(in.getMetaKind() == kind::metakind::VARIABLE) {
return in;
}
}
*/
+ // these special cases should go away when theory rewriting comes online
if(in.getKind() == kind::EQUAL) {
Assert(in.getNumChildren() == 2);
if(in[0] == in[1]) {
//setRewriteCache(in, out);
return out;
}
+ } else if(in.getKind() == kind::DISTINCT) {
+ vector<Node> diseqs;
+ for(TNode::iterator i = in.begin(); i != in.end(); ++i) {
+ TNode::iterator j = i;
+ while(++j != in.end()) {
+ Node eq = NodeManager::currentNM()->mkNode(CVC4::kind::EQUAL, *i, *j);
+ Node neq = NodeManager::currentNM()->mkNode(CVC4::kind::NOT, eq);
+ diseqs.push_back(neq);
+ }
+ }
+ Node out =
+ diseqs.size() == 1
+ ? diseqs[0]
+ : NodeManager::currentNM()->mkNode(CVC4::kind::AND, diseqs);
+ //setRewriteCache(in, out);
+ return out;
} else {
Node out = rewriteChildren(in);
//setRewriteCache(in, out);
for(TNode::iterator c = in.begin(); c != in.end(); ++c) {
b << rewrite(*c);
}
+ Debug("rewrite") << "rewrote-children of " << in << std::endl
+ << "got " << b << std::endl;
return Node(b);
}
Assert(k >= 0 && k < kind::LAST_KIND);
- if(k == kind::APPLY) {
- // FIXME: we don't yet have a Type-to-Theory map. When we do,
- // look up the type of the LHS and return that Theory (?)
- // k = n.getOperator().getKind();
- return &d_uf;
- //Unimplemented();
- } else if(k == kind::VARIABLE) {
+ if(k == kind::VARIABLE) {
return &d_uf;
//Unimplemented();
} else if(k == kind::EQUAL) {
+++ /dev/null
-/********************* */
-/** theoryof_table_epilogue.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.
- **
- ** The epilogue section for the automatically-generated theoryOf table.
- ** See the mktheoryof script.
- **/
-
-};/* class TheoryOfTable */
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__THEORYOF_TABLE_H */
+++ /dev/null
-/********************* */
-/** theoryof_table_middle.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.
- **
- ** The middle section for the automatically-generated theoryOf table.
- ** See the mktheoryof script.
- **/
-
-namespace CVC4 {
-namespace theory {
-
-class Theory;
-
-class TheoryOfTable {
-
- Theory** d_table;
-
-public:
-
- TheoryOfTable() :
- d_table(new Theory*[::CVC4::kind::LAST_KIND]) {
- }
-
- ~TheoryOfTable() {
- delete [] d_table;
- }
-
- Theory* operator[](TNode n) {
- Assert(n.getKind() >= 0 && n.getKind() < ::CVC4::kind::LAST_KIND,
- "illegal to inquire theoryOf(UNDEFINED_KIND or out-of-range)");
- return d_table[n.getKind()];
- }
-
- Theory* operator[](::CVC4::Kind k) {
- Assert(k >= 0 && k < ::CVC4::kind::LAST_KIND,
- "illegal to inquire theoryOf(UNDEFINED_KIND or out-of-range)");
- return d_table[k];
- }
+++ /dev/null
-/********************* */
-/** theoryof_table_prologue.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.
- **
- ** The prologue section for the automatically-generated theoryOf table.
- ** See the mktheoryof script.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__THEORYOF_TABLE_H
-#define __CVC4__THEORY__THEORYOF_TABLE_H
-
-#include "expr/kind.h"
-#include "util/Assert.h"
-
--- /dev/null
+/********************* */
+/** theoryof_table_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.
+ **
+ ** The template for the automatically-generated theoryOf table.
+ ** See the mktheoryof script.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__THEORYOF_TABLE_H
+#define __CVC4__THEORY__THEORYOF_TABLE_H
+
+#include "expr/kind.h"
+#include "util/Assert.h"
+
+${theoryof_table_includes}
+
+namespace CVC4 {
+namespace theory {
+
+class Theory;
+
+class TheoryOfTable {
+
+ Theory** d_table;
+
+public:
+
+ TheoryOfTable() :
+ d_table(new Theory*[::CVC4::kind::LAST_KIND]) {
+ }
+
+ ~TheoryOfTable() {
+ delete [] d_table;
+ }
+
+ Theory* operator[](TNode n) {
+ Assert(n.getKind() >= 0 && n.getKind() < ::CVC4::kind::LAST_KIND,
+ "illegal to inquire theoryOf(UNDEFINED_KIND or out-of-range)");
+ return d_table[n.getKind()];
+ }
+
+ Theory* operator[](::CVC4::Kind k) {
+ Assert(k >= 0 && k < ::CVC4::kind::LAST_KIND,
+ "illegal to inquire theoryOf(UNDEFINED_KIND or out-of-range)");
+ return d_table[k];
+ }
+${theoryof_table_registers}
+};/* class TheoryOfTable */
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__THEORYOF_TABLE_H */
# src/expr/builtin_kinds.
#
-parameterized APPLY "uninterpreted function application"
+theory ::CVC4::theory::uf::TheoryUF "theory_uf.h"
+
+parameterized APPLY_UF 1: "uninterpreted function application"
+++ /dev/null
-/********************* */
-/** theory_def.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.
- **
- ** Definition for TheoryUF (for purposes of linking to the
- ** theory-code-finding mechanisms in the parent directory).
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__UF__THEORY_DEF_H
-#define __CVC4__THEORY__UF__THEORY_DEF_H
-
-#include "theory/uf/theory_uf.h"
-
-#endif /* __CVC4__THEORY__UF__THEORY_DEF_H */
n.setAttribute(ECAttr(), ecN);
}
- /* If the node is an APPLY, we need to add it to the predecessor list
+ /* If the node is an APPLY_UF, we need to add it to the predecessor list
* of its children.
*/
- if(n.getKind() == APPLY){
+ if(n.getKind() == APPLY_UF){
TNode::iterator cIter = n.begin();
- //The first element of an apply is the function symbol which should not
- //have an associated ECData, so it needs to be skipped.
- ++cIter;
for(; cIter != n.end(); ++cIter){
TNode child = *cIter;
}
bool TheoryUF::equiv(TNode x, TNode y){
- Assert(x.getKind() == kind::APPLY);
- Assert(y.getKind() == kind::APPLY);
+ Assert(x.getKind() == kind::APPLY_UF);
+ Assert(y.getKind() == kind::APPLY_UF);
if(x.getNumChildren() != y.getNumChildren())
return false;
if(x.getOperator() != y.getOperator())
return false;
+ // intentionally don't look at operator
+
TNode::iterator xIter = x.begin();
TNode::iterator yIter = y.begin();
- //Skip operator of the applies
- ++xIter;
- ++yIter;
-
while(xIter != x.end()){
if(!sameCongruenceClass(*xIter, *yIter)){
NodeBuilder<> nb(kind::AND);
nb << diseq;
- for(unsigned i=0; i<d_assertions.size(); ++i)
+ for(unsigned i = 0; i < d_assertions.size(); ++i) {
nb << d_assertions[i];
+ }
- Node conflict = nb;
-
+ Assert(nb.getNumChildren() > 0);
+ Node conflict = nb.getNumChildren() == 1 ? nb[0] : nb;
Debug("uf") << "conflict constructed : " << conflict << std::endl;
#include "theory/theory.h"
#include "context/context.h"
+#include "context/cdo.h"
#include "context/cdlist.h"
#include "theory/uf/ecdata.h"
**
** A multiprecision integer constant.
**/
-#include <gmpxx.h>
-#include <string>
-
#ifndef __CVC4__INTEGER_H
#define __CVC4__INTEGER_H
+#include <gmpxx.h>
+#include <string>
+
namespace CVC4 {
/** Hashes the gmp integer primitive in a word by word fashion. */
friend class CVC4::Rational;
};/* class Integer */
-std::ostream& operator<<(std::ostream& os, const Integer& n);
+struct IntegerHashFcn {
+ static inline size_t hash(const CVC4::Integer& i) {
+ return i.hash();
+ }
+};
+std::ostream& operator<<(std::ostream& os, const Integer& n);
}/* CVC4 namespace */
-#endif /* __CVC4__RATIONAL_H */
-
+#endif /* __CVC4__INTEGER_H */
** different than the values used to construct the Rational.
**/
+#ifndef __CVC4__RATIONAL_H
+#define __CVC4__RATIONAL_H
+
#include <gmpxx.h>
#include <string>
#include "integer.h"
-#ifndef __CVC4__RATIONAL_H
-#define __CVC4__RATIONAL_H
-
namespace CVC4 {
class Rational {
};/* class Rational */
+struct RationalHashFcn {
+ static inline size_t hash(const CVC4::Rational& r) {
+ return r.hash();
+ }
+};
+
std::ostream& operator<<(std::ostream& os, const Rational& n);
}/* CVC4 namespace */
#endif /* __CVC4__RATIONAL_H */
-
expr/node_black \
expr/kind_black \
expr/node_builder_black \
+ expr/node_manager_white \
expr/attribute_white \
expr/attribute_black \
parser/parser_black \
theory/theory_uf_white \
util/assert_white \
util/configuration_white \
- util/output_white \
- util/integer_black \
- util/integer_white \
- util/rational_white
+ util/output_white
# Things that aren't tests but that tests rely on and need to
# go into the distribution
/*tests: Node& operator=(const Node&); */
void testOperatorAssign() {
Node a, b;
- Node c = d_nodeManager->mkNode(NOT);
+ Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar());
b = c;
TS_ASSERT(b==c);
void testOperatorLessThan() {
/* We don't have access to the ids so we can't test the implementation
- * in the black box tests.
- */
-
+ * in the black box tests. */
- Node a = d_nodeManager->mkVar();
- Node b = d_nodeManager->mkVar();
+ Node a = d_nodeManager->mkVar(d_nodeManager->booleanType(), "a");
+ Node b = d_nodeManager->mkVar(d_nodeManager->booleanType(), "b");
TS_ASSERT(a<b || b<a);
TS_ASSERT(!(a<b && b<a));
- Node c = d_nodeManager->mkNode(NULL_EXPR);
- Node d = d_nodeManager->mkNode(NULL_EXPR);
+ Node c = d_nodeManager->mkNode(AND, a, b);
+ Node d = d_nodeManager->mkNode(AND, a, b);
TS_ASSERT(!(c<d));
TS_ASSERT(!(d<c));
* But what would be a convincing test of this property?
*/
- //Simple test of descending descendant property
+ // simple test of descending descendant property
Node child = d_nodeManager->mkNode(TRUE);
Node parent = d_nodeManager->mkNode(NOT, child);
TS_ASSERT(child < parent);
- //Slightly less simple test of DD property.
+ // slightly less simple test of DD property
std::vector<Node> chain;
- int N = 500;
- Node curr = d_nodeManager->mkNode(NULL_EXPR);
- for(int i=0;i<N;i++) {
+ const int N = 500;
+ Node curr = d_nodeManager->mkNode(OR, a, b);
+ chain.push_back(curr);
+ for(int i = 0; i < N; ++i) {
+ curr = d_nodeManager->mkNode(AND, curr, curr);
chain.push_back(curr);
- curr = d_nodeManager->mkNode(AND, curr);
}
- for(int i=0;i<N;i++) {
- for(int j=i+1;j<N;j++) {
+ for(int i = 0; i < N; ++i) {
+ for(int j = i + 1; j < N; ++j) {
Node chain_i = chain[i];
Node chain_j = chain[j];
- TS_ASSERT(chain_i<chain_j);
+ TS_ASSERT(chain_i < chain_j);
}
}
-
}
void testEqNode() {
- /*Node eqNode(const Node& right) const;*/
+ /* Node eqNode(const Node& right) const; */
Node left = d_nodeManager->mkNode(TRUE);
- Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE)));
+ Node right = d_nodeManager->mkNode(NOT, d_nodeManager->mkNode(FALSE));
Node eq = left.eqNode(right);
-
TS_ASSERT(EQUAL == eq.getKind());
- TS_ASSERT(2 == eq.getNumChildren());
+ TS_ASSERT(2 == eq.getNumChildren());
TS_ASSERT(eq[0] == left);
TS_ASSERT(eq[1] == right);
}
void testNotNode() {
- /* Node notNode() const;*/
+ /* Node notNode() const; */
Node child = d_nodeManager->mkNode(TRUE);
Node parent = child.notNode();
void testIteNode() {
/*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/
- Node cnd = d_nodeManager->mkNode(PLUS);
+ Node a = d_nodeManager->mkVar();
+ Node b = d_nodeManager->mkVar();
+
+ Node cnd = d_nodeManager->mkNode(PLUS, a, b);
Node thenBranch = d_nodeManager->mkNode(TRUE);
- Node elseBranch = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE)));
+ Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkNode(FALSE));
Node ite = cnd.iteNode(thenBranch, elseBranch);
-
- TS_ASSERT(ITE == ite.getKind());
- TS_ASSERT(3 == ite.getNumChildren());
+ TS_ASSERT(ITE == ite.getKind());
+ TS_ASSERT(3 == ite.getNumChildren());
TS_ASSERT(*(ite.begin()) == cnd);
TS_ASSERT(*(++ite.begin()) == thenBranch);
TS_ASSERT(*(++eq.begin()) == right);
}
- void testKindSingleton(Kind k) {
- Node n = d_nodeManager->mkNode(k);
- TS_ASSERT(k == n.getKind());
- }
-
void testGetKind() {
/*inline Kind getKind() const; */
- testKindSingleton(NOT);
- testKindSingleton(NULL_EXPR);
- testKindSingleton(ITE);
- testKindSingleton(SKOLEM);
- }
+ Node a = d_nodeManager->mkVar();
+ Node b = d_nodeManager->mkVar();
+
+ Node n = d_nodeManager->mkNode(NOT, a);
+ TS_ASSERT(NOT == n.getKind());
+
+ n = d_nodeManager->mkNode(IFF, a, b);
+ TS_ASSERT(IFF == n.getKind());
+ n = d_nodeManager->mkNode(PLUS, a, b);
+ TS_ASSERT(PLUS == n.getKind());
+
+ n = d_nodeManager->mkNode(UMINUS, a);
+ TS_ASSERT(UMINUS == n.getKind());
+ }
void testGetOperator() {
Type* sort = d_nodeManager->mkSort("T");
Node f = d_nodeManager->mkVar(predType);
Node a = d_nodeManager->mkVar(booleanType);
- Node fa = d_nodeManager->mkNode(kind::APPLY, f, a);
+ Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a);
TS_ASSERT( fa.hasOperator() );
TS_ASSERT( !f.hasOperator() );
TS_ASSERT( !a.hasOperator() );
+ TS_ASSERT( fa.getNumChildren() == 1 );
+ TS_ASSERT( f.getNumChildren() == 0 );
+ TS_ASSERT( a.getNumChildren() == 0 );
+
TS_ASSERT( f == fa.getOperator() );
+#ifdef CVC4_ASSERTIONS
TS_ASSERT_THROWS( f.getOperator(), AssertionException );
TS_ASSERT_THROWS( a.getOperator(), AssertionException );
+#endif /* CVC4_ASSERTIONS */
}
- void testNaryExpForSize(Kind k, int N){
+ void testNaryExpForSize(Kind k, int N) {
NodeBuilder<> nbz(k);
- for(int i=0;i<N;i++){
- nbz << Node::null();
+ Node trueNode = d_nodeManager->mkNode(TRUE);
+ for(int i = 0; i < N; ++i) {
+ nbz << trueNode;
}
Node result = nbz;
- TS_ASSERT( N == result.getNumChildren());
+ TS_ASSERT( N == result.getNumChildren() );
}
- void testNumChildren(){
+ void testNumChildren() {
/*inline size_t getNumChildren() const;*/
+ Node trueNode = d_nodeManager->mkNode(TRUE);
+
//test 0
TS_ASSERT(0 == (Node::null()).getNumChildren());
//test 1
- TS_ASSERT(1 == (Node::null().notNode()).getNumChildren());
+ TS_ASSERT(1 == trueNode.notNode().getNumChildren());
//test 2
- TS_ASSERT(2 == (Node::null().andNode(Node::null())).getNumChildren() );
+ TS_ASSERT(2 == trueNode.andNode(trueNode).getNumChildren());
//Bigger tests
srand(0);
int trials = 500;
- for(int i=0;i<trials; i++){
- int N = rand() % 1000;
- testNaryExpForSize(NOT, N);
+ for(int i = 0; i < trials; ++i) {
+ int N = rand() % 1000 + 2;
+ testNaryExpForSize(AND, N);
}
+#ifdef CVC4_ASSERTIONS
+ TS_ASSERT_THROWS( testNaryExpForSize(AND, 0), AssertionException );
+ TS_ASSERT_THROWS( testNaryExpForSize(AND, 1), AssertionException );
+ TS_ASSERT_THROWS( testNaryExpForSize(NOT, 0), AssertionException );
+ TS_ASSERT_THROWS( testNaryExpForSize(NOT, 2), AssertionException );
+#endif /* CVC4_ASSERTIONS */
}
- void testIterator(){
+ void testIterator() {
NodeBuilder<> b;
Node x = d_nodeManager->mkVar();
Node y = d_nodeManager->mkVar();
}
}
- void testToString(){
+ void testToString() {
Type* booleanType = d_nodeManager->booleanType();
Node w = d_nodeManager->mkVar(booleanType, "w");
TS_ASSERT(n.toString() == "(AND (OR w x) y z)");
}
- void testToStream(){
+ void testToStream() {
Type* booleanType = d_nodeManager->booleanType();
Node w = d_nodeManager->mkVar(booleanType, "w");
Node z = d_nodeManager->mkVar(booleanType, "z");
Node m = NodeBuilder<>() << x << y << kind::OR;
Node n = NodeBuilder<>() << w << m << z << kind::AND;
+ Node o = NodeBuilder<>() << n << n << kind::XOR;
stringstream sstr;
n.toStream(sstr);
TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
+
+ sstr.str(string());
+ o.toStream(sstr);
+ TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
+
+ sstr.str(string());
+ sstr << n;
+ TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
+
+ sstr.str(string());
+ sstr << o;
+ TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
+
+ sstr.str(string());
+ sstr << Node::setdepth(0) << n;
+ TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
+
+ sstr.str(string());
+ sstr << Node::setdepth(0) << o;
+ TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
+
+ sstr.str(string());
+ sstr << Node::setdepth(1) << n;
+ TS_ASSERT(sstr.str() == "(AND w (OR (...) (...)) z)");
+
+ sstr.str(string());
+ sstr << Node::setdepth(1) << o;
+ TS_ASSERT(sstr.str() == "(XOR (AND (...) (...) (...)) (AND (...) (...) (...)))");
+
+ sstr.str(string());
+ sstr << Node::setdepth(2) << n;
+ TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
+
+ sstr.str(string());
+ sstr << Node::setdepth(2) << o;
+ TS_ASSERT(sstr.str() == "(XOR (AND w (OR (...) (...)) z) (AND w (OR (...) (...)) z))");
+
+ sstr.str(string());
+ sstr << Node::setdepth(3) << n;
+ TS_ASSERT(sstr.str() == "(AND w (OR x y) z)");
+
+ sstr.str(string());
+ sstr << Node::setdepth(3) << o;
+ TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
}
};
template <unsigned N>
void push_back(NodeBuilder<N>& nb, int n){
- for(int i=0; i<n; ++i){
- nb << Node::null();
+ for(int i = 0; i < n; ++i){
+ nb << d_nm->mkNode(TRUE);
}
}
Node i_0 = d_nm->mkNode(FALSE);
Node i_2 = d_nm->mkNode(TRUE);
- Node i_K = d_nm->mkNode(NOT);
-
+ Node i_K = d_nm->mkNode(NOT, i_0);
#ifdef CVC4_DEBUG
TS_ASSERT_THROWS_ANYTHING(arr[-1];);
TS_ASSERT_EQUALS(arr[0], i_0);
TS_ASSERT_EQUALS(arr[2], i_2);
- push_back(arr, K-3);
+ push_back(arr, K - 3);
TS_ASSERT_EQUALS(arr[0], i_0);
TS_ASSERT_EQUALS(arr[2], i_2);
- for(int i=3;i<K;++i) TS_ASSERT_EQUALS(arr[i], Node::null());
+ for(int i = 3; i < K; ++i) {
+ TS_ASSERT_EQUALS(arr[i], d_nm->mkNode(TRUE));
+ }
arr << i_K;
-
TS_ASSERT_EQUALS(arr[0], i_0);
TS_ASSERT_EQUALS(arr[2], i_2);
- for(int i=3;i<K;++i) TS_ASSERT_EQUALS(arr[i], Node::null());
+ for(int i = 3; i < K; ++i) {
+ TS_ASSERT_EQUALS(arr[i], d_nm->mkNode(TRUE));
+ }
TS_ASSERT_EQUALS(arr[K], i_K);
#ifdef CVC4_DEBUG
Node n = arr;
- TS_ASSERT_THROWS_ANYTHING(arr[0];);
+ TS_ASSERT_THROWS_ANYTHING(arr[0]);
#endif
}
void testStreamInsertionKind() {
/* NodeBuilder& operator<<(const Kind& k); */
-#ifdef CVC4_DEBUG
+#ifdef CVC4_ASSERTIONS
NodeBuilder<> spec(specKind);
- TS_ASSERT_THROWS_ANYTHING( spec << PLUS; );
-#endif
+ TS_ASSERT_THROWS( spec << PLUS, AssertionException );
+#endif /* CVC4_ASSERTIONS */
NodeBuilder<> noSpec;
noSpec << specKind;
TS_ASSERT_EQUALS(modified.getKind(), specKind);
NodeBuilder<> nb(specKind);
+ nb << d_nm->mkNode(TRUE) << d_nm->mkNode(FALSE);
Node n = nb;// avoid warning on clear()
nb.clear(PLUS);
-#ifdef CVC4_DEBUG
- TS_ASSERT_THROWS_ANYTHING( nb << PLUS; );
-#endif
+#ifdef CVC4_ASSERTIONS
+ TS_ASSERT_THROWS(n = nb, AssertionException);
+ nb.clear(PLUS);
+#endif /* CVC4_ASSERTIONS */
+
+#ifdef CVC4_ASSERTIONS
+ TS_ASSERT_THROWS( nb << PLUS, AssertionException );
+#endif /* CVC4_ASSERTIONS */
NodeBuilder<> testRef;
TS_ASSERT_EQUALS((testRef << specKind).getKind(), specKind);
-#ifdef CVC4_DEBUG
+#ifdef CVC4_ASSERTIONS
NodeBuilder<> testTwo;
- TS_ASSERT_THROWS_ANYTHING(testTwo << specKind << PLUS;);
-#endif
+ TS_ASSERT_THROWS(testTwo << specKind << PLUS, AssertionException);
+#endif /* CVC4_ASSERTIONS */
NodeBuilder<> testMixOrder1;
- TS_ASSERT_EQUALS((testMixOrder1<< specKind << d_nm->mkNode(TRUE)).getKind(),
+ TS_ASSERT_EQUALS((testMixOrder1 << specKind << d_nm->mkNode(TRUE)).getKind(),
specKind);
NodeBuilder<> testMixOrder2;
- TS_ASSERT_EQUALS((testMixOrder2<< d_nm->mkNode(TRUE)<<specKind).getKind(),
+ TS_ASSERT_EQUALS((testMixOrder2 << d_nm->mkNode(TRUE) << specKind).getKind(),
specKind);
}
TS_ASSERT_EQUALS(nb.getNumChildren(), K);
TS_ASSERT_DIFFERS(nb.begin(), nb.end());
-#ifdef CVC4_DEBUG
+#ifdef CVC4_ASSERTIONS
Node n = nb;
- TS_ASSERT_THROWS_ANYTHING(nb << n;);
-#endif
+ TS_ASSERT_THROWS(nb << n, AssertionException);
+#endif /* CVC4_ASSERTIONS */
NodeBuilder<> overflow(specKind);
TS_ASSERT_EQUALS(overflow.getKind(), specKind);
TS_ASSERT_EQUALS(nexplicit.getKind(), specKind);
TS_ASSERT_EQUALS(nexplicit.getNumChildren(), K);
-#ifdef CVC4_DEBUG
- TS_ASSERT_THROWS_ANYTHING(Node blah = implicit);
-#endif
+#ifdef CVC4_ASSERTIONS
+ TS_ASSERT_THROWS(Node blah = implicit, AssertionException);
+#endif /* CVC4_ASSERTIONS */
}
void testToStream() {
string astr, bstr, cstr;
stringstream astream, bstream, cstream;
- push_back(a,K/2);
- push_back(b,K/2);
- push_back(c,K/2);
+ push_back(a, K / 2);
+ push_back(b, K / 2);
a.toStream(astream);
b.toStream(bstream);
// build one-past-the-end
for(size_t j = 0; j <= n; ++j) {
- b << Node::null();
+ b << d_nm->mkNode(TRUE);
}
}
} catch(Exception e) {
--- /dev/null
+/********************* */
+/** node_manager_white.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.
+ **
+ ** White box testing of CVC4::NodeManager.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <string>
+
+#include "expr/node_manager.h"
+#include "context/context.h"
+
+#include "util/rational.h"
+#include "util/integer.h"
+
+using namespace CVC4;
+using namespace CVC4::expr;
+using namespace CVC4::context;
+
+class NodeManagerWhite : public CxxTest::TestSuite {
+
+ Context* d_ctxt;
+ NodeManager* d_nm;
+ NodeManagerScope* d_scope;
+
+public:
+
+ void setUp() {
+ d_ctxt = new Context;
+ d_nm = new NodeManager(d_ctxt);
+ d_scope = new NodeManagerScope(d_nm);
+ }
+
+ void tearDown() {
+ delete d_scope;
+ delete d_nm;
+ delete d_ctxt;
+ }
+
+ void testMkConstInt() {
+ Integer i = "3";
+ Node n = d_nm->mkConst(i);
+ Node m = d_nm->mkConst(i);
+ TS_ASSERT_EQUALS(n.getId(), m.getId());
+ }
+};
void testRegisterTerm() {
TS_ASSERT(d_dummy->doneWrapper());
- Node x = d_nm->mkVar();
- Node f = d_nm->mkVar();
- Node f_x = d_nm->mkNode(kind::APPLY, f, x);
- Node f_f_x = d_nm->mkNode(kind::APPLY, f, f_x);
+ Type* typeX = d_nm->booleanType();
+ Type* typeF = d_nm->mkFunctionType(typeX, typeX);
+
+ Node x = d_nm->mkVar(typeX, "x");
+ Node f = d_nm->mkVar(typeF, "f");
+ Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
+ Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
Node f_x_eq_x = f_x.eqNode(x);
Node x_eq_f_f_x = x.eqNode(f_f_x);
TS_ASSERT_EQUALS(got, f_x_eq_x);
- TS_ASSERT_EQUALS(4, d_dummy->d_registered.size());
+ TS_ASSERT_EQUALS(5, d_dummy->d_registered.size());
TS_ASSERT(d_dummy->d_registered.find(x) != d_dummy->d_registered.end());
TS_ASSERT(d_dummy->d_registered.find(f) != d_dummy->d_registered.end());
TS_ASSERT(d_dummy->d_registered.find(f_x) != d_dummy->d_registered.end());
TS_ASSERT(d_dummy->d_registered.find(f_x_eq_x) != d_dummy->d_registered.end());
+ TS_ASSERT(d_dummy->d_registered.find(d_nm->operatorOf(kind::EQUAL)) != d_dummy->d_registered.end());
TS_ASSERT(d_dummy->d_registered.find(f_f_x) == d_dummy->d_registered.end());
TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) == d_dummy->d_registered.end());
TS_ASSERT_EQUALS(got, x_eq_f_f_x);
- TS_ASSERT_EQUALS(6, d_dummy->d_registered.size());
+ TS_ASSERT_EQUALS(7, d_dummy->d_registered.size());
TS_ASSERT(d_dummy->d_registered.find(f_f_x) != d_dummy->d_registered.end());
TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) != d_dummy->d_registered.end());
void testPushPopChain() {
Node x = d_nm->mkVar();
Node f = d_nm->mkVar();
- Node f_x = d_nm->mkNode(kind::APPLY, f, x);
- Node f_f_x = d_nm->mkNode(kind::APPLY, f, f_x);
- Node f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_x);
- Node f_f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_f_x);
- Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_f_f_x);
+ Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
+ Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
+ Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
+ Node f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_x);
+ Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_f_x);
Node f3_x_eq_x = f_f_f_x.eqNode(x);
Node f5_x_eq_x = f_f_f_f_f_x.eqNode(x);
void testSimpleChain() {
Node x = d_nm->mkVar();
Node f = d_nm->mkVar();
- Node f_x = d_nm->mkNode(kind::APPLY, f, x);
- Node f_f_x = d_nm->mkNode(kind::APPLY, f, f_x);
- Node f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_x);
+ Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
+ Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
+ Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
Node f_f_x_eq_x = f_f_x.eqNode(x);
Node f_f_f_x_neq_f_x = (f_f_f_x.eqNode(f_x)).notNode();
void testSelfInconsistent() {
Node x = d_nm->mkVar();
Node x_neq_x = (x.eqNode(x)).notNode();
- Node and_x_neq_x = d_nm->mkNode(kind::AND, x_neq_x);
d_euf->assertFact(x_neq_x);
d_euf->check(d_level);
TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls());
- TS_ASSERT_EQUALS(and_x_neq_x, d_outputChannel.getIthNode(0));
+ TS_ASSERT_EQUALS(x_neq_x, d_outputChannel.getIthNode(0));
TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
}
void testChain() {
Node x = d_nm->mkVar();
Node f = d_nm->mkVar();
- Node f_x = d_nm->mkNode(kind::APPLY, f, x);
- Node f_f_x = d_nm->mkNode(kind::APPLY, f, f_x);
- Node f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_x);
- Node f_f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_f_x);
- Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_f_f_x);
+ Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
+ Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
+ Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
+ Node f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_x);
+ Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_f_x);
Node f3_x_eq_x = f_f_f_x.eqNode(x);
Node f5_x_eq_x = f_f_f_f_f_x.eqNode(x);
void testPushPopB() {
Node x = d_nm->mkVar();
Node f = d_nm->mkVar();
- Node f_x = d_nm->mkNode(kind::APPLY, f, x);
+ Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
Node f_x_eq_x = f_x.eqNode(x);
d_euf->assertFact( f_x_eq_x );
projects / cvc5.git / commitdiff