From 669f6cf3f912517650c548b42afc57f08cab7294 Mon Sep 17 00:00:00 2001 From: Peter Goodman Date: Mon, 11 Dec 2017 19:40:39 -0500 Subject: [PATCH] Made the OneOf example work. --- examples/OneOf.cpp | 17 ++++++---- src/include/deepstate/DeepState.hpp | 50 +++++++++++++++++++++++++++++ 2 files changed, 60 insertions(+), 7 deletions(-) diff --git a/examples/OneOf.cpp b/examples/OneOf.cpp index 6886452..968efc8 100644 --- a/examples/OneOf.cpp +++ b/examples/OneOf.cpp @@ -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[]) { diff --git a/src/include/deepstate/DeepState.hpp b/src/include/deepstate/DeepState.hpp index 3df4b41..251dc05 100644 --- a/src/include/deepstate/DeepState.hpp +++ b/src/include/deepstate/DeepState.hpp @@ -191,11 +191,61 @@ class Symbolic> : template <> \ class Symbolic { \ public: \ + using SelfType = Symbolic; \ + \ 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; \ };