ref/ref_vector minor convenience changes (#5322)

* Add ref_vector_core::push_back(ref<T>&&) * Make operator bool() explicit
Z3Prover · May 31, 2021 · 46f8b15 · 46f8b15
1 parent 50cf321
commit 46f8b15
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 2 deletions.
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
@@ -153,7 +153,7 @@ class lemma {
     expr_ref_vector const &get_cube();
     void update_cube(pob_ref const &p, expr_ref_vector &cube);
 
-    bool has_pob() {return m_pob;}
+    bool has_pob() {return !!m_pob;}
     pob_ref &get_pob() {return m_pob;}
     unsigned weakness() {return m_weakness;}
 

diff --git a/src/util/ref.h b/src/util/ref.h
@@ -66,10 +66,14 @@ class ref {
         return m_ptr;
     }
 
-    operator bool() const {
+    explicit operator bool() const {
         return m_ptr != nullptr;
     }
 
+    bool operator!() const {
+        return m_ptr == nullptr;
+    }
+
     const T & operator*() const {
         return *m_ptr;
     }

diff --git a/src/util/ref_vector.h b/src/util/ref_vector.h
@@ -20,6 +20,7 @@ Revision History:
 
 #include "util/vector.h"
 #include "util/obj_ref.h"
+#include "util/ref.h"
 
 /**
    \brief Vector of smart pointers.
@@ -113,6 +114,11 @@ class ref_vector_core : public Ref {
         return *this;
     }
 
+    ref_vector_core& push_back(ref<T>&& n) {
+        m_nodes.push_back(n.detach());
+        return *this;
+    }
+
     void pop_back() {
         SASSERT(!m_nodes.empty());
         T * n = m_nodes.back();