mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

Add matrix operations needed for implementing non-naive sign determination

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-08 17:58:34 -08:00
parent ff809db16d
commit 9c8b428ffb
3 changed files with 644 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

86
src/test/rcf.cpp
View file

@ -17,6 +17,7 @@ Notes:
--*/
#include"realclosure.h"
#include"mpz_matrix.h"
static void tst1() {
unsynch_mpq_manager qm;
@ -66,6 +67,87 @@ static void tst1() {
std::cout << interval_pp((a + eps)/(a - eps)) << std::endl;
}
void tst_rcf() {
tst1();
static void tst2() {
enable_trace("mpz_matrix");
unsynch_mpq_manager nm;
small_object_allocator allocator;
mpz_matrix_manager mm(nm, allocator);
scoped_mpz_matrix A(mm);
mm.mk(3, 3, A);
// Matrix
// 1 1 1
// 0 1 -1
// 0 1 1
A.set(0, 0, 1); A.set(0, 1, 1); A.set(0, 2, 1);
A.set(1, 0, 0); A.set(1, 1, 1); A.set(1, 2, -1);
A.set(2, 0, 0); A.set(2, 1, 1); A.set(2, 2, 1);
std::cout << A;
{
int b[3];
int c[3] = { 10, -2, 8 };
std::cout << "solve: " << mm.solve(A, b, c) << "\n";
for (unsigned i = 0; i < 3; i++) std::cout << b[i] << " ";
std::cout << "\n";
}
scoped_mpz_matrix A2(mm);
mm.tensor_product(A, A, A2);
std::cout << A2;
scoped_mpz_matrix B(mm);
unsigned cols[] = { 1, 3, 7, 8 };
mm.filter_cols(A2, 4, cols, B);
std::cout << B;
scoped_mpz_matrix C(mm);
unsigned perm[] = { 8, 7, 6, 5, 4, 3, 2, 1, 0 };
mm.permute_rows(B, perm, C);
std::cout << C;
}
static void tst_solve(unsigned n, int _A[], int _b[], int _c[], bool solved) {
unsynch_mpq_manager nm;
small_object_allocator allocator;
mpz_matrix_manager mm(nm, allocator);
scoped_mpz_matrix A(mm);
mm.mk(n, n, A);
for (unsigned i = 0; i < n; i++)
for (unsigned j = 0; j < n; j++)
A.set(i, j, _A[i*n + j]);
svector<int> b;
b.resize(n, 0);
if (mm.solve(A, b.c_ptr(), _c)) {
SASSERT(solved);
for (unsigned i = 0; i < n; i++) {
SASSERT(b[i] == _b[i]);
}
}
else {
SASSERT(!solved);
}
}
static void tst_lin_indep(unsigned m, unsigned n, int _A[], unsigned ex_sz, unsigned ex_r[]) {
unsynch_mpq_manager nm;
small_object_allocator allocator;
mpz_matrix_manager mm(nm, allocator);
scoped_mpz_matrix A(mm);
mm.mk(m, n, A);
for (unsigned i = 0; i < m; i++)
for (unsigned j = 0; j < n; j++)
A.set(i, j, _A[i*n + j]);
unsigned_vector r;
mm.linear_independent_rows(A, r);
SASSERT(r.size() == ex_sz);
for (unsigned i = 0; i < ex_sz; i++) {
SASSERT(r[i] == ex_r[i]);
}
}
void tst_rcf() {
// tst1();
tst2();
{ int A[] = {0, 1, 1, 1, 0, 1, 1, 1, -1}; int c[] = {10, 4, -4}; int b[] = {-2, 4, 6}; tst_solve(3, A, b, c, true); }
{ int A[] = {1, 1, 1, 0, 1, 1, 0, 1, 1}; int c[] = {3, 2, 2}; int b[] = {1, 1, 1}; tst_solve(3, A, b, c, false); }
{ int A[] = {1, 1, 1, 0, 1, 1, 0, 1, 1, 1, 1, 1, 1, 0, -1}; unsigned r[] = {0, 1, 4}; tst_lin_indep(5, 3, A, 3, r); }
{ int A[] = {1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, -1}; unsigned r[] = {0, 4}; tst_lin_indep(5, 3, A, 2, r); }
{ int A[] = {1, 1, 1, 1, 1, 1, 1, 0, 1, 2, 1, 2, 3, 1, 3}; unsigned r[] = {0, 2}; tst_lin_indep(5, 3, A, 2, r); }
}