diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /src/context/cdo.h | |
parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) |
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Diffstat (limited to 'src/context/cdo.h')
-rw-r--r-- | src/context/cdo.h | 45 |
1 files changed, 28 insertions, 17 deletions
diff --git a/src/context/cdo.h b/src/context/cdo.h index f4c4a7e29..025e8e337 100644 --- a/src/context/cdo.h +++ b/src/context/cdo.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): barrett ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -40,13 +40,29 @@ class CDO : public ContextObj { */ T d_data; +protected: + + /** + * 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) CVC4_UNUSED; + /** * 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); + Debug("context") << "save cdo " << this << " (value " << get() << ")"; + ContextObj* p = new(pCMM) CDO<T>(*this); + Debug("context") << " to " << p << std::endl; + return p; } /** @@ -54,20 +70,11 @@ class CDO : public ContextObj { * saved data back from the saved copy using operator= for T. */ virtual void restore(ContextObj* pContextObj) { + //Debug("context") << "restore cdo " << this << " from " << get(); d_data = ((CDO<T>*) pContextObj)->d_data; + //Debug("context") << " to " << get() << std::endl; } - /** - * 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: /** @@ -75,7 +82,8 @@ public: * value of d_data. */ CDO(Context* context) : - ContextObj(context) { + ContextObj(context), + d_data(T()) { } /** @@ -90,7 +98,8 @@ public: * allocating contextual objects with non-standard allocators." */ CDO(bool allocatedInCMM, Context* context) : - ContextObj(allocatedInCMM, context) { + ContextObj(allocatedInCMM, context), + d_data(T()) { } /** @@ -100,7 +109,8 @@ public: * is assigned by the default constructor for T */ CDO(Context* context, const T& data) : - ContextObj(context) { + ContextObj(context), + d_data(T()) { makeCurrent(); d_data = data; } @@ -119,7 +129,8 @@ public: * allocating contextual objects with non-standard allocators." */ CDO(bool allocatedInCMM, Context* context, const T& data) : - ContextObj(allocatedInCMM, context) { + ContextObj(allocatedInCMM, context), + d_data(T()) { makeCurrent(); d_data = data; } |