mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

add apply_permutation tests (#7322)

Browse source 
* add permutation unit tests

* update test

* update

* Update permutation.cpp

fix macos build

* add apply_permutation tests

* update test

* Update permutation.cpp

* fix permutation tests

---------

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
LiviaSun 2024-08-02 18:29:33 -07:00 committed by GitHub
parent ea9fa17f86
commit fce4b36dad
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 49 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

84
src/test/permutation.cpp
View file

@ -2,10 +2,11 @@
#include <sstream> #include <sstream>
#include "util/permutation.h" #include "util/permutation.h"
#include "util/util.h" #include "util/util.h"
#include "util/debug.h"
void swap(unsigned m1, unsigned m2) noexcept { std::swap(m1, m2); } void swap(unsigned m1, unsigned m2) noexcept { std::swap(m1, m2); }
void test_constructor() { static void test_constructor() {
permutation p(5); permutation p(5);
for (unsigned i = 0; i < 5; ++i) { for (unsigned i = 0; i < 5; ++i) {
SASSERT(p(i) == i); SASSERT(p(i) == i);
@ -13,7 +14,7 @@ void test_constructor() {
} }
} }
void test_reset() { static void test_reset() {
permutation p(3); permutation p(3);
p.swap(0, 2); p.swap(0, 2);
p.reset(3); p.reset(3);
@ -23,7 +24,7 @@ void test_reset() {
} }
} }
void test_swap() { static void test_swap() {
permutation p(4); permutation p(4);
p.swap(1, 3); p.swap(1, 3);
SASSERT(p(1) == 3); SASSERT(p(1) == 3);
@ -32,7 +33,7 @@ void test_swap() {
SASSERT(p.inv(3) == 1); SASSERT(p.inv(3) == 1);
} }
void test_move_after() { static void test_move_after() {
permutation p(5); permutation p(5);
p.move_after(1, 3); p.move_after(1, 3);
SASSERT(p(0) == 0); SASSERT(p(0) == 0);
@ -42,36 +43,36 @@ void test_move_after() {
SASSERT(p(4) == 4); SASSERT(p(4) == 4);
} }
void test_apply_permutation() { void apply_permutation_copy(unsigned sz, unsigned const * src, unsigned const * p, unsigned * target) {
permutation p(4); for (unsigned i = 0; i < sz; i++) {
int data[] = {10, 20, 30, 40}; target[i] = src[p[i]];
unsigned perm[] = {2, 1, 0, 3}; }
apply_permutation(4, data, perm);
std::cout << "000 " << data[0] << std::endl;
std::cout << "222 " << data[2] << std::endl;
SASSERT(data[0] == 10);
SASSERT(data[1] == 20);
SASSERT(data[2] == 30);
SASSERT(data[3] == 40);
} }
void test_apply_permutation_core() static void test_apply_permutation(unsigned sz, unsigned num_tries, unsigned max = UINT_MAX) {
{ unsigned_vector data;
permutation p(4); unsigned_vector p;
int data[] = {10, 20, 30, 40}; unsigned_vector new_data;
unsigned perm[] = {2, 1, 0, 3}; data.resize(sz);
apply_permutation_core(4, data, perm); p.resize(sz);
std::cout << "000 " << data[0] << std::endl; new_data.resize(sz);
std::cout << "222 " << data[2] << std::endl; random_gen g;
for (unsigned i = 0; i < sz; i++)
SASSERT(data[0] == 10); p[i] = i;
SASSERT(data[1] == 20); // fill data with random numbers
SASSERT(data[2] == 30); for (unsigned i = 0; i < sz; i++)
SASSERT(data[3] == 40); data[i] = g() % max;
for (unsigned k = 0; k < num_tries; k ++) {
shuffle(p.size(), p.data(), g);
apply_permutation_copy(sz, data.data(), p.data(), new_data.data());
apply_permutation(sz, data.data(), p.data());
for (unsigned i = 0; i < 0; i++)
ENSURE(data[i] == new_data[i]);
}
} }
void test_check_invariant() {
static void test_check_invariant() {
permutation p(4); permutation p(4);
SASSERT(p.check_invariant()); SASSERT(p.check_invariant());
p.swap(0, 2); p.swap(0, 2);
@ -80,7 +81,7 @@ void test_check_invariant() {
SASSERT(p.check_invariant()); SASSERT(p.check_invariant());
} }
void test_display() { static void test_display() {
permutation p(4); permutation p(4);
std::ostringstream out; std::ostringstream out;
p.display(out); p.display(out);
@ -92,10 +93,23 @@ void tst_permutation() {
test_reset(); test_reset();
test_swap(); test_swap();
test_move_after(); test_move_after();
// test_apply_permutation();
// test_apply_permutation_core();
test_check_invariant(); test_check_invariant();
test_display(); test_display();
test_apply_permutation(10, 1000, 5);
test_apply_permutation(10, 1000, 1000);
test_apply_permutation(10, 1000, UINT_MAX);
test_apply_permutation(100, 1000, 33);
test_apply_permutation(100, 1000, 1000);
test_apply_permutation(100, 1000, UINT_MAX);
test_apply_permutation(1000, 1000, 121);
test_apply_permutation(1000, 1000, 1000);
test_apply_permutation(1000, 1000, UINT_MAX);
test_apply_permutation(33, 1000, 121);
test_apply_permutation(33, 1000, 1000);
test_apply_permutation(33, 1000, UINT_MAX);
test_apply_permutation(121, 1000, 121);
test_apply_permutation(121, 1000, 1000);
test_apply_permutation(121, 1000, UINT_MAX);
std::cout << "All tests passed!" << std::endl; std::cout << "All tests passed!" << std::endl;
} }