diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-03-30 04:59:16 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-03-30 04:59:16 +0000 |
| commit | e24352317b31bfcc9e3be53909e152cfdcd72a28 (patch) | |
| tree | 917163e1cdd3302e3ce343748861c9206789a896 | |
| parent | 3b19c6c93f12eab5ecbcb7d6c164cc9ca541313c (diff) | |
Highlights of this commit are:
* add NodeManagerWhite unit test
* change kind::APPLY to kind::APPLY_UF
* better APPLY handling: operators are no longer considered children
* more efficient pool lookup; the NodeValue doesn't have to be as fully constructed for the lookup to proceed
* extend DSL for kind declarations
+ new "theory" command declares a theory and its header. theory_def.h no longer required.
+ arity enforced on operators
+ constant mapping, hashing, equality
* CONSTANT metakinds supported (via Node::getConst<T>(), for example, Node::getConst<CVC4::Rational>() gets a Rational out of a Node (assuming it is of CONST_RATIONAL kind)
* added CONST_RATIONAL and CONST_INTEGER kinds
* builtin operators (AND, OR, PLUS, etc..) returned by Node::getOperator() are now CONSTANT metakind and are created by NodeManager
* Pretty-printing of Nodes now has a depth limit settable by a stream manipulator (e.g. "cout << Node::setdepth(5) << m << endl;" prints DAG rooted at m to a depth of 5)
* getters added to Node, TNode, NodeValue, etc., for operators and metakinds
* build-time generators for kind.h, metakind.h, and theoryof_table.h headers now have a simpler design and flag errors better, and the templates (kind_template.h etc.) are easier to understand.
* DISTINCT is now a kind, and the SMT parser now passes through DISTINCT nodes instead of blowing them up into ANDs. Until theory rewriting is online, though, DISTINCTs are directly blown up into conjunctions in TheoryEngine::rewrite().
* add gmpxx detection and inclusion
* better Asserts throughout, some documentation, cleanup
49 files changed, 1939 insertions, 813 deletions
diff --git a/configure.ac b/configure.ac index b3af2153b..985a26903 100644 --- a/configure.ac +++ b/configure.ac @@ -417,8 +417,8 @@ if test -n "$CXXTEST"; then fi # Checks for libraries. -AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])]) -AC_CHECK_LIB(gmpxx, __gmpz_init, , AC_MSG_ERROR(libgmpxx.a is not found)) +AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP (libgmp) not found, see http://gmplib.org/])]) +AC_CHECK_LIB(gmpxx, __gmpz_init, , [AC_MSG_ERROR([GNU MP C++ library (libgmpxx) not found, see http://gmplib.org/])]) # Check for antlr C++ runtime (defined in config/antlr.m4) AC_LIB_ANTLR 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 */ - diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 1d5bcc230..b80d3bea3 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -4,6 +4,7 @@ UNIT_TESTS = \ expr/node_black \ expr/kind_black \ expr/node_builder_black \ + expr/node_manager_white \ expr/attribute_white \ expr/attribute_black \ parser/parser_black \ @@ -14,10 +15,7 @@ UNIT_TESTS = \ theory/theory_uf_white \ util/assert_white \ util/configuration_white \ - util/output_white \ - util/integer_black \ - util/integer_white \ - util/rational_white + util/output_white # Things that aren't tests but that tests rely on and need to # go into the distribution diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 21c19a8f9..c92ea31f5 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -196,7 +196,7 @@ public: /*tests: Node& operator=(const Node&); */ void testOperatorAssign() { Node a, b; - Node c = d_nodeManager->mkNode(NOT); + Node c = d_nodeManager->mkNode(NOT, d_nodeManager->mkVar()); b = c; TS_ASSERT(b==c); @@ -210,18 +210,16 @@ public: void testOperatorLessThan() { /* We don't have access to the ids so we can't test the implementation - * in the black box tests. - */ - + * in the black box tests. */ - Node a = d_nodeManager->mkVar(); - Node b = d_nodeManager->mkVar(); + Node a = d_nodeManager->mkVar(d_nodeManager->booleanType(), "a"); + Node b = d_nodeManager->mkVar(d_nodeManager->booleanType(), "b"); TS_ASSERT(a<b || b<a); TS_ASSERT(!(a<b && b<a)); - Node c = d_nodeManager->mkNode(NULL_EXPR); - Node d = d_nodeManager->mkNode(NULL_EXPR); + Node c = d_nodeManager->mkNode(AND, a, b); + Node d = d_nodeManager->mkNode(AND, a, b); TS_ASSERT(!(c<d)); TS_ASSERT(!(d<c)); @@ -233,48 +231,47 @@ public: * But what would be a convincing test of this property? */ - //Simple test of descending descendant property + // simple test of descending descendant property Node child = d_nodeManager->mkNode(TRUE); Node parent = d_nodeManager->mkNode(NOT, child); TS_ASSERT(child < parent); - //Slightly less simple test of DD property. + // slightly less simple test of DD property std::vector<Node> chain; - int N = 500; - Node curr = d_nodeManager->mkNode(NULL_EXPR); - for(int i=0;i<N;i++) { + const int N = 500; + Node curr = d_nodeManager->mkNode(OR, a, b); + chain.push_back(curr); + for(int i = 0; i < N; ++i) { + curr = d_nodeManager->mkNode(AND, curr, curr); chain.push_back(curr); - curr = d_nodeManager->mkNode(AND, curr); } - for(int i=0;i<N;i++) { - for(int j=i+1;j<N;j++) { + for(int i = 0; i < N; ++i) { + for(int j = i + 1; j < N; ++j) { Node chain_i = chain[i]; Node chain_j = chain[j]; - TS_ASSERT(chain_i<chain_j); + TS_ASSERT(chain_i < chain_j); } } - } void testEqNode() { - /*Node eqNode(const Node& right) const;*/ + /* Node eqNode(const Node& right) const; */ Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, d_nodeManager->mkNode(FALSE)); Node eq = left.eqNode(right); - TS_ASSERT(EQUAL == eq.getKind()); - TS_ASSERT(2 == eq.getNumChildren()); + TS_ASSERT(2 == eq.getNumChildren()); TS_ASSERT(eq[0] == left); TS_ASSERT(eq[1] == right); } void testNotNode() { - /* Node notNode() const;*/ + /* Node notNode() const; */ Node child = d_nodeManager->mkNode(TRUE); Node parent = child.notNode(); @@ -320,14 +317,16 @@ public: void testIteNode() { /*Node iteNode(const Node& thenpart, const Node& elsepart) const;*/ - Node cnd = d_nodeManager->mkNode(PLUS); + Node a = d_nodeManager->mkVar(); + Node b = d_nodeManager->mkVar(); + + Node cnd = d_nodeManager->mkNode(PLUS, a, b); Node thenBranch = d_nodeManager->mkNode(TRUE); - Node elseBranch = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node elseBranch = d_nodeManager->mkNode(NOT, d_nodeManager->mkNode(FALSE)); Node ite = cnd.iteNode(thenBranch, elseBranch); - - TS_ASSERT(ITE == ite.getKind()); - TS_ASSERT(3 == ite.getNumChildren()); + TS_ASSERT(ITE == ite.getKind()); + TS_ASSERT(3 == ite.getNumChildren()); TS_ASSERT(*(ite.begin()) == cnd); TS_ASSERT(*(++ite.begin()) == thenBranch); @@ -378,20 +377,24 @@ public: TS_ASSERT(*(++eq.begin()) == right); } - void testKindSingleton(Kind k) { - Node n = d_nodeManager->mkNode(k); - TS_ASSERT(k == n.getKind()); - } - void testGetKind() { /*inline Kind getKind() const; */ - testKindSingleton(NOT); - testKindSingleton(NULL_EXPR); - testKindSingleton(ITE); - testKindSingleton(SKOLEM); - } + Node a = d_nodeManager->mkVar(); + Node b = d_nodeManager->mkVar(); + + Node n = d_nodeManager->mkNode(NOT, a); + TS_ASSERT(NOT == n.getKind()); + + n = d_nodeManager->mkNode(IFF, a, b); + TS_ASSERT(IFF == n.getKind()); + n = d_nodeManager->mkNode(PLUS, a, b); + TS_ASSERT(PLUS == n.getKind()); + + n = d_nodeManager->mkNode(UMINUS, a); + TS_ASSERT(UMINUS == n.getKind()); + } void testGetOperator() { Type* sort = d_nodeManager->mkSort("T"); @@ -400,50 +403,65 @@ public: Node f = d_nodeManager->mkVar(predType); Node a = d_nodeManager->mkVar(booleanType); - Node fa = d_nodeManager->mkNode(kind::APPLY, f, a); + Node fa = d_nodeManager->mkNode(kind::APPLY_UF, f, a); TS_ASSERT( fa.hasOperator() ); TS_ASSERT( !f.hasOperator() ); TS_ASSERT( !a.hasOperator() ); + TS_ASSERT( fa.getNumChildren() == 1 ); + TS_ASSERT( f.getNumChildren() == 0 ); + TS_ASSERT( a.getNumChildren() == 0 ); + TS_ASSERT( f == fa.getOperator() ); +#ifdef CVC4_ASSERTIONS TS_ASSERT_THROWS( f.getOperator(), AssertionException ); TS_ASSERT_THROWS( a.getOperator(), AssertionException ); +#endif /* CVC4_ASSERTIONS */ } - void testNaryExpForSize(Kind k, int N){ + void testNaryExpForSize(Kind k, int N) { NodeBuilder<> nbz(k); - for(int i=0;i<N;i++){ - nbz << Node::null(); + Node trueNode = d_nodeManager->mkNode(TRUE); + for(int i = 0; i < N; ++i) { + nbz << trueNode; } Node result = nbz; - TS_ASSERT( N == result.getNumChildren()); + TS_ASSERT( N == result.getNumChildren() ); } - void testNumChildren(){ + void testNumChildren() { /*inline size_t getNumChildren() const;*/ + Node trueNode = d_nodeManager->mkNode(TRUE); + //test 0 TS_ASSERT(0 == (Node::null()).getNumChildren()); //test 1 - TS_ASSERT(1 == (Node::null().notNode()).getNumChildren()); + TS_ASSERT(1 == trueNode.notNode().getNumChildren()); //test 2 - TS_ASSERT(2 == (Node::null().andNode(Node::null())).getNumChildren() ); + TS_ASSERT(2 == trueNode.andNode(trueNode).getNumChildren()); //Bigger tests srand(0); int trials = 500; - for(int i=0;i<trials; i++){ - int N = rand() % 1000; - testNaryExpForSize(NOT, N); + for(int i = 0; i < trials; ++i) { + int N = rand() % 1000 + 2; + testNaryExpForSize(AND, N); } +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS( testNaryExpForSize(AND, 0), AssertionException ); + TS_ASSERT_THROWS( testNaryExpForSize(AND, 1), AssertionException ); + TS_ASSERT_THROWS( testNaryExpForSize(NOT, 0), AssertionException ); + TS_ASSERT_THROWS( testNaryExpForSize(NOT, 2), AssertionException ); +#endif /* CVC4_ASSERTIONS */ } - void testIterator(){ + void testIterator() { NodeBuilder<> b; Node x = d_nodeManager->mkVar(); Node y = d_nodeManager->mkVar(); @@ -468,7 +486,7 @@ public: } } - void testToString(){ + void testToString() { Type* booleanType = d_nodeManager->booleanType(); Node w = d_nodeManager->mkVar(booleanType, "w"); @@ -481,7 +499,7 @@ public: TS_ASSERT(n.toString() == "(AND (OR w x) y z)"); } - void testToStream(){ + void testToStream() { Type* booleanType = d_nodeManager->booleanType(); Node w = d_nodeManager->mkVar(booleanType, "w"); @@ -490,9 +508,54 @@ public: Node z = d_nodeManager->mkVar(booleanType, "z"); Node m = NodeBuilder<>() << x << y << kind::OR; Node n = NodeBuilder<>() << w << m << z << kind::AND; + Node o = NodeBuilder<>() << n << n << kind::XOR; stringstream sstr; n.toStream(sstr); TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); + + sstr.str(string()); + o.toStream(sstr); + TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); + + sstr.str(string()); + sstr << n; + TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); + + sstr.str(string()); + sstr << o; + TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); + + sstr.str(string()); + sstr << Node::setdepth(0) << n; + TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); + + sstr.str(string()); + sstr << Node::setdepth(0) << o; + TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); + + sstr.str(string()); + sstr << Node::setdepth(1) << n; + TS_ASSERT(sstr.str() == "(AND w (OR (...) (...)) z)"); + + sstr.str(string()); + sstr << Node::setdepth(1) << o; + TS_ASSERT(sstr.str() == "(XOR (AND (...) (...) (...)) (AND (...) (...) (...)))"); + + sstr.str(string()); + sstr << Node::setdepth(2) << n; + TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); + + sstr.str(string()); + sstr << Node::setdepth(2) << o; + TS_ASSERT(sstr.str() == "(XOR (AND w (OR (...) (...)) z) (AND w (OR (...) (...)) z))"); + + sstr.str(string()); + sstr << Node::setdepth(3) << n; + TS_ASSERT(sstr.str() == "(AND w (OR x y) z)"); + + sstr.str(string()); + sstr << Node::setdepth(3) << o; + TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))"); } }; diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 46e524f59..cae2e0637 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -56,8 +56,8 @@ public: template <unsigned N> void push_back(NodeBuilder<N>& nb, int n){ - for(int i=0; i<n; ++i){ - nb << Node::null(); + for(int i = 0; i < n; ++i){ + nb << d_nm->mkNode(TRUE); } } @@ -295,8 +295,7 @@ public: Node i_0 = d_nm->mkNode(FALSE); Node i_2 = d_nm->mkNode(TRUE); - Node i_K = d_nm->mkNode(NOT); - + Node i_K = d_nm->mkNode(NOT, i_0); #ifdef CVC4_DEBUG TS_ASSERT_THROWS_ANYTHING(arr[-1];); @@ -314,23 +313,26 @@ public: TS_ASSERT_EQUALS(arr[0], i_0); TS_ASSERT_EQUALS(arr[2], i_2); - push_back(arr, K-3); + push_back(arr, K - 3); TS_ASSERT_EQUALS(arr[0], i_0); TS_ASSERT_EQUALS(arr[2], i_2); - for(int i=3;i<K;++i) TS_ASSERT_EQUALS(arr[i], Node::null()); + for(int i = 3; i < K; ++i) { + TS_ASSERT_EQUALS(arr[i], d_nm->mkNode(TRUE)); + } arr << i_K; - TS_ASSERT_EQUALS(arr[0], i_0); TS_ASSERT_EQUALS(arr[2], i_2); - for(int i=3;i<K;++i) TS_ASSERT_EQUALS(arr[i], Node::null()); + for(int i = 3; i < K; ++i) { + TS_ASSERT_EQUALS(arr[i], d_nm->mkNode(TRUE)); + } TS_ASSERT_EQUALS(arr[K], i_K); #ifdef CVC4_DEBUG Node n = arr; - TS_ASSERT_THROWS_ANYTHING(arr[0];); + TS_ASSERT_THROWS_ANYTHING(arr[0]); #endif } @@ -383,10 +385,10 @@ public: void testStreamInsertionKind() { /* NodeBuilder& operator<<(const Kind& k); */ -#ifdef CVC4_DEBUG +#ifdef CVC4_ASSERTIONS NodeBuilder<> spec(specKind); - TS_ASSERT_THROWS_ANYTHING( spec << PLUS; ); -#endif + TS_ASSERT_THROWS( spec << PLUS, AssertionException ); +#endif /* CVC4_ASSERTIONS */ NodeBuilder<> noSpec; noSpec << specKind; @@ -399,26 +401,32 @@ public: TS_ASSERT_EQUALS(modified.getKind(), specKind); NodeBuilder<> nb(specKind); + nb << d_nm->mkNode(TRUE) << d_nm->mkNode(FALSE); Node n = nb;// avoid warning on clear() nb.clear(PLUS); -#ifdef CVC4_DEBUG - TS_ASSERT_THROWS_ANYTHING( nb << PLUS; ); -#endif +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(n = nb, AssertionException); + nb.clear(PLUS); +#endif /* CVC4_ASSERTIONS */ + +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS( nb << PLUS, AssertionException ); +#endif /* CVC4_ASSERTIONS */ NodeBuilder<> testRef; TS_ASSERT_EQUALS((testRef << specKind).getKind(), specKind); -#ifdef CVC4_DEBUG +#ifdef CVC4_ASSERTIONS NodeBuilder<> testTwo; - TS_ASSERT_THROWS_ANYTHING(testTwo << specKind << PLUS;); -#endif + TS_ASSERT_THROWS(testTwo << specKind << PLUS, AssertionException); +#endif /* CVC4_ASSERTIONS */ NodeBuilder<> testMixOrder1; - TS_ASSERT_EQUALS((testMixOrder1<< specKind << d_nm->mkNode(TRUE)).getKind(), + TS_ASSERT_EQUALS((testMixOrder1 << specKind << d_nm->mkNode(TRUE)).getKind(), specKind); NodeBuilder<> testMixOrder2; - TS_ASSERT_EQUALS((testMixOrder2<< d_nm->mkNode(TRUE)<<specKind).getKind(), + TS_ASSERT_EQUALS((testMixOrder2 << d_nm->mkNode(TRUE) << specKind).getKind(), specKind); } @@ -433,10 +441,10 @@ public: TS_ASSERT_EQUALS(nb.getNumChildren(), K); TS_ASSERT_DIFFERS(nb.begin(), nb.end()); -#ifdef CVC4_DEBUG +#ifdef CVC4_ASSERTIONS Node n = nb; - TS_ASSERT_THROWS_ANYTHING(nb << n;); -#endif + TS_ASSERT_THROWS(nb << n, AssertionException); +#endif /* CVC4_ASSERTIONS */ NodeBuilder<> overflow(specKind); TS_ASSERT_EQUALS(overflow.getKind(), specKind); @@ -518,9 +526,9 @@ public: TS_ASSERT_EQUALS(nexplicit.getKind(), specKind); TS_ASSERT_EQUALS(nexplicit.getNumChildren(), K); -#ifdef CVC4_DEBUG - TS_ASSERT_THROWS_ANYTHING(Node blah = implicit); -#endif +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(Node blah = implicit, AssertionException); +#endif /* CVC4_ASSERTIONS */ } void testToStream() { @@ -535,9 +543,8 @@ public: string astr, bstr, cstr; stringstream astream, bstream, cstream; - push_back(a,K/2); - push_back(b,K/2); - push_back(c,K/2); + push_back(a, K / 2); + push_back(b, K / 2); a.toStream(astream); b.toStream(bstream); @@ -661,7 +668,7 @@ public: // build one-past-the-end for(size_t j = 0; j <= n; ++j) { - b << Node::null(); + b << d_nm->mkNode(TRUE); } } } catch(Exception e) { diff --git a/test/unit/expr/node_manager_white.h b/test/unit/expr/node_manager_white.h new file mode 100644 index 000000000..a43e32908 --- /dev/null +++ b/test/unit/expr/node_manager_white.h @@ -0,0 +1,56 @@ +/********************* */ +/** node_manager_white.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information. + ** + ** White box testing of CVC4::NodeManager. + **/ + +#include <cxxtest/TestSuite.h> + +#include <string> + +#include "expr/node_manager.h" +#include "context/context.h" + +#include "util/rational.h" +#include "util/integer.h" + +using namespace CVC4; +using namespace CVC4::expr; +using namespace CVC4::context; + +class NodeManagerWhite : public CxxTest::TestSuite { + + Context* d_ctxt; + NodeManager* d_nm; + NodeManagerScope* d_scope; + +public: + + void setUp() { + d_ctxt = new Context; + d_nm = new NodeManager(d_ctxt); + d_scope = new NodeManagerScope(d_nm); + } + + void tearDown() { + delete d_scope; + delete d_nm; + delete d_ctxt; + } + + void testMkConstInt() { + Integer i = "3"; + Node n = d_nm->mkConst(i); + Node m = d_nm->mkConst(i); + TS_ASSERT_EQUALS(n.getId(), m.getId()); + } +}; diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 908ab81fc..5941b3e5d 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -211,10 +211,13 @@ public: void testRegisterTerm() { TS_ASSERT(d_dummy->doneWrapper()); - Node x = d_nm->mkVar(); - Node f = d_nm->mkVar(); - Node f_x = d_nm->mkNode(kind::APPLY, f, x); - Node f_f_x = d_nm->mkNode(kind::APPLY, f, f_x); + Type* typeX = d_nm->booleanType(); + Type* typeF = d_nm->mkFunctionType(typeX, typeX); + + Node x = d_nm->mkVar(typeX, "x"); + Node f = d_nm->mkVar(typeF, "f"); + Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); + Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); Node f_x_eq_x = f_x.eqNode(x); Node x_eq_f_f_x = x.eqNode(f_f_x); @@ -225,11 +228,12 @@ public: TS_ASSERT_EQUALS(got, f_x_eq_x); - TS_ASSERT_EQUALS(4, d_dummy->d_registered.size()); + TS_ASSERT_EQUALS(5, d_dummy->d_registered.size()); TS_ASSERT(d_dummy->d_registered.find(x) != d_dummy->d_registered.end()); TS_ASSERT(d_dummy->d_registered.find(f) != d_dummy->d_registered.end()); TS_ASSERT(d_dummy->d_registered.find(f_x) != d_dummy->d_registered.end()); TS_ASSERT(d_dummy->d_registered.find(f_x_eq_x) != d_dummy->d_registered.end()); + TS_ASSERT(d_dummy->d_registered.find(d_nm->operatorOf(kind::EQUAL)) != d_dummy->d_registered.end()); TS_ASSERT(d_dummy->d_registered.find(f_f_x) == d_dummy->d_registered.end()); TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) == d_dummy->d_registered.end()); @@ -239,7 +243,7 @@ public: TS_ASSERT_EQUALS(got, x_eq_f_f_x); - TS_ASSERT_EQUALS(6, d_dummy->d_registered.size()); + TS_ASSERT_EQUALS(7, d_dummy->d_registered.size()); TS_ASSERT(d_dummy->d_registered.find(f_f_x) != d_dummy->d_registered.end()); TS_ASSERT(d_dummy->d_registered.find(x_eq_f_f_x) != d_dummy->d_registered.end()); diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index 6958634e6..7be68aaa1 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -118,11 +118,11 @@ public: void testPushPopChain() { Node x = d_nm->mkVar(); Node f = d_nm->mkVar(); - Node f_x = d_nm->mkNode(kind::APPLY, f, x); - Node f_f_x = d_nm->mkNode(kind::APPLY, f, f_x); - Node f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_x); - Node f_f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_f_x); - Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_f_f_x); + Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); + Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); + Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x); + Node f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_x); + Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_f_x); Node f3_x_eq_x = f_f_f_x.eqNode(x); Node f5_x_eq_x = f_f_f_f_f_x.eqNode(x); @@ -173,9 +173,9 @@ public: void testSimpleChain() { Node x = d_nm->mkVar(); Node f = d_nm->mkVar(); - Node f_x = d_nm->mkNode(kind::APPLY, f, x); - Node f_f_x = d_nm->mkNode(kind::APPLY, f, f_x); - Node f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_x); + Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); + Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); + Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x); Node f_f_x_eq_x = f_f_x.eqNode(x); Node f_f_f_x_neq_f_x = (f_f_f_x.eqNode(f_x)).notNode(); @@ -198,13 +198,12 @@ public: void testSelfInconsistent() { Node x = d_nm->mkVar(); Node x_neq_x = (x.eqNode(x)).notNode(); - Node and_x_neq_x = d_nm->mkNode(kind::AND, x_neq_x); d_euf->assertFact(x_neq_x); d_euf->check(d_level); TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); - TS_ASSERT_EQUALS(and_x_neq_x, d_outputChannel.getIthNode(0)); + TS_ASSERT_EQUALS(x_neq_x, d_outputChannel.getIthNode(0)); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); } @@ -228,11 +227,11 @@ public: void testChain() { Node x = d_nm->mkVar(); Node f = d_nm->mkVar(); - Node f_x = d_nm->mkNode(kind::APPLY, f, x); - Node f_f_x = d_nm->mkNode(kind::APPLY, f, f_x); - Node f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_x); - Node f_f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_f_x); - Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_f_f_x); + Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); + Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x); + Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x); + Node f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_x); + Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_f_x); Node f3_x_eq_x = f_f_f_x.eqNode(x); Node f5_x_eq_x = f_f_f_f_f_x.eqNode(x); @@ -270,7 +269,7 @@ public: void testPushPopB() { Node x = d_nm->mkVar(); Node f = d_nm->mkVar(); - Node f_x = d_nm->mkNode(kind::APPLY, f, x); + Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x); Node f_x_eq_x = f_x.eqNode(x); d_euf->assertFact( f_x_eq_x ); |