mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-20 23:56:37 +00:00
Code Activity

Add check for arg length

Browse source
This commit is contained in:
Jonas Jongejan 2024-10-19 13:23:29 -04:00
parent b28c86132e
commit d4f46b5ad2
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/api/js/src/high-level/high-level.ts
View file

@ -959,6 +959,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
function PbEq(args: [Bool<Name>, ...Bool<Name>[]], coeffs: [number, ...number[]], k: number): Bool<Name> {
_assertContext(...args);
if (args.length !== coeffs.length) {
throw new Error('Number of arguments and coefficients must match');
}
return new BoolImpl(
check(
Z3.mk_pbeq(
@ -973,6 +976,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
function PbGe(args: [Bool<Name>, ...Bool<Name>[]], coeffs: [number, ...number[]], k: number): Bool<Name> {
_assertContext(...args);
if (args.length !== coeffs.length) {
throw new Error('Number of arguments and coefficients must match');
}
return new BoolImpl(
check(
Z3.mk_pbge(
@ -987,6 +993,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
function PbLe(args: [Bool<Name>, ...Bool<Name>[]], coeffs: [number, ...number[]], k: number): Bool<Name> {
_assertContext(...args);
if (args.length !== coeffs.length) {
throw new Error('Number of arguments and coefficients must match');
}
return new BoolImpl(
check(
Z3.mk_pble(