mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 03:15:41 +00:00
Code Activity

Cleanup

Browse source
This commit is contained in:
CEisenhofer 2022-11-14 15:31:24 +01:00
parent 1a5231fbf2
commit 2ef27064c7
4 changed files with 64 additions and 80 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -30,9 +30,9 @@ static const unsigned unassigned_col = UINT32_MAX;
///returns popcnt ///returns popcnt
unsigned PackedRow::find_watchVar( unsigned PackedRow::find_watchVar(
sat::literal_vector& tmp_clause, literal_vector& tmp_clause,
const unsigned_vector& col_to_var, const unsigned_vector& col_to_var,
char_vector &var_has_resp_row, bool_vector &var_has_resp_row,
unsigned& non_resp_var) { unsigned& non_resp_var) {
unsigned popcnt = 0; unsigned popcnt = 0;
non_resp_var = UINT_MAX; non_resp_var = UINT_MAX;
@ -98,7 +98,7 @@ void PackedRow::get_reason(
gret PackedRow::propGause( gret PackedRow::propGause(
const unsigned_vector& col_to_var, const unsigned_vector& col_to_var,
char_vector &var_has_resp_row, bool_vector &var_has_resp_row,
unsigned& new_resp_var, unsigned& new_resp_var,
PackedRow& tmp_col, PackedRow& tmp_col,
PackedRow& tmp_col2, PackedRow& tmp_col2,
@ -273,16 +273,13 @@ void EGaussian::fill_matrix() {
} }
mat.resize(num_rows, num_cols); // initial gaussian matrix mat.resize(num_rows, num_cols); // initial gaussian matrix
bdd_matrix.clear();
for (unsigned row = 0; row < num_rows; row++) { for (unsigned row = 0; row < num_rows; row++) {
const xor_clause& c = m_xorclauses[row]; const xor_clause& c = m_xorclauses[row];
mat[row].set(c, var_to_col, num_cols); mat[row].set(c, var_to_col, num_cols);
char_vector line; char_vector line;
line.resize(num_rows, 0); line.resize(num_rows, 0);
line[row] = 1; line[row] = 1;
bdd_matrix.push_back(line);
} }
SASSERT(bdd_matrix.size() == num_rows);
// reset // reset
var_has_resp_row.clear(); var_has_resp_row.clear();
@ -294,7 +291,7 @@ void EGaussian::fill_matrix() {
//reset satisfied_xor state //reset satisfied_xor state
SASSERT(m_solver.m_num_scopes == 0); SASSERT(m_solver.m_num_scopes == 0);
satisfied_xors.clear(); satisfied_xors.clear();
satisfied_xors.resize(num_rows, 0); satisfied_xors.resize(num_rows, false);
} }
void EGaussian::delete_gauss_watch_this_matrix() { void EGaussian::delete_gauss_watch_this_matrix() {
@ -346,7 +343,6 @@ bool EGaussian::full_init(bool& created) {
case gret::prop: case gret::prop:
SASSERT(m_solver.m_num_scopes == 0); SASSERT(m_solver.m_num_scopes == 0);
m_solver.s().propagate(false); // TODO: Can we really do this here? m_solver.s().propagate(false); // TODO: Can we really do this here?
// m_solver.ok = m_solver.propagate<false>().isNull();
if (inconsistent()) { if (inconsistent()) {
TRACE("xor", tout << "eliminate & adjust matrix during init lead to UNSAT\n";); TRACE("xor", tout << "eliminate & adjust matrix during init lead to UNSAT\n";);
return false; return false;
@ -394,42 +390,38 @@ bool EGaussian::full_init(bool& created) {
} }
void EGaussian::eliminate() { void EGaussian::eliminate() {
PackedMatrix::iterator end_row_it = mat.begin() + num_rows; // TODO: Why twice? gauss_jordan_elim
PackedMatrix::iterator rowI = mat.begin(); const unsigned end_row = num_rows;
unsigned rowI = 0;
unsigned row_i = 0; unsigned row_i = 0;
unsigned col = 0; unsigned col = 0;
// Gauss-Jordan Elimination // Gauss-Jordan Elimination
while (row_i != num_rows && col != num_cols) { while (row_i != num_rows && col != num_cols) {
PackedMatrix::iterator row_with_1_in_col = rowI; unsigned row_with_1_in_col = rowI;
unsigned row_with_1_in_col_n = row_i; unsigned row_with_1_in_col_n = row_i;
// Find first "1" in column. // Find first "1" in column.
for (; row_with_1_in_col != end_row_it; ++row_with_1_in_col, row_with_1_in_col_n++) { for (; row_with_1_in_col < end_row; ++row_with_1_in_col, row_with_1_in_col_n++) {
if ((*row_with_1_in_col)[col]) if (mat[row_with_1_in_col][col])
break; break;
} }
// We have found a "1" in this column // We have found a "1" in this column
if (row_with_1_in_col != end_row_it) { if (row_with_1_in_col < end_row) {
var_has_resp_row[col_to_var[col]] = 1; var_has_resp_row[col_to_var[col]] = true;
// swap row row_with_1_in_col and rowIt // swap row row_with_1_in_col and rowIt
if (row_with_1_in_col != rowI) { if (row_with_1_in_col != rowI)
(*rowI).swapBoth(*row_with_1_in_col); mat[rowI].swapBoth(mat[row_with_1_in_col]);
std::swap(bdd_matrix[row_i], bdd_matrix[row_with_1_in_col_n]);
}
// XOR into *all* rows that have a "1" in column COL // XOR into *all* rows that have a "1" in column COL
// Since we XOR into *all*, this is Gauss-Jordan (and not just Gauss) // Since we XOR into *all*, this is Gauss-Jordan (and not just Gauss)
unsigned k = 0; unsigned k = 0;
for (PackedMatrix::iterator k_row = mat.begin() for (unsigned k_row = 0; k_row < end_row; ++k_row, k++) {
; k_row != end_row_it
; ++k_row, k++
) {
// xor rows K and I // xor rows K and I
if (k_row != rowI && (*k_row)[col]) { if (k_row != rowI && mat[k_row][col]) {
(*k_row).xor_in(*rowI); mat[k_row].xor_in(mat[rowI]);
} }
} }
row_i++; row_i++;
@ -439,7 +431,7 @@ void EGaussian::eliminate() {
} }
} }
sat::literal_vector* EGaussian::get_reason(const unsigned row, int& out_ID) { literal_vector* EGaussian::get_reason(const unsigned row, int& out_ID) {
if (!xor_reasons[row].m_must_recalc) { if (!xor_reasons[row].m_must_recalc) {
out_ID = xor_reasons[row].m_ID; out_ID = xor_reasons[row].m_ID;
return &(xor_reasons[row].m_reason); return &(xor_reasons[row].m_reason);
@ -447,7 +439,7 @@ sat::literal_vector* EGaussian::get_reason(const unsigned row, int& out_ID) {
// Clean up previous one // Clean up previous one
svector<literal>& to_fill = xor_reasons[row].m_reason; literal_vector& to_fill = xor_reasons[row].m_reason;
to_fill.clear(); to_fill.clear();
mat[row].get_reason( mat[row].get_reason(
@ -493,7 +485,7 @@ gret EGaussian::init_adjust_matrix() {
} }
TRACE("xor", tout << "-> empty on row: " << row_i;); TRACE("xor", tout << "-> empty on row: " << row_i;);
TRACE("xor", tout << "-> Satisfied XORs set for row: " << row_i;); TRACE("xor", tout << "-> Satisfied XORs set for row: " << row_i;);
satisfied_xors[row_i] = 1; satisfied_xors[row_i] = true;
break; break;
//Unit (i.e. toplevel unit) //Unit (i.e. toplevel unit)
@ -508,13 +500,13 @@ gret EGaussian::init_adjust_matrix() {
TRACE("xor", tout << "-> UNIT during adjust: " << tmp_clause[0];); TRACE("xor", tout << "-> UNIT during adjust: " << tmp_clause[0];);
TRACE("xor", tout << "-> Satisfied XORs set for row: " << row_i;); TRACE("xor", tout << "-> Satisfied XORs set for row: " << row_i;);
satisfied_xors[row_i] = 1; satisfied_xors[row_i] = true;
SASSERT(check_row_satisfied(row_i)); SASSERT(check_row_satisfied(row_i));
//adjusting //adjusting
row.setZero(); // reset this row all zero row.setZero(); // reset this row all zero
row_to_var_non_resp.push_back(UINT32_MAX); row_to_var_non_resp.push_back(UINT32_MAX);
var_has_resp_row[tmp_clause[0].var()] = 0; var_has_resp_row[tmp_clause[0].var()] = false;
return gret::prop; return gret::prop;
} }
@ -535,7 +527,7 @@ gret EGaussian::init_adjust_matrix() {
row.setZero(); row.setZero();
row_to_var_non_resp.push_back(UINT32_MAX); // delete non-basic value in this row row_to_var_non_resp.push_back(UINT32_MAX); // delete non-basic value in this row
var_has_resp_row[tmp_clause[0].var()] = 0; // delete basic value in this row var_has_resp_row[tmp_clause[0].var()] = false; // delete basic value in this row
break; break;
} }
@ -579,7 +571,7 @@ void EGaussian::delete_gausswatch(const unsigned row_n) {
unsigned EGaussian::get_max_level(const gauss_data& gqd, const unsigned row_n) { unsigned EGaussian::get_max_level(const gauss_data& gqd, const unsigned row_n) {
int ID; int ID;
auto cl = get_reason(row_n, ID); literal_vector* cl = get_reason(row_n, ID);
unsigned nMaxLevel = gqd.currLevel; unsigned nMaxLevel = gqd.currLevel;
unsigned nMaxInd = 1; unsigned nMaxInd = 1;
@ -634,8 +626,8 @@ bool EGaussian::find_truths(
//var has a responsible row, so THIS row must be it! //var has a responsible row, so THIS row must be it!
//since if a var has a responsible row, only ONE row can have a 1 there //since if a var has a responsible row, only ONE row can have a 1 there
was_resp_var = true; was_resp_var = true;
var_has_resp_row[row_to_var_non_resp[row_n]] = 1; var_has_resp_row[row_to_var_non_resp[row_n]] = true;
var_has_resp_row[var] = 0; var_has_resp_row[var] = false;
} }
unsigned new_resp_var; unsigned new_resp_var;
@ -663,8 +655,8 @@ bool EGaussian::find_truths(
TRACE("xor", tout << "--> conflict";); TRACE("xor", tout << "--> conflict";);
if (was_resp_var) { // recover if (was_resp_var) { // recover
var_has_resp_row[row_to_var_non_resp[row_n]] = 0; var_has_resp_row[row_to_var_non_resp[row_n]] = false;
var_has_resp_row[var] = 1; var_has_resp_row[var] = true;
} }
return false; return false;
@ -684,12 +676,12 @@ bool EGaussian::find_truths(
gqd.status = gauss_res::prop; gqd.status = gauss_res::prop;
if (was_resp_var) { // recover if (was_resp_var) { // recover
var_has_resp_row[row_to_var_non_resp[row_n]] = 0; var_has_resp_row[row_to_var_non_resp[row_n]] = false;
var_has_resp_row[var] = 1; var_has_resp_row[var] = true;
} }
TRACE("xor", tout << "--> Satisfied XORs set for row: " << row_n;); TRACE("xor", tout << "--> Satisfied XORs set for row: " << row_n;);
satisfied_xors[row_n] = 1; satisfied_xors[row_n] = true;
SASSERT(check_row_satisfied(row_n)); SASSERT(check_row_satisfied(row_n));
return true; return true;
} }
@ -719,8 +711,8 @@ bool EGaussian::find_truths(
//so elimination will be needed //so elimination will be needed
//clear old one, add new resp //clear old one, add new resp
var_has_resp_row[row_to_var_non_resp[row_n]] = 0; var_has_resp_row[row_to_var_non_resp[row_n]] = false;
var_has_resp_row[new_resp_var] = 1; var_has_resp_row[new_resp_var] = true;
// store the eliminate variable & row // store the eliminate variable & row
gqd.new_resp_var = new_resp_var; gqd.new_resp_var = new_resp_var;
@ -742,12 +734,12 @@ bool EGaussian::find_truths(
find_truth_ret_satisfied++; find_truth_ret_satisfied++;
ws[j++] = ws[i]; ws[j++] = ws[i];
if (was_resp_var) { // recover if (was_resp_var) { // recover
var_has_resp_row[row_to_var_non_resp[row_n]] = 0; var_has_resp_row[row_to_var_non_resp[row_n]] = false;
var_has_resp_row[var] = 1; var_has_resp_row[var] = true;
} }
TRACE("xor", tout << "--> Satisfied XORs set for row: " << row_n;); TRACE("xor", tout << "--> Satisfied XORs set for row: " << row_n;);
satisfied_xors[row_n] = 1; satisfied_xors[row_n] = true;
SASSERT(check_row_satisfied(row_n)); SASSERT(check_row_satisfied(row_n));
return true; return true;
@ -843,7 +835,7 @@ void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) {
<< " is being watched on var: " << orig_non_resp_var + 1 << " is being watched on var: " << orig_non_resp_var + 1
<< " i.e. it must contain '1' for this var's column";); << " i.e. it must contain '1' for this var's column";);
SASSERT(satisfied_xors[row_i] == 0); SASSERT(!satisfied_xors[row_i]);
(*rowI).xor_in(*(mat.begin() + new_resp_row_n)); (*rowI).xor_in(*(mat.begin() + new_resp_row_n));
elim_xored_rows++; elim_xored_rows++;
@ -919,7 +911,7 @@ void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) {
gqd.status = gauss_res::prop; gqd.status = gauss_res::prop;
TRACE("xor", tout << "---> Satisfied XORs set for row: " << row_i;); TRACE("xor", tout << "---> Satisfied XORs set for row: " << row_i;);
satisfied_xors[row_i] = 1; satisfied_xors[row_i] = true;
SASSERT(check_row_satisfied(row_i)); SASSERT(check_row_satisfied(row_i));
break; break;
} }
@ -946,7 +938,7 @@ void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) {
row_to_var_non_resp[row_i] = p; row_to_var_non_resp[row_i] = p;
TRACE("xor", tout << "---> Satisfied XORs set for row: " << row_i;); TRACE("xor", tout << "---> Satisfied XORs set for row: " << row_i;);
satisfied_xors[row_i] = 1; satisfied_xors[row_i] = true;
SASSERT(check_row_satisfied(row_i)); SASSERT(check_row_satisfied(row_i));
break; break;
default: default:

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

@ -391,13 +391,13 @@ namespace xr {
unsigned find_watchVar( unsigned find_watchVar(
sat::literal_vector& tmp_clause, sat::literal_vector& tmp_clause,
const unsigned_vector& col_to_var, const unsigned_vector& col_to_var,
char_vector &var_has_resp_row, bool_vector &var_has_resp_row,
unsigned& non_resp_var); unsigned& non_resp_var);
// using find nonbasic value after watch list is enter // using find nonbasic value after watch list is enter
gret propGause( gret propGause(
const unsigned_vector& col_to_var, const unsigned_vector& col_to_var,
char_vector &var_has_resp_row, bool_vector &var_has_resp_row,
unsigned& new_resp_var, unsigned& new_resp_var,
PackedRow& tmp_col, PackedRow& tmp_col,
PackedRow& tmp_col2, PackedRow& tmp_col2,
@ -559,7 +559,7 @@ namespace xr {
gauss_data& gqd gauss_data& gqd
); );
sat::literal_vector* get_reason(const unsigned row, int& out_ID); literal_vector* get_reason(const unsigned row, int& out_ID);
// when basic variable is touched , eliminate one col // when basic variable is touched , eliminate one col
void eliminate_col( void eliminate_col(
@ -637,20 +637,19 @@ namespace xr {
// Is the clause at this ROW satisfied already? // Is the clause at this ROW satisfied already?
// satisfied_xors[row] tells me that // satisfied_xors[row] tells me that
// TODO: Are characters enough? // TODO: Maybe compress further
char_vector satisfied_xors; bool_vector satisfied_xors;
// Someone is responsible for this column if TRUE // Someone is responsible for this column if TRUE
///we always WATCH this variable // we always WATCH this variable
char_vector var_has_resp_row; bool_vector var_has_resp_row;
///row_to_var_non_resp[ROW] gives VAR it's NOT responsible for // row_to_var_non_resp[ROW] gives VAR it's NOT responsible for
///we always WATCH this variable // we always WATCH this variable
unsigned_vector row_to_var_non_resp; unsigned_vector row_to_var_non_resp;
PackedMatrix mat; PackedMatrix mat;
svector<char_vector> bdd_matrix; // TODO: we will probably not need it
unsigned_vector var_to_col; ///var->col mapping. Index with VAR unsigned_vector var_to_col; ///var->col mapping. Index with VAR
unsigned_vector col_to_var; ///col->var mapping. Index with COL unsigned_vector col_to_var; ///col->var mapping. Index with COL
unsigned num_rows = 0; unsigned num_rows = 0;
@ -670,7 +669,7 @@ namespace xr {
inline void EGaussian::canceling() { inline void EGaussian::canceling() {
cancelled_since_val_update = true; cancelled_since_val_update = true;
memset(satisfied_xors.data(), 0, satisfied_xors.size()); memset(satisfied_xors.data(), false, satisfied_xors.size());
} }
inline double EGaussian::get_density() { inline double EGaussian::get_density() {

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

@ -28,7 +28,7 @@ namespace xr {
class xor_matrix_finder { class xor_matrix_finder {
struct matrix_shape { struct matrix_shape {
matrix_shape(uint32_t matrix_num) : m_num(matrix_num) {} matrix_shape(unsigned matrix_num) : m_num(matrix_num) {}
matrix_shape() {} matrix_shape() {}

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

@ -336,11 +336,6 @@ namespace xr {
case 0: case 0:
if (x.m_rhs) if (x.m_rhs)
s().set_conflict(); s().set_conflict();
/*TODO: Implement
if (inconsistent()) {
SASSERT(m_solver.unsat_cl_ID == 0);
m_solver.unsat_cl_ID = solver->clauseID;
}*/
return false; return false;
case 1: { case 1: {
s().assign_scoped(sat::literal(x[0], !x.m_rhs)); s().assign_scoped(sat::literal(x[0], !x.m_rhs));
@ -589,10 +584,8 @@ namespace xr {
for (unsigned i = 0; i < 2 * s().num_vars(); i++) { for (unsigned i = 0; i < 2 * s().num_vars(); i++) {
const auto& ws = s().get_wlist(i); const auto& ws = s().get_wlist(i);
for (const auto& w: ws) { for (const auto& w: ws) {
if (w.is_binary_clause()/* TODO: Does redundancy information exist in Z3? Can we use learned instead of "!w.red()"?*/ && !w.is_learned()) { if (w.is_binary_clause()/* TODO: Does redundancy information exist in Z3? Can we use learned instead of "!w.red()"?*/ && !w.is_learned())
bool_var v = w.get_literal().var(); s().mark_visited(w.get_literal().var());
s().mark_visited(v);
}
} }
} }
@ -601,7 +594,7 @@ namespace xr {
if (cl->red() || cl->used_in_xor()) { if (cl->red() || cl->used_in_xor()) {
continue; continue;
}*/ }*/
// TODO: maybe again instead // TODO: maybe again this instead
if (cl->is_learned()) if (cl->is_learned())
continue; continue;
for (literal l: *cl) for (literal l: *cl)