diff options
Diffstat (limited to 'src')
42 files changed, 1702 insertions, 703 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 0b6dbed4b..7b34fe431 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -17,7 +17,7 @@ libexpr_la_SOURCES = \ attribute.h \ attribute.cpp \ @srcdir@/kind.h \ - node_builder.cpp \ + @srcdir@/metakind.h \ node_manager.cpp \ expr_manager.cpp \ node_value.cpp \ @@ -28,20 +28,26 @@ libexpr_la_SOURCES = \ 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 diff --git a/src/expr/builtin_kinds b/src/expr/builtin_kinds index f687e3b81..bb224aa91 100644 --- a/src/expr/builtin_kinds +++ b/src/expr/builtin_kinds @@ -2,47 +2,119 @@ # # 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" diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index 6f611cf95..5acd0736a 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -177,6 +177,7 @@ Expr BoolExpr::iteExpr(const Expr& then_e, const Expr& else_e) const { } void Expr::printAst(std::ostream & o, int indent) const { + ExprManagerScope ems(*this); getNode().printAst(o, indent); } diff --git a/src/expr/kind_epilogue.h b/src/expr/kind_epilogue.h deleted file mode 100644 index 3d029bec4..000000000 --- a/src/expr/kind_epilogue.h +++ /dev/null @@ -1,26 +0,0 @@ -/********************* */ -/** 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 */ diff --git a/src/expr/kind_prologue.h b/src/expr/kind_prologue.h deleted file mode 100644 index 32a96dcd9..000000000 --- a/src/expr/kind_prologue.h +++ /dev/null @@ -1,31 +0,0 @@ -/********************* */ -/** 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, diff --git a/src/expr/kind_middle.h b/src/expr/kind_template.h index a4ba5a92b..2b675be0f 100644 --- a/src/expr/kind_middle.h +++ b/src/expr/kind_template.h @@ -1,5 +1,5 @@ /********************* */ -/** kind_middle.h +/** kind_template.h ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -10,10 +10,23 @@ ** 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. + ** 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 */ @@ -24,6 +37,8 @@ // 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; @@ -33,3 +48,25 @@ inline std::ostream& operator<<(std::ostream& out, CVC4::Kind 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 */ diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h new file mode 100644 index 000000000..95e107313 --- /dev/null +++ b/src/expr/metakind_template.h @@ -0,0 +1,285 @@ +/********************* */ +/** metakind_template.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** Template for the metakind header. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__KIND__METAKIND_H +#define __CVC4__KIND__METAKIND_H + +#include <iostream> + +#include "expr/kind.h" +#include "util/Assert.h" + +${metakind_includes} + +namespace CVC4 { + +namespace expr { + class NodeValue; +}/* CVC4::expr namespace */ + +namespace kind { +namespace metakind { + +/** + * Static, compile-time information about types T representing CVC4 + * constants: + * + * typename ConstantMap<T>::OwningTheory + * + * The theory in charge of constructing T when constructing Nodes + * with NodeManager::mkConst(T). + * + * typename ConstantMap<T>::kind + * + * The kind to use when constructing Nodes with + * NodeManager::mkConst(T). + */ +template <class T> +struct ConstantMap; + +/** + * Static, compile-time information about kinds k and what type their + * corresponding CVC4 constants are: + * + * typename ConstantMapReverse<k>::T + * + * Constant type for kind k. + */ +template <Kind k> +struct ConstantMapReverse; + +/** + * Static, compile-time mapping from CONSTANT kinds to comparison + * functors on NodeValue*. The single element of this structure is: + * + * static bool NodeValueCompare<K, pool>::compare(NodeValue* x, NodeValue* y) + * + * Compares x and y, given that they are both K-kinded (and the + * meta-kind of K is CONSTANT). If pool == true, one of x and y + * (but not both) may be a "non-inlined" NodeValue. If pool == + * false, neither x nor y may be a "non-inlined" NodeValue. + */ +template <Kind k, bool pool> +struct NodeValueConstCompare { + inline static bool compare(const ::CVC4::expr::NodeValue* x, + const ::CVC4::expr::NodeValue* y); + inline static size_t constHash(const ::CVC4::expr::NodeValue* nv); +};/* NodeValueConstCompare<k, pool> */ + +struct NodeValueCompare { + template <bool pool> + inline static bool compare(const ::CVC4::expr::NodeValue* nv1, + const ::CVC4::expr::NodeValue* nv2); + inline static size_t constHash(const ::CVC4::expr::NodeValue* nv); +};/* struct NodeValueCompare */ + +struct NodeValueConstPrinter { + inline static void toStream(std::ostream& out, + const ::CVC4::expr::NodeValue* nv); +}; + +/** + * "metakinds" represent the "kinds" of kinds at the meta-level. + * "metakind" is an ugly name but it's not used by client code, just + * by the expr package, and the intent here is to keep it from + * polluting the kind namespace. For more documentation on what these + * mean, see src/expr/builtin_kinds. + */ +enum MetaKind_t { + INVALID = -1, /*! special node non-kinds like NULL_EXPR or LAST_KIND */ + VARIABLE, /*! special node kinds: no operator */ + OPERATOR, /*! operators that get "inlined" */ + PARAMETERIZED, /*! parameterized ops (like APPLYs) that carry extra data */ + CONSTANT /*! constants */ +};/* enum MetaKind_t */ + +}/* CVC4::kind::metakind namespace */ + +// import MetaKind into the "CVC4::kind" namespace but keep the +// individual MetaKind constants under kind::metakind:: +typedef ::CVC4::kind::metakind::MetaKind_t MetaKind; + +static inline MetaKind metaKindOf(Kind k) { + static const MetaKind metaKinds[] = { + metakind::INVALID, /* NULL_EXPR */ +${metakind_kinds} + metakind::INVALID /* LAST_KIND */ + };/* metaKinds[] */ + + return metaKinds[k]; +}/* metaKindOf(k) */ + +}/* CVC4::kind namespace */ + +namespace expr { + class NodeValue; +}/* CVC4::expr namespace */ + +namespace kind { +namespace metakind { + +/* these are #defines so their sum can be #if-checked in node_value.h */ +#define __CVC4__EXPR__NODE_VALUE__NBITS__REFCOUNT 8 +#define __CVC4__EXPR__NODE_VALUE__NBITS__KIND 8 +#define __CVC4__EXPR__NODE_VALUE__NBITS__ID 32 +#define __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN 16 + +static const unsigned MAX_CHILDREN = + (1u << __CVC4__EXPR__NODE_VALUE__NBITS__NCHILDREN) - 1; + +}/* CVC4::kind::metakind namespace */ +}/* CVC4::kind namespace */ + +namespace expr { + +// Comparison predicate +struct NodeValueEq { + inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const { + return ::CVC4::kind::metakind::NodeValueCompare::compare<false>(nv1, nv2); + } +}; + +// Comparison predicate +struct NodeValuePoolEq { + inline bool operator()(const NodeValue* nv1, const NodeValue* nv2) const { + return ::CVC4::kind::metakind::NodeValueCompare::compare<true>(nv1, nv2); + } +}; + +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ + +#include "expr/node_value.h" + +#endif /* __CVC4__KIND__METAKIND_H */ + +#ifdef __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP + +namespace CVC4 { +namespace kind { +namespace metakind { + +template <Kind k, bool pool> +inline bool NodeValueConstCompare<k, pool>::compare(const ::CVC4::expr::NodeValue* x, + const ::CVC4::expr::NodeValue* y) { + typedef typename ConstantMapReverse<k>::T T; + if(pool) { + if(x->d_nchildren == 1) { + Assert(y->d_nchildren == 0); + return compare(y, x); + return *reinterpret_cast<T*>(x->d_children[0]) == y->getConst<T>(); + } else if(y->d_nchildren == 1) { + Assert(x->d_nchildren == 0); + return x->getConst<T>() == *reinterpret_cast<T*>(y->d_children[0]); + } + } + + Assert(x->d_nchildren == 0); + Assert(y->d_nchildren == 0); + return x->getConst<T>() == y->getConst<T>(); +} + +template <Kind k, bool pool> +inline size_t NodeValueConstCompare<k, pool>::constHash(const ::CVC4::expr::NodeValue* nv) { + typedef typename ConstantMapReverse<k>::T T; + return nv->getConst<T>().hash(); +} + +${metakind_constantMaps} + +template <bool pool> +inline bool NodeValueCompare::compare(const ::CVC4::expr::NodeValue* nv1, + const ::CVC4::expr::NodeValue* nv2) { + if(nv1->d_kind != nv2->d_kind) { + return false; + } + + if(nv1->getMetaKind() == kind::metakind::CONSTANT) { + switch(nv1->d_kind) { +${metakind_compares} + default: + Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv1->d_kind)); + } + } + + if(nv1->d_nchildren != nv2->d_nchildren) { + return false; + } + + ::CVC4::expr::NodeValue::const_nv_iterator i = nv1->nv_begin(); + ::CVC4::expr::NodeValue::const_nv_iterator j = nv2->nv_begin(); + ::CVC4::expr::NodeValue::const_nv_iterator i_end = nv1->nv_end(); + + while(i != i_end) { + if((*i) != (*j)) { + return false; + } + ++i; + ++j; + } + + return true; +} + +inline size_t NodeValueCompare::constHash(const ::CVC4::expr::NodeValue* nv) { + Assert(nv->getMetaKind() == kind::metakind::CONSTANT); + + switch(nv->d_kind) { +${metakind_constHashes} + default: + Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind)); + } +} + +inline void NodeValueConstPrinter::toStream(std::ostream& out, + const ::CVC4::expr::NodeValue* nv) { + Assert(nv->getMetaKind() == kind::metakind::CONSTANT); + + switch(nv->d_kind) { +${metakind_constPrinters} + default: + Unhandled(::CVC4::expr::NodeValue::dKindToKind(nv->d_kind)); + } +} + +inline unsigned getLowerBoundForKind(::CVC4::Kind k) { + static const unsigned lbs[] = { + 0, /* NULL_EXPR */ +${metakind_lbchildren} + + 0 /* LAST_KIND */ + }; + + return lbs[k]; +} + +inline unsigned getUpperBoundForKind(::CVC4::Kind k) { + static const unsigned ubs[] = { + 0, /* NULL_EXPR */ +${metakind_ubchildren} + + 0, /* LAST_KIND */ + }; + + return ubs[k]; +} + +}/* CVC4::kind::metakind namespace */ +}/* CVC4::kind namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__NODE_MANAGER_NEEDS_CONSTANT_MAP */ diff --git a/src/expr/mkkind b/src/expr/mkkind index cffdc0caa..6d75164d1 100755 --- a/src/expr/mkkind +++ b/src/expr/mkkind @@ -5,7 +5,7 @@ # 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: # @@ -14,11 +14,13 @@ # 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: ** @@ -29,44 +31,125 @@ cat <<EOF 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" diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind new file mode 100755 index 000000000..15551d54d --- /dev/null +++ b/src/expr/mkmetakind @@ -0,0 +1,248 @@ +#!/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" diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 5c3f1b771..bf1997381 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -16,11 +16,14 @@ #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 */ diff --git a/src/expr/node.h b/src/expr/node.h index ebe06ead2..343f03a1f 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -58,6 +58,7 @@ class NodeValue; class AttributeManager; }/* CVC4::expr::attr namespace */ + class NodeSetDepth; }/* CVC4::expr namespace */ /** @@ -208,8 +209,7 @@ public: * @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)); } /** @@ -234,7 +234,7 @@ public: 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. @@ -251,12 +251,26 @@ public: } /** + * 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 * @return the value of the attribute @@ -352,11 +366,27 @@ public: * 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. * @param indent number of spaces to indent the formula by. @@ -387,7 +417,85 @@ private: } } -};/* 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. @@ -395,8 +503,8 @@ private: * @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; } @@ -418,7 +526,13 @@ struct NodeHashFunction { 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> @@ -493,17 +607,25 @@ NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) : 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"); } } @@ -513,6 +635,8 @@ NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) { 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"); } } @@ -521,11 +645,10 @@ NodeTemplate<ref_count>::~NodeTemplate() throw(AssertionException) { 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> @@ -533,6 +656,8 @@ void NodeTemplate<ref_count>::assignNodeValue(expr::NodeValue* ev) { d_nv = ev; if(ref_count) { d_nv->inc(); + } else { + Assert(d_nv->d_rc > 0, "TNode assigned to NodeValue with rc == 0"); } } @@ -548,6 +673,8 @@ operator=(const NodeTemplate& e) { 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; @@ -565,6 +692,10 @@ operator=(const NodeTemplate<!ref_count>& e) { 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; @@ -623,16 +754,24 @@ void NodeTemplate<ref_count>::printAst(std::ostream& out, int ind) const { 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 << ')'; } @@ -644,36 +783,31 @@ void NodeTemplate<ref_count>::printAst(std::ostream& out, int ind) const { */ 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); } } @@ -682,30 +816,8 @@ NodeTemplate<true> NodeTemplate<ref_count>::getOperator() const { * 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> diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp deleted file mode 100644 index a7bc5f67d..000000000 --- a/src/expr/node_builder.cpp +++ /dev/null @@ -1,14 +0,0 @@ -/********************* */ -/** 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. - ** - **/ - diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 76307a525..4df174604 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -223,6 +223,7 @@ namespace CVC4 { }/* CVC4 namespace */ #include "expr/kind.h" +#include "expr/metakind.h" #include "util/Assert.h" #include "expr/node_value.h" #include "util/output.h" @@ -407,7 +408,9 @@ protected: } 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) { @@ -459,6 +462,12 @@ public: 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"); @@ -468,8 +477,9 @@ public: /** 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)); } /** @@ -493,8 +503,10 @@ public: 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); } @@ -535,6 +547,7 @@ public: /** 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(); @@ -547,9 +560,9 @@ public: 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); @@ -587,7 +600,10 @@ public: 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) { } @@ -848,16 +864,20 @@ inline OrNodeBuilder AndNodeBuilder::operator||(const NodeTemplate<rc>& n) { 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); } @@ -872,16 +892,20 @@ inline OrNodeBuilder& OrNodeBuilder::operator||(const NodeTemplate<rc>& n) { 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); } @@ -902,22 +926,28 @@ inline MultNodeBuilder PlusNodeBuilder::operator*(const NodeTemplate<rc>& n) { 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); } @@ -928,7 +958,8 @@ inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate<rc>& n) { 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> @@ -937,97 +968,118 @@ inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate<rc>& n) { 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); } @@ -1044,13 +1096,17 @@ inline NodeTemplate<true> operator-(const NodeTemplate<rc>& a) { 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); @@ -1058,13 +1114,18 @@ inline NodeBuilderBase<Builder>::NodeBuilderBase(expr::NodeValue* buf, unsigned } 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); @@ -1082,6 +1143,8 @@ inline NodeBuilderBase<Builder>::~NodeBuilderBase() { 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() )) { @@ -1184,9 +1247,9 @@ NodeBuilderBase<Builder>::operator Node() { // 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. */ @@ -1206,7 +1269,7 @@ NodeBuilderBase<Builder>::operator Node() { // 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(); @@ -1215,6 +1278,22 @@ NodeBuilderBase<Builder>::operator Node() { 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 @@ -1225,8 +1304,9 @@ NodeBuilderBase<Builder>::operator Node() { ** 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. */ @@ -1239,9 +1319,7 @@ NodeBuilderBase<Builder>::operator Node() { 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. */ @@ -1257,7 +1335,7 @@ NodeBuilderBase<Builder>::operator Node() { * 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) { @@ -1275,9 +1353,10 @@ NodeBuilderBase<Builder>::operator Node() { 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 { @@ -1285,13 +1364,13 @@ NodeBuilderBase<Builder>::operator Node() { ** 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 @@ -1300,9 +1379,7 @@ NodeBuilderBase<Builder>::operator Node() { 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. */ @@ -1315,14 +1392,16 @@ NodeBuilderBase<Builder>::operator Node() { * 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); } } @@ -1339,10 +1418,11 @@ NodeBuilderBase<Builder>::operator Node() const { // 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: " @@ -1360,14 +1440,30 @@ NodeBuilderBase<Builder>::operator Node() const { // 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 @@ -1378,8 +1474,9 @@ NodeBuilderBase<Builder>::operator Node() const { ** 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. */ @@ -1387,9 +1484,7 @@ NodeBuilderBase<Builder>::operator Node() const { * 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. */ @@ -1404,7 +1499,7 @@ NodeBuilderBase<Builder>::operator Node() const { * 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) { @@ -1425,9 +1520,10 @@ NodeBuilderBase<Builder>::operator Node() const { (*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 { @@ -1435,19 +1531,17 @@ NodeBuilderBase<Builder>::operator Node() const { ** 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. */ @@ -1459,7 +1553,7 @@ NodeBuilderBase<Builder>::operator Node() const { * 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) { @@ -1480,9 +1574,10 @@ NodeBuilderBase<Builder>::operator Node() const { (*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); } } @@ -1516,7 +1611,7 @@ void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) { 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; } diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index ee370f682..29749ee5d 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -25,8 +25,31 @@ namespace CVC4 { __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(); } @@ -34,15 +57,6 @@ NodeManager::~NodeManager() { 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(). @@ -81,6 +95,9 @@ void 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. @@ -111,14 +128,18 @@ void NodeManager::reclaimZombies() { // 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); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5e6d431b6..6e24cce74 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -27,6 +27,7 @@ #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" @@ -55,30 +56,32 @@ class NodeManager { 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. */ @@ -87,12 +90,12 @@ class NodeManager { 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.. @@ -105,17 +108,26 @@ class NodeManager { */ 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. */ @@ -154,6 +166,21 @@ public: /** 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 @@ -165,11 +192,6 @@ public: 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 @@ -422,6 +444,15 @@ inline Type* NodeManager::getType(TNode n) const { 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!"); @@ -436,12 +467,35 @@ inline void NodeManager::poolRemove(expr::NodeValue* nv) { }/* 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); } @@ -489,6 +543,63 @@ inline Node NodeManager::mkVar() { 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 */ diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index 840f41143..0138aa2a5 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -19,6 +19,8 @@ #include "expr/node_value.h" #include "expr/node.h" +#include "expr/kind.h" +#include "expr/metakind.h" #include <sstream> using namespace std; @@ -36,9 +38,19 @@ string NodeValue::toString() const { 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), @@ -48,14 +60,23 @@ void NodeValue::toStream(std::ostream& out) const { 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 << ')'; } } diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 995a63180..7dd90913f 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -19,12 +19,15 @@ #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> @@ -40,8 +43,25 @@ class PlusNodeBuilder; 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. */ @@ -50,39 +70,47 @@ class 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(); @@ -146,14 +174,10 @@ private: 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 @@ -162,7 +186,11 @@ public: * 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(); @@ -173,43 +201,17 @@ public: 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; @@ -223,19 +225,27 @@ public: 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. @@ -244,12 +254,14 @@ struct NodeValueIDHashFunction { 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 { @@ -306,13 +318,34 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const { 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 */ @@ -326,6 +359,11 @@ inline CVC4::NodeTemplate<ref_count> NodeValue::iterator<ref_count>::operator*() 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 */ diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index d20e59db3..98fde0556 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -241,7 +241,7 @@ unsigned int AntlrParser::minArity(Kind kind) { case OR: return 1; - case APPLY: + case APPLY_UF: case EQUAL: case IFF: case IMPLIES: @@ -278,7 +278,7 @@ unsigned int AntlrParser::maxArity(Kind kind) { return 3; case AND: - case APPLY: + case APPLY_UF: case PLUS: case OR: return UINT_MAX; diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 55ae0ff73..acf0394d0 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -323,7 +323,7 @@ term returns [CVC4::Expr t] 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 diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index 4f93caa87..b876e1649 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -126,19 +126,17 @@ annotatedFormula returns [CVC4::Expr formula] : /* 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) @@ -164,7 +162,7 @@ annotatedFormula returns [CVC4::Expr formula] { 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; } diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index d387cf7a9..32ea1d2be 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -21,16 +21,12 @@ libtheory_la_LIBADD = \ 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) diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index f6540b9da..2f2c77d36 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -4,9 +4,22 @@ # 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" diff --git a/src/theory/arith/theory_def.h b/src/theory/arith/theory_def.h deleted file mode 100644 index da4239724..000000000 --- a/src/theory/arith/theory_def.h +++ /dev/null @@ -1,32 +0,0 @@ -/********************* */ -/** 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 */ diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 63bff7ec9..f27a49e4b 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -3,3 +3,5 @@ # For documentation on this file format, please refer to # src/expr/builtin_kinds. # + +theory ::CVC4::theory::arrays::TheoryArrays "theory_arrays.h" diff --git a/src/theory/arrays/theory_def.h b/src/theory/arrays/theory_def.h deleted file mode 100644 index 68eec69e8..000000000 --- a/src/theory/arrays/theory_def.h +++ /dev/null @@ -1,32 +0,0 @@ -/********************* */ -/** 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 */ diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index f70876ac5..12869aad0 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -4,11 +4,14 @@ # 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" diff --git a/src/theory/booleans/theory_def.h b/src/theory/booleans/theory_def.h deleted file mode 100644 index 626431593..000000000 --- a/src/theory/booleans/theory_def.h +++ /dev/null @@ -1,32 +0,0 @@ -/********************* */ -/** 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 */ diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index 63bff7ec9..dc2ad4d35 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -3,3 +3,5 @@ # For documentation on this file format, please refer to # src/expr/builtin_kinds. # + +theory ::CVC4::theory::bv::TheoryBV "theory_bv.h" diff --git a/src/theory/bv/theory_def.h b/src/theory/bv/theory_def.h deleted file mode 100644 index e16adb94a..000000000 --- a/src/theory/bv/theory_def.h +++ /dev/null @@ -1,24 +0,0 @@ -/********************* */ -/** 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 */ diff --git a/src/theory/mktheoryof b/src/theory/mktheoryof index b80985c47..ef967342b 100755 --- a/src/theory/mktheoryof +++ b/src/theory/mktheoryof @@ -14,11 +14,13 @@ # 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: ** @@ -29,47 +31,108 @@ cat <<EOF 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" diff --git a/src/theory/theory.h b/src/theory/theory.h index f77e6cdf1..42bdaf2dd 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -383,6 +383,19 @@ Node TheoryImpl<T>::get() { 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; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 2323a305b..f953f97b9 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -90,8 +90,7 @@ Node TheoryEngine::rewrite(TNode in) { return getRewriteCache(in); } - if(in.getKind() == kind::VARIABLE || - in.getKind() == kind::SKOLEM) { + if(in.getMetaKind() == kind::metakind::VARIABLE) { return in; } @@ -108,6 +107,7 @@ Node TheoryEngine::rewrite(TNode 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]) { @@ -115,6 +115,22 @@ Node TheoryEngine::rewrite(TNode in) { //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); diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 15c80434f..b8c2d5a75 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -133,6 +133,8 @@ class TheoryEngine { 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); } @@ -205,13 +207,7 @@ public: 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) { diff --git a/src/theory/theoryof_table_epilogue.h b/src/theory/theoryof_table_epilogue.h deleted file mode 100644 index 11f75183a..000000000 --- a/src/theory/theoryof_table_epilogue.h +++ /dev/null @@ -1,22 +0,0 @@ -/********************* */ -/** 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 */ diff --git a/src/theory/theoryof_table_prologue.h b/src/theory/theoryof_table_prologue.h deleted file mode 100644 index 6e83d6d2c..000000000 --- a/src/theory/theoryof_table_prologue.h +++ /dev/null @@ -1,24 +0,0 @@ -/********************* */ -/** 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" - diff --git a/src/theory/theoryof_table_middle.h b/src/theory/theoryof_table_template.h index 54be78b95..465c4ee6d 100644 --- a/src/theory/theoryof_table_middle.h +++ b/src/theory/theoryof_table_template.h @@ -1,5 +1,5 @@ /********************* */ -/** theoryof_table_middle.h +/** theoryof_table_template.h ** Original author: mdeters ** Major contributors: none ** Minor contributors (to current version): none @@ -10,10 +10,20 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** The middle section for the automatically-generated theoryOf table. + ** 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 { @@ -44,3 +54,10 @@ public: "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 */ diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 9280141ea..8cbf975f2 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -4,4 +4,6 @@ # src/expr/builtin_kinds. # -parameterized APPLY "uninterpreted function application" +theory ::CVC4::theory::uf::TheoryUF "theory_uf.h" + +parameterized APPLY_UF 1: "uninterpreted function application" diff --git a/src/theory/uf/theory_def.h b/src/theory/uf/theory_def.h deleted file mode 100644 index b5cdda4ec..000000000 --- a/src/theory/uf/theory_def.h +++ /dev/null @@ -1,24 +0,0 @@ -/********************* */ -/** 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 */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index cd477a910..4f15cca75 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -107,15 +107,12 @@ void TheoryUF::registerTerm(TNode n){ 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; @@ -148,8 +145,8 @@ bool TheoryUF::sameCongruenceClass(TNode x, TNode y){ } 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; @@ -157,13 +154,11 @@ bool TheoryUF::equiv(TNode x, TNode y){ 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)){ @@ -258,11 +253,12 @@ Node TheoryUF::constructConflict(TNode diseq){ 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; diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 9e57311b5..87c33e958 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -30,6 +30,7 @@ #include "theory/theory.h" #include "context/context.h" +#include "context/cdo.h" #include "context/cdlist.h" #include "theory/uf/ecdata.h" diff --git a/src/util/integer.h b/src/util/integer.h index 1ac8eab78..c86e836c7 100644 --- a/src/util/integer.h +++ b/src/util/integer.h @@ -12,13 +12,13 @@ ** ** 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. */ @@ -148,10 +148,14 @@ public: 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 */ diff --git a/src/util/rational.h b/src/util/rational.h index b22f44a2c..fdd125587 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -19,13 +19,13 @@ ** 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 { @@ -181,9 +181,14 @@ public: };/* 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 */ - |