diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-03-05 08:26:37 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-03-05 08:26:37 +0000 |
commit | 88b52c971b43248e6ceacf1c8140a06427d0418d (patch) | |
tree | 4ee443c898a858fcdd658f3f043e4180eddd8784 /src/context/cdo.h | |
parent | 29cc307cdf2c42bebf4f5615874a864783f47fd0 (diff) |
* 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
Diffstat (limited to 'src/context/cdo.h')
-rw-r--r-- | src/context/cdo.h | 122 |
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 */ |