3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-15 17:49:59 +00:00

Add vector::resize tests including vector<rational>

Co-authored-by: levnach <5377127+levnach@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-03-11 23:54:01 +00:00
parent 385b11f55b
commit 01f9709ff6

View file

@ -17,8 +17,92 @@ Revision History:
--*/
#include "util/vector.h"
#include "util/rational.h"
#include <iostream>
static void tst_resize_rational() {
// grow from empty using default initialization (zero)
vector<rational> v;
v.resize(4);
ENSURE(v.size() == 4);
for (unsigned i = 0; i < 4; ++i)
ENSURE(v[i].is_zero());
// shrink: elements below new size are preserved
v.resize(2);
ENSURE(v.size() == 2);
for (unsigned i = 0; i < 2; ++i)
ENSURE(v[i].is_zero());
// grow with explicit value initialization
rational half(1, 2);
v.resize(6, half);
ENSURE(v.size() == 6);
for (unsigned i = 0; i < 2; ++i)
ENSURE(v[i].is_zero());
for (unsigned i = 2; i < 6; ++i)
ENSURE(v[i] == half);
// resize to same size is a no-op
rational three(3);
v.resize(6, three);
ENSURE(v.size() == 6);
for (unsigned i = 2; i < 6; ++i)
ENSURE(v[i] == half);
// resize to zero clears the vector
v.resize(0);
ENSURE(v.empty());
// grow again after being empty
rational neg(-7);
v.resize(3, neg);
ENSURE(v.size() == 3);
for (unsigned i = 0; i < 3; ++i)
ENSURE(v[i] == neg);
}
static void tst_resize() {
// grow from empty using default initialization
svector<int> v;
v.resize(5);
ENSURE(v.size() == 5);
ENSURE(v.capacity() >= 5);
for (unsigned i = 0; i < 5; ++i)
ENSURE(v[i] == 0);
// shrink: elements below new size are preserved, size shrinks
v.resize(3);
ENSURE(v.size() == 3);
for (unsigned i = 0; i < 3; ++i)
ENSURE(v[i] == 0);
// grow with explicit value initialization
v.resize(7, 42);
ENSURE(v.size() == 7);
for (unsigned i = 0; i < 3; ++i)
ENSURE(v[i] == 0);
for (unsigned i = 3; i < 7; ++i)
ENSURE(v[i] == 42);
// resize to same size is a no-op
v.resize(7, 99);
ENSURE(v.size() == 7);
for (unsigned i = 3; i < 7; ++i)
ENSURE(v[i] == 42);
// resize to zero clears the vector
v.resize(0);
ENSURE(v.empty());
ENSURE(v.size() == 0);
// grow again after being empty
v.resize(4, 10);
ENSURE(v.size() == 4);
for (unsigned i = 0; i < 4; ++i)
ENSURE(v[i] == 10);
}
static void tst1() {
svector<int> v1;
ENSURE(v1.empty());
@ -58,5 +142,7 @@ static void tst1() {
}
void tst_vector() {
tst_resize_rational();
tst_resize();
tst1();
}