From 47190ae7e59a231c7d04a209a47167e40c81d870 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 29 Oct 2025 03:08:49 -0700
Subject: [PATCH] fix C++ example and add polymorphic interface for C++

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/c++/example.cpp | 13 ++++++++-----
 src/api/c++/z3++.h       | 19 +++++++++++++++++++
 src/ast/euf/ho_matcher.h |  7 +++----
 3 files changed, 30 insertions(+), 9 deletions(-)

diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index c3902dfff..2bb5510e4 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -1024,14 +1024,17 @@ void polymorphic_datatype_example() {
     symbol is_pair_name = ctx.str_symbol("is-pair");
     symbol first_name = ctx.str_symbol("first");
     symbol second_name = ctx.str_symbol("second");
-    
+ 
     symbol field_names[2] = {first_name, second_name};
-    sort field_sorts[2] = {alpha, beta};  // Use type variables
+    sort _field_sorts[2] = {alpha, beta};
+    sort_vector field_sorts(ctx);
+    field_sorts.push_back(alpha);  // Use type variables
+    field_sorts.push_back(beta);   // Use type variables   
     
     constructors cs(ctx);
-    cs.add(mk_pair_name, is_pair_name, 2, field_names, field_sorts);
-    sort pair = ctx.datatype(pair_name, cs);
-    
+    cs.add(mk_pair_name, is_pair_name, 2, field_names, _field_sorts);
+    sort pair = ctx.datatype(pair_name, field_sorts, cs);
+
     std::cout << "Created parametric datatype: " << pair << "\n";
     
     // Instantiate Pair with concrete types: (Pair Int Real)
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 1f4dee430..e55b41462 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -331,6 +331,15 @@ namespace z3 {
          */
         sort datatype(symbol const& name, constructors const& cs);
 
+        /**
+           \brief Create a parametric recursive datatype.
+           \c name is the name of the recursive datatype
+           \c params - the sort parameters of the datatype
+           \c cs - the \c n constructors used to define the datatype
+           References to the datatype and mutually recursive datatypes can be created using \ref datatype_sort.
+         */ 
+        sort datatype(symbol const &name, sort_vector const &params, constructors const &cs);
+
         /**
            \brief Create a set of mutually recursive datatypes.
            \c n - number of recursive datatypes
@@ -3621,6 +3630,16 @@ namespace z3 {
         return sort(*this, s);
     }
 
+    inline sort context::datatype(symbol const &name, sort_vector const& params, constructors const &cs) {
+        array<Z3_sort> _params(params);
+        array<Z3_constructor> _cs(cs.size());
+        for (unsigned i = 0; i < cs.size(); ++i)
+            _cs[i] = cs[i];
+        Z3_sort s = Z3_mk_polymorphic_datatype(*this, name, _params.size(), _params.ptr(), cs.size(), _cs.ptr());
+        check_error();
+        return sort(*this, s);
+    }
+
     inline sort_vector context::datatypes(
         unsigned n, symbol const* names,
         constructor_list *const* cons) {
diff --git a/src/ast/euf/ho_matcher.h b/src/ast/euf/ho_matcher.h
index 007bdea2c..65477078c 100644
--- a/src/ast/euf/ho_matcher.h
+++ b/src/ast/euf/ho_matcher.h
@@ -100,14 +100,14 @@ namespace euf {
 
     class match_goals {
     protected:
-        ast_manager &m;
         ho_matcher& ho;
+        ast_manager &m;
         
         match_goal* m_expensive = nullptr, *m_cheap = nullptr;
         match_goal* pop(match_goal*& q);
         
     public:
-        match_goals(ho_matcher& em, ast_manager &m) : m(m), ho(em) {}
+        match_goals(ho_matcher& em, ast_manager& m) : ho(em), m(m) {}
         bool empty() const { return m_cheap == nullptr && m_expensive == nullptr; }
         void reset() { m_cheap = m_expensive = nullptr; }
         void push(unsigned level, unsigned offset, expr_ref const& pat, expr_ref const& t);
@@ -158,7 +158,6 @@ namespace euf {
     };
 
     class unitary_patterns {
-        ast_manager& m;
         array_util a;
         vector<expr_ref_vector> m_patterns;
         vector<svector<lbool>>  m_is_unitary;
@@ -181,7 +180,7 @@ namespace euf {
         }
 
     public:
-        unitary_patterns(ast_manager& m) : m(m), a(m) {}
+        unitary_patterns(ast_manager& m) : a(m) {}
 
         bool is_unitary(unsigned offset, expr* p) const {
             return find(offset, p) == l_true;