Add missing API functions to C++, Java, C#, and TypeScript bindings (#8152)

* Initial plan

* Add missing API functions to C++, Java, C#, and TypeScript bindings

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

* Fix TypeScript type errors in new API functions

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

* Address code review comments and add documentation

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

* Fix TypeScript async issue in polynomialSubresultants

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

* Delete API_COHERENCE_FIXES.md

---------

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

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

@@ -1732,6 +1732,19 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       return new BoolImpl(check(Z3.mk_set_subset(contextPtr, a.ast, b.ast)));
     }
 
+    function mkPartialOrder(sort: Sort<Name>, index: number): FuncDecl<Name> {
+      return new FuncDeclImpl(check(Z3.mk_partial_order(contextPtr, sort.ptr, index)));
+    }
+
+    function mkTransitiveClosure(f: FuncDecl<Name>): FuncDecl<Name> {
+      return new FuncDeclImpl(check(Z3.mk_transitive_closure(contextPtr, f.ptr)));
+    }
+
+    async function polynomialSubresultants(p: Arith<Name>, q: Arith<Name>, x: Arith<Name>): Promise<AstVector<Name, Arith<Name>>> {
+      const result = await Z3.polynomial_subresultants(contextPtr, p.ast, q.ast, x.ast);
+      return new AstVectorImpl<ArithImpl>(check(result));
+    }
+
     class AstImpl<Ptr extends Z3_ast> implements Ast<Name, Ptr> {
       declare readonly __typename: Ast['__typename'];
       readonly ctx: Context<Name>;
@@ -4632,6 +4645,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       FullSet,
       isMember,
       isSubset,
+      mkPartialOrder,
+      mkTransitiveClosure,
+      polynomialSubresultants,
     };
     cleanup.register(ctx, () => Z3.del_context(contextPtr));
     return ctx;

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

@@ -827,6 +827,32 @@ export interface Context<Name extends string = 'main'> {
 
   /** @category Operations */
   isSubset<ElemSort extends AnySort<Name>>(a: SMTSet<Name, ElemSort>, b: SMTSet<Name, ElemSort>): Bool<Name>;
+
+  /**
+   * Create a partial order relation over a sort.
+   * @param sort The sort of the relation
+   * @param index The index of the relation
+   * @category Operations
+   */
+  mkPartialOrder(sort: Sort<Name>, index: number): FuncDecl<Name>;
+
+  /**
+   * Create the transitive closure of a binary relation.
+   * The resulting relation is recursive.
+   * @param f A binary relation represented as a function declaration
+   * @category Operations
+   */
+  mkTransitiveClosure(f: FuncDecl<Name>): FuncDecl<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.
+   * @param p Arithmetic term
+   * @param q Arithmetic term
+   * @param x Variable with respect to which subresultants are computed
+   * @category Operations
+   */
+  polynomialSubresultants(p: Arith<Name>, q: Arith<Name>, x: Arith<Name>): Promise<AstVector<Name, Arith<Name>>>;
 }
 
 export interface Ast<Name extends string = 'main', Ptr = unknown> {