Made the OneOf example work.

This commit is contained in:
Peter Goodman
2017-12-11 19:40:39 -05:00
parent 76ff9ec5b3
commit 669f6cf3f9
2 changed files with 60 additions and 7 deletions
+10 -7
View File
@@ -24,13 +24,16 @@ TEST(OneOfExample, ProduceSixtyOrHigher) {
symbolic_int x;
ASSUME_LT(x, 3);
while(1) {
OneOf([x] {x += 1; printf ("-1\n");},
[x] {x -= 1; printf ("+1\n");},
[x] {x *= 2; printf ("*2\n");},
[x] {x = 0; printf ("=0\n");});
ASSERT_LE(x,60) << x << " is six!";
};
while (1) {
OneOf(
[&x] {x += 1; printf("-1\n");},
[&x] {x -= 1; printf("+1\n");},
[&x] {x *= 2; printf("*2\n");},
[&x] {x = 0; printf("=0\n");});
ASSERT_LE(x, 60)
<< x << " is sixty!";
};
}
int main(int argc, char *argv[]) {
+50
View File
@@ -191,11 +191,61 @@ class Symbolic<std::vector<T>> :
template <> \
class Symbolic<tname> { \
public: \
using SelfType = Symbolic<tname>; \
\
DEEPSTATE_INLINE Symbolic(void) \
: value(DeepState_ ## Tname()) {} \
\
DEEPSTATE_INLINE Symbolic(tname that) \
: value(that) {} \
\
DEEPSTATE_INLINE Symbolic(const SelfType &that) \
: value(that.value) {} \
\
DEEPSTATE_INLINE Symbolic(SelfType &&that) \
: value(std::move(that.value)) {} \
\
DEEPSTATE_INLINE operator tname (void) const { \
return value; \
} \
SelfType &operator=(const SelfType &that) = default; \
SelfType &operator=(SelfType &&that) = default; \
SelfType &operator=(tname that) { \
value = that; \
return *this; \
} \
SelfType &operator+=(tname that) { \
value += that; \
return *this; \
} \
SelfType &operator-=(tname that) { \
value -= that; \
return *this; \
} \
SelfType &operator*=(tname that) { \
value *= that; \
return *this; \
} \
SelfType &operator/=(tname that) { \
value /= that; \
return *this; \
} \
SelfType &operator>>=(tname that) { \
value >>= that; \
return *this; \
} \
SelfType &operator<<=(tname that) { \
value <<= that; \
return *this; \
} \
tname &operator++(void) { \
return ++value; \
} \
tname operator++(int) { \
auto prev_value = value; \
value++; \
return prev_value; \
} \
tname value; \
};