diff options
| -rw-r--r-- | config.h.in | 111 | ||||
| -rw-r--r-- | config/cvc4.m4 | 3 | ||||
| -rw-r--r-- | configure.ac | 56 | ||||
| -rw-r--r-- | src/expr/attribute.h | 54 | ||||
| -rw-r--r-- | src/expr/node.cpp | 44 | ||||
| -rw-r--r-- | src/expr/node.h | 21 | ||||
| -rw-r--r-- | src/prop/cnf_stream.h | 8 | ||||
| -rw-r--r-- | src/theory/output_channel.h | 16 | ||||
| -rw-r--r-- | src/theory/theory.h | 10 |
9 files changed, 164 insertions, 159 deletions
diff --git a/config.h.in b/config.h.in new file mode 100644 index 000000000..798fd63fa --- /dev/null +++ b/config.h.in @@ -0,0 +1,111 @@ +/* config.h.in. Generated from configure.ac by autoheader. */ + +/* Major component of the version of CVC4. */ +#undef CVC4_MAJOR + +/* Minor component of the version of CVC4. */ +#undef CVC4_MINOR + +/* Release component of the version of CVC4. */ +#undef CVC4_RELEASE + +/* Full release string for CVC4. */ +#undef CVC4_RELEASE_STRING + +/* Define to 1 if you have the <dlfcn.h> header file. */ +#undef HAVE_DLFCN_H + +/* Define to 1 if you have the <getopt.h> header file. */ +#undef HAVE_GETOPT_H + +/* Define to 1 if you have the <inttypes.h> header file. */ +#undef HAVE_INTTYPES_H + +/* Define to 1 if you have the `gmp' library (-lgmp). */ +#undef HAVE_LIBGMP + +/* Define to 1 if you have the <memory.h> header file. */ +#undef HAVE_MEMORY_H + +/* Define to 1 if stdbool.h conforms to C99. */ +#undef HAVE_STDBOOL_H + +/* Define to 1 if you have the <stdint.h> header file. */ +#undef HAVE_STDINT_H + +/* Define to 1 if you have the <stdlib.h> header file. */ +#undef HAVE_STDLIB_H + +/* Define to 1 if you have the <strings.h> header file. */ +#undef HAVE_STRINGS_H + +/* Define to 1 if you have the <string.h> header file. */ +#undef HAVE_STRING_H + +/* Define to 1 if you have the <sys/stat.h> header file. */ +#undef HAVE_SYS_STAT_H + +/* Define to 1 if you have the <sys/types.h> header file. */ +#undef HAVE_SYS_TYPES_H + +/* Define to 1 if you have the <unistd.h> header file. */ +#undef HAVE_UNISTD_H + +/* Define to 1 if the system has the type `_Bool'. */ +#undef HAVE__BOOL + +/* Define to the sub-directory in which libtool stores uninstalled libraries. + */ +#undef LT_OBJDIR + +/* Name of package */ +#undef PACKAGE + +/* Define to the address where bug reports for this package should be sent. */ +#undef PACKAGE_BUGREPORT + +/* Define to the full name of this package. */ +#undef PACKAGE_NAME + +/* Define to the full name and version of this package. */ +#undef PACKAGE_STRING + +/* Define to the one symbol short name of this package. */ +#undef PACKAGE_TARNAME + +/* Define to the home page for this package. */ +#undef PACKAGE_URL + +/* Define to the version of this package. */ +#undef PACKAGE_VERSION + +/* Define to 1 if you have the ANSI C header files. */ +#undef STDC_HEADERS + +/* Version number of package */ +#undef VERSION + +/* Define for Solaris 2.5.1 so the uint32_t typedef from <sys/synch.h>, + <pthread.h>, or <semaphore.h> is not used. If the typedef were allowed, the + #define below would cause a syntax error. */ +#undef _UINT32_T + +/* Define for Solaris 2.5.1 so the uint64_t typedef from <sys/synch.h>, + <pthread.h>, or <semaphore.h> is not used. If the typedef were allowed, the + #define below would cause a syntax error. */ +#undef _UINT64_T + +/* Define to `unsigned int' if <sys/types.h> does not define. */ +#undef size_t + +/* Define to the type of an unsigned integer type of width exactly 16 bits if + such a type exists and the standard includes do not define it. */ +#undef uint16_t + +/* Define to the type of an unsigned integer type of width exactly 32 bits if + such a type exists and the standard includes do not define it. */ +#undef uint32_t + +/* Define to the type of an unsigned integer type of width exactly 64 bits if + such a type exists and the standard includes do not define it. */ +#undef uint64_t diff --git a/config/cvc4.m4 b/config/cvc4.m4 index 1cde462b5..42dfaead5 100644 --- a/config/cvc4.m4 +++ b/config/cvc4.m4 @@ -18,8 +18,7 @@ for ac_option do case $ac_option in -*|*=*) ;; - production|debug|default|competition) - ac_cvc4_build_profile_set=yes + *) ac_cvc4_build_profile_set=yes AC_MSG_NOTICE([CVC4: building profile $ac_option]) ac_option="--with-build=$ac_option" ;; esac diff --git a/configure.ac b/configure.ac index 8c1141b9d..36f6d6c16 100644 --- a/configure.ac +++ b/configure.ac @@ -4,7 +4,7 @@ dnl Preprocess CL args. Defined in config/cvc4.m4 CVC4_AC_INIT -AC_PREREQ(2.61) +AC_PREREQ(2.64) AC_INIT AC_CONFIG_SRCDIR([src/include/cvc4_config.h]) AC_CONFIG_AUX_DIR([config]) @@ -30,7 +30,7 @@ CVC4_RELEASE_STRING=prerelease # # For more information, see: # http://www.gnu.org/software/libtool/manual/libtool.html#Versioning -# For guidance on when to change the version number, refer to the +# For guidance on when to change the version number, refer to the # developer's guide. CVC4_LIBRARY_VERSION=$CVC4_MAJOR:$CVC4_MINOR:$CVC4_RELEASE @@ -195,24 +195,10 @@ case "$with_build" in ;; esac -# permit a static binary -AC_MSG_CHECKING([whether to build a static binary]) -AC_ARG_ENABLE([static-binary], - [AS_HELP_STRING([--enable-static-binary], - [build a statically-linked binary [default=no]])]) -if test -z "${enable_static_binary+set}"; then - enable_static_binary=no -fi -AC_MSG_RESULT([$enable_static_binary]) -if test "${enable_static_binary}" = yes -a "${enable_static}" != yes; then - enable_static=yes - AC_MSG_WARN([forcing static-library building, --enable-static-binary given]) -fi - AC_MSG_CHECKING([whether to optimize libcvc4]) AC_ARG_ENABLE([optimized], - [AS_HELP_STRING([--enable-optimized], + [AS_HELP_STRING([--enable-optimized], [optimize the build])]) if test -z "${enable_optimized+set}"; then @@ -227,8 +213,8 @@ fi AC_MSG_CHECKING([whether to include debugging symbols in libcvc4]) -AC_ARG_ENABLE([debug-symbols], - [AS_HELP_STRING([--disable-debug-symbols], +AC_ARG_ENABLE([debug-symbols], + [AS_HELP_STRING([--disable-debug-symbols], [do not include debug symbols in libcvc4])]) if test -z "${enable_debug_symbols+set}"; then @@ -243,8 +229,8 @@ fi AC_MSG_CHECKING([whether to include assertions in build]) -AC_ARG_ENABLE([assertions], - [AS_HELP_STRING([--disable-assertions], +AC_ARG_ENABLE([assertions], + [AS_HELP_STRING([--disable-assertions], [turn off assertions in build])]) if test -z "${enable_assertions+set}"; then @@ -258,8 +244,8 @@ if test "$enable_assertions" = yes; then fi AC_MSG_CHECKING([whether to do a traceable build of CVC4]) -AC_ARG_ENABLE([tracing], - [AS_HELP_STRING([--disable-tracing], +AC_ARG_ENABLE([tracing], + [AS_HELP_STRING([--disable-tracing], [remove all tracing code from CVC4])]) if test -z "${enable_tracing+set}"; then @@ -273,8 +259,8 @@ if test "$enable_tracing" = yes; then fi AC_MSG_CHECKING([whether to do a muzzled build of CVC4]) -AC_ARG_ENABLE([muzzle], - [AS_HELP_STRING([--enable-muzzle], +AC_ARG_ENABLE([muzzle], + [AS_HELP_STRING([--enable-muzzle], [completely silence CVC4; remove ALL non-result output from build])]) if test -z "${enable_muzzle+set}"; then @@ -288,8 +274,8 @@ if test "$enable_muzzle" = yes; then fi AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4]) -AC_ARG_ENABLE([coverage], - [AS_HELP_STRING([--enable-coverage], +AC_ARG_ENABLE([coverage], + [AS_HELP_STRING([--enable-coverage], [build with support for gcov coverage testing])]) if test -z "${enable_coverage+set}"; then @@ -305,8 +291,8 @@ fi AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4]) -AC_ARG_ENABLE([profiling], - [AS_HELP_STRING([--enable-profiling], +AC_ARG_ENABLE([profiling], + [AS_HELP_STRING([--enable-profiling], [build with support for gprof profiling])]) if test -z "${enable_profiling+set}"; then @@ -339,11 +325,9 @@ DX_PS_FEATURE(OFF) DX_DOT_FEATURE(OFF) DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc) -AC_ARG_VAR(CXXTEST, [path to CxxTest installation]) - AC_SUBST([CXXTEST]) -AC_ARG_WITH([cxxtest-dir], +AC_ARG_WITH([cxxtest-dir], [AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])], [CXXTEST="$withval"]) @@ -405,7 +389,7 @@ AC_LIB_ANTLR AC_CHECK_HEADERS([getopt.h unistd.h]) # Checks for typedefs, structures, and compiler characteristics. -#AC_HEADER_STDBOOL +AC_HEADER_STDBOOL AC_TYPE_UINT16_T AC_TYPE_UINT32_T AC_TYPE_UINT64_T @@ -423,7 +407,7 @@ if test "$enable_shared" = yes; then BUILDING_SHARED=1; fi if test "$enable_static" = yes; then BUILDING_STATIC=1; fi AC_SUBST(BUILDING_SHARED) AC_SUBST(BUILDING_STATIC) -AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes]) +AM_CONDITIONAL([STATIC_BINARY], [test "$enable_shared" != yes -a "$enable_static" = yes]) AC_SUBST(CVC4_LIBRARY_VERSION) AC_SUBST(CVC4_PARSER_LIBRARY_VERSION) @@ -494,10 +478,6 @@ gcov support : $enable_coverage gprof support: $enable_profiling unit tests : $support_unit_tests -static libs : $enable_static -shared libs : $enable_shared -static binary: $enable_static_binary - CPPFLAGS : $CPPFLAGS CXXFLAGS : $CXXFLAGS LDFLAGS : $LDFLAGS diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 1d2705240..12de9eb5f 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -56,7 +56,7 @@ namespace expr { struct AttrHashFcn { enum { LARGE_PRIME = 1 }; - std::size_t operator()(const std::pair<uint64_t, SoftNode>& p) const { + std::size_t operator()(const std::pair<unsigned, SoftNode>& p) const { return p.first * LARGE_PRIME + p.second.hash(); } }; @@ -122,7 +122,7 @@ struct KindTableMapping { // use a TAG to indicate which table it should be in template <class value_type> -struct AttrHash : public __gnu_cxx::hash_map<std::pair<uint64_t, SoftNode>, value_type, AttrHashFcn> {}; +struct AttrHash : public __gnu_cxx::hash_map<std::pair<unsigned, SoftNode>, value_type, AttrHashFcn> {}; template <> class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> { @@ -215,23 +215,19 @@ class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHas public: - typedef std::pair<uint64_t, SoftNode> key_type; + typedef std::pair<unsigned, SoftNode> key_type; typedef bool data_type; typedef std::pair<const key_type, data_type> value_type; typedef BitIterator iterator; typedef ConstBitIterator const_iterator; - BitIterator find(const std::pair<uint64_t, SoftNode>& k) { + BitIterator find(const std::pair<unsigned, SoftNode>& k) { super::iterator i = super::find(k.second); if(i == super::end()) { return BitIterator(); } - Debug.printf("boolattr", - "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", - &(*i).second, - (unsigned long long)((*i).second), - unsigned(k.first)); + Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first); return BitIterator(*i, k.first); } @@ -239,16 +235,12 @@ public: return BitIterator(); } - ConstBitIterator find(const std::pair<uint64_t, SoftNode>& k) const { + ConstBitIterator find(const std::pair<unsigned, SoftNode>& k) const { super::const_iterator i = super::find(k.second); if(i == super::end()) { return ConstBitIterator(); } - Debug.printf("boolattr", - "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", - &(*i).second, - (unsigned long long)((*i).second), - unsigned(k.first)); + Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first); return ConstBitIterator(*i, k.first); } @@ -256,7 +248,7 @@ public: return ConstBitIterator(); } - BitAccessor operator[](const std::pair<uint64_t, SoftNode>& k) { + BitAccessor operator[](const std::pair<unsigned, SoftNode>& k) { uint64_t& word = super::operator[](k.second); return BitAccessor(word, k.first); } @@ -276,18 +268,18 @@ struct Attribute { /** cleanup routine when the Node goes away */ static inline void cleanup(const value_t&) {} - static inline uint64_t getId() { return s_id; } - static inline uint64_t getHashValue() { return s_hashValue; } + static inline unsigned getId() { return s_id; } + static inline unsigned getHashValue() { return s_hashValue; } static const bool has_default_value = false; private: /** an id */ - static const uint64_t s_id; + static const unsigned s_id; /** an extra hash value (to avoid same-value-type collisions) */ - static const uint64_t s_hashValue; + static const unsigned s_hashValue; }; /** @@ -302,13 +294,13 @@ struct Attribute<T, bool> { /** cleanup routine when the Node goes away */ static inline void cleanup(const bool&) {} - static inline uint64_t getId() { return s_id; } - static inline uint64_t getHashValue() { return s_hashValue; } + static inline unsigned getId() { return s_id; } + static inline unsigned getHashValue() { return s_hashValue; } static const bool has_default_value = true; static const bool default_value = false; - static inline uint64_t checkID(uint64_t id) { + static inline unsigned checkID(unsigned id) { AlwaysAssert(id <= 63, "Too many boolean node attributes registered during initialization !"); return id; @@ -317,10 +309,10 @@ struct Attribute<T, bool> { private: /** a bit assignment */ - static const uint64_t s_id; + static const unsigned s_id; /** an extra hash value (to avoid same-value-type collisions) */ - static const uint64_t s_hashValue; + static const unsigned s_hashValue; }; // SPECIFIC, GLOBAL ATTRIBUTE DEFINITIONS ====================================== @@ -331,11 +323,11 @@ namespace attr { template <class T> struct LastAttributeId { - static uint64_t s_id; + static unsigned s_id; }; template <class T> - uint64_t LastAttributeId<T>::s_id = 0; + unsigned LastAttributeId<T>::s_id = 0; }/* CVC4::expr::attr namespace */ typedef Attribute<attr::VarName, std::string> VarNameAttr; @@ -344,16 +336,16 @@ typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr; // ATTRIBUTE IDENTIFIER ASSIGNMENT ============================================= template <class T, class value_t> -const uint64_t Attribute<T, value_t>::s_id = +const unsigned Attribute<T, value_t>::s_id = attr::LastAttributeId<typename KindValueToTableValueMapping<value_t>::table_value_type>::s_id++; template <class T, class value_t> -const uint64_t Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id; +const unsigned Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id; template <class T> -const uint64_t Attribute<T, bool>::s_id = +const unsigned Attribute<T, bool>::s_id = Attribute<T, bool>::checkID(attr::LastAttributeId<bool>::s_id++); template <class T> -const uint64_t Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id; +const unsigned Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id; class AttributeManager; diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 79490d58e..644570b24 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -97,83 +97,51 @@ Node& Node::operator=(const Node& e) { } Node Node::eqExpr(const Node& right) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - return NodeManager::currentNM()->mkNode(EQUAL, *this, right); } Node Node::notExpr() const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - return NodeManager::currentNM()->mkNode(NOT, *this); } Node Node::andExpr(const Node& right) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - return NodeManager::currentNM()->mkNode(AND, *this, right); } Node Node::orExpr(const Node& right) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - return NodeManager::currentNM()->mkNode(OR, *this, right); } Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart); } Node Node::iffExpr(const Node& right) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - return NodeManager::currentNM()->mkNode(IFF, *this, right); } Node Node::impExpr(const Node& right) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - return NodeManager::currentNM()->mkNode(IMPLIES, *this, right); } Node Node::xorExpr(const Node& right) const { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - return NodeManager::currentNM()->mkNode(XOR, *this, right); } -static void indent(ostream & o, int indent) { - for(int i=0; i < indent; i++) { +static void indent(ostream & o, int indent){ + for(int i=0; i < indent; i++) o << ' '; - } } void Node::printAst(ostream & o, int ind) const { indent(o, ind); o << '('; o << getKind(); - if(getKind() == VARIABLE) { + if(getKind() == VARIABLE){ o << ' ' << getId(); - } else if(getNumChildren() >= 1) { - for(Node::iterator child = begin(); child != end(); ++child) { + + }else if(getNumChildren() >= 1){ + for(Node::iterator child = begin(); child != end(); ++child){ o << endl; (*child).printAst(o, ind + 1); } diff --git a/src/expr/node.h b/src/expr/node.h index a39dc5b7e..463ff8144 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -48,6 +48,7 @@ using CVC4::expr::NodeValue; class Node { friend class NodeValue; + friend class SoftNode; /** A convenient null-valued encapsulated pointer */ static Node s_null; @@ -105,7 +106,7 @@ public: bool operator!=(const Node& e) const { return d_ev != e.d_ev; } Node operator[](int i) const { - Assert(i >= 0 && unsigned(i) < d_ev->d_nchildren); + Assert(i >= 0 && i < d_ev->d_nchildren); return Node(d_ev->d_children[i]); } @@ -129,11 +130,9 @@ public: Node impExpr(const Node& right) const; Node xorExpr(const Node& right) const; - /* Node plusExpr(const Node& right) const; Node uMinusExpr() const; Node multExpr(const Node& right) const; - */ inline Kind getKind() const; @@ -172,9 +171,9 @@ public: * @param indent number of spaces to indent the formula by. */ void printAst(std::ostream & o, int indent = 0) const; - + private: - + /** * Pretty printer for use within gdb * This is not intended to be used outside of gdb. @@ -263,30 +262,18 @@ inline size_t Node::getNumChildren() const { template <class AttrKind> inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - return NodeManager::currentNM()->getAttribute(*this, AttrKind()); } template <class AttrKind> inline bool Node::hasAttribute(const AttrKind&, typename AttrKind::value_type* ret) { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret); } template <class AttrKind> inline void Node::setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { - Assert( NodeManager::currentNM() != NULL, - "There is no current CVC4::NodeManager associated to this thread.\n" - "Perhaps a public-facing function is missing a NodeManagerScope ?" ); - NodeManager::currentNM()->setAttribute(*this, AttrKind(), value); } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index d7bb3c265..1bb71860c 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -116,14 +116,6 @@ public: CnfStream(SatSolver* satSolver); /** - * Destructs a CnfStream. This implementation does nothing, but we - * need a virtual destructor for safety in case subclasses have a - * destructor. - */ - virtual ~CnfStream() { - } - - /** * Converts and asserts a formula. * @param node node to convert and assert * @param whether the sat solver can choose to remove this clause diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index c530434f5..cec499a13 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -28,14 +28,6 @@ class OutputChannel { public: /** - * Destructs an OutputChannel. This implementation does nothing, - * but we need a virtual destructor for safety in case subclasses - * have a destructor. - */ - virtual ~OutputChannel() { - } - - /** * With safePoint(), the theory signals that it is at a safe point * and can be interrupted. */ @@ -76,14 +68,6 @@ class ExplainOutputChannel { public: /** - * Destructs an ExplainOutputChannel. This implementation does - * nothing, but we need a virtual destructor for safety in case - * subclasses have a destructor. - */ - virtual ~ExplainOutputChannel() { - } - - /** * With safePoint(), the theory signals that it is at a safe point * and can be interrupted. The default implementation never * interrupts. diff --git a/src/theory/theory.h b/src/theory/theory.h index dffc99053..8b83f71cf 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -58,20 +58,12 @@ public: static bool fullEffort(Effort e) { return e >= FULL_EFFORT; } /** - * Construct a Theory. + * Construct a theory. */ Theory() { } /** - * Destructs a Theory. This implementation does nothing, but we - * need a virtual destructor for safety in case subclasses have a - * destructor. - */ - virtual ~Theory() { - } - - /** * Prepare for a Node. * * When get() is called to get the next thing off the theory queue, |