feat: add Z3_mk_type_variable to .NET, TypeScript, and C++ bindings

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/fa8f5e03-a1d9-4867-9d0b-4b8bf9972e2a

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

src/api/c++/z3++.h

@@ -420,6 +420,12 @@ namespace z3 {
         sort uninterpreted_sort(char const* name);
         sort uninterpreted_sort(symbol const& name);
 
+        /**
+           \brief create a type variable sort with the name given by the string or symbol.
+         */
+        sort type_variable(char const* name);
+        sort type_variable(symbol const& name);
+
         func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
         func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
         func_decl function(symbol const&  name, sort_vector const& domain, sort const& range);
@@ -792,6 +798,10 @@ namespace z3 {
             \brief Return true if this sort is a Floating point sort.
         */
         bool is_fpa() const { return sort_kind() == Z3_FLOATING_POINT_SORT; }
+        /**
+            \brief Return true if this sort is a type variable sort.
+        */
+        bool is_type_var() const { return sort_kind() == Z3_TYPE_VAR; }
 
         /**
             \brief Return the size of this Bit-vector sort.
@@ -3869,6 +3879,13 @@ namespace z3 {
     inline sort context::uninterpreted_sort(symbol const& name) {
         return to_sort(*this, Z3_mk_uninterpreted_sort(*this, name));
     }
+    inline sort context::type_variable(char const* name) {
+        Z3_symbol _name = Z3_mk_string_symbol(*this, name);
+        return to_sort(*this, Z3_mk_type_variable(*this, _name));
+    }
+    inline sort context::type_variable(symbol const& name) {
+        return to_sort(*this, Z3_mk_type_variable(*this, name));
+    }
 
     inline func_decl context::function(symbol const & name, unsigned arity, sort const * domain, sort const & range) {
         array<Z3_sort> args(arity);

src/api/dotnet/CMakeLists.txt

@@ -113,6 +113,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
     Symbol.cs
     Tactic.cs
     TupleSort.cs
+    TypeVarSort.cs
     UninterpretedSort.cs
     UserPropagator.cs
     Version.cs

src/api/dotnet/Context.cs

@@ -227,6 +227,26 @@ namespace Microsoft.Z3
             return MkUninterpretedSort(sym);
         }
 
+        /// <summary>
+        /// Create a new type variable sort.
+        /// </summary>
+        public TypeVarSort MkTypeVariable(Symbol s)
+        {
+            Debug.Assert(s != null);
+
+            CheckContextMatch(s);
+            return new TypeVarSort(this, s);
+        }
+
+        /// <summary>
+        /// Create a new type variable sort.
+        /// </summary>
+        public TypeVarSort MkTypeVariable(string str)
+        {
+            using var sym = MkSymbol(str);
+            return MkTypeVariable(sym);
+        }
+
         /// <summary>
         /// Create a new integer sort.
         /// </summary>

src/api/dotnet/TypeVarSort.cs

@@ -0,0 +1,44 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    TypeVarSort.cs
+
+Abstract:
+
+    Z3 Managed API: Type Variable Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Type variable sorts for use in polymorphic functions and datatypes.
+    /// </summary>
+    public class TypeVarSort : Sort
+    {
+        #region Internal
+        internal TypeVarSort(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Debug.Assert(ctx != null);
+        }
+        internal TypeVarSort(Context ctx, Symbol s)
+            : base(ctx, Native.Z3_mk_type_variable(ctx.nCtx, s.NativeObject))
+        {
+            Debug.Assert(ctx != null);
+            Debug.Assert(s != null);
+        }
+        #endregion
+    }
+}

src/api/js/src/high-level/high-level.ts

@@ -743,6 +743,7 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel {
     /////////////
     const Sort = {
       declare: (name: string) => new SortImpl(Z3.mk_uninterpreted_sort(contextPtr, _toSymbol(name))),
+      typeVariable: (name: string) => new SortImpl(Z3.mk_type_variable(contextPtr, _toSymbol(name))),
     };
     const Function = {
       declare: <DomainSort extends Sort<Name>[], RangeSort extends Sort<Name>>(

src/api/js/src/high-level/types.ts

@@ -1988,6 +1988,7 @@ export interface Statistics<Name extends string = 'main'> extends Iterable<Stati
  */
 export interface SortCreation<Name extends string> {
   declare(name: string): Sort<Name>;
+  typeVariable(name: string): Sort<Name>;
 }
 
 export interface Sort<Name extends string = 'main'> extends Ast<Name, Z3_sort> {