3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00

Support BitVectors in the TypeScript Optimize API (#7480)

This is just a change in type declarations to allow calling minimize/maximize with BitVectors.
This commit is contained in:
Dmitri 2024-12-30 18:49:30 +02:00 committed by GitHub
parent 19c95f8561
commit f99e1ee581
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -1524,11 +1524,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
return new AstVectorImpl(check(Z3.optimize_get_assertions(contextPtr, this.ptr)));
}
maximize(expr: Arith<Name>) {
maximize(expr: Arith<Name> | BitVec<number, Name>) {
check(Z3.optimize_maximize(contextPtr, this.ptr, expr.ast));
}
minimize(expr: Arith<Name>) {
minimize(expr: Arith<Name> | BitVec<number, Name>) {
check(Z3.optimize_minimize(contextPtr, this.ptr, expr.ast));
}