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

@@ -188,6 +188,30 @@ public class Expr<R extends Sort> 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<R> 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<R>) 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}.
      * 

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<Name> {
+      declare readonly __typename: Fixedpoint['__typename'];
+
+      readonly ctx: Context<Name>;
+      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<Name>[]) {
+        constraints.forEach(constraint => {
+          _assertContext(constraint);
+          check(Z3.fixedpoint_assert(contextPtr, this.ptr, constraint.ast));
+        });
+      }
+
+      registerRelation(pred: FuncDecl<Name>): void {
+        _assertContext(pred);
+        check(Z3.fixedpoint_register_relation(contextPtr, this.ptr, pred.ptr));
+      }
+
+      addRule(rule: Bool<Name>, name?: string): void {
+        _assertContext(rule);
+        const symbol = _toSymbol(name ?? '');
+        check(Z3.fixedpoint_add_rule(contextPtr, this.ptr, rule.ast, symbol));
+      }
+
+      addFact(pred: FuncDecl<Name>, ...args: number[]): void {
+        _assertContext(pred);
+        check(Z3.fixedpoint_add_fact(contextPtr, this.ptr, pred.ptr, args));
+      }
+
+      updateRule(rule: Bool<Name>, name: string): void {
+        _assertContext(rule);
+        const symbol = _toSymbol(name);
+        check(Z3.fixedpoint_update_rule(contextPtr, this.ptr, rule.ast, symbol));
+      }
+
+      async query(query: Bool<Name>): Promise<CheckSatResult> {
+        _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<Name>[]): Promise<CheckSatResult> {
+        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<Name> | 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<Name>): number {
+        _assertContext(pred);
+        return check(Z3.fixedpoint_get_num_levels(contextPtr, this.ptr, pred.ptr));
+      }
+
+      getCoverDelta(level: number, pred: FuncDecl<Name>): Expr<Name> | 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<Name>, property: Expr<Name>): void {
+        _assertContext(pred);
+        _assertContext(property);
+        check(Z3.fixedpoint_add_cover(contextPtr, this.ptr, level, pred.ptr, property.ast));
+      }
+
+      getRules(): AstVector<Name, Bool<Name>> {
+        return new AstVectorImpl(check(Z3.fixedpoint_get_rules(contextPtr, this.ptr)));
+      }
+
+      getAssertions(): AstVector<Name, Bool<Name>> {
+        return new AstVectorImpl(check(Z3.fixedpoint_get_assertions(contextPtr, this.ptr)));
+      }
+
+      setPredicateRepresentation(pred: FuncDecl<Name>, 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<Name, Bool<Name>> {
+        const av = check(Z3.fixedpoint_from_string(contextPtr, this.ptr, s));
+        return new AstVectorImpl(av);
+      }
+
+      fromFile(file: string): AstVector<Name, Bool<Name>> {
+        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<Name> {
       declare readonly __typename: Model['__typename'];
       readonly ctx: Context<Name>;
@@ -3287,6 +3441,32 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       return _toExpr(check(Z3.substitute(contextPtr, t.ast, from, to)));
     }
 
+    function substituteVars(t: Expr<Name>, ...to: Expr<Name>[]): Expr<Name> {
+      _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<Name>,
+      ...substitutions: [FuncDecl<Name>, Expr<Name>][]
+    ): Expr<Name> {
+      _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<Name> {
       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<Name>,
@@ -3431,6 +3612,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       Extract,
 
       substitute,
+      substituteVars,
+      substituteFuns,
       simplify,
 
       /////////////

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<Name extends string = 'main'> {
 
   readonly Optimize: new () => Optimize<Name>;
 
+  readonly Fixedpoint: new () => Fixedpoint<Name>;
+
   /**
    * Creates an empty Model
    * @see {@link Solver.model} for common usage of Model
@@ -638,6 +641,12 @@ export interface Context<Name extends string = 'main'> {
   /** @category Operations */
   substitute(t: Expr<Name>, ...substitutions: [Expr<Name>, Expr<Name>][]): Expr<Name>;
 
+  /** @category Operations */
+  substituteVars(t: Expr<Name>, ...to: Expr<Name>[]): Expr<Name>;
+
+  /** @category Operations */
+  substituteFuns(t: Expr<Name>, ...substitutions: [FuncDecl<Name>, Expr<Name>][]): Expr<Name>;
+
   simplify(expr: Expr<Name>): Promise<Expr<Name>>;
 
   /** @category Operations */
@@ -1006,6 +1015,153 @@ export interface Optimize<Name extends string = 'main'> {
   release(): void;
 }
 
+export interface Fixedpoint<Name extends string = 'main'> {
+  /** @hidden */
+  readonly __typename: 'Fixedpoint';
+
+  readonly ctx: Context<Name>;
+  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<Name>[]): void;
+
+  /**
+   * Register a predicate as a recursive relation.
+   * @param pred - Function declaration to register as a recursive relation
+   */
+  registerRelation(pred: FuncDecl<Name>): 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>, 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<Name>, ...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>, 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<Name>): Promise<CheckSatResult>;
+
+  /**
+   * 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<Name>[]): Promise<CheckSatResult>;
+
+  /**
+   * 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<Name> | 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<Name>): 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<Name>): Expr<Name> | 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<Name>, property: Expr<Name>): void;
+
+  /**
+   * Retrieve set of rules added to the fixedpoint context.
+   * @returns Vector of rules
+   */
+  getRules(): AstVector<Name, Bool<Name>>;
+
+  /**
+   * Retrieve set of assertions added to the fixedpoint context.
+   * @returns Vector of assertions
+   */
+  getAssertions(): AstVector<Name, Bool<Name>>;
+
+  /**
+   * Set predicate representation for the Datalog engine.
+   * @param pred - The predicate function declaration
+   * @param kinds - Array of representation kinds
+   */
+  setPredicateRepresentation(pred: FuncDecl<Name>, 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<Name, Bool<Name>>;
+
+  /**
+   * 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<Name, Bool<Name>>;
+
+  /**
+   * 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<Name extends string> {
   new (): Model<Name>;