mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

Final fixes

Browse source
This commit is contained in:
Clemens Eisenhofer 2022-12-08 12:40:26 +01:00
parent 32b5dc31d1
commit f7d9cdd18b
2 changed files with 19 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -763,6 +763,19 @@ inline void EGaussian::update_cols_vals_set(literal lit) {
// In case the argument is false it only updates the recently added variables. If true, it recalculates all // In case the argument is false it only updates the recently added variables. If true, it recalculates all
void EGaussian::update_cols_vals_set(bool force) { void EGaussian::update_cols_vals_set(bool force) {
SASSERT(initialized); SASSERT(initialized);
auto output_rows = [this]() {
std::cout << "Col-Unassigned: ";
for (int i = 0; i < 64 * m_cols_unset->size; ++i) {
std::cout << (*m_cols_unset)[i];
}
std::cout << "\n";
std::cout << "Col-Values: ";
for (int i = 0; i < 64 * m_cols_vals->size; ++i) {
std::cout << (*m_cols_vals)[i];
}
std::cout << std::endl;
};
if (recalculate_values || force) { if (recalculate_values || force) {
m_cols_vals->setZero(); m_cols_vals->setZero();
@ -779,6 +792,7 @@ void EGaussian::update_cols_vals_set(bool force) {
last_val_update = m_solver.s().trail_size(); last_val_update = m_solver.s().trail_size();
recalculate_values = false; recalculate_values = false;
TRACE("xor", tout << "last val update set to " << last_val_update << "\n"); TRACE("xor", tout << "last val update set to " << last_val_update << "\n");
output_rows();
return; return;
} }
@ -797,17 +811,7 @@ void EGaussian::update_cols_vals_set(bool force) {
} }
} }
last_val_update = m_solver.s().trail_size(); last_val_update = m_solver.s().trail_size();
output_rows();
std::cout << "Col-Unassigned: ";
for (int i = 0; i < 64 * m_cols_unset->size; ++i) {
std::cout << (*m_cols_unset)[i];
}
std::cout << "\n";
std::cout << "Col-Values: ";
for (int i = 0; i < 64 * m_cols_vals->size; ++i) {
std::cout << (*m_cols_vals)[i];
}
std::cout << std::endl;
} }
void EGaussian::prop_lit(const gauss_data& gqd, unsigned row_i, literal ret_lit_prop) { void EGaussian::prop_lit(const gauss_data& gqd, unsigned row_i, literal ret_lit_prop) {

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

@ -280,13 +280,13 @@ namespace xr {
} }
m_justifications_lim.shrink(old_sz); m_justifications_lim.shrink(old_sz);
m_justifications.shrink(old_sz);*/ m_justifications.shrink(old_sz);*/
check_need_gauss_jordan_disable(); // Do this before enforcing recalcultion!
for (unsigned i = 0; i < m_gmatrices.size(); i++) for (unsigned i = 0; i < m_gmatrices.size(); i++)
if (m_gmatrices[i] && !m_gqueuedata[i].disabled) if (m_gmatrices[i] && !m_gqueuedata[i].disabled)
m_gmatrices[i]->enforce_recalculate(); m_gmatrices[i]->enforce_recalculate();
check_need_gauss_jordan_disable();
if (m_region) if (m_region)
m_region->pop_scope(num_scopes); m_region->pop_scope(num_scopes);
} }
@ -408,7 +408,7 @@ namespace xr {
} }
} }
// disables matrixes if applicable // disables matrices if applicable
void solver::check_need_gauss_jordan_disable() { void solver::check_need_gauss_jordan_disable() {
for (unsigned i = 0; i < m_gqueuedata.size(); i++) { for (unsigned i = 0; i < m_gqueuedata.size(); i++) {
auto& gqd = m_gqueuedata[i]; auto& gqd = m_gqueuedata[i];
@ -423,7 +423,7 @@ namespace xr {
}*/ }*/
gqd.reset(); gqd.reset();
m_gmatrices[i]->update_cols_vals_set(false); m_gmatrices[i]->update_cols_vals_set(false); // TODO: Probably we don't need this as we reset it anyway afterwards everywhere we call this function. Remove?
} }
} }