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

Justifications

Browse source
This commit is contained in:
CEisenhofer 2022-12-07 15:53:17 +01:00
parent 7d58a29bd5
commit b5647f4d35
3 changed files with 90 additions and 48 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -53,12 +53,9 @@ unsigned PackedRow::population_cnt(
return popcnt; return popcnt;
} }
void PackedRow::get_reason( // Gets the reason why the literal "prop" was propagated
sat::literal_vector& tmp_clause, void PackedRow::get_reason(literal_vector& tmp_clause, const unsigned_vector& column_to_var, PackedRow& cols_vals, PackedRow& tmp_col2, literal prop) {
const unsigned_vector& col_to_var,
PackedRow& cols_vals,
PackedRow& tmp_col2,
literal prop) {
tmp_col2.set_and(*this, cols_vals); tmp_col2.set_and(*this, cols_vals);
for (int i = 0; i < size; i++) { for (int i = 0; i < size; i++) {
if (!mp[i]) if (!mp[i])
@ -70,15 +67,13 @@ void PackedRow::get_reason(
while (at != 0) { while (at != 0) {
unsigned col = extra + (at - 1) + i * 64; unsigned col = extra + (at - 1) + i * 64;
SASSERT((*this)[col] == 1); SASSERT((*this)[col] == 1);
unsigned var = col_to_var[col]; unsigned var = column_to_var[col];
if (var == prop.var()) { if (var == prop.var()) {
tmp_clause.push_back(prop); tmp_clause.push_back(~prop); // TODO: Why not negated?
std::swap(tmp_clause[0], tmp_clause.back()); std::swap(tmp_clause[0], tmp_clause.back());
} }
else { else
bool val_bool = tmp_col2[col]; // NSB: double check if z3 use of sign is compatible tmp_clause.push_back(literal(var, tmp_col2[col])); // NSB: double check if z3 use of sign is compatible
tmp_clause.push_back(sat::literal(var, val_bool));
}
extra += at; extra += at;
if (extra == 64) if (extra == 64)
@ -408,9 +403,8 @@ void EGaussian::eliminate() {
// 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)
for (unsigned k_row = 0; k_row < end_row; k_row++) { for (unsigned k_row = 0; k_row < end_row; k_row++) {
// xor rows K and I // xor rows K and I
if (k_row != row_i && m_mat[k_row][col]) { if (k_row != row_i && m_mat[k_row][col])
m_mat[k_row].xor_in(m_mat[row_i]); m_mat[k_row].xor_in(m_mat[row_i]);
}
} }
row_i++; row_i++;
} }
@ -586,7 +580,7 @@ bool EGaussian::find_truths(
svector<gauss_watched>& ws, svector<gauss_watched>& ws,
unsigned& i, unsigned& i,
unsigned& j, unsigned& j,
unsigned var, bool_var var,
unsigned row_n, unsigned row_n,
gauss_data& gqd) { gauss_data& gqd) {
@ -683,8 +677,6 @@ bool EGaussian::find_truths(
TRACE("xor", tout << "--> found new watch: " << new_resp_var+1;); TRACE("xor", tout << "--> found new watch: " << new_resp_var+1;);
find_truth_ret_fnewwatch++; find_truth_ret_fnewwatch++;
// printf("%d:This row is find new watch:%d => orig %d p:%d n",row_n ,
// new_resp_var,orig_basic , p);
if (was_resp_var) { if (was_resp_var) {
/// clear watchlist, because only one responsible value in watchlist /// clear watchlist, because only one responsible value in watchlist
@ -785,6 +777,17 @@ void EGaussian::update_cols_vals_set(bool force) {
} }
} }
last_val_update = m_solver.s().trail_size(); last_val_update = m_solver.s().trail_size();
std::cout << "Col-Unassigned: ";
for (int i = 0; i < 64 * cols_unset->size; ++i) {
std::cout << (*cols_unset)[i];
}
std::cout << "\n";
std::cout << "Col-Values: ";
for (int i = 0; i < 64 * cols_vals->size; ++i) {
std::cout << (*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) {

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

@ -46,19 +46,19 @@ namespace xr {
friend class solver; friend class solver;
unsigned matrix_num; unsigned m_matrix_idx;
unsigned row_num; unsigned m_row_idx;
//XOR //XOR
justification(const unsigned matrix_num, const unsigned row_num): justification(unsigned matrix_idx, unsigned row_idx):
matrix_num(matrix_num), m_matrix_idx(matrix_idx),
row_num(row_num) { m_row_idx(row_idx) {
SASSERT(matrix_num != -1); SASSERT(matrix_idx != -1);
SASSERT(row_num != -1); SASSERT(row_idx != -1);
} }
public: public:
justification() : matrix_num(-1), row_num(-1) {} justification() : m_matrix_idx(-1), m_row_idx(-1) {}
void deallocate(small_object_allocator& a) { a.deallocate(get_obj_size(), sat::constraint_base::mem2base_ptr(this)); } void deallocate(small_object_allocator& a) { a.deallocate(get_obj_size(), sat::constraint_base::mem2base_ptr(this)); }
sat::ext_constraint_idx to_index() const { return sat::constraint_base::mem2base(this); } sat::ext_constraint_idx to_index() const { return sat::constraint_base::mem2base(this); }
@ -67,20 +67,20 @@ namespace xr {
} }
static size_t get_obj_size() { return sat::constraint_base::obj_size(sizeof(justification)); } static size_t get_obj_size() { return sat::constraint_base::obj_size(sizeof(justification)); }
unsigned get_matrix_num() const { unsigned get_matrix_idx() const {
return matrix_num; return m_matrix_idx;
} }
unsigned get_row_num() const { unsigned get_row_idx() const {
return row_num; return m_row_idx;
} }
bool isNull() const { bool isNull() const {
return matrix_num == -1; return m_matrix_idx == -1;
} }
bool operator==(const justification other) const { bool operator==(const justification other) const {
return matrix_num == other.matrix_num && row_num == other.row_num; return m_matrix_idx == other.m_matrix_idx && m_row_idx == other.m_row_idx;
} }
bool operator!=(const justification other) const { bool operator!=(const justification other) const {
@ -90,7 +90,7 @@ namespace xr {
inline std::ostream& operator<<(std::ostream& os, const justification& pb) { inline std::ostream& operator<<(std::ostream& os, const justification& pb) {
if (!pb.isNull()) { if (!pb.isNull()) {
return os << " xor reason, matrix= " << pb.get_matrix_num() << " row: " << pb.get_row_num(); return os << " xor reason, matrix= " << pb.get_matrix_idx() << " row: " << pb.get_row_idx();
} }
return os << " NULL"; return os << " NULL";
} }
@ -198,15 +198,15 @@ namespace xr {
return false; return false;
} }
const unsigned& operator[](const unsigned at) const { const unsigned& operator[](unsigned at) const {
return m_vars[at]; return m_vars[at];
} }
unsigned& operator[](const unsigned at) { unsigned& operator[](unsigned at) {
return m_vars[at]; return m_vars[at];
} }
void shrink(const unsigned newsize) { void shrink(unsigned newsize) {
m_vars.shrink(newsize); m_vars.shrink(newsize);
} }
@ -274,8 +274,8 @@ namespace xr {
friend class PackedMatrix; friend class PackedMatrix;
friend class EGaussian; friend class EGaussian;
PackedRow(const unsigned _size, int64_t* const _mp) : PackedRow(unsigned _size, int64_t* const _mp) :
mp(_mp+1), mp(_mp + 1),
rhs_internal(*_mp), rhs_internal(*_mp),
size(_size) {} size(_size) {}
@ -375,7 +375,7 @@ namespace xr {
} }
} }
inline bool operator[](const unsigned i) const { inline bool operator[](unsigned i) const {
return (mp[i / 64] >> (i % 64)) & 1; return (mp[i / 64] >> (i % 64)) & 1;
} }
@ -414,7 +414,7 @@ namespace xr {
void get_reason( void get_reason(
literal_vector& tmp_clause, literal_vector& tmp_clause,
const unsigned_vector& col_to_var, const unsigned_vector& column_to_var,
PackedRow& cols_vals, PackedRow& cols_vals,
PackedRow& tmp_col2, PackedRow& tmp_col2,
literal prop literal prop
@ -441,7 +441,7 @@ namespace xr {
#endif #endif
} }
void resize(const unsigned num_rows, unsigned num_cols) { void resize(unsigned num_rows, unsigned num_cols) {
num_cols = num_cols / 64 + (bool)(num_cols % 64); num_cols = num_cols / 64 + (bool)(num_cols % 64);
if (numRows * (numCols + 1) < (int)num_rows * ((int)num_cols + 1)) { if (numRows * (numCols + 1) < (int)num_rows * ((int)num_cols + 1)) {
size_t size = sizeof(int64_t) * num_rows*(num_cols+1); size_t size = sizeof(int64_t) * num_rows*(num_cols+1);
@ -458,7 +458,7 @@ namespace xr {
numCols = num_cols; numCols = num_cols;
} }
void resizeNumRows(const unsigned num_rows) { void resizeNumRows(unsigned num_rows) {
SASSERT((int)num_rows <= numRows); SASSERT((int)num_rows <= numRows);
numRows = num_rows; numRows = num_rows;
} }
@ -564,12 +564,12 @@ namespace xr {
~EGaussian(); ~EGaussian();
bool is_initialized() const; bool is_initialized() const;
///returns FALSE in case of conflict // returns FALSE in case of conflict
bool find_truths( bool find_truths(
svector<gauss_watched>& ws, svector<gauss_watched>& ws,
unsigned& i, unsigned& i,
unsigned& j, unsigned& j,
unsigned var, bool_var var,
unsigned row_n, unsigned row_n,
gauss_data& gqd gauss_data& gqd
); );
@ -589,6 +589,26 @@ namespace xr {
void update_matrix_no(unsigned n); void update_matrix_no(unsigned n);
void check_watchlist_sanity(); void check_watchlist_sanity();
void move_back_xor_clauses(); void move_back_xor_clauses();
void output_variable_assignment(std::ostream& out, sat::solver* s) {
for (unsigned i = 0; i < m_num_cols; i++) {
out << "v" << m_column_to_var[i] << "=" << (s->value(m_column_to_var[i]) == l_undef ? "?" : (s->value(m_column_to_var[i]) == l_true ? "1" : "0")) << " ";
}
out << std::endl;
for (unsigned i = 0; i < m_num_cols; i++) {
out << "v" << m_column_to_var[i] << "=";
if (s->get_justification(m_column_to_var[i]).is_none())
out << "d";
else if (s->get_justification(m_column_to_var[i]).is_binary_clause())
out << "b";
else if (s->get_justification(m_column_to_var[i]).is_clause())
out << "c";
else
out << "j" << s->get_justification(m_column_to_var[i]).get_ext_justification_idx();
out << " ";
}
out << std::endl;
}
private: private:
xr::solver& m_solver; // original sat solver xr::solver& m_solver; // original sat solver
@ -652,9 +672,13 @@ namespace xr {
// TODO: Maybe compress further // TODO: Maybe compress further
bool_vector satisfied_xors; bool_vector satisfied_xors;
// Someone is responsible for this column if TRUE // Someone is responsible for this column if the respective entry is true
// we always WATCH this variable // we always WATCH this variable
// A variable is responsible if there is only one row that has a 1 there // A variable is responsible if there is only one row that has a 1 there
// v1 v2 v3
// 1 0 1
// 0 1 1
// "row 0" is responsible for v1, "row 1" is responsible for v2
bool_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

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

@ -227,9 +227,24 @@ namespace xr {
return sat::justification(-1); return sat::justification(-1);
} }
void solver::get_antecedents(sat::literal l, sat::ext_justification_idx idx, void solver::get_antecedents(literal l, sat::ext_justification_idx idx,
sat::literal_vector & r, bool probing) { literal_vector & r, bool probing) {
auto& j = justification::from_index(idx);
int32_t ID;
literal_vector* cl = m_gmatrices[j.get_matrix_idx()]->get_reason(j.get_row_idx(), ID);
std::cout << "Justification from matrix " << j.get_matrix_idx() << " on row " << j.get_row_idx() << " (ID: " << ID << "):\n";
for (unsigned i = 0; i < cl->size(); i++) {
std::cout << (*cl)[i] << "(" << s().value((*cl)[i]) << ") ";
(*cl)[i].neg();
}
std::cout << std::endl;
r.append(*cl);
std::cout << "Overall assignments: ";
m_gmatrices[j.get_matrix_idx()]->output_variable_assignment(std::cout, &s());
} }
sat::check_result solver::check() { sat::check_result solver::check() {
@ -342,7 +357,7 @@ namespace xr {
s().set_conflict(); s().set_conflict();
return false; return false;
case 1: { case 1: {
s().assign_scoped(sat::literal(constraint[0], !constraint.m_rhs)); s().assign_scoped(literal(constraint[0], !constraint.m_rhs));
s().propagate(false); s().propagate(false);
return false; return false;
} }