From 6d14d2e3b86b58a1f5bb1a40c1cc7820c1fb6e34 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sat, 10 Jan 2026 12:04:50 -0800 Subject: [PATCH] Add missing API methods: Java substituteFuns, TypeScript Fixedpoint and substitution APIs (#8138) * Initial plan * Add substituteFuns to Java and substitute methods to TypeScript Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add Fixedpoint (Datalog) API to TypeScript bindings Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Improve error message in Java substituteFuns method Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix TypeScript build error: use .ptr instead of .decl for FuncDecl Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Fix TypeScript build errors: handle optional symbols and pointer null checks 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> --- src/api/java/Expr.java | 24 ++++ src/api/js/src/high-level/high-level.ts | 183 ++++++++++++++++++++++++ src/api/js/src/high-level/types.ts | 156 ++++++++++++++++++++ 3 files changed, 363 insertions(+) diff --git a/src/api/java/Expr.java b/src/api/java/Expr.java index 910869bcd..b15624871 100644 --- a/src/api/java/Expr.java +++ b/src/api/java/Expr.java @@ -188,6 +188,30 @@ public class Expr extends AST getNativeObject(), to.length, Expr.arrayToNative(to))); } + /** + * Substitute functions in {@code from} with the expressions in {@code to}. + * The expressions in {@code to} can have free variables. The free variable + * in {@code to[i]} at de-Bruijn index 0 refers to the first argument of + * {@code from[i]}, the free variable at index 1 corresponds to the second + * argument, and so on. + * Remarks: The arrays {@code from} and {@code to} must have the same size. + * @param from Array of function declarations to be substituted + * @param to Array of expressions to substitute with + * @throws Z3Exception on error + * @return an Expr + **/ + public Expr substituteFuns(FuncDecl[] from, Expr[] to) + { + getContext().checkContextMatch(from); + getContext().checkContextMatch(to); + if (from.length != to.length) { + throw new Z3Exception("Arrays 'from' and 'to' must have the same length"); + } + return (Expr) Expr.create(getContext(), Native.substituteFuns(getContext().nCtx(), + getNativeObject(), from.length, AST.arrayToNative(from), + Expr.arrayToNative(to))); + } + /** * Translates (copies) the term to the Context {@code ctx}. * diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 517bbe50e..f8d2ef12c 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -38,6 +38,7 @@ import { Z3_params, Z3_func_entry, Z3_optimize, + Z3_fixedpoint, } from '../low-level'; import { AnyAst, @@ -66,6 +67,7 @@ import { Context, ContextCtor, Expr, + Fixedpoint, FuncDecl, FuncDeclSignature, FuncInterp, @@ -1694,6 +1696,158 @@ export function createApi(Z3: Z3Core): Z3HighLevel { } } + class FixedpointImpl implements Fixedpoint { + declare readonly __typename: Fixedpoint['__typename']; + + readonly ctx: Context; + private _ptr: Z3_fixedpoint | null; + get ptr(): Z3_fixedpoint { + _assertPtr(this._ptr); + return this._ptr; + } + + constructor(ptr: Z3_fixedpoint = Z3.mk_fixedpoint(contextPtr)) { + this.ctx = ctx; + let myPtr: Z3_fixedpoint; + myPtr = ptr; + this._ptr = myPtr; + Z3.fixedpoint_inc_ref(contextPtr, myPtr); + cleanup.register(this, () => Z3.fixedpoint_dec_ref(contextPtr, myPtr), this); + } + + set(key: string, value: any): void { + Z3.fixedpoint_set_params(contextPtr, this.ptr, _toParams(key, value)); + } + + help(): string { + return check(Z3.fixedpoint_get_help(contextPtr, this.ptr)); + } + + add(...constraints: Bool[]) { + constraints.forEach(constraint => { + _assertContext(constraint); + check(Z3.fixedpoint_assert(contextPtr, this.ptr, constraint.ast)); + }); + } + + registerRelation(pred: FuncDecl): void { + _assertContext(pred); + check(Z3.fixedpoint_register_relation(contextPtr, this.ptr, pred.ptr)); + } + + addRule(rule: Bool, name?: string): void { + _assertContext(rule); + const symbol = _toSymbol(name ?? ''); + check(Z3.fixedpoint_add_rule(contextPtr, this.ptr, rule.ast, symbol)); + } + + addFact(pred: FuncDecl, ...args: number[]): void { + _assertContext(pred); + check(Z3.fixedpoint_add_fact(contextPtr, this.ptr, pred.ptr, args)); + } + + updateRule(rule: Bool, name: string): void { + _assertContext(rule); + const symbol = _toSymbol(name); + check(Z3.fixedpoint_update_rule(contextPtr, this.ptr, rule.ast, symbol)); + } + + async query(query: Bool): Promise { + _assertContext(query); + const result = await asyncMutex.runExclusive(() => + check(Z3.fixedpoint_query(contextPtr, this.ptr, query.ast)), + ); + switch (result) { + case Z3_lbool.Z3_L_FALSE: + return 'unsat'; + case Z3_lbool.Z3_L_TRUE: + return 'sat'; + case Z3_lbool.Z3_L_UNDEF: + return 'unknown'; + default: + assertExhaustive(result); + } + } + + async queryRelations(...relations: FuncDecl[]): Promise { + relations.forEach(rel => _assertContext(rel)); + const decls = relations.map(rel => rel.ptr); + const result = await asyncMutex.runExclusive(() => + check(Z3.fixedpoint_query_relations(contextPtr, this.ptr, decls)), + ); + switch (result) { + case Z3_lbool.Z3_L_FALSE: + return 'unsat'; + case Z3_lbool.Z3_L_TRUE: + return 'sat'; + case Z3_lbool.Z3_L_UNDEF: + return 'unknown'; + default: + assertExhaustive(result); + } + } + + getAnswer(): Expr | null { + const ans = check(Z3.fixedpoint_get_answer(contextPtr, this.ptr)); + return ans ? _toExpr(ans) : null; + } + + getReasonUnknown(): string { + return check(Z3.fixedpoint_get_reason_unknown(contextPtr, this.ptr)); + } + + getNumLevels(pred: FuncDecl): number { + _assertContext(pred); + return check(Z3.fixedpoint_get_num_levels(contextPtr, this.ptr, pred.ptr)); + } + + getCoverDelta(level: number, pred: FuncDecl): Expr | null { + _assertContext(pred); + const res = check(Z3.fixedpoint_get_cover_delta(contextPtr, this.ptr, level, pred.ptr)); + return res ? _toExpr(res) : null; + } + + addCover(level: number, pred: FuncDecl, property: Expr): void { + _assertContext(pred); + _assertContext(property); + check(Z3.fixedpoint_add_cover(contextPtr, this.ptr, level, pred.ptr, property.ast)); + } + + getRules(): AstVector> { + return new AstVectorImpl(check(Z3.fixedpoint_get_rules(contextPtr, this.ptr))); + } + + getAssertions(): AstVector> { + return new AstVectorImpl(check(Z3.fixedpoint_get_assertions(contextPtr, this.ptr))); + } + + setPredicateRepresentation(pred: FuncDecl, kinds: string[]): void { + _assertContext(pred); + const symbols = kinds.map(kind => _toSymbol(kind)); + check(Z3.fixedpoint_set_predicate_representation(contextPtr, this.ptr, pred.ptr, symbols)); + } + + toString(): string { + return check(Z3.fixedpoint_to_string(contextPtr, this.ptr, [])); + } + + fromString(s: string): AstVector> { + const av = check(Z3.fixedpoint_from_string(contextPtr, this.ptr, s)); + return new AstVectorImpl(av); + } + + fromFile(file: string): AstVector> { + const av = check(Z3.fixedpoint_from_file(contextPtr, this.ptr, file)); + return new AstVectorImpl(av); + } + + release() { + Z3.fixedpoint_dec_ref(contextPtr, this.ptr); + this._ptr = null; + cleanup.unregister(this); + } + } + class ModelImpl implements Model { declare readonly __typename: Model['__typename']; readonly ctx: Context; @@ -3287,6 +3441,32 @@ export function createApi(Z3: Z3Core): Z3HighLevel { return _toExpr(check(Z3.substitute(contextPtr, t.ast, from, to))); } + function substituteVars(t: Expr, ...to: Expr[]): Expr { + _assertContext(t); + const toAsts: Z3_ast[] = []; + for (const expr of to) { + _assertContext(expr); + toAsts.push(expr.ast); + } + return _toExpr(check(Z3.substitute_vars(contextPtr, t.ast, toAsts))); + } + + function substituteFuns( + t: Expr, + ...substitutions: [FuncDecl, Expr][] + ): Expr { + _assertContext(t); + const from: Z3_func_decl[] = []; + const to: Z3_ast[] = []; + for (const [f, body] of substitutions) { + _assertContext(f); + _assertContext(body); + from.push(f.ptr); + to.push(body.ast); + } + return _toExpr(check(Z3.substitute_funs(contextPtr, t.ast, from, to))); + } + function ast_from_string(s: string): Ast { const sort_names: Z3_symbol[] = []; const sorts: Z3_sort[] = []; @@ -3308,6 +3488,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel { ///////////// Solver: SolverImpl, Optimize: OptimizeImpl, + Fixedpoint: FixedpointImpl, Model: ModelImpl, Tactic: TacticImpl, AstVector: AstVectorImpl as AstVectorCtor, @@ -3431,6 +3612,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel { Extract, substitute, + substituteVars, + substituteFuns, simplify, ///////////// diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index c52edf001..ffc7aecc3 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -6,6 +6,7 @@ import { Z3_constructor, Z3_constructor_list, Z3_decl_kind, + Z3_fixedpoint, Z3_func_decl, Z3_func_entry, Z3_func_interp, @@ -333,6 +334,8 @@ export interface Context { readonly Optimize: new () => Optimize; + readonly Fixedpoint: new () => Fixedpoint; + /** * Creates an empty Model * @see {@link Solver.model} for common usage of Model @@ -638,6 +641,12 @@ export interface Context { /** @category Operations */ substitute(t: Expr, ...substitutions: [Expr, Expr][]): Expr; + /** @category Operations */ + substituteVars(t: Expr, ...to: Expr[]): Expr; + + /** @category Operations */ + substituteFuns(t: Expr, ...substitutions: [FuncDecl, Expr][]): Expr; + simplify(expr: Expr): Promise>; /** @category Operations */ @@ -1006,6 +1015,153 @@ export interface Optimize { release(): void; } +export interface Fixedpoint { + /** @hidden */ + readonly __typename: 'Fixedpoint'; + + readonly ctx: Context; + readonly ptr: Z3_fixedpoint; + + /** + * Set a configuration option for the fixedpoint solver. + * @param key - Configuration parameter name + * @param value - Configuration parameter value + */ + set(key: string, value: any): void; + + /** + * Return a string describing all available options. + */ + help(): string; + + /** + * Assert a constraint (or multiple) into the fixedpoint solver as background axioms. + */ + add(...constraints: Bool[]): void; + + /** + * Register a predicate as a recursive relation. + * @param pred - Function declaration to register as a recursive relation + */ + registerRelation(pred: FuncDecl): void; + + /** + * Add a rule (Horn clause) to the fixedpoint solver. + * @param rule - The rule as a Boolean expression (implication) + * @param name - Optional name for the rule + */ + addRule(rule: Bool, name?: string): void; + + /** + * Add a table fact to the fixedpoint solver. + * @param pred - The predicate (function declaration) + * @param args - Arguments to the predicate as integers + */ + addFact(pred: FuncDecl, ...args: number[]): void; + + /** + * Update a named rule in the fixedpoint solver. + * @param rule - The rule as a Boolean expression (implication) + * @param name - Name of the rule to update + */ + updateRule(rule: Bool, name: string): void; + + /** + * Query the fixedpoint solver to determine if the formula is derivable. + * @param query - The query as a Boolean expression + * @returns A promise that resolves to 'sat', 'unsat', or 'unknown' + */ + query(query: Bool): Promise; + + /** + * Query the fixedpoint solver for a set of relations. + * @param relations - Array of function declarations representing relations to query + * @returns A promise that resolves to 'sat', 'unsat', or 'unknown' + */ + queryRelations(...relations: FuncDecl[]): Promise; + + /** + * Retrieve the answer (satisfying instance or proof of unsatisfiability) from the last query. + * @returns Expression containing the answer, or null if not available + */ + getAnswer(): Expr | null; + + /** + * Retrieve the reason why the fixedpoint engine returned 'unknown'. + * @returns A string explaining why the result was unknown + */ + getReasonUnknown(): string; + + /** + * Retrieve the number of levels explored for a given predicate. + * @param pred - The predicate function declaration + * @returns The number of levels + */ + getNumLevels(pred: FuncDecl): number; + + /** + * Retrieve the cover of a predicate at a given level. + * @param level - The level to query + * @param pred - The predicate function declaration + * @returns Expression representing the cover, or null if not available + */ + getCoverDelta(level: number, pred: FuncDecl): Expr | null; + + /** + * Add a property about the predicate at the given level. + * @param level - The level to add the property at + * @param pred - The predicate function declaration + * @param property - The property as an expression + */ + addCover(level: number, pred: FuncDecl, property: Expr): void; + + /** + * Retrieve set of rules added to the fixedpoint context. + * @returns Vector of rules + */ + getRules(): AstVector>; + + /** + * Retrieve set of assertions added to the fixedpoint context. + * @returns Vector of assertions + */ + getAssertions(): AstVector>; + + /** + * Set predicate representation for the Datalog engine. + * @param pred - The predicate function declaration + * @param kinds - Array of representation kinds + */ + setPredicateRepresentation(pred: FuncDecl, kinds: string[]): void; + + /** + * Convert the fixedpoint context to a string. + * @returns String representation of the fixedpoint context + */ + toString(): string; + + /** + * Parse an SMT-LIB2 string with fixedpoint rules and add them to the context. + * @param s - SMT-LIB2 string to parse + * @returns Vector of queries from the parsed string + */ + fromString(s: string): AstVector>; + + /** + * Parse an SMT-LIB2 file with fixedpoint rules and add them to the context. + * @param file - Path to the file to parse + * @returns Vector of queries from the parsed file + */ + fromFile(file: string): AstVector>; + + /** + * Manually decrease the reference count of the fixedpoint + * This is automatically done when the fixedpoint is garbage collected, + * but calling this eagerly can help release memory sooner. + */ + release(): void; +} + /** @hidden */ export interface ModelCtor { new (): Model;