From 5d7833e65e75e19f1ae8bbeea8360c45d585d879 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 16 Dec 2022 10:28:57 +0100 Subject: [PATCH] Warn on unused result (mainly for substitution::add) --- src/math/polysat/assignment.h | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/math/polysat/assignment.h b/src/math/polysat/assignment.h index 2f8f65474..458b8410d 100644 --- a/src/math/polysat/assignment.h +++ b/src/math/polysat/assignment.h @@ -53,13 +53,13 @@ namespace polysat { public: substitution(dd::pdd_manager& m); - substitution add(pvar var, rational const& value) const; - pdd apply_to(pdd const& p) const; + [[nodiscard]] substitution add(pvar var, rational const& value) const; + [[nodiscard]] pdd apply_to(pdd const& p) const; - bool contains(pvar var) const; - bool value(pvar var, rational& out_value) const; + [[nodiscard]] bool contains(pvar var) const; + [[nodiscard]] bool value(pvar var, rational& out_value) const; - bool empty() const { return m_subst.is_one(); } + [[nodiscard]] bool empty() const { return m_subst.is_one(); } pdd const& to_pdd() const { return m_subst; } unsigned bit_width() const { return to_pdd().power_of_2(); }