From 5aac5c98b3e3cac7d9382b6fbd221fcddca4a7ff Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 11 Jan 2026 13:59:30 -0800 Subject: [PATCH] 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 --- src/api/c++/z3++.h | 43 +++++++++++++++++++++++++ src/api/dotnet/Context.cs | 38 ++++++++++++++++++++++ src/api/java/Context.java | 36 ++++++++++++++++++++- src/api/js/src/high-level/high-level.ts | 16 +++++++++ src/api/js/src/high-level/types.ts | 26 +++++++++++++++ 5 files changed, 158 insertions(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 6dd71655a..4f2e4a507 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -82,6 +82,36 @@ namespace z3 { inline void set_param(char const * param, int value) { auto str = std::to_string(value); Z3_global_param_set(param, str.c_str()); } inline void reset_params() { Z3_global_param_reset_all(); } + /** + \brief Return Z3 version number information. + */ + inline void get_version(unsigned& major, unsigned& minor, unsigned& build_number, unsigned& revision_number) { + Z3_get_version(&major, &minor, &build_number, &revision_number); + } + + /** + \brief Return a string that fully describes the version of Z3 in use. + */ + inline std::string get_full_version() { + return std::string(Z3_get_full_version()); + } + + /** + \brief Enable tracing messages tagged as \c tag when Z3 is compiled in debug mode. + It is a NOOP otherwise. + */ + inline void enable_trace(char const * tag) { + Z3_enable_trace(tag); + } + + /** + \brief Disable tracing messages tagged as \c tag when Z3 is compiled in debug mode. + It is a NOOP otherwise. + */ + inline void disable_trace(char const * tag) { + Z3_disable_trace(tag); + } + /** \brief Exception used to sign API usage errors. */ @@ -2315,6 +2345,19 @@ namespace z3 { return to_func_decl(a.ctx(), Z3_mk_tree_order(a.ctx(), a, index)); } + /** + \brief Return the nonzero subresultants of p and q with respect to the "variable" x. + + \pre p, q and x are Z3 expressions where p and q are arithmetic terms. + Note that, any subterm that cannot be viewed as a polynomial is assumed to be a variable. + */ + inline expr_vector polynomial_subresultants(expr const& p, expr const& q, expr const& x) { + check_context(p, q); check_context(p, x); + Z3_ast_vector r = Z3_polynomial_subresultants(p.ctx(), p, q, x); + p.check_error(); + return expr_vector(p.ctx(), r); + } + template<> class cast_ast { public: ast operator()(context & c, Z3_ast a) { return ast(c, a); } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 49f183428..df45378a4 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -4849,6 +4849,44 @@ namespace Microsoft.Z3 return a.NativeObject; } + /// + /// Create a partial order relation over a sort. + /// + /// The sort of the relation. + /// The index of the relation. + public FuncDecl MkPartialOrder(Sort a, uint index) + { + return new FuncDecl(this, Native.Z3_mk_partial_order(this.nCtx, a.NativeObject, index)); + } + + /// + /// Create the transitive closure of a binary relation. + /// + /// The resulting relation is recursive. + /// A binary relation represented as a function declaration. + public FuncDecl MkTransitiveClosure(FuncDecl f) + { + return new FuncDecl(this, Native.Z3_mk_transitive_closure(this.nCtx, f.NativeObject)); + } + + /// + /// Return the nonzero subresultants of p and q with respect to the "variable" x. + /// + /// + /// p, q and x are Z3 expressions where p and q are arithmetic terms. + /// Note that any subterm that cannot be viewed as a polynomial is assumed to be a variable. + /// + /// First arithmetic term. + /// Second arithmetic term. + /// The variable with respect to which subresultants are computed. + public ASTVector PolynomialSubresultants(Expr p, Expr q, Expr x) + { + CheckContextMatch(p); + CheckContextMatch(q); + CheckContextMatch(x); + return new ASTVector(this, Native.Z3_polynomial_subresultants(this.nCtx, p.NativeObject, q.NativeObject, x.NativeObject)); + } + /// /// Return a string describing all available parameters to Expr.Simplify. /// diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 9a8218537..fad1884c9 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -4291,7 +4291,7 @@ public class Context implements AutoCloseable { } /** - * Creates or a partial order. + * Creates a partial order. * @param index The index of the order. * @param sort The sort of the order. */ @@ -4306,6 +4306,40 @@ public class Context implements AutoCloseable { ); } + /** + * Create the transitive closure of a binary relation. + * The resulting relation is recursive. + * @param f function declaration of a binary relation + */ + public final FuncDecl mkTransitiveClosure(FuncDecl f) { + return (FuncDecl) FuncDecl.create( + this, + Native.mkTransitiveClosure( + nCtx(), + f.getNativeObject() + ) + ); + } + + /** + * 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 + */ + public final ASTVector polynomialSubresultants(Expr p, Expr q, Expr x) { + return new ASTVector( + this, + Native.polynomialSubresultants( + nCtx(), + p.getNativeObject(), + q.getNativeObject(), + x.getNativeObject() + ) + ); + } + /** * Wraps an AST. * Remarks: This function is used for transitions between diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 609cd350c..6998592e0 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/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, index: number): FuncDecl { + return new FuncDeclImpl(check(Z3.mk_partial_order(contextPtr, sort.ptr, index))); + } + + function mkTransitiveClosure(f: FuncDecl): FuncDecl { + return new FuncDeclImpl(check(Z3.mk_transitive_closure(contextPtr, f.ptr))); + } + + async function polynomialSubresultants(p: Arith, q: Arith, x: Arith): Promise>> { + const result = await Z3.polynomial_subresultants(contextPtr, p.ast, q.ast, x.ast); + return new AstVectorImpl(check(result)); + } + class AstImpl implements Ast { declare readonly __typename: Ast['__typename']; readonly ctx: Context; @@ -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; diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index f089482a4..54ed4ee1f 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -827,6 +827,32 @@ export interface Context { /** @category Operations */ isSubset>(a: SMTSet, b: SMTSet): Bool; + + /** + * 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, index: number): FuncDecl; + + /** + * 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): FuncDecl; + + /** + * 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, q: Arith, x: Arith): Promise>>; } export interface Ast {