Add Java APIs for polymorphic datatypes (#8438)

* Initial plan

* Add Java APIs for polymorphic datatypes and type variables

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

* Fix code review issue and add documentation

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

* Add TypeVarSort.java to CMakeLists.txt for Java bindings

The CMake build was failing because TypeVarSort.java was not included in the Z3_JAVA_JAR_SOURCE_FILES list in src/api/java/CMakeLists.txt. Added it in alphabetical order between TupleSort.java and UninterpretedSort.java.

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>

examples/java/PolymorphicDatatypeExample.java

@@ -0,0 +1,138 @@
+/**
+Copyright (c) 2024 Microsoft Corporation
+   
+Module Name:
+
+    PolymorphicDatatypeExample.java
+
+Abstract:
+
+    Example demonstrating the use of polymorphic (parametric) datatypes in Z3's Java API.
+    This example creates a polymorphic List[T] datatype and demonstrates its usage.
+
+Author:
+
+    GitHub Copilot 2024-01-30
+
+Notes:
+    
+**/
+
+import com.microsoft.z3.*;
+
+public class PolymorphicDatatypeExample {
+    
+    /**
+     * Create a polymorphic List[T] datatype.
+     * This is equivalent to:
+     *   datatype List[T] = nil | cons(head: T, tail: List[T])
+     */
+    static void polymorphicListExample(Context ctx) {
+        System.out.println("PolymorphicListExample");
+        
+        // Create a type variable T
+        TypeVarSort T = ctx.mkTypeVariable("T");
+        
+        // Create constructors for the List[T] datatype
+        // nil constructor (no arguments)
+        Constructor<Object> nil = ctx.mkConstructor("nil", "is_nil", null, null, null);
+        
+        // cons constructor with head:T and tail:List[T]
+        String[] fieldNames = new String[] { "head", "tail" };
+        Sort[] fieldSorts = new Sort[] { T, null }; // null means recursive reference
+        int[] sortRefs = new int[] { 0, 0 }; // both refer to the datatype being defined
+        Constructor<Object> cons = ctx.mkConstructor("cons", "is_cons", fieldNames, fieldSorts, sortRefs);
+        
+        // Create the polymorphic List[T] datatype
+        Constructor<Object>[] constructors = new Constructor[] { nil, cons };
+        DatatypeSort<Object> listSort = ctx.mkPolymorphicDatatypeSort("List", new Sort[]{T}, constructors);
+        
+        System.out.println("Created polymorphic List datatype: " + listSort);
+        
+        // Get the constructor and accessor functions
+        FuncDecl<?>[] listConstructors = listSort.getConstructors();
+        FuncDecl<?> nilDecl = listConstructors[0];
+        FuncDecl<?> consDecl = listConstructors[1];
+        
+        System.out.println("nil constructor: " + nilDecl);
+        System.out.println("cons constructor: " + consDecl);
+        
+        // Get accessors
+        FuncDecl<?>[][] accessors = listSort.getAccessors();
+        if (accessors.length > 1 && accessors[1].length == 2) {
+            FuncDecl<?> headAccessor = accessors[1][0];
+            FuncDecl<?> tailAccessor = accessors[1][1];
+            System.out.println("head accessor: " + headAccessor);
+            System.out.println("tail accessor: " + tailAccessor);
+        }
+        
+        System.out.println("Polymorphic List example completed successfully!");
+    }
+    
+    /**
+     * Create a polymorphic Option[T] datatype (like Maybe in Haskell).
+     * This is equivalent to:
+     *   datatype Option[T] = none | some(value: T)
+     */
+    static void polymorphicOptionExample(Context ctx) {
+        System.out.println("\nPolymorphicOptionExample");
+        
+        // Create a type variable T
+        TypeVarSort T = ctx.mkTypeVariable("T");
+        
+        // Create constructors for Option[T]
+        Constructor<Object> none = ctx.mkConstructor("none", "is_none", null, null, null);
+        
+        String[] fieldNames = new String[] { "value" };
+        Sort[] fieldSorts = new Sort[] { T };
+        int[] sortRefs = new int[] { 0 }; // not used since T is not recursive
+        Constructor<Object> some = ctx.mkConstructor("some", "is_some", fieldNames, fieldSorts, sortRefs);
+        
+        // Create the polymorphic Option[T] datatype
+        Constructor<Object>[] constructors = new Constructor[] { none, some };
+        DatatypeSort<Object> optionSort = ctx.mkPolymorphicDatatypeSort("Option", new Sort[]{T}, constructors);
+        
+        System.out.println("Created polymorphic Option datatype: " + optionSort);
+        
+        FuncDecl<?>[] optionConstructors = optionSort.getConstructors();
+        System.out.println("none constructor: " + optionConstructors[0]);
+        System.out.println("some constructor: " + optionConstructors[1]);
+        
+        System.out.println("Polymorphic Option example completed successfully!");
+    }
+    
+    /**
+     * Demonstrate type variables can be created with different names
+     */
+    static void typeVariableExample(Context ctx) {
+        System.out.println("\nTypeVariableExample");
+        
+        TypeVarSort T = ctx.mkTypeVariable("T");
+        TypeVarSort U = ctx.mkTypeVariable("U");
+        TypeVarSort V = ctx.mkTypeVariable("V");
+        
+        System.out.println("Created type variable T: " + T);
+        System.out.println("Created type variable U: " + U);
+        System.out.println("Created type variable V: " + V);
+        
+        // Type variables can be used as sort parameters
+        System.out.println("Type variables can be used as parameters for polymorphic datatypes");
+    }
+
+    public static void main(String[] args) {
+        try {
+            // Use try-with-resources to ensure proper cleanup
+            try (Context ctx = new Context()) {
+                typeVariableExample(ctx);
+                polymorphicListExample(ctx);
+                polymorphicOptionExample(ctx);
+                
+                System.out.println("\n=== All polymorphic datatype examples completed successfully! ===");
+            }
+        } catch (Exception e) {
+            System.err.println("Error: " + e.getMessage());
+            e.printStackTrace();
+            System.exit(1);
+        }
+    }
+}

examples/java/README

@@ -1,5 +1,13 @@
 A small example using the Z3 Java bindings.   
 
+## Examples
+
+- **JavaExample.java** - General examples demonstrating various Z3 features
+- **JavaGenericExample.java** - Examples using generic Z3 types
+- **PolymorphicDatatypeExample.java** - Examples of parametric/polymorphic datatypes with type variables
+- **SeqOperationsExample.java** - Examples of sequence operations
+- **RCFExample.java** - Examples using real closed fields
+
 ## IDE Setup
 
 For detailed instructions on setting up Z3 Java bindings in Eclipse, IntelliJ IDEA, 
@@ -26,3 +34,37 @@ In certain environments, depending on the developing process, the Z3 library is
 To disable the automated loading process, the user can set the environment variable "z3.skipLibraryLoad=true".
 In that case, the calling application should directly load the corresponding libraries before any interaction with Z3.
 
+## Polymorphic Datatypes
+
+Z3's Java API now supports polymorphic (parametric) datatypes, similar to generic types in Java or templates in C++.
+These allow you to define datatypes that are parameterized by type variables.
+
+### Creating Type Variables
+
+```java
+Context ctx = new Context();
+TypeVarSort T = ctx.mkTypeVariable("T");
+TypeVarSort U = ctx.mkTypeVariable("U");
+```
+
+### Creating Polymorphic Datatypes
+
+Example: Polymorphic List[T]
+```java
+// Create type variable
+TypeVarSort T = ctx.mkTypeVariable("T");
+
+// Define constructors
+Constructor<Object> nil = ctx.mkConstructor("nil", "is_nil", null, null, null);
+Constructor<Object> cons = ctx.mkConstructor("cons", "is_cons",
+    new String[]{"head", "tail"},
+    new Sort[]{T, null},  // null means recursive reference to List[T]
+    new int[]{0, 0});
+
+// Create the polymorphic datatype
+DatatypeSort<Object> listSort = ctx.mkPolymorphicDatatypeSort("List",
+    new Sort[]{T}, new Constructor[]{nil, cons});
+```
+
+See `PolymorphicDatatypeExample.java` for complete working examples.
+

src/api/java/CMakeLists.txt

@@ -158,6 +158,7 @@ set(Z3_JAVA_JAR_SOURCE_FILES
   Symbol.java
   Tactic.java
   TupleSort.java
+  TypeVarSort.java
   UninterpretedSort.java
   UserPropagatorBase.java
   Version.java

src/api/java/Context.java

@@ -473,6 +473,88 @@ public class Context implements AutoCloseable {
         return mkDatatypeSorts(mkSymbols(names), c);
     }
 
+    /**
+     * Create a type variable for use in polymorphic functions and datatypes.
+     * Type variables can be used as sort parameters in polymorphic datatypes.
+     * @param name name of the type variable
+     * @return a new type variable sort
+     **/
+    public TypeVarSort mkTypeVariable(Symbol name)
+    {
+        checkContextMatch(name);
+        return new TypeVarSort(this, name);
+    }
+
+    /**
+     * Create a type variable for use in polymorphic functions and datatypes.
+     * Type variables can be used as sort parameters in polymorphic datatypes.
+     * @param name name of the type variable
+     * @return a new type variable sort
+     **/
+    public TypeVarSort mkTypeVariable(String name)
+    {
+        return mkTypeVariable(mkSymbol(name));
+    }
+
+    /**
+     * Create a polymorphic (parametric) datatype sort.
+     * A polymorphic datatype is parameterized by type variables, allowing it to
+     * work with different types. This is similar to generic types in programming languages.
+     * 
+     * @param name name of the datatype sort
+     * @param parameters array of type variable sorts to parameterize the datatype
+     * @param constructors array of constructor specifications
+     * @return a new polymorphic datatype sort
+     * 
+     * Example:
+     * <pre>
+     * // Create a polymorphic List datatype: List[T]
+     * TypeVarSort T = ctx.mkTypeVariable("T");
+     * Constructor&lt;Object&gt; nil = ctx.mkConstructor("nil", "is_nil", null, null, null);
+     * Constructor&lt;Object&gt; cons = ctx.mkConstructor("cons", "is_cons",
+     *     new String[]{"head", "tail"},
+     *     new Sort[]{T, null}, // head has type T, tail is recursive reference
+     *     new int[]{0, 0}); // sortRef 0 refers back to List[T]
+     * DatatypeSort&lt;Object&gt; listSort = ctx.mkPolymorphicDatatypeSort("List",
+     *     new Sort[]{T}, new Constructor[]{nil, cons});
+     * </pre>
+     **/
+    public <R> DatatypeSort<R> mkPolymorphicDatatypeSort(Symbol name, Sort[] parameters, Constructor<R>[] constructors)
+    {
+        checkContextMatch(name);
+        checkContextMatch(parameters);
+        checkContextMatch(constructors);
+        
+        int numParams = parameters.length;
+        long[] paramsNative = AST.arrayToNative(parameters);
+        
+        int numConstructors = constructors.length;
+        long[] constructorsNative = new long[numConstructors];
+        for (int i = 0; i < numConstructors; i++) {
+            constructorsNative[i] = constructors[i].getNativeObject();
+        }
+        
+        long nativeSort = Native.mkPolymorphicDatatype(nCtx(), name.getNativeObject(),
+                numParams, paramsNative, numConstructors, constructorsNative);
+        
+        return new DatatypeSort<>(this, nativeSort);
+    }
+
+    /**
+     * Create a polymorphic (parametric) datatype sort.
+     * A polymorphic datatype is parameterized by type variables, allowing it to
+     * work with different types. This is similar to generic types in programming languages.
+     * 
+     * @param name name of the datatype sort
+     * @param parameters array of type variable sorts to parameterize the datatype
+     * @param constructors array of constructor specifications
+     * @return a new polymorphic datatype sort
+     **/
+    public <R> DatatypeSort<R> mkPolymorphicDatatypeSort(String name, Sort[] parameters, Constructor<R>[] constructors)
+    {
+        return mkPolymorphicDatatypeSort(mkSymbol(name), parameters, constructors);
+    }
+
     /**
      * Update a datatype field at expression t with value v.
      * The function performs a record update at t. The field

src/api/java/TypeVarSort.java

@@ -0,0 +1,27 @@
+/**
+Copyright (c) 2024 Microsoft Corporation
+   
+Module Name:
+
+    TypeVarSort.java
+
+Abstract:
+
+Author:
+
+    GitHub Copilot 2024-01-30
+
+Notes:
+    
+**/
+
+package com.microsoft.z3;
+
+/**
+ * A type variable sort for use in polymorphic functions and datatypes.
+ **/
+public class TypeVarSort extends Sort
+{
+    TypeVarSort(Context ctx, long obj) { super(ctx, obj); }
+    TypeVarSort(Context ctx, Symbol s) { super(ctx, Native.mkTypeVariable(ctx.nCtx(), s.getNativeObject())); }
+}