From f99e1ee5816aa8645985a67e6e63f5822f2c818d Mon Sep 17 00:00:00 2001
From: Dmitri <dmitri666@gmail.com>
Date: Mon, 30 Dec 2024 18:49:30 +0200
Subject: [PATCH] Support BitVectors in the TypeScript Optimize API (#7480)
This is just a change in type declarations to allow calling minimize/maximize with BitVectors.
---
src/api/js/src/high-level/high-level.ts | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts
index 405d4a5e5a..177241bfd6 100644
--- a/src/api/js/src/high-level/high-level.ts
+++ b/src/api/js/src/high-level/high-level.ts
@@ -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));
}