* 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, 122 insertions, 0 deletions

diff --git a/src/context/cdo.h b/src/context/cdo.h
new file mode 100644
index 000000000..6c30a70f4
--- /dev/null
+++ b/src/context/cdo.h
@@ -0,0 +1,122 @@
+/*********************                                                        */
+/** cdo.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.
+ **
+ ** A context-dependent object.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__CDO_H
+#define __CVC4__CONTEXT__CDO_H
+
+#include "context/context.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+namespace context {
+
+/**
+ * Most basic template for context-dependent objects.  Simply makes a copy
+ * (using the copy constructor) of class T when saving, and copies it back
+ * (using operator=) during restore.
+ */
+template <class T>
+class CDO : public ContextObj {
+
+  /**
+   * The data of type T being stored in this context-dependent object.
+   */
+  T d_data;
+
+  /**
+   * Implementation of mandatory ContextObj method save: simply copies the
+   * current data to a copy using the copy constructor.  Memory is allocated
+   * using the ContextMemoryManager.
+   */
+  virtual ContextObj* save(ContextMemoryManager* pCMM) {
+    return new(pCMM) CDO<T>(*this);
+  }
+
+  /**
+   * Implementation of mandatory ContextObj method restore: simply copies the
+   * saved data back from the saved copy using operator= for T.
+   */
+  virtual void restore(ContextObj* pContextObj) {
+    d_data = ((CDO<T>*) pContextObj)->d_data;
+  }
+
+  /**
+   * Copy constructor - it's private to ensure it is only used by save().
+   * Basic CDO objects, cannot be copied-they have to be unique.
+   */
+  CDO(const CDO<T>& cdo) : ContextObj(cdo), d_data(cdo.d_data) {}
+
+  /**
+   * operator= for CDO is private to ensure CDO object is not copied.
+   */
+  CDO<T>& operator=(const CDO<T>& cdo) {}
+
+public:
+  /**
+   * Main constructor - uses default constructor for T to create the initial
+   * value of d_data.
+   */
+  CDO(Context* context) : ContextObj(context) {}
+
+  /**
+   * Constructor from object of type T.  Creates a ContextObj and sets the data
+   * to the given data value.  Note that this value is only valid in the
+   * current Scope.  If the Scope is popped, the value will revert to whatever
+   * is assigned by the default constructor for T
+   */
+  CDO(Context* context, const T& data) : ContextObj(context) {
+    makeCurrent();
+    d_data = data;
+  }
+
+  /**
+   * Destructor - no need to do anything.
+   */
+  ~CDO() throw() {}
+
+  /**
+   * Set the data in the CDO.  First call makeCurrent.
+   */
+  void set(const T& data) {
+    makeCurrent();
+    d_data = data;
+  }
+
+  /**
+   * Get the current data from the CDO.  Read-only.
+   */
+  const T& get() const { return d_data; }
+
+  /**
+   * For convenience, define operator T to be the same as get().
+   */
+  operator T() { return get(); }
+
+  /**
+   * For convenience, define operator= that takes an object of type T.
+   */
+  CDO<T>& operator=(const T& data) {
+    set(data);
+    return *this;
+  }
+
+};/* class CDO */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDO_H */