diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-09-09 17:25:10 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2021-09-09 17:25:10 -0700 |
| commit | 5fbc99c94d65b7e3fc0212e9f1e49ae8907643fe (patch) | |
| tree | bbbc618a8d5294a20fe55845904a09cf09a069e6 /src | |
| parent | e6634f01004b01278dedcd39e20b233c8da95e3e (diff) | |
update
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/check.h | 17 | ||||
| -rw-r--r-- | src/include/cvc5_public.h | 17 | ||||
| -rw-r--r-- | src/theory/theory.h | 5 |
3 files changed, 17 insertions, 22 deletions
diff --git a/src/base/check.h b/src/base/check.h index 91b492c45..916d6a6a1 100644 --- a/src/base/check.h +++ b/src/base/check.h @@ -39,23 +39,6 @@ #include "base/exception.h" #include "cvc5_export.h" -// Define CVC5_PREDICT_FALSE(x) that helps the compiler predict that x will be -// false (if there is compiler support). -#ifdef __has_builtin -#if __has_builtin(__builtin_expect) -#define CVC5_PREDICT_FALSE(x) (__builtin_expect(x, false)) -#define CVC5_PREDICT_TRUE(x) (__builtin_expect(x, true)) -#else -#define CVC5_PREDICT_FALSE(x) x -#define CVC5_PREDICT_TRUE(x) x -#endif -#else -#define CVC5_PREDICT_FALSE(x) x -#define CVC5_PREDICT_TRUE(x) x -#endif - -#define CVC5_FALLTHROUGH [[fallthrough]] - namespace cvc5 { // Implementation notes: diff --git a/src/include/cvc5_public.h b/src/include/cvc5_public.h index 4109c013f..7b43739ae 100644 --- a/src/include/cvc5_public.h +++ b/src/include/cvc5_public.h @@ -20,6 +20,23 @@ #include <stddef.h> #include <stdint.h> +// Define CVC5_PREDICT_FALSE(x) that helps the compiler predict that x will be +// false (if there is compiler support). +#ifdef __has_builtin +#if __has_builtin(__builtin_expect) +#define CVC5_PREDICT_FALSE(x) (__builtin_expect(x, false)) +#define CVC5_PREDICT_TRUE(x) (__builtin_expect(x, true)) +#else +#define CVC5_PREDICT_FALSE(x) x +#define CVC5_PREDICT_TRUE(x) x +#endif +#else +#define CVC5_PREDICT_FALSE(x) x +#define CVC5_PREDICT_TRUE(x) x +#endif + +#define CVC5_FALLTHROUGH [[fallthrough]] + // CVC5_UNUSED is to mark something (e.g. local variable, function) // as being _possibly_ unused, so that the compiler generates no // warning about it. This might be the case for e.g. a variable diff --git a/src/theory/theory.h b/src/theory/theory.h index b49d838b4..ccda5fa77 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -440,11 +440,6 @@ class Theory : protected EnvObj EFFORT_LAST_CALL = 200 }; /* enum Effort */ - static bool standardEffortOrMore(Effort e) { return e >= EFFORT_STANDARD; } - static bool standardEffortOnly(Effort e) - { - return e >= EFFORT_STANDARD && e < EFFORT_FULL; - } static bool fullEffort(Effort e) { return e == EFFORT_FULL; } /** |