From 75eca46d93b140667bbd36fa4bb900f5ebf89e39 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Feb 2013 17:32:27 -0800 Subject: [PATCH] added Karr test Signed-off-by: Nikolaj Bjorner --- src/muz_qe/heap_trie.h | 8 +- src/muz_qe/hilbert_basis.cpp | 19 +++- src/test/heap_trie.cpp | 1 + src/test/hilbert_basis.cpp | 5 +- src/test/karr.cpp | 213 +++++++++++++++++++++++++++++++++++ src/test/main.cpp | 1 + 6 files changed, 238 insertions(+), 9 deletions(-) create mode 100644 src/test/karr.cpp diff --git a/src/muz_qe/heap_trie.h b/src/muz_qe/heap_trie.h index e50a85505..a99861359 100644 --- a/src/muz_qe/heap_trie.h +++ b/src/muz_qe/heap_trie.h @@ -518,7 +518,7 @@ private: SASSERT(m_keys.size() == num_keys()); iterator it = begin(); trie* new_root = mk_trie(); - IF_VERBOSE(1, verbose_stream() << "before reshuffle: " << m_root->num_nodes() << " nodes\n";); + IF_VERBOSE(2, verbose_stream() << "before reshuffle: " << m_root->num_nodes() << " nodes\n";); for (; it != end(); ++it) { IF_VERBOSE(2, for (unsigned i = 0; i < num_keys(); ++i) { @@ -539,7 +539,7 @@ private: m_keys[i] = new_keys[i]; } - IF_VERBOSE(1, verbose_stream() << "after reshuffle: " << new_root->num_nodes() << " nodes\n";); + IF_VERBOSE(2, verbose_stream() << "after reshuffle: " << new_root->num_nodes() << " nodes\n";); IF_VERBOSE(2, it = begin(); for (; it != end(); ++it) { @@ -559,7 +559,7 @@ private: if (index == num_keys()) { SASSERT(n->ref_count() > 0); bool r = check(to_leaf(n)->get_value()); - IF_VERBOSE(1, + IF_VERBOSE(2, for (unsigned j = 0; j < index; ++j) { verbose_stream() << " "; } @@ -572,7 +572,7 @@ private: for (unsigned i = 0; i < nodes.size(); ++i) { ++m_stats.m_num_find_le_nodes; node* m = nodes[i].second; - IF_VERBOSE(1, + IF_VERBOSE(2, for (unsigned j = 0; j < index; ++j) { verbose_stream() << " "; } diff --git a/src/muz_qe/hilbert_basis.cpp b/src/muz_qe/hilbert_basis.cpp index 59b513d8d..e7c7928a3 100644 --- a/src/muz_qe/hilbert_basis.cpp +++ b/src/muz_qe/hilbert_basis.cpp @@ -21,9 +21,8 @@ Revision History: #include "heap.h" #include "map.h" #include "heap_trie.h" +#include "stopwatch.h" -template -class rational_map : public map {}; typedef int_hashtable > int_table; @@ -263,7 +262,10 @@ class hilbert_basis::index { void reset() { memset(this, 0, sizeof(*this)); } }; - typedef rational_map value_map; + template + class numeral_map : public map {}; + + typedef numeral_map value_map; hilbert_basis& hb; value_map m_neg; value_index m_pos; @@ -793,9 +795,18 @@ lbool hilbert_basis::saturate() { init_basis(); m_current_ineq = 0; while (!m_cancel && m_current_ineq < m_ineqs.size()) { - IF_VERBOSE(1, { statistics st; collect_statistics(st); st.display(verbose_stream()); }); select_inequality(); + stopwatch sw; + sw.start(); lbool r = saturate(m_ineqs[m_current_ineq], m_iseq[m_current_ineq]); + IF_VERBOSE(1, + { statistics st; + collect_statistics(st); + st.display(verbose_stream()); + sw.stop(); + verbose_stream() << "time: " << sw.get_seconds() << "\n"; + }); + ++m_stats.m_num_saturations; if (r != l_true) { return r; diff --git a/src/test/heap_trie.cpp b/src/test/heap_trie.cpp index 7b57f97f2..dd04f7b98 100644 --- a/src/test/heap_trie.cpp +++ b/src/test/heap_trie.cpp @@ -25,6 +25,7 @@ static void find_le(heap_trie_t& ht, unsigned num_keys, unsigned const* keys) { } + void tst_heap_trie() { heap_trie_t ht; diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp index 69d733f68..bd5d20f8d 100644 --- a/src/test/hilbert_basis.cpp +++ b/src/test/hilbert_basis.cpp @@ -253,7 +253,7 @@ static void saturate_basis(hilbert_basis& hb) { case l_true: std::cout << "sat\n"; hb.display(std::cout); - validate_sat(hb); + //validate_sat(hb); break; case l_false: std::cout << "unsat\n"; @@ -523,6 +523,9 @@ void tst_hilbert_basis() { tst4(); tst4(); tst4(); + tst4(); + tst4(); + tst4(); tst5(); tst6(); tst7(); diff --git a/src/test/karr.cpp b/src/test/karr.cpp new file mode 100644 index 000000000..f6e572670 --- /dev/null +++ b/src/test/karr.cpp @@ -0,0 +1,213 @@ +#include "hilbert_basis.h" + +/* + Test generation of linear congruences a la Karr. + + */ +namespace karr { + + struct matrix { + vector > A; + vector b; + + unsigned size() const { return A.size(); } + + void reset() { + A.reset(); + b.reset(); + } + + matrix& operator=(matrix const& other) { + reset(); + append(other); + return *this; + } + + void append(matrix const& other) { + A.append(other.A); + b.append(other.b); + } + + void display(std::ostream& out) { + for (unsigned i = 0; i < A.size(); ++i) { + for (unsigned j = 0; j < A[i].size(); ++j) { + out << A[i][j] << " "; + } + out << " = " << -b[i] << "\n"; + } + } + }; + + // treat src as a homogeneous matrix. + void dualizeH(matrix& dst, matrix const& src) { + hilbert_basis hb; + for (unsigned i = 0; i < src.size(); ++i) { + vector v(src.A[i]); + v.append(src.b[i]); + hb.add_eq(v, rational(0)); + } + for (unsigned i = 0; i < 1 + src.A[0].size(); ++i) { + hb.set_is_int(i); + } + lbool is_sat = hb.saturate(); + hb.display(std::cout); + SASSERT(is_sat == l_true); + dst.reset(); + unsigned basis_size = hb.get_basis_size(); + bool first_initial = true; + for (unsigned i = 0; i < basis_size; ++i) { + bool is_initial; + vector soln; + hb.get_basis_solution(i, soln, is_initial); + if (!is_initial) { + dst.b.push_back(soln.back()); + soln.pop_back(); + dst.A.push_back(soln); + } + } + } + + // treat src as an inhomegeneous matrix. + void dualizeI(matrix& dst, matrix const& src) { + hilbert_basis hb; + for (unsigned i = 0; i < src.size(); ++i) { + hb.add_eq(src.A[i], -src.b[i]); + } + for (unsigned i = 0; i < src.A[0].size(); ++i) { + hb.set_is_int(i); + } + lbool is_sat = hb.saturate(); + hb.display(std::cout); + SASSERT(is_sat == l_true); + dst.reset(); + unsigned basis_size = hb.get_basis_size(); + bool first_initial = true; + for (unsigned i = 0; i < basis_size; ++i) { + bool is_initial; + vector soln; + hb.get_basis_solution(i, soln, is_initial); + if (is_initial && first_initial) { + dst.A.push_back(soln); + dst.b.push_back(rational(1)); + first_initial = false; + } + else if (!is_initial) { + dst.A.push_back(soln); + dst.b.push_back(rational(0)); + } + } + } + + void juxtapose(matrix& dst, matrix const& M, matrix const& N) { + dst = M; + dst.append(N); + } + + void join(matrix& dst, matrix const& M, matrix const& N) { + matrix MD, ND, dstD; + dualizeI(MD, M); + dualizeI(ND, N); + juxtapose(dstD, MD, ND); + dualizeH(dst, dstD); + } + + void joinD(matrix& dst, matrix const& MD, matrix const& ND) { + matrix dstD; + juxtapose(dstD, MD, ND); + dualizeH(dst, dstD); + } + + void transition( + matrix& dst, + matrix const& src, + matrix const& Ab) { + matrix T; + // length of rows in Ab are twice as long as + // length of rows in src. + SASSERT(2*src.A[0].size() == Ab.A[0].size()); + vector zeros; + for (unsigned i = 0; i < src.A[0].size(); ++i) { + zeros.push_back(rational(0)); + } + for (unsigned i = 0; i < src.size(); ++i) { + T.A.push_back(src.A[i]); + T.A.back().append(zeros); + } + T.b.append(src.b); + T.append(Ab); + + T.display(std::cout << "T:\n"); + matrix TD; + dualizeI(TD, T); + TD.display(std::cout << "TD:\n"); + for (unsigned i = 0; i < TD.size(); ++i) { + vector v; + v.append(src.size(), TD.A[i].c_ptr() + src.size()); + dst.A.push_back(v); + dst.b.push_back(TD.b[i]); + } + dst.display(std::cout << "dst\n"); + } + + static vector V(int i, int j) { + vector v; + v.push_back(rational(i)); + v.push_back(rational(j)); + return v; + } + + static vector V(int i, int j, int k, int l) { + vector v; + v.push_back(rational(i)); + v.push_back(rational(j)); + v.push_back(rational(k)); + v.push_back(rational(l)); + return v; + } + +#define R(_x_) rational(_x_) + + + static void tst1() { + matrix Theta; + matrix Ab; + + // + Theta.A.push_back(V(1, 0)); + Theta.b.push_back(R(0)); + Theta.A.push_back(V(0, 1)); + Theta.b.push_back(R(-2)); + + Theta.display(std::cout << "Theta\n"); + + Ab.A.push_back(V(-1, 0, 1, 0)); + Ab.b.push_back(R(1)); + Ab.A.push_back(V(-1, -2, 0, 1)); + Ab.b.push_back(R(1)); + + Ab.display(std::cout << "Ab\n"); + + matrix ThetaD; + dualizeI(ThetaD, Theta); + ThetaD.display(std::cout); + + matrix t1D, e1; + transition(t1D, Theta, Ab); + joinD(e1, t1D, ThetaD); + + t1D.display(std::cout << "t1D\n"); + e1.display(std::cout << "e1\n"); + + matrix t2D, e2; + transition(t2D, e1, Ab); + joinD(e2, t2D, ThetaD); + + t2D.display(std::cout << "t2D\n"); + e2.display(std::cout << "e2\n"); + } + +}; + +void tst_karr() { + karr::tst1(); +} diff --git a/src/test/main.cpp b/src/test/main.cpp index 9dc12be1c..c48f4529e 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -209,6 +209,7 @@ int main(int argc, char ** argv) { TST(rcf); TST(hilbert_basis); TST(heap_trie); + TST(karr); } void initialize_mam() {}