1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Tim King |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* A context-dependent "maybe" template type |
13 |
|
* |
14 |
|
* This implements a CDMaybe. |
15 |
|
* This has either been set in the context or it has not. |
16 |
|
* Template parameter T must have a default constructor and support |
17 |
|
* assignment. |
18 |
|
*/ |
19 |
|
|
20 |
|
#include "cvc5_private.h" |
21 |
|
|
22 |
|
#pragma once |
23 |
|
|
24 |
|
#include "context/cdo.h" |
25 |
|
#include "context/context.h" |
26 |
|
|
27 |
|
namespace cvc5 { |
28 |
|
namespace context { |
29 |
|
|
30 |
9910 |
class CDRaised { |
31 |
|
private: |
32 |
|
context::CDO<bool> d_flag; |
33 |
|
|
34 |
|
public: |
35 |
9913 |
CDRaised(context::Context* c) |
36 |
9913 |
: d_flag(c, false) |
37 |
9913 |
{} |
38 |
|
|
39 |
|
|
40 |
900907 |
bool isRaised() const { |
41 |
900907 |
return d_flag.get(); |
42 |
|
} |
43 |
|
|
44 |
2103 |
void raise(){ |
45 |
2103 |
Assert(!isRaised()); |
46 |
2103 |
d_flag.set(true); |
47 |
2103 |
} |
48 |
|
|
49 |
|
};/* class CDRaised */ |
50 |
|
|
51 |
|
template <class T> |
52 |
9910 |
class CDMaybe { |
53 |
|
private: |
54 |
|
typedef std::pair<bool, T> BoolTPair; |
55 |
|
context::CDO<BoolTPair> d_data; |
56 |
|
|
57 |
|
public: |
58 |
19826 |
CDMaybe(context::Context* c) : d_data(c, std::make_pair(false, T())) |
59 |
9913 |
{} |
60 |
|
|
61 |
964396 |
bool isSet() const { |
62 |
964396 |
return d_data.get().first; |
63 |
|
} |
64 |
|
|
65 |
1618 |
void set(const T& d){ |
66 |
1618 |
Assert(!isSet()); |
67 |
3236 |
d_data.set(std::make_pair(true, d)); |
68 |
1618 |
} |
69 |
|
|
70 |
1618 |
const T& get() const{ |
71 |
1618 |
Assert(isSet()); |
72 |
1618 |
return d_data.get().second; |
73 |
|
} |
74 |
|
};/* class CDMaybe<T> */ |
75 |
|
|
76 |
|
} // namespace context |
77 |
|
} // namespace cvc5 |