mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

update logging for hilbert

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-02-26 19:14:52 -08:00
parent e0c73d9bc1
commit 2a75f1d71e
2 changed files with 15 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/muz_qe/heap_trie.h
View file

@ -518,7 +518,7 @@ private:
SASSERT(m_keys.size() == num_keys()); SASSERT(m_keys.size() == num_keys());
iterator it = begin(); iterator it = begin();
trie* new_root = mk_trie(); 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) { for (; it != end(); ++it) {
IF_VERBOSE(2, IF_VERBOSE(2,
for (unsigned i = 0; i < num_keys(); ++i) { for (unsigned i = 0; i < num_keys(); ++i) {
@ -539,7 +539,7 @@ private:
m_keys[i] = new_keys[i]; 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, IF_VERBOSE(2,
it = begin(); it = begin();
for (; it != end(); ++it) { for (; it != end(); ++it) {
@ -559,7 +559,7 @@ private:
if (index == num_keys()) { if (index == num_keys()) {
SASSERT(n->ref_count() > 0); SASSERT(n->ref_count() > 0);
bool r = check(to_leaf(n)->get_value()); bool r = check(to_leaf(n)->get_value());
IF_VERBOSE(1, IF_VERBOSE(2,
for (unsigned j = 0; j < index; ++j) { for (unsigned j = 0; j < index; ++j) {
verbose_stream() << " "; verbose_stream() << " ";
} }
@ -572,7 +572,7 @@ private:
for (unsigned i = 0; i < nodes.size(); ++i) { for (unsigned i = 0; i < nodes.size(); ++i) {
++m_stats.m_num_find_le_nodes; ++m_stats.m_num_find_le_nodes;
node* m = nodes[i].second; node* m = nodes[i].second;
IF_VERBOSE(1, IF_VERBOSE(2,
for (unsigned j = 0; j < index; ++j) { for (unsigned j = 0; j < index; ++j) {
verbose_stream() << " "; verbose_stream() << " ";
} }

20
src/muz_qe/hilbert_basis.cpp
View file

@ -21,6 +21,7 @@ Revision History:
#include "heap.h" #include "heap.h"
#include "map.h" #include "map.h"
#include "heap_trie.h" #include "heap_trie.h"
#include "stopwatch.h"
template<typename Value> template<typename Value>
class rational_map : public map<rational, Value, rational::hash_proc, rational::eq_proc> {}; class rational_map : public map<rational, Value, rational::hash_proc, rational::eq_proc> {};
@ -777,9 +778,18 @@ lbool hilbert_basis::saturate() {
init_basis(); init_basis();
m_current_ineq = 0; m_current_ineq = 0;
while (!m_cancel && m_current_ineq < m_ineqs.size()) { while (!m_cancel && m_current_ineq < m_ineqs.size()) {
IF_VERBOSE(1, { statistics st; collect_statistics(st); st.display(verbose_stream()); });
select_inequality(); select_inequality();
stopwatch sw;
sw.start();
lbool r = saturate(m_ineqs[m_current_ineq], m_iseq[m_current_ineq]); 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; ++m_stats.m_num_saturations;
if (r != l_true) { if (r != l_true) {
return r; return r;
@ -933,14 +943,6 @@ lbool hilbert_basis::saturate(num_vector const& ineq, bool is_eq) {
m_free_list.push_back(m_basis.back()); m_free_list.push_back(m_basis.back());
m_basis.pop_back(); m_basis.pop_back();
} }
for (unsigned i = 0; i < init_basis_size; ++i) {
offset_t idx = m_basis[i];
if (vec(idx).weight().is_neg()) {
m_basis[i] = m_basis.back();
m_basis.pop_back();
}
}
m_basis.append(m_zero); m_basis.append(m_zero);
std::sort(m_basis.begin(), m_basis.end(), vector_lt_t(*this)); std::sort(m_basis.begin(), m_basis.end(), vector_lt_t(*this));
m_zero.reset(); m_zero.reset();