mirror of
https://github.com/Z3Prover/z3
synced 2026-01-21 01:24:43 +00:00
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>
This commit is contained in:
Copilot
GitHub
parent
495e1f44ba
commit
6d14d2e3b8
3 changed files with 363 additions and 0 deletions
|
|
@ -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}.
|
||||
*
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
||||
/////////////
|
||||
|
|
|
|||
|
|
@ -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>;
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue