From 5ba939ad5eabac44317ecd24867b00d0a632be9a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 3 Apr 2018 12:40:18 -0700
Subject: [PATCH] add tuple shortcut and example to C++ API

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/c++/example.cpp | 11 +++++++++++
 src/api/c++/z3++.h       | 22 ++++++++++++++++++++++
 2 files changed, 33 insertions(+)

diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index df977268a..ed5bf7086 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -920,6 +920,16 @@ void enum_sort_example() {
     std::cout << "2: " << result_goal.as_expr() << std::endl;
 }
 
+void tuple_example() {
+    std::cout << "tuple example\n";
+    context ctx;
+    const char * names[] = { "first", "second" };
+    sort sorts[2] = { ctx.int_sort(), ctx.bool_sort() };
+    func_decl_vector projs(ctx);
+    func_decl pair = ctx.tuple_sort("pair", 2, names, sorts, projs);
+    std::cout << pair << "\n";
+}
+
 void expr_vector_example() {
     std::cout << "expr_vector example\n";
     context c;
@@ -1179,6 +1189,7 @@ int main() {
         incremental_example2(); std::cout << "\n";
         incremental_example3(); std::cout << "\n";
         enum_sort_example(); std::cout << "\n";
+        tuple_example(); std::cout << "\n";
         expr_vector_example(); std::cout << "\n";
         exists_expr_vector_example(); std::cout << "\n";
         substitute_example(); std::cout << "\n";
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 42467cb22..6f46f9440 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -267,6 +267,15 @@ namespace z3 {
            and in \c ts the predicates for testing if terms of the enumeration sort correspond to an enumeration.
         */
         sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts);
+
+        /**
+           \brief Return a tuple constructor.
+           \c name is the name of the returned constructor,
+           \c n are the number of arguments, \c names and \c sorts are their projected sorts.
+           \c projs is an output paramter. It contains the set of projection functions.
+        */
+        func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs);
+
         /**
            \brief create an uninterpreted sort with the name given by the string or symbol.
          */
@@ -2432,6 +2441,19 @@ namespace z3 {
         for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); }
         return s;
     }
+    inline func_decl context::tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs) {
+        array<Z3_symbol> _names(n);
+        array<Z3_sort> _sorts(n);
+        for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
+        array<Z3_func_decl> _projs(n);
+        Z3_symbol _name = Z3_mk_string_symbol(*this, name);
+        Z3_func_decl tuple;
+        sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr()));
+        check_error();
+        for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); }
+        return func_decl(*this, tuple);
+    }
+
     inline sort context::uninterpreted_sort(char const* name) {
         Z3_symbol _name = Z3_mk_string_symbol(*this, name);
         return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name));