mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 01:13:18 +00:00
Code Activity

fix polarity of antecedents

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-12-07 10:59:51 -08:00
parent 923fcf4771
commit 850d35b95b
4 changed files with 27 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_solver.cpp
View file

@ -2793,6 +2793,7 @@ namespace sat {
bool_var var = antecedent.var(); bool_var var = antecedent.var();
unsigned var_lvl = lvl(var); unsigned var_lvl = lvl(var);
SASSERT(var < num_vars()); SASSERT(var < num_vars());
SASSERT(value(antecedent) == l_true);
TRACE("sat_verbose", tout << "process " << var << "@" << var_lvl << " marked " << is_marked(var) << " conflict " << m_conflict_lvl << "\n";); TRACE("sat_verbose", tout << "process " << var << "@" << var_lvl << " marked " << is_marked(var) << " conflict " << m_conflict_lvl << "\n";);
if (!is_marked(var) && var_lvl > 0) { if (!is_marked(var) && var_lvl > 0) {
mark(var); mark(var);
@ -2823,6 +2824,7 @@ namespace sat {
auto idx = js.get_ext_justification_idx(); auto idx = js.get_ext_justification_idx();
m_ext_antecedents.reset(); m_ext_antecedents.reset();
m_ext->get_antecedents(consequent, idx, m_ext_antecedents, probing); m_ext->get_antecedents(consequent, idx, m_ext_antecedents, probing);
DEBUG_CODE(for (auto lit : m_ext_antecedents) SASSERT(value(lit) == l_true););
} }
bool solver::is_two_phase() const { bool solver::is_two_phase() const {

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

@ -54,7 +54,7 @@ unsigned PackedRow::population_cnt(
} }
// Gets the reason why the literal "prop" was propagated // Gets the reason why the literal "prop" was propagated
void PackedRow::get_reason(literal_vector& tmp_clause, const unsigned_vector& column_to_var, PackedRow& cols_vals, PackedRow& tmp_col2, literal prop) { void PackedRow::get_reason(literal_vector& antecedents, const unsigned_vector& column_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++) {
@ -69,11 +69,11 @@ void PackedRow::get_reason(literal_vector& tmp_clause, const unsigned_vector& co
SASSERT((*this)[col] == 1); SASSERT((*this)[col] == 1);
unsigned var = column_to_var[col]; unsigned var = column_to_var[col];
if (var == prop.var()) { if (var == prop.var()) {
tmp_clause.push_back(~prop); // TODO: Why not negated? antecedents.push_back(prop);
std::swap(tmp_clause[0], tmp_clause.back()); std::swap(antecedents[0], antecedents.back());
} }
else else
tmp_clause.push_back(literal(var, tmp_col2[col])); // NSB: double check if z3 use of sign is compatible antecedents.push_back(literal(var, !tmp_col2[col]));
extra += at; extra += at;
if (extra == 64) if (extra == 64)
@ -416,10 +416,10 @@ void EGaussian::eliminate() {
std::cout << "-------------" << std::endl; std::cout << "-------------" << std::endl;
} }
literal_vector* EGaussian::get_reason(unsigned row, int& out_ID) { literal_vector& EGaussian::get_reason(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;
} }
// Clean up previous one // Clean up previous one
@ -436,7 +436,7 @@ literal_vector* EGaussian::get_reason(unsigned row, int& out_ID) {
xor_reasons[row].m_must_recalc = false; xor_reasons[row].m_must_recalc = false;
xor_reasons[row].m_ID = out_ID; xor_reasons[row].m_ID = out_ID;
return &to_fill; return to_fill;
} }
// Creates binary clauses, assigns variables, adds conflicts based on the (reduced) gaussian-matrix. Also sets up the gaussian watchlist // Creates binary clauses, assigns variables, adds conflicts based on the (reduced) gaussian-matrix. Also sets up the gaussian watchlist
@ -556,12 +556,12 @@ void EGaussian::delete_gausswatch(unsigned row_n) {
unsigned EGaussian::get_max_level(const gauss_data& gqd, unsigned row_n) { unsigned EGaussian::get_max_level(const gauss_data& gqd, unsigned row_n) {
int ID; int ID;
literal_vector* cl = get_reason(row_n, ID); literal_vector& ante = get_reason(row_n, ID);
unsigned nMaxLevel = gqd.currLevel; unsigned nMaxLevel = gqd.currLevel;
unsigned nMaxInd = 1; unsigned nMaxInd = 1;
for (unsigned i = 1; i < cl->size(); i++) { for (unsigned i = ante.size(); i-- > 0; ) {
literal l = (*cl)[i]; literal l = ante[i];
unsigned nLevel = m_solver.s().lvl(l); unsigned nLevel = m_solver.s().lvl(l);
if (nLevel > nMaxLevel) { if (nLevel > nMaxLevel) {
nMaxLevel = nLevel; nMaxLevel = nLevel;
@ -571,7 +571,7 @@ unsigned EGaussian::get_max_level(const gauss_data& gqd, unsigned row_n) {
//should we?? //should we??
if (nMaxInd != 1) if (nMaxInd != 1)
std::swap((*cl)[1], (*cl)[nMaxInd]); std::swap(ante[1], ante[nMaxInd]);
return nMaxLevel; return nMaxLevel;
} }

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

@ -574,7 +574,7 @@ namespace xr {
gauss_data& gqd gauss_data& gqd
); );
literal_vector* get_reason(unsigned row, int& out_ID); literal_vector& get_reason(unsigned row, int& out_ID);
// when basic variable is touched , eliminate one col // when basic variable is touched , eliminate one col
void eliminate_column( void eliminate_column(
@ -590,21 +590,21 @@ namespace xr {
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) { void display_assignment(std::ostream& out, sat::solver& s) {
for (unsigned i = 0; i < m_num_cols; i++) { 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 << "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; out << std::endl;
for (unsigned i = 0; i < m_num_cols; i++) { for (unsigned i = 0; i < m_num_cols; i++) {
out << "v" << m_column_to_var[i] << "="; out << "v" << m_column_to_var[i] << "=";
if (s->get_justification(m_column_to_var[i]).is_none()) if (s.get_justification(m_column_to_var[i]).is_none())
out << "d"; out << "d";
else if (s->get_justification(m_column_to_var[i]).is_binary_clause()) else if (s.get_justification(m_column_to_var[i]).is_binary_clause())
out << "b"; out << "b";
else if (s->get_justification(m_column_to_var[i]).is_clause()) else if (s.get_justification(m_column_to_var[i]).is_clause())
out << "c"; out << "c";
else else
out << "j" << s->get_justification(m_column_to_var[i]).get_ext_justification_idx(); out << "j" << s.get_justification(m_column_to_var[i]).get_ext_justification_idx();
out << " "; out << " ";
} }
out << std::endl; out << std::endl;

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

@ -233,17 +233,16 @@ namespace xr {
auto& j = justification::from_index(idx); auto& j = justification::from_index(idx);
int32_t ID; int32_t ID;
literal_vector* cl = m_gmatrices[j.get_matrix_idx()]->get_reason(j.get_row_idx(), ID); literal_vector const& ante = 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"; 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++) { for (auto lit : ante)
std::cout << (*cl)[i] << "(" << s().value((*cl)[i]) << ") "; std::cout << lit << "(" << s().value(lit) << ") ";
}
std::cout << std::endl; std::cout << std::endl;
r.append(*cl); r.append(ante);
std::cout << "Overall assignments: "; std::cout << "Overall assignments: ";
m_gmatrices[j.get_matrix_idx()]->output_variable_assignment(std::cout, &s()); m_gmatrices[j.get_matrix_idx()]->display_assignment(std::cout, s());
} }
sat::check_result solver::check() { sat::check_result solver::check() {