diff options
author | Tim King <taking@cs.nyu.edu> | 2012-04-24 18:36:40 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-04-24 18:36:40 +0000 |
commit | c0f5194dd56c5127c5c6dab5e59997eccc2d78a5 (patch) | |
tree | 080d465b923832f14d67da4431642609d66b921b /src/context/cdmaybe.h | |
parent | 5676b8bddcf001ba567ebb6d8e7b42dbd13ac9f3 (diff) |
This commit merges in the branch branches/arithmetic/congruence into trunk. Here are a summary of the changes:
- Adds CDMaybe and CDRaised in cdmaybe.h
- Add test for congruence over arithmetic terms and constants
- Renames DifferenceManager to CongruenceManager
- Changes a number of internal details for CongruenceManager
Diffstat (limited to 'src/context/cdmaybe.h')
-rw-r--r-- | src/context/cdmaybe.h | 65 |
1 files changed, 65 insertions, 0 deletions
diff --git a/src/context/cdmaybe.h b/src/context/cdmaybe.h new file mode 100644 index 000000000..3c95ab126 --- /dev/null +++ b/src/context/cdmaybe.h @@ -0,0 +1,65 @@ +/** + * This implements a CDMaybe. + * This has either been set in the context or it has not. + * T must have a default constructor and support assignment. + */ + +#include "cvc4_private.h" + +#pragma once + +#include "context/cdo.h" +#include "context/context.h" + +namespace CVC4 { +namespace context { + +class CDRaised { +private: + context::CDO<bool> d_flag; + +public: + CDRaised(context::Context* c) + : d_flag(c, false) + {} + + + bool isRaised() const { + return d_flag.get(); + } + + void raise(){ + Assert(!isRaised()); + d_flag.set(true); + } + +}; /* class CDRaised */ + +template <class T> +class CDMaybe { +private: + typedef std::pair<bool, T> BoolTPair; + context::CDO<BoolTPair> d_data; + +public: + CDMaybe(context::Context* c) : d_data(c, std::make_pair(false, T())) + {} + + bool isSet() const { + return d_data.get().first; + } + + void set(const T& d){ + Assert(!isSet()); + d_data.set(std::make_pair(true, d)); + } + + const T& get() const{ + Assert(isSet()); + return d_data.get().second; + } +}; /* class CDMaybe<T> */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + |