fix issues 1-10: add missing API bindings across Go, Julia, TypeScript, OCaml, and Java (#9432)

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/b89f3b76-dfd7-47ec-97dd-8ae5e8e88a4a

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/api/go/char.go

@@ -0,0 +1,43 @@
+package z3
+
+/*
+#include "z3.h"
+*/
+import "C"
+
+// Char operations
+
+// MkCharSort creates the character sort (Unicode characters).
+func (c *Context) MkCharSort() *Sort {
+	return newSort(c, C.Z3_mk_char_sort(c.ptr))
+}
+
+// MkChar creates a character literal from a Unicode code point.
+func (c *Context) MkChar(ch uint) *Expr {
+	return newExpr(c, C.Z3_mk_char(c.ptr, C.uint(ch)))
+}
+
+// MkCharLe creates a character less-than-or-equal predicate (ch1 ≤ ch2).
+func (c *Context) MkCharLe(ch1, ch2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_char_le(c.ptr, ch1.ptr, ch2.ptr))
+}
+
+// MkCharToInt converts a character to its integer (Unicode code point) value.
+func (c *Context) MkCharToInt(ch *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_char_to_int(c.ptr, ch.ptr))
+}
+
+// MkCharToBV converts a character to a bit-vector.
+func (c *Context) MkCharToBV(ch *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_char_to_bv(c.ptr, ch.ptr))
+}
+
+// MkCharFromBV converts a bit-vector to a character.
+func (c *Context) MkCharFromBV(bv *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_char_from_bv(c.ptr, bv.ptr))
+}
+
+// MkCharIsDigit creates a predicate that is true if the character is a decimal digit.
+func (c *Context) MkCharIsDigit(ch *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_char_is_digit(c.ptr, ch.ptr))
+}

src/api/go/relations.go

@@ -0,0 +1,38 @@
+package z3
+
+/*
+#include "z3.h"
+*/
+import "C"
+
+// Special relation constructors
+
+// MkLinearOrder creates a linear (total) order relation over the given sort.
+// The id parameter distinguishes multiple linear orders over the same sort.
+func (c *Context) MkLinearOrder(s *Sort, id uint) *FuncDecl {
+	return newFuncDecl(c, C.Z3_mk_linear_order(c.ptr, s.ptr, C.uint(id)))
+}
+
+// MkPartialOrder creates a partial order relation over the given sort.
+// The id parameter distinguishes multiple partial orders over the same sort.
+func (c *Context) MkPartialOrder(s *Sort, id uint) *FuncDecl {
+	return newFuncDecl(c, C.Z3_mk_partial_order(c.ptr, s.ptr, C.uint(id)))
+}
+
+// MkPiecewiseLinearOrder creates a piecewise linear order relation over the given sort.
+// The id parameter distinguishes multiple piecewise linear orders over the same sort.
+func (c *Context) MkPiecewiseLinearOrder(s *Sort, id uint) *FuncDecl {
+	return newFuncDecl(c, C.Z3_mk_piecewise_linear_order(c.ptr, s.ptr, C.uint(id)))
+}
+
+// MkTreeOrder creates a tree order relation over the given sort.
+// The id parameter distinguishes multiple tree orders over the same sort.
+func (c *Context) MkTreeOrder(s *Sort, id uint) *FuncDecl {
+	return newFuncDecl(c, C.Z3_mk_tree_order(c.ptr, s.ptr, C.uint(id)))
+}
+
+// MkTransitiveClosure creates the transitive closure of a binary relation.
+// The resulting relation is recursive.
+func (c *Context) MkTransitiveClosure(f *FuncDecl) *FuncDecl {
+	return newFuncDecl(c, C.Z3_mk_transitive_closure(c.ptr, f.ptr))
+}

src/api/go/set.go

@@ -0,0 +1,77 @@
+package z3
+
+/*
+#include "z3.h"
+*/
+import "C"
+
+// Regular (array-encoded) Set operations
+
+// MkSetSort creates a set sort with the given element sort.
+func (c *Context) MkSetSort(elemSort *Sort) *Sort {
+	return newSort(c, C.Z3_mk_set_sort(c.ptr, elemSort.ptr))
+}
+
+// MkEmptySet creates an empty set of the given element sort.
+func (c *Context) MkEmptySet(elemSort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_empty_set(c.ptr, elemSort.ptr))
+}
+
+// MkFullSet creates the full set (universe) of the given element sort.
+func (c *Context) MkFullSet(elemSort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_full_set(c.ptr, elemSort.ptr))
+}
+
+// MkSetAdd adds an element to a set.
+func (c *Context) MkSetAdd(set, elem *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_set_add(c.ptr, set.ptr, elem.ptr))
+}
+
+// MkSetDel removes an element from a set.
+func (c *Context) MkSetDel(set, elem *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_set_del(c.ptr, set.ptr, elem.ptr))
+}
+
+// MkSetUnion creates the union of two or more sets.
+func (c *Context) MkSetUnion(sets ...*Expr) *Expr {
+	if len(sets) == 0 {
+		return nil
+	}
+	cSets := make([]C.Z3_ast, len(sets))
+	for i, s := range sets {
+		cSets[i] = s.ptr
+	}
+	return newExpr(c, C.Z3_mk_set_union(c.ptr, C.uint(len(sets)), &cSets[0]))
+}
+
+// MkSetIntersect creates the intersection of two or more sets.
+func (c *Context) MkSetIntersect(sets ...*Expr) *Expr {
+	if len(sets) == 0 {
+		return nil
+	}
+	cSets := make([]C.Z3_ast, len(sets))
+	for i, s := range sets {
+		cSets[i] = s.ptr
+	}
+	return newExpr(c, C.Z3_mk_set_intersect(c.ptr, C.uint(len(sets)), &cSets[0]))
+}
+
+// MkSetDifference creates the set difference (set1 \ set2).
+func (c *Context) MkSetDifference(set1, set2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_set_difference(c.ptr, set1.ptr, set2.ptr))
+}
+
+// MkSetComplement creates the complement of a set.
+func (c *Context) MkSetComplement(set *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_set_complement(c.ptr, set.ptr))
+}
+
+// MkSetMember creates a membership predicate: elem ∈ set.
+func (c *Context) MkSetMember(elem, set *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_set_member(c.ptr, elem.ptr, set.ptr))
+}
+
+// MkSetSubset creates a subset predicate: set1 ⊆ set2.
+func (c *Context) MkSetSubset(set1, set2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_set_subset(c.ptr, set1.ptr, set2.ptr))
+}

src/api/java/Context.java

@@ -4616,6 +4616,38 @@ public class Context implements AutoCloseable {
         );
     }
 
+    /**
+     * Creates a piecewise linear order.
+     * @param index The index of the order.
+     * @param sort The sort of the order.
+     */
+    public final <R extends Sort> FuncDecl<BoolSort> mkPiecewiseLinearOrder(R sort, int index) {
+        return (FuncDecl<BoolSort>) FuncDecl.create(
+                this,
+                Native.mkPiecewiseLinearOrder(
+                    nCtx(),
+                    sort.getNativeObject(),
+                    index
+                )
+        );
+    }
+
+    /**
+     * Creates a tree order.
+     * @param index The index of the order.
+     * @param sort The sort of the order.
+     */
+    public final <R extends Sort> FuncDecl<BoolSort> mkTreeOrder(R sort, int index) {
+        return (FuncDecl<BoolSort>) FuncDecl.create(
+                this,
+                Native.mkTreeOrder(
+                    nCtx(),
+                    sort.getNativeObject(),
+                    index
+                )
+        );
+    }
+
     /**
      * Return the nonzero subresultants of p and q with respect to the "variable" x.
      * Note that any subterm that cannot be viewed as a polynomial is assumed to be a variable.

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

@@ -1957,10 +1957,46 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel {
       return new FuncDeclImpl(check(Z3.mk_partial_order(contextPtr, sort.ptr, index)));
     }
 
+    function mkLinearOrder(sort: Sort<Name>, index: number): FuncDecl<Name> {
+      return new FuncDeclImpl(check(Z3.mk_linear_order(contextPtr, sort.ptr, index)));
+    }
+
+    function mkPiecewiseLinearOrder(sort: Sort<Name>, index: number): FuncDecl<Name> {
+      return new FuncDeclImpl(check(Z3.mk_piecewise_linear_order(contextPtr, sort.ptr, index)));
+    }
+
+    function mkTreeOrder(sort: Sort<Name>, index: number): FuncDecl<Name> {
+      return new FuncDeclImpl(check(Z3.mk_tree_order(contextPtr, sort.ptr, index)));
+    }
+
     function mkTransitiveClosure(f: FuncDecl<Name>): FuncDecl<Name> {
       return new FuncDeclImpl(check(Z3.mk_transitive_closure(contextPtr, f.ptr)));
     }
 
+    function mkChar(ch: number): Expr<Name> {
+      return new ExprImpl(check(Z3.mk_char(contextPtr, ch)));
+    }
+
+    function mkCharLe(ch1: Expr<Name>, ch2: Expr<Name>): Bool<Name> {
+      return new BoolImpl(check(Z3.mk_char_le(contextPtr, ch1.ast, ch2.ast)));
+    }
+
+    function mkCharToInt(ch: Expr<Name>): Arith<Name> {
+      return new ArithImpl(check(Z3.mk_char_to_int(contextPtr, ch.ast)));
+    }
+
+    function mkCharToBV(ch: Expr<Name>): Expr<Name> {
+      return new ExprImpl(check(Z3.mk_char_to_bv(contextPtr, ch.ast)));
+    }
+
+    function mkCharFromBV(bv: Expr<Name>): Expr<Name> {
+      return new ExprImpl(check(Z3.mk_char_from_bv(contextPtr, bv.ast)));
+    }
+
+    function mkCharIsDigit(ch: Expr<Name>): Bool<Name> {
+      return new BoolImpl(check(Z3.mk_char_is_digit(contextPtr, ch.ast)));
+    }
+
     async function polynomialSubresultants(
       p: Arith<Name>,
       q: Arith<Name>,
@@ -5490,7 +5526,16 @@ export function createApi(Z3: Z3Core, em?: any): Z3HighLevel {
       Full,
 
       mkPartialOrder,
+      mkLinearOrder,
+      mkPiecewiseLinearOrder,
+      mkTreeOrder,
       mkTransitiveClosure,
+      mkChar,
+      mkCharLe,
+      mkCharToInt,
+      mkCharToBV,
+      mkCharFromBV,
+      mkCharIsDigit,
       polynomialSubresultants,
     };
     cleanup.register(ctx, () => Z3.del_context(contextPtr));

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

@@ -933,6 +933,30 @@ export interface Context<Name extends string = 'main'> {
    */
   mkPartialOrder(sort: Sort<Name>, index: number): FuncDecl<Name>;
 
+  /**
+   * Create a linear (total) order relation over a sort.
+   * @param sort The sort of the relation
+   * @param index The index of the relation
+   * @category Operations
+   */
+  mkLinearOrder(sort: Sort<Name>, index: number): FuncDecl<Name>;
+
+  /**
+   * Create a piecewise linear order relation over a sort.
+   * @param sort The sort of the relation
+   * @param index The index of the relation
+   * @category Operations
+   */
+  mkPiecewiseLinearOrder(sort: Sort<Name>, index: number): FuncDecl<Name>;
+
+  /**
+   * Create a tree order relation over a sort.
+   * @param sort The sort of the relation
+   * @param index The index of the relation
+   * @category Operations
+   */
+  mkTreeOrder(sort: Sort<Name>, index: number): FuncDecl<Name>;
+
   /**
    * Create the transitive closure of a binary relation.
    * The resulting relation is recursive.
@@ -941,6 +965,49 @@ export interface Context<Name extends string = 'main'> {
    */
   mkTransitiveClosure(f: FuncDecl<Name>): FuncDecl<Name>;
 
+  /**
+   * Create a character literal from a Unicode code point.
+   * @param ch The Unicode code point
+   * @category Characters
+   */
+  mkChar(ch: number): Expr<Name>;
+
+  /**
+   * Create a character less-than-or-equal predicate (ch1 ≤ ch2).
+   * @param ch1 First character
+   * @param ch2 Second character
+   * @category Characters
+   */
+  mkCharLe(ch1: Expr<Name>, ch2: Expr<Name>): Bool<Name>;
+
+  /**
+   * Convert a character to its integer (Unicode code point) value.
+   * @param ch The character expression
+   * @category Characters
+   */
+  mkCharToInt(ch: Expr<Name>): Arith<Name>;
+
+  /**
+   * Convert a character to a bit-vector.
+   * @param ch The character expression
+   * @category Characters
+   */
+  mkCharToBV(ch: Expr<Name>): Expr<Name>;
+
+  /**
+   * Convert a bit-vector to a character.
+   * @param bv The bit-vector expression
+   * @category Characters
+   */
+  mkCharFromBV(bv: Expr<Name>): Expr<Name>;
+
+  /**
+   * Create a predicate that is true if the character is a decimal digit.
+   * @param ch The character expression
+   * @category Characters
+   */
+  mkCharIsDigit(ch: Expr<Name>): Bool<Name>;
+
   /**
    * Return the nonzero subresultants of p and q with respect to the "variable" x.
    * Note that any subterm that cannot be viewed as a polynomial is assumed to be a variable.

src/api/julia/z3jl.cpp

@@ -320,6 +320,20 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
     m.method("finite_set_map", &finite_set_map);
     m.method("finite_set_filter", &finite_set_filter);
     m.method("finite_set_range", &finite_set_range);
+    m.method("empty_set", &empty_set);
+    m.method("full_set", &full_set);
+    m.method("set_add", &set_add);
+    m.method("set_del", &set_del);
+    m.method("set_union", &set_union);
+    m.method("set_intersect", &set_intersect);
+    m.method("set_difference", &set_difference);
+    m.method("set_complement", &set_complement);
+    m.method("set_member", &set_member);
+    m.method("set_subset", &set_subset);
+    m.method("linear_order", &linear_order);
+    m.method("partial_order", &partial_order);
+    m.method("piecewise_linear_order", &piecewise_linear_order);
+    m.method("tree_order", &tree_order);
 
     // -------------------------------------------------------------------------
 
@@ -629,7 +643,13 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m)
         .MM(context, string_sort)
         .MM(context, seq_sort)
         .MM(context, re_sort)
+        .MM(context, char_sort)
         .MM(context, finite_set_sort)
+        .method("set_sort", [](context &c, sort s) {
+            Z3_sort r = Z3_mk_set_sort(c, s);
+            c.check_error();
+            return sort(c, r);
+        })
         .method("array_sort", static_cast<sort (context::*)(sort, sort)>(&context::array_sort))
         .method("array_sort", static_cast<sort (context::*)(sort_vector const&, sort)>(&context::array_sort))
         .method("fpa_sort", static_cast<sort (context::*)(unsigned, unsigned)>(&context::fpa_sort))

src/api/ml/z3.ml

@@ -1350,6 +1350,15 @@ struct
   let mk_range = Z3native.mk_finite_set_range
 end
 
+module SpecialRelation =
+struct
+  let mk_linear_order = Z3native.mk_linear_order
+  let mk_partial_order = Z3native.mk_partial_order
+  let mk_piecewise_linear_order = Z3native.mk_piecewise_linear_order
+  let mk_tree_order = Z3native.mk_tree_order
+  let mk_transitive_closure = Z3native.mk_transitive_closure
+end
+
 module FloatingPoint =
 struct
   module RoundingMode =

src/api/ml/z3.mli

@@ -2140,6 +2140,31 @@ sig
 
 end
 
+(** Special relation constructors *)
+module SpecialRelation :
+sig
+  (** Create a linear (total) order relation over the given sort.
+      The [id] parameter distinguishes multiple linear orders over the same sort. *)
+  val mk_linear_order : context -> Sort.sort -> int -> FuncDecl.func_decl
+
+  (** Create a partial order relation over the given sort.
+      The [id] parameter distinguishes multiple partial orders over the same sort. *)
+  val mk_partial_order : context -> Sort.sort -> int -> FuncDecl.func_decl
+
+  (** Create a piecewise linear order relation over the given sort.
+      The [id] parameter distinguishes multiple piecewise linear orders over the same sort. *)
+  val mk_piecewise_linear_order : context -> Sort.sort -> int -> FuncDecl.func_decl
+
+  (** Create a tree order relation over the given sort.
+      The [id] parameter distinguishes multiple tree orders over the same sort. *)
+  val mk_tree_order : context -> Sort.sort -> int -> FuncDecl.func_decl
+
+  (** Create the transitive closure of a binary relation.
+      The resulting relation is recursive. *)
+  val mk_transitive_closure : context -> FuncDecl.func_decl -> FuncDecl.func_decl
+
+end
+
 (** Floating-Point Arithmetic *)
 module FloatingPoint :
 sig