diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2017-11-09 04:47:02 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-09 04:47:02 -0800 |
commit | a9cf481470c324a04f2254c5745eee26c45cb309 (patch) | |
tree | ad9065cae3e2728b41becc51697955e2ce8b26c1 /test/unit/util | |
parent | 9444927c027e96f0fce22398611b97c274eff6b3 (diff) |
Add modular arithmetic operators. (#1321)
This adds functions on Integers to compute modular addition, multiplication and inverse.
This is required for the Gaussian Elimination preprocessing pass for BV.
Diffstat (limited to 'test/unit/util')
-rw-r--r-- | test/unit/util/integer_black.h | 85 |
1 files changed, 85 insertions, 0 deletions
diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h index ac86051dd..c4c551363 100644 --- a/test/unit/util/integer_black.h +++ b/test/unit/util/integer_black.h @@ -471,4 +471,89 @@ public: Integer one_from_string(leadingZeroes,2); TS_ASSERT_EQUALS(one, one_from_string); } + + void testModAdd() + { + for (unsigned i = 0; i <= 10; ++i) + { + for (unsigned j = 0; j <= 10; ++j) + { + Integer yy; + Integer x(i); + Integer y = x + j; + Integer yp = x.modAdd(j, 3); + for (yy = y; yy >= 3; yy -= 3) + ; + TS_ASSERT(yp == yy); + yp = x.modAdd(j, 7); + for (yy = y; yy >= 7; yy -= 7) + ; + TS_ASSERT(yp == yy); + yp = x.modAdd(j, 11); + for (yy = y; yy >= 11; yy -= 11) + ; + TS_ASSERT(yp == yy); + } + } + } + + void testModMultiply() + { + for (unsigned i = 0; i <= 10; ++i) + { + for (unsigned j = 0; j <= 10; ++j) + { + Integer yy; + Integer x(i); + Integer y = x * j; + Integer yp = x.modMultiply(j, 3); + for (yy = y; yy >= 3; yy -= 3) + ; + TS_ASSERT(yp == yy); + yp = x.modMultiply(j, 7); + for (yy = y; yy >= 7; yy -= 7) + ; + TS_ASSERT(yp == yy); + yp = x.modMultiply(j, 11); + for (yy = y; yy >= 11; yy -= 11) + ; + TS_ASSERT(yp == yy); + } + } + } + + void testModInverse() + { + for (unsigned i = 0; i <= 10; ++i) + { + Integer x(i); + Integer inv = x.modInverse(3); + if (i == 0 || i == 3 || i == 6 || i == 9) + { + TS_ASSERT(inv == -1); /* no inverse */ + } + else + { + TS_ASSERT(x.modMultiply(inv, 3) == 1); + } + inv = x.modInverse(7); + if (i == 0 || i == 7) + { + TS_ASSERT(inv == -1); /* no inverse */ + } + else + { + TS_ASSERT(x.modMultiply(inv, 7) == 1); + } + inv = x.modInverse(11); + if (i == 0) + { + TS_ASSERT(inv == -1); /* no inverse */ + } + else + { + TS_ASSERT(x.modMultiply(inv, 11) == 1); + } + } + } }; |