summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/check.h24
-rw-r--r--src/base/output.h8
-rw-r--r--src/include/cvc5_public.h34
-rw-r--r--src/preprocessing/util/ite_utilities.cpp2
-rw-r--r--src/smt_util/boolean_simplification.h5
-rw-r--r--src/theory/booleans/circuit_propagator.h2
-rw-r--r--src/theory/quantifiers/term_tuple_enumerator.cpp4
-rw-r--r--src/theory/theory.h13
-rw-r--r--src/theory/theory_engine.cpp2
-rw-r--r--src/theory/valuation.h2
-rw-r--r--test/unit/theory/theory_white.cpp6
11 files changed, 33 insertions, 69 deletions
diff --git a/src/base/check.h b/src/base/check.h
index ac12e2acb..916d6a6a1 100644
--- a/src/base/check.h
+++ b/src/base/check.h
@@ -39,30 +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
-
-#ifdef __has_cpp_attribute
-#if __has_cpp_attribute(fallthrough)
-#define CVC5_FALLTHROUGH [[fallthrough]]
-#endif // __has_cpp_attribute(fallthrough)
-#endif // __has_cpp_attribute
-#ifndef CVC5_FALLTHROUGH
-#define CVC5_FALLTHROUGH
-#endif
-
namespace cvc5 {
// Implementation notes:
diff --git a/src/base/output.h b/src/base/output.h
index c0dbb3d7c..cc6bfb316 100644
--- a/src/base/output.h
+++ b/src/base/output.h
@@ -469,10 +469,10 @@ extern DumpOutC DumpOutChannel CVC5_EXPORT;
// just parenthesize it e.g. !(Debug("foo").isOn())
class __cvc5_true
{
- void operator!() CVC5_UNUSED;
- void operator~() CVC5_UNUSED;
- void operator-() CVC5_UNUSED;
- void operator+() CVC5_UNUSED;
+ CVC5_UNUSED void operator!();
+ CVC5_UNUSED void operator~();
+ CVC5_UNUSED void operator-();
+ CVC5_UNUSED void operator+();
public:
inline operator bool() { return true; }
diff --git a/src/include/cvc5_public.h b/src/include/cvc5_public.h
index ede5f5223..7b43739ae 100644
--- a/src/include/cvc5_public.h
+++ b/src/include/cvc5_public.h
@@ -20,23 +20,29 @@
#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
// only used in DEBUG builds.
-
-#ifdef __GNUC__
-#define CVC5_UNUSED __attribute__((__unused__))
-#define CVC5_NORETURN __attribute__((__noreturn__))
-#define CVC5_CONST_FUNCTION __attribute__((__const__))
-#define CVC5_PURE_FUNCTION __attribute__((__pure__))
-#define CVC5_WARN_UNUSED_RESULT __attribute__((__warn_unused_result__))
-#else /* ! __GNUC__ */
-#define CVC5_UNUSED
-#define CVC5_NORETURN
-#define CVC5_CONST_FUNCTION
-#define CVC5_PURE_FUNCTION
-#define CVC5_WARN_UNUSED_RESULT
-#endif /* __GNUC__ */
+#define CVC5_UNUSED [[maybe_unused]]
+#define CVC5_NORETURN [[noreturn]]
+#define CVC5_WARN_UNUSED_RESULT [[nodiscard]]
#endif /* CVC5_PUBLIC_H */
diff --git a/src/preprocessing/util/ite_utilities.cpp b/src/preprocessing/util/ite_utilities.cpp
index 9f59ad397..63f09d553 100644
--- a/src/preprocessing/util/ite_utilities.cpp
+++ b/src/preprocessing/util/ite_utilities.cpp
@@ -1456,7 +1456,7 @@ uint32_t countReachable(TNode x, Kind k)
Node ITESimplifier::simpITEAtom(TNode atom)
{
- static int CVC5_UNUSED instance = 0;
+ CVC5_UNUSED static int instance = 0;
Debug("ite::atom") << "still simplifying " << (++instance) << endl;
Node attempt = transformAtom(atom);
Debug("ite::atom") << " finished " << instance << endl;
diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h
index a2cabb3a9..39324844e 100644
--- a/src/smt_util/boolean_simplification.h
+++ b/src/smt_util/boolean_simplification.h
@@ -36,9 +36,8 @@ class BooleanSimplification {
BooleanSimplification() = delete;
BooleanSimplification(const BooleanSimplification&) = delete;
- static bool push_back_associative_commute_recursive(
- Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)
- CVC5_WARN_UNUSED_RESULT;
+ CVC5_WARN_UNUSED_RESULT static bool push_back_associative_commute_recursive(
+ Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode);
public:
/**
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index d01ec081e..feef06a90 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -99,7 +99,7 @@ class CircuitPropagator
* @return a trust node encapsulating the proof for a conflict as a lemma that
* proves false, or the null trust node otherwise
*/
- TrustNode propagate() CVC5_WARN_UNUSED_RESULT;
+ CVC5_WARN_UNUSED_RESULT TrustNode propagate();
/**
* Get the back edges of this circuit.
diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp
index b75ebe288..f505d2774 100644
--- a/src/theory/quantifiers/term_tuple_enumerator.cpp
+++ b/src/theory/quantifiers/term_tuple_enumerator.cpp
@@ -154,8 +154,8 @@ class TermTupleEnumeratorBase : public TermTupleEnumeratorInterface
/** Set up terms for given variable. */
virtual size_t prepareTerms(size_t variableIx) = 0;
/** Get a given term for a given variable. */
- virtual Node getTerm(size_t variableIx,
- size_t term_index) CVC5_WARN_UNUSED_RESULT = 0;
+ CVC5_WARN_UNUSED_RESULT virtual Node getTerm(size_t variableIx,
+ size_t term_index) = 0;
};
/**
diff --git a/src/theory/theory.h b/src/theory/theory.h
index a59ee5c5f..ccda5fa77 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -440,18 +440,7 @@ class Theory : protected EnvObj
EFFORT_LAST_CALL = 200
}; /* enum Effort */
- static inline bool standardEffortOrMore(Effort e) CVC5_CONST_FUNCTION
- {
- return e >= EFFORT_STANDARD;
- }
- static inline bool standardEffortOnly(Effort e) CVC5_CONST_FUNCTION
- {
- return e >= EFFORT_STANDARD && e < EFFORT_FULL;
- }
- static inline bool fullEffort(Effort e) CVC5_CONST_FUNCTION
- {
- return e == EFFORT_FULL;
- }
+ static bool fullEffort(Effort e) { return e == EFFORT_FULL; }
/**
* Get the id for this Theory.
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 13e41978c..e2789a5b5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -695,7 +695,7 @@ void TheoryEngine::postsolve() {
d_inSatMode = false;
// Reset the interrupt flag
d_interrupted = false;
- bool CVC5_UNUSED wasInConflict = d_inConflict;
+ CVC5_UNUSED bool wasInConflict = d_inConflict;
try {
// Definition of the statement that is to be run by every theory
diff --git a/src/theory/valuation.h b/src/theory/valuation.h
index 192b5dfc8..2b95829e0 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -151,7 +151,7 @@ public:
* differ from the input due to theory-rewriting and preprocessing,
* as well as CNF conversion
*/
- Node ensureLiteral(TNode n) CVC5_WARN_UNUSED_RESULT;
+ CVC5_WARN_UNUSED_RESULT Node ensureLiteral(TNode n);
/**
* This returns the theory-preprocessed form of term n. The theory
diff --git a/test/unit/theory/theory_white.cpp b/test/unit/theory/theory_white.cpp
index 915b469db..eb80723fd 100644
--- a/test/unit/theory/theory_white.cpp
+++ b/test/unit/theory/theory_white.cpp
@@ -61,14 +61,8 @@ TEST_F(TestTheoryWhite, effort)
Theory::Effort s = Theory::EFFORT_STANDARD;
Theory::Effort f = Theory::EFFORT_FULL;
- ASSERT_TRUE(Theory::standardEffortOnly(s));
- ASSERT_FALSE(Theory::standardEffortOnly(f));
-
ASSERT_FALSE(Theory::fullEffort(s));
ASSERT_TRUE(Theory::fullEffort(f));
-
- ASSERT_TRUE(Theory::standardEffortOrMore(s));
- ASSERT_TRUE(Theory::standardEffortOrMore(f));
}
TEST_F(TestTheoryWhite, done)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback