* public/private code untangled (smt/smt_engine.h no longer #includes

  expr/node.h).  This removes the warnings we had during compilation,
  and heads off a number of potential linking errors due to improper
  inlining of private (library-only) stuff in client (out-of-library)
  code.

* "configure" now takes some options as part of a "bare-option" build
  type (e.g., "./configure debug-coverage" or "./configure production-muzzle").

* split cdo.h, cdlist.h, cdmap.h, and cdset.h from context.h

* split cdlist_black unit test from context_black

* implement CDMap<>.

* give ExprManagers ownership of the context (and have SmtEngine share
  that one)

* fix main driver to properly report file-not-found

* fix MemoryMappedInputBuffer class to report reasons for
  "errno"-returned system errors

* src/expr/attribute.h: context-dependent attribute kinds now
  supported

* test/unit/expr/node_white.h: context-dependent attribute tests

* src/prop/cnf_conversion.h and associated parts of src/util/options.h
  and src/main/getopt.cpp: obsolete command-line option, removed.

* src/util/Assert.h: assertions are now somewhat more useful (in debug
  builds, anyway) during stack unwinding.

* test/unit/theory/theory_black.h: test context-dependent behavior of
  registerTerm() attribute for theories

* src/expr/node_builder.h: formatting, fixes for arithmetic
  convenience node builders, check memory allocations

* test/unit/expr/node_builder_black.h: add tessts for addition,
  subtraction, unary minus, and multiplication convenience node
  builders

* src/expr/attribute.h: more comments

* (various) code formatting, comment cleanup, added throws specifier
  to some destructors

* contrib/code-checker: prototype perl script to test (some) code policy

* contrib/indent-settings: command line for GNU indent to indent using
  CVC4 style (sort of; this is a work in progress)

* COPYING: legal stuff

* DESIGN_QUESTIONS: obsolete, removed

1 files changed, 35 insertions, 16 deletions

diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 523c5387b..bd74fd4d4 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -24,7 +24,7 @@
 
 #include "cvc4_config.h"
 #include <stdint.h>
-#include "kind.h"
+#include "expr/kind.h"
 
 #include <string>
 #include <iterator>
@@ -98,7 +98,7 @@ class NodeValue {
   NodeValue(int);
 
   /** Destructor decrements the ref counts of its children */
-  ~NodeValue() throw();
+  ~NodeValue();
 
   typedef NodeValue** nv_iterator;
   typedef NodeValue const* const* const_nv_iterator;
@@ -150,16 +150,19 @@ public:
   }
 
   /**
-   * Hash this expression.
+   * Hash this 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!  For example, this gives
+   * collisions for all VARIABLEs.
    * @return the hash value of this expression.
    */
-  size_t hash() const {
+  size_t internalHash() const {
     size_t hash = d_kind;
     const_nv_iterator i = nv_begin();
     const_nv_iterator i_end = nv_end();
-    while (i != i_end) {
+    while(i != i_end) {
       hash ^= (*i)->d_id + 0x9e3779b9 + (hash << 6) + (hash >> 2);
-      ++ i;
+      ++i;
     }
     return hash;
   }
@@ -209,7 +212,27 @@ public:
   static inline Kind dKindToKind(unsigned d) {
     return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d);
   }
-};
+};/* 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
+ * collisions for all VARIABLEs.
+ */
+struct NodeValueInternalHashFcn {
+  inline size_t operator()(const NodeValue* nv) const {
+    return (size_t) nv->internalHash();
+  }
+};/* struct NodeValueHashFcn */
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#include "node_manager.h"
+
+namespace CVC4 {
+namespace expr {
 
 inline NodeValue::NodeValue() :
   d_id(0),
@@ -225,7 +248,7 @@ inline NodeValue::NodeValue(int) :
   d_nchildren(0) {
 }
 
-inline NodeValue::~NodeValue() throw() {
+inline NodeValue::~NodeValue() {
   for(nv_iterator i = nv_begin(); i != nv_end(); ++i) {
     (*i)->dec();
   }
@@ -243,7 +266,10 @@ inline void NodeValue::dec() {
   if(EXPECT_TRUE( d_rc < MAX_RC )) {
     --d_rc;
     if(EXPECT_FALSE( d_rc == 0 )) {
-      // FIXME gc
+      Assert(NodeManager::currentNM() != NULL,
+             "No current NodeManager on destruction of NodeValue: "
+             "maybe a public CVC4 interface function is missing a NodeManagerScope ?");
+      NodeManager::currentNM()->gc(this);
     }
   }
 }
@@ -264,13 +290,6 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const {
   return d_children + d_nchildren;
 }
 
-// for hash_maps, hash_sets, ...
-struct NodeValueHashFcn {
-  size_t operator()(const CVC4::expr::NodeValue* nv) const {
-    return (size_t)nv->hash();
-  }
-};/* struct NodeValueHashFcn */
-
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */