diff options
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 */ + |