mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-30 13:19:04 +00:00
Code Activity

some tracing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-07 11:47:48 -08:00
parent 9561dd3371
commit 626d736904
3 changed files with 10 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/sat/smt/xor_gaussian.cpp
View file

@ -609,7 +609,7 @@ bool EGaussian::find_truths(
<< "mat[" << matrix_no << "] find_truths\n" << "mat[" << matrix_no << "] find_truths\n"
<< "-> row: " << row_n << "\n" << "-> row: " << row_n << "\n"
<< "-> var: " << var+1 << "\n" << "-> var: " << var+1 << "\n"
<< "-> dec lev:" << m_solver.s().scope_lvl()); << "-> dec lev:" << m_solver.s().scope_lvl() << "\n");
SASSERT(row_n < m_num_rows); SASSERT(row_n < m_num_rows);
SASSERT(satisfied_xors.size() > row_n); SASSERT(satisfied_xors.size() > row_n);
@ -654,7 +654,7 @@ bool EGaussian::find_truths(
xor_reasons[row_n].m_propagated = sat::null_literal; xor_reasons[row_n].m_propagated = sat::null_literal;
gqd.conflict = m_solver.mk_justification(m_solver.s().scope_lvl(), matrix_no, row_n); gqd.conflict = m_solver.mk_justification(m_solver.s().scope_lvl(), matrix_no, row_n);
gqd.status = gauss_res::confl; gqd.status = gauss_res::confl;
TRACE("xor", tout << "--> conflict";); TRACE("xor", tout << "--> conflict\n");
if (was_resp_var) { // recover if (was_resp_var) { // recover
var_has_resp_row[row_to_var_non_resp[row_n]] = false; var_has_resp_row[row_to_var_non_resp[row_n]] = false;
@ -776,9 +776,11 @@ void EGaussian::update_cols_vals_set(bool force) {
} }
last_val_update = m_solver.s().trail_size(); last_val_update = m_solver.s().trail_size();
cancelled_since_val_update = false; cancelled_since_val_update = false;
TRACE("xor", tout << "last val update set to " << last_val_update << "\n");
return; return;
} }
TRACE("xor", tout << last_val_update << " " << m_solver.s().trail_size() << "\n");
SASSERT(m_solver.s().trail_size() >= last_val_update); SASSERT(m_solver.s().trail_size() >= last_val_update);
for (unsigned i = last_val_update; i < m_solver.s().trail_size(); i++) { for (unsigned i = last_val_update; i < m_solver.s().trail_size(); i++) {
bool_var var = m_solver.s().trail_literal(i).var(); bool_var var = m_solver.s().trail_literal(i).var();

2
src/sat/smt/xor_gaussian.h
View file

@ -587,7 +587,7 @@ namespace xr {
); );
void canceling(); void canceling();
bool full_init(bool& created); bool full_init(bool& created);
void update_cols_vals_set(bool force = false); void update_cols_vals_set(bool force);
bool must_disable(gauss_data& gqd); bool must_disable(gauss_data& gqd);
void check_invariants(); void check_invariants();
void update_matrix_no(unsigned n); void update_matrix_no(unsigned n);

4
src/sat/smt/xor_solver.cpp
View file

@ -139,7 +139,7 @@ namespace xr {
force_push(); force_push();
for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head) { for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head) {
literal p = m_prop_queue[m_prop_queue_head]; literal p = m_prop_queue[m_prop_queue_head];
std::cout << "Propagating: " << p.var() << " = " << !p.sign() << std::endl; std::cout << "Propagating: " << p.var() << " := " << !p.sign() << std::endl;
SASSERT(s().lvl(p) == s().scope_lvl()); SASSERT(s().lvl(p) == s().scope_lvl());
sat::justification conflict = gauss_jordan_elim(p); sat::justification conflict = gauss_jordan_elim(p);
if (!conflict.is_none()) { if (!conflict.is_none()) {
@ -158,7 +158,7 @@ namespace xr {
for (unsigned i = 0; i < m_gqueuedata.size(); i++) { for (unsigned i = 0; i < m_gqueuedata.size(); i++) {
if (m_gqueuedata[i].disabled || !m_gmatrices[i]->is_initialized()) continue; if (m_gqueuedata[i].disabled || !m_gmatrices[i]->is_initialized()) continue;
m_gqueuedata[i].reset(); m_gqueuedata[i].reset();
m_gmatrices[i]->update_cols_vals_set(); m_gmatrices[i]->update_cols_vals_set(false);
} }
bool confl_in_gauss = false; bool confl_in_gauss = false;