Refactor counter::get_max_positive to use std::optional (#8289)

* Initial plan

* Refactor counter::get_max_positive to use std::optional

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix C++17 compatibility by replacing transform() with has_value()/value()

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Address code review: avoid calling get_max_positive twice

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/ast/rewriter/ast_counter.cpp

@@ -49,21 +49,18 @@ void counter::collect_positive(uint_set & acc) const {
             acc.insert(kv.m_key); 
 }
 
-bool counter::get_max_positive(unsigned & res) const {
+std::optional<unsigned> counter::get_max_positive() const {
-    bool found = false;
+    std::optional<unsigned> result;
     for (auto const& kv : *this) {
-        if (kv.m_value > 0 && (!found || kv.m_key > res) ) { 
+        if (kv.m_value > 0 && (!result || kv.m_key > *result)) {
-            found = true;
+            result = kv.m_key;
-            res = kv.m_key;
         }
     }
-    return found;
+    return result;
 }
 
-unsigned counter::get_max_positive() const {
+unsigned counter::get_max_positive_or_zero() const {
-    unsigned max_pos;
+    return get_max_positive().value_or(0);
-    VERIFY(get_max_positive(max_pos));
-    return max_pos;
 }
 
 int counter::get_max_counter_value() const {

src/ast/rewriter/ast_counter.h

@@ -23,6 +23,7 @@ Revision History:
 
 #pragma once
 
+#include <optional>
 #include "ast/ast.h"
 #include "util/map.h"
 #include "util/uint_set.h"
@@ -55,8 +56,8 @@ public:
     void collect_positive(uint_set & acc) const;
     unsigned get_positive_count() const;
 
-    bool get_max_positive(unsigned & res) const;
+    std::optional<unsigned> get_max_positive() const;
-    unsigned get_max_positive() const;
+    unsigned get_max_positive_or_zero() const;
 
     /**
        Since the default counter value of a counter is zero, the result is never negative.

src/muz/base/dl_util.cpp

@@ -486,7 +486,7 @@ namespace datalog {
         DEBUG_CODE(
             counter ctr;
             ctr.count(permutation);
-            SASSERT(permutation.empty() || ctr.get_max_positive()==permutation.size()-1);
+            SASSERT(permutation.empty() || ctr.get_max_positive().value_or(0)==permutation.size()-1);
             SASSERT(permutation.empty() || ctr.get_positive_count()==permutation.size());
             );
         unsigned sz = permutation.size();

src/muz/rel/dl_mk_explanations.cpp

@@ -585,7 +585,7 @@ namespace datalog {
         }
         counter ctr;
         ctr.count(joined_col_cnt, tgt_cols);
-        if (ctr.get_max_counter_value()>1 || (joined_col_cnt && ctr.get_max_positive()!=joined_col_cnt-1)) {
+        if (ctr.get_max_counter_value()>1 || (joined_col_cnt && ctr.get_max_positive().value_or(0)!=joined_col_cnt-1)) {
             return nullptr;
         }
         return alloc(intersection_filter_fn, *this);
@@ -712,8 +712,8 @@ namespace datalog {
     rule * mk_explanations::get_e_rule(rule * r) {
         rule_counter ctr;
         ctr.count_rule_vars(r);
-        unsigned max_var;
+        auto max_var = ctr.get_max_positive();
-        unsigned next_var = ctr.get_max_positive(max_var) ? (max_var+1) : 0;
+        unsigned next_var = max_var.has_value() ? (*max_var + 1) : 0;
         unsigned head_var = next_var++;
         app_ref e_head(get_e_lit(r->get_head(), head_var), m_manager);
 

src/muz/rel/dl_mk_similarity_compressor.cpp

@@ -382,9 +382,9 @@ namespace datalog {
 
         rule_counter ctr;
         ctr.count_rule_vars(r);
-        unsigned max_var_idx, new_var_idx_base;
+        unsigned new_var_idx_base;
-        if (ctr.get_max_positive(max_var_idx)) {
+        if (auto max_var_idx = ctr.get_max_positive()) {
-            new_var_idx_base = max_var_idx+1;
+            new_var_idx_base = *max_var_idx + 1;
         }
         else {
             new_var_idx_base = 0;

src/muz/rel/dl_sparse_table.cpp

@@ -386,7 +386,7 @@ namespace datalog {
             }
             counter ctr;
             ctr.count(key_len, key_cols);
-            if (ctr.get_max_counter_value()!=1 || ctr.get_max_positive()!=non_func_cols-1) {
+            if (ctr.get_max_counter_value()!=1 || ctr.get_max_positive().value_or(0)!=non_func_cols-1) {
                 return false;
             }
             SASSERT(ctr.get_positive_count() == non_func_cols);
@@ -467,7 +467,7 @@ namespace datalog {
         //Maybe we might keep a list of indexes that contain functional columns and on an update reset 
         //only those.
         SASSERT(key_len == 0 || 
-            counter().count(key_len, key_cols).get_max_positive()<get_signature().first_functional());
+            counter().count(key_len, key_cols).get_max_positive().value_or(0)<get_signature().first_functional());
 #endif
         key_spec kspec;
         kspec.append(key_len, key_cols);
@@ -808,8 +808,8 @@ namespace datalog {
         if (col_cnt == 0) {
             return false;
         }
-        return counter().count(col_cnt, cols1).get_max_positive()>=s1.first_functional()
+        return counter().count(col_cnt, cols1).get_max_positive().value_or(0)>=s1.first_functional()
-            || counter().count(col_cnt, cols2).get_max_positive()>=s2.first_functional();
+            || counter().count(col_cnt, cols2).get_max_positive().value_or(0)>=s2.first_functional();
     }
 
 
@@ -1138,7 +1138,7 @@ namespace datalog {
             ctr.count(m_cols2);
             m_joining_neg_non_functional = ctr.get_max_counter_value() == 1
                 && ctr.get_positive_count() == neg_first_func 
-                && (neg_first_func == 0 || ctr.get_max_positive() == neg_first_func-1);
+                && (neg_first_func == 0 || ctr.get_max_positive().value_or(0) == neg_first_func-1);
         }
 
         /**