mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

adding checks for #570

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-05-03 11:09:05 -07:00
parent 6895cc7cc6
commit 91af947863
2 changed files with 25 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/sat/sat_clause_set.cpp
View file

@ -35,6 +35,8 @@ namespace sat {
unsigned id = c.id(); unsigned id = c.id();
if (id >= m_id2pos.size()) if (id >= m_id2pos.size())
return; return;
if (empty())
return;
unsigned pos = m_id2pos[id]; unsigned pos = m_id2pos[id];
if (pos == UINT_MAX) if (pos == UINT_MAX)
return; return;
@ -52,7 +54,11 @@ namespace sat {
clause & clause_set::erase() { clause & clause_set::erase() {
SASSERT(!empty()); SASSERT(!empty());
clause & c = *m_set.back(); clause & c = *m_set.back();
m_id2pos[c.id()] = UINT_MAX; SASSERT(c.id() < m_id2pos.size());
SASSERT(m_id2pos[c.id()] == m_set.size()-1);
if (c.id() < m_id2pos.size()) {
m_id2pos[c.id()] = UINT_MAX;
}
m_set.pop_back(); m_set.pop_back();
return c; return c;
} }

26
src/smt/theory_arith_core.h
View file

@ -1866,7 +1866,7 @@ namespace smt {
template<typename Ext> template<typename Ext>
template<bool Lazy> template<bool Lazy>
void theory_arith<Ext>::pivot(theory_var x_i, theory_var x_j, numeral const & a_ij, bool apply_gcd_test) { void theory_arith<Ext>::pivot(theory_var x_i, theory_var x_j, numeral const & a_ij, bool apply_gcd_test) {
TRACE("arith_pivot", tout << "pivoting: v" << x_i << ", v" << x_j << "\n";); TRACE("arith_pivoting", tout << "pivoting: v" << x_i << ", v" << x_j << "\n";);
m_stats.m_pivots++; m_stats.m_pivots++;
SASSERT(is_base(x_i) || is_quasi_base(x_i)); SASSERT(is_base(x_i) || is_quasi_base(x_i));
SASSERT(x_i != x_j); SASSERT(x_i != x_j);
@ -2067,14 +2067,14 @@ namespace smt {
theory_var max = get_num_vars(); theory_var max = get_num_vars();
theory_var result = max; theory_var result = max;
row const & r = m_rows[get_var_row(x_i)]; row const & r = m_rows[get_var_row(x_i)];
int n;
int best_col_sz = INT_MAX; int best_col_sz = INT_MAX;
int best_so_far = INT_MAX; int best_so_far = INT_MAX;
int n = 0;
typename vector<row_entry>::const_iterator it = r.begin_entries(); typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries(); typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) { for (; it != end; ++it) {
if (!it->is_dead()) { if (!it->is_dead()) {
theory_var x_j = it->m_var; theory_var x_j = it->m_var;
numeral const & a_ij = it->m_coeff; numeral const & a_ij = it->m_coeff;
@ -2090,14 +2090,14 @@ namespace smt {
best_so_far = num; best_so_far = num;
best_col_sz = col_sz; best_col_sz = col_sz;
n = 1; n = 1;
} }
else if (num == best_so_far && col_sz == best_col_sz) { else if (num == best_so_far && col_sz == best_col_sz) {
n++; n++;
if (m_random()%n == 0) { if (m_random()%n == 0) {
result = x_j; result = x_j;
out_a_ij = a_ij; out_a_ij = a_ij;
} }
} }
} }
} }
} }
@ -2174,6 +2174,7 @@ namespace smt {
inf_numeral curr_error; inf_numeral curr_error;
typename var_heap::iterator it = m_to_patch.begin(); typename var_heap::iterator it = m_to_patch.begin();
typename var_heap::iterator end = m_to_patch.end(); typename var_heap::iterator end = m_to_patch.end();
//unsigned n = 0;
for (; it != end; ++it) { for (; it != end; ++it) {
theory_var v = *it; theory_var v = *it;
if (below_lower(v)) if (below_lower(v))
@ -2188,7 +2189,16 @@ namespace smt {
<< ", best_error: " << best_error << ", curr_error: " << curr_error << "\n";); << ", best_error: " << best_error << ", curr_error: " << curr_error << "\n";);
best = v; best = v;
best_error = curr_error; best_error = curr_error;
//n = 2;
} }
#if 0
else if (false && n > 0 && curr_error == best_error) {
n++;
if (m_random()%n == 0) {
best = v;
}
}
#endif
} }
if (best == null_theory_var) if (best == null_theory_var)
m_to_patch.clear(); // all variables are satisfied m_to_patch.clear(); // all variables are satisfied