Experimental patch for Homebrew's Z3 library to support C++17.

z3-cpp-17-support.patch

diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp
index 7da470221..29136cf0c 100644
--- a/src/ast/array_decl_plugin.cpp
+++ b/src/ast/array_decl_plugin.cpp
@@ -17,7 +17,6 @@ Revision History:
 
 --*/
 #include<sstream>
-#include<format>
 #include "ast/array_decl_plugin.h"
 #include "util/warning.h"
 #include "ast/ast_pp.h"
@@ -140,7 +139,7 @@ func_decl * array_decl_plugin::mk_const(sort * s, unsigned arity, sort * const *
 
 func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const* domain) {
     if (arity != f->get_arity()) {
-        m_manager->raise_exception(std::format("map expects to take as many arguments as the function being mapped, it was given {} but expects {}",
+        m_manager->raise_exception(pseudo_format("map expects to take as many arguments as the function being mapped, it was given {} but expects {}",
                                                 arity, f->get_arity()));
         return nullptr;
     }
@@ -156,21 +155,21 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const*
     unsigned dom_arity = get_array_arity(domain[0]);
     for (unsigned i = 0; i < arity; ++i) {
         if (!is_array_sort(domain[i])) {
-            m_manager->raise_exception(std::format("map expects an array sort as argument at position {}", i));
+            m_manager->raise_exception(pseudo_format("map expects an array sort as argument at position {}", i));
             return nullptr;
         }
         if (get_array_arity(domain[i]) != dom_arity) {
-            m_manager->raise_exception(std::format("map expects all arguments to have the same array domain,  this is not the case for argument {}", i));
+            m_manager->raise_exception(pseudo_format("map expects all arguments to have the same array domain,  this is not the case for argument {}", i));
             return nullptr;
         }
         for (unsigned j = 0; j < dom_arity; ++j) {
             if (get_array_domain(domain[i],j) != get_array_domain(domain[0],j)) {
-                m_manager->raise_exception(std::format("map expects all arguments to have the same array domain, this is not the case for argument {}", i));
+                m_manager->raise_exception(pseudo_format("map expects all arguments to have the same array domain, this is not the case for argument {}", i));
                 return nullptr;
             }
         }
         if (get_array_range(domain[i]) != f->get_domain(i)) {
-            m_manager->raise_exception(std::format("map expects the argument at position {} to have the array range the same as the function", i));
+            m_manager->raise_exception(pseudo_format("map expects the argument at position {} to have the array range the same as the function", i));
             return nullptr;
         }
     }
@@ -231,7 +230,7 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
     parameter const* parameters = s->get_parameters();
  
     if (num_parameters != arity) {
-        m_manager->raise_exception(std::format("select requires {} arguments, but was provided with {} arguments", 
+        m_manager->raise_exception(pseudo_format("select requires {} arguments, but was provided with {} arguments", 
                                                 num_parameters, arity));
         return nullptr;
     }
@@ -241,7 +240,7 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
         if (!parameters[i].is_ast() || 
             !is_sort(parameters[i].get_ast()) || 
             !m_manager->compatible_sorts(domain[i+1], to_sort(parameters[i].get_ast()))) {
-            m_manager->raise_exception(std::format("domain sort {} and parameter {} do not match",
+            m_manager->raise_exception(pseudo_format("domain sort {} and parameter {} do not match",
                                                     to_string(sort_ref(domain[i+1], *m_manager)),
                                                     to_string(parameter_pp(parameters[i], *m_manager))));
             return nullptr;
@@ -267,7 +266,7 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) {
         return nullptr;
     }
     if (arity != num_parameters+1) {
-        m_manager->raise_exception(std::format("store expects the first argument to be an array taking {}, instead it was passed {} arguments",
+        m_manager->raise_exception(pseudo_format("store expects the first argument to be an array taking {}, instead it was passed {} arguments",
                                                 num_parameters+1, arity - 1));
         UNREACHABLE();
         return nullptr;
@@ -282,7 +281,7 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) {
         sort* srt1 = to_sort(parameters[i].get_ast());
         sort* srt2 = domain[i+1];
         if (!m_manager->compatible_sorts(srt1, srt2)) {
-            m_manager->raise_exception(std::format("domain sort {} and parameter sort {} do not match",
+            m_manager->raise_exception(pseudo_format("domain sort {} and parameter sort {} do not match",
                                                     to_string(sort_ref(srt2, *m_manager)),
                                                     to_string(sort_ref(srt1, *m_manager))));
             UNREACHABLE();
@@ -317,11 +316,11 @@ func_decl * array_decl_plugin::mk_array_ext(unsigned arity, sort * const * domai
 bool array_decl_plugin::check_set_arguments(unsigned arity, sort * const * domain) {
     for (unsigned i = 0; i < arity; ++i) {
         if (domain[i] != domain[0]) {
-            m_manager->raise_exception(std::format("arguments {} and {} have different sorts", 1, i+1));
+            m_manager->raise_exception(pseudo_format("arguments {} and {} have different sorts", 1, i+1));
             return false;
         }
         if (domain[i]->get_family_id() != m_family_id) {
-            m_manager->raise_exception(std::format("argument {} is not of array sort", i+1));
+            m_manager->raise_exception(pseudo_format("argument {} is not of array sort", i+1));
             return false;
         }
     }
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 1583fb4ec..643036338 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -17,7 +17,6 @@ Revision History:
 
 --*/
 #include <sstream>
-#include <format>
 #include <cstring>
 #include "ast/ast.h"
 #include "ast/ast_pp.h"
@@ -1016,7 +1015,7 @@ sort* basic_decl_plugin::join(sort* s1, sort* s2) {
         return s2;
     if (s2 == m_bool_sort && s1->get_family_id() == arith_family_id)
         return s1;
-    throw ast_exception(std::format("Sorts {} and {} are incompatible", 
+    throw ast_exception(pseudo_format("Sorts {} and {} are incompatible", 
                                      to_string(mk_pp(s1, *m_manager)), 
                                      to_string(mk_pp(s2, *m_manager))));
 }
@@ -1695,7 +1694,7 @@ ast * ast_manager::register_node_core(ast * n) {
         SASSERT(contains);
         SASSERT(m_ast_table.contains(n));
         if (is_func_decl(r) && to_func_decl(r)->get_range() != to_func_decl(n)->get_range()) {
-            throw ast_exception(std::format("Recycling of declaration for the same name '{}' and domain, but different range type is not permitted",
+            throw ast_exception(pseudo_format("Recycling of declaration for the same name '{}' and domain, but different range type is not permitted",
                                              to_func_decl(r)->get_name().str()));
         }
         deallocate_node(n, ::get_node_size(n));
@@ -2019,7 +2018,7 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c
         for (unsigned i = 0; i < num_args; ++i) {
             sort * given = args[i]->get_sort();
             if (!compatible_sorts(expected, given)) {
-                throw ast_exception(std::format("invalid function application for {}, sort mismatch on argument at position {}, expected {} but given {}",
+                throw ast_exception(pseudo_format("invalid function application for {}, sort mismatch on argument at position {}, expected {} but given {}",
                                                  to_string(decl->get_name()),
                                                  i + 1,
                                                  to_string(mk_pp(expected, m)),
@@ -2035,7 +2034,7 @@ void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * c
             sort * expected = decl->get_domain(i);
             sort * given    = args[i]->get_sort();
             if (!compatible_sorts(expected, given)) {
-                throw ast_exception(std::format("invalid function application for {}, sort mismatch on argument at position {}, expected {} but given {}",
+                throw ast_exception(pseudo_format("invalid function application for {}, sort mismatch on argument at position {}, expected {} but given {}",
                                                  to_string(decl->get_name()),
                                                  i + 1,
                                                  to_string(mk_pp(expected, m)),
@@ -2194,7 +2193,7 @@ void ast_manager::check_args(func_decl* f, unsigned n, expr* const* es) {
         sort * actual_sort   = es[i]->get_sort();
         sort * expected_sort = f->is_associative() ? f->get_domain(0) : f->get_domain(i);
         if (expected_sort != actual_sort) {
-            throw ast_exception(std::format("Sort mismatch at argument #{} for function {} supplied sort is {}",
+            throw ast_exception(pseudo_format("Sort mismatch at argument #{} for function {} supplied sort is {}",
                                              i + 1,
                                              to_string(mk_pp(f, *this)),
                                              to_string(mk_pp(actual_sort, *this))));
@@ -2220,8 +2219,8 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar
     if (type_error) {
         std::string arg_list;
         for (unsigned i = 0; i < num_args; ++i)
-            arg_list += std::format("\narg: {}\n", to_string(mk_pp(args[i], *this)));
-        throw ast_exception(std::format("Wrong number of arguments ({}) passed to function {} {}",
+            arg_list += pseudo_format("\narg: {}\n", to_string(mk_pp(args[i], *this)));
+        throw ast_exception(pseudo_format("Wrong number of arguments ({}) passed to function {} {}",
                                          num_args,
                                          to_string(mk_pp(decl, *this)),
                                          arg_list));
diff --git a/src/ast/ast_pp.h b/src/ast/ast_pp.h
index 4fb0daef0..74ee81e7e 100644
--- a/src/ast/ast_pp.h
+++ b/src/ast/ast_pp.h
@@ -79,3 +79,35 @@ inline std::string to_string(T const& obj) {
     return std::move(strm).str();
 }
 
+// Base case: No more arguments left to format
+inline void format_helper(std::ostringstream& oss, std::string_view fmt) {
+    oss << fmt;
+}
+
+// Recursive case: Process the next placeholder
+template <typename T, typename... Args>
+void format_helper(std::ostringstream& oss, std::string_view fmt, T&& first, Args&&... rest) {
+    size_t pos = fmt.find("{}");
+
+    if (pos == std::string_view::npos) {
+        // No more placeholders found, dump the rest of the string
+        oss << fmt;
+        return;
+    }
+
+    // Append text up to the placeholder, then append the argument
+    oss << fmt.substr(0, pos);
+    oss << std::forward<T>(first);
+
+    // Move past the "{}" placeholder and parse remaining arguments
+    format_helper(oss, fmt.substr(pos + 2), std::forward<Args>(rest)...);
+}
+
+// Entry point matching the basic std::format signature
+template <typename... Args>
+std::string pseudo_format(std::string_view fmt, Args&&... args) {
+    std::ostringstream oss;
+    format_helper(oss, fmt, std::forward<Args>(args)...);
+    return oss.str();
+}
+
diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp
index 76dc8fe07..4e7293faa 100644
--- a/src/ast/bv_decl_plugin.cpp
+++ b/src/ast/bv_decl_plugin.cpp
@@ -17,7 +17,6 @@ Revision History:
 
 --*/
 #include<sstream>
-#include<format>
 #include "ast/bv_decl_plugin.h"
 #include "ast/arith_decl_plugin.h"
 #include "util/warning.h"
@@ -673,7 +672,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
         }
         for (unsigned i = 0; i < num_args; ++i) {
             if (args[i]->get_sort() != r->get_domain(i)) {
-                m.raise_exception(std::format("Argument {} at position {} has sort {} it does not match declaration {}",
+                m.raise_exception(pseudo_format("Argument {} at position {} has sort {} it does not match declaration {}",
                                                to_string(mk_pp(args[i], m)),
                                                i,
                                                to_string(mk_pp(args[i]->get_sort(), m)),
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index d875262b3..04e9d02cb 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -18,7 +18,6 @@ Revision History:
 --*/
 
 #include<sstream>
-#include<format>
 #include "util/warning.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
@@ -379,7 +378,7 @@ namespace datatype {
                 return nullptr;
             }
             if (rng != domain[1]) {
-                m.raise_exception(std::format("second argument to field update should be {} instead of {}",
+                m.raise_exception(pseudo_format("second argument to field update should be {} instead of {}",
                                                to_string(mk_ismt2_pp(rng, m)),
                                                to_string(mk_ismt2_pp(domain[1], m))));
                 return nullptr;
diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp
index af4d30add..128edb11c 100644
--- a/src/ast/dl_decl_plugin.cpp
+++ b/src/ast/dl_decl_plugin.cpp
@@ -17,7 +17,6 @@ Revision History:
 
 --*/
 #include<sstream>
-#include<format>
 
 #include "ast/ast_pp.h"
 #include "ast/array_decl_plugin.h"
@@ -53,7 +52,7 @@ namespace datalog {
         if (low <= val && val <= up) {
             return true;
         }
-        m_manager->raise_exception(std::format("{}, value is not within bound {} <= {} <= {}", msg, low, val, up));
+        m_manager->raise_exception(pseudo_format("{}, value is not within bound {} <= {} <= {}", msg, low, val, up));
         return false;
     }
 
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 634ced5c9..864c9cbae 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -21,7 +21,6 @@ Revision History:
 #include "ast/array_decl_plugin.h"
 #include "ast/ast_pp.h"
 #include <sstream>
-#include <format>
 
 
 seq_decl_plugin::seq_decl_plugin(): m_init(false),
@@ -83,7 +82,7 @@ void seq_decl_plugin::match_assoc(psig& sig, unsigned dsz, sort *const* dom, sor
     ptr_vector<sort> binding;
     ast_manager& m = *m_manager;
     if (dsz == 0) {
-        m.raise_exception(std::format("Unexpected number of arguments to '{}' at least one argument expected {} given",
+        m.raise_exception(pseudo_format("Unexpected number of arguments to '{}' at least one argument expected {} given",
                                        sig.m_name.str(), dsz));
     }
     bool is_match = true;
@@ -101,9 +100,9 @@ void seq_decl_plugin::match_assoc(psig& sig, unsigned dsz, sort *const* dom, sor
         }
         std::string range_str;
         if (range) {
-            range_str = std::format(" and range: {}", to_string(mk_pp(range, m)));
+            range_str = pseudo_format(" and range: {}", to_string(mk_pp(range, m)));
         }
-        m.raise_exception(std::format("Sort of function '{}' does not match the declared type. Given domain: {}{}",
+        m.raise_exception(pseudo_format("Sort of function '{}' does not match the declared type. Given domain: {}{}",
                                        sig.m_name.str(), domain_str, range_str));
     }
     range_out = apply_binding(binding, sig.m_range);
@@ -114,7 +113,7 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran
     m_binding.reset();
     ast_manager& m = *m_manager;
     if (sig.m_dom.size() != dsz) {
-        m.raise_exception(std::format("Unexpected number of arguments to '{}' {} arguments expected {} given",
+        m.raise_exception(pseudo_format("Unexpected number of arguments to '{}' {} arguments expected {} given",
                                        sig.m_name.str(), sig.m_dom.size(), dsz));
     }
     bool is_match = true;
@@ -131,18 +130,18 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran
         }
         std::string range_str;
         if (range) {
-            range_str = std::format(" and range: {}", to_string(mk_pp(range, m)));
+            range_str = pseudo_format(" and range: {}", to_string(mk_pp(range, m)));
         }
         std::string expected_domain;
         for (unsigned i = 0; i < dsz; ++i) {
             expected_domain += to_string(mk_pp(sig.m_dom[i].get(), m)) + " ";
         }
 
-        m.raise_exception(std::format("Sort of polymorphic function '{}' does not match the declared type. \nGiven domain: {}{}\nExpected domain: {}",
+        m.raise_exception(pseudo_format("Sort of polymorphic function '{}' does not match the declared type. \nGiven domain: {}{}\nExpected domain: {}",
                                        sig.m_name.str(), given_domain, range_str, expected_domain));
     }
     if (!range && dsz == 0) {
-        m.raise_exception(std::format("Sort of polymorphic function '{}' is ambiguous. Function takes no arguments and sort of range has not been constrained",
+        m.raise_exception(pseudo_format("Sort of polymorphic function '{}' is ambiguous. Function takes no arguments and sort of range has not been constrained",
                                        sig.m_name.str()));
     }
     range_out = apply_binding(m_binding, sig.m_range);

Thanks to the diff. It reduces 11 errors to 4 on my machine (Monterey 12.7.6):

z3-z3-4.16.0/src/util/obj_hashtable.h:135:24: error: no matching constructor for initialization of 'obj_map<func_decl, quantifier *>::key_data'
        m_table.insert(key_data(k, v));
                       ^        ~~~~
z3-z3-4.16.0/src/util/obj_hashtable.h:201:24: error: no matching conversion for functional-style cast from 'func_decl *' to 'obj_map<func_decl, func_decl *>::key_data'
        m_table.remove(key_data(k));
                       ^~~~~~~~~~
z3-z3-4.16.0/src/util/obj_hashtable.h:201:24: error: no matching conversion for functional-style cast from 'func_decl *' to 'obj_map<func_decl, quantifier *>::key_data'
        m_table.remove(key_data(k));
                       ^~~~~~~~~~

z3-z3-4.16.0/src/util/obj_hashtable.h:135:24: error: no matching constructor for initialization of 'obj_map<func_decl, func_decl *>::key_data'
        m_table.insert(key_data(k, v));
                       ^        ~~~~

Hi @swamp-agr.

For that issue, I'm using this patch:

https://github.com/Z3Prover/z3/commit/054d71455d353a93dcb167446614b52dd0472f9a.patch