From 46f8b15c145d630a65ef4c347ec69e0505f6b872 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Mon, 31 May 2021 19:27:46 +0200
Subject: [PATCH] ref/ref_vector minor convenience changes (#5322)

* Add ref_vector_core::push_back(ref<T>&&)

* Make operator bool() explicit
---
 src/muz/spacer/spacer_context.h | 2 +-
 src/util/ref.h                  | 6 +++++-
 src/util/ref_vector.h           | 6 ++++++
 3 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index ca0c462ad..b62da0766 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -153,7 +153,7 @@ public:
     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
index 764eb416b..1f30aae82 100644
--- a/src/util/ref.h
+++ b/src/util/ref.h
@@ -66,10 +66,14 @@ public:
         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
index 9e502335e..406f7be61 100644
--- 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 @@ public:
         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();