From 443683c51e98a8706a9e70f1c9289b209261537a Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Thu, 25 Apr 2024 08:50:06 -0700 Subject: [PATCH] Add Vec API (#876) --- Source/Core/base.bpl | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl index e97e858e3..11adac487 100644 --- a/Source/Core/base.bpl +++ b/Source/Core/base.bpl @@ -126,11 +126,17 @@ function {:inline} Vec_Swap(v: Vec T, i: int, j: int): Vec T ) } -function {:inline} Vec_Remove(v: Vec T): Vec T { - ( - var cond, new_len := 0 < v->len, v->len - 1; - Vec(v->contents[new_len := if (cond) then Default() else v->contents[new_len]], if (cond) then new_len else v->len) - ) +function {:inline} Vec_Remove(v: Vec T): Vec T +{ + ( + var cond, new_len := 0 < v->len, v->len - 1; + Vec(v->contents[new_len := if (cond) then Default() else v->contents[new_len]], if (cond) then new_len else v->len) + ) +} + +function {:inline} Vec_Contains(v: Vec T, i: int): bool +{ + 0 <= i && i < Vec_Len(v) } // extensionality lemma to be used explicitly by the programmer