mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

Changes

Browse source
This commit is contained in:
CEisenhofer 2022-11-30 10:49:41 +01:00
parent 2ef27064c7
commit dc9069641c
4 changed files with 102 additions and 46 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -816,27 +816,27 @@ bool EGaussian::inconsistent() const {
void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) {
const unsigned new_resp_row_n = gqd.new_resp_row;
PackedMatrix::iterator rowI = mat.begin();
PackedMatrix::iterator end = mat.end();
const unsigned new_resp_col = var_to_col[gqd.new_resp_var];
unsigned row_size = mat.num_rows();
unsigned row_i = 0;
elim_called++;
while (rowI != end) {
while (row_i < row_size) {
//Row has a '1' in eliminating column, and it's not the row responsible
if (new_resp_row_n != row_i && (*rowI)[new_resp_col]) {
PackedRow row = mat[row_i];
if (new_resp_row_n != row_i && row[new_resp_col]) {
// detect orignal non-basic watch list change or not
unsigned orig_non_resp_var = row_to_var_non_resp[row_i];
unsigned orig_non_resp_col = var_to_col[orig_non_resp_var];
SASSERT((*rowI)[orig_non_resp_col]);
SASSERT(row[orig_non_resp_col]);
TRACE("xor", tout << "--> This row " << row_i
<< " is being watched on var: " << orig_non_resp_var + 1
<< " i.e. it must contain '1' for this var's column";);
SASSERT(!satisfied_xors[row_i]);
(*rowI).xor_in(*(mat.begin() + new_resp_row_n));
row.xor_in(*(mat.begin() + new_resp_row_n));
elim_xored_rows++;
@ -844,7 +844,7 @@ void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) {
// (it's the only '1' in that column).
// But non-responsible can be eliminated. So let's check that
// and then deal with it if we have to
if (!(*rowI)[orig_non_resp_col]) {
if (!row[orig_non_resp_col]) {
// Delete orignal non-responsible var from watch list
if (orig_non_resp_var != gqd.new_resp_var) {
@ -857,7 +857,7 @@ void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) {
literal ret_lit_prop;
unsigned new_non_resp_var = 0;
const gret ret = (*rowI).propGause(
const gret ret = row.propGause(
col_to_var,
var_has_resp_row,
new_non_resp_var,
@ -950,7 +950,6 @@ void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) {
TRACE("xor", tout << "--> OK, this row " << row_i << " still contains '1', can still be responsible";);
}
}
++rowI;
row_i++;
}

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

@ -476,11 +476,11 @@ namespace xr {
}
inline PackedRow operator[](const unsigned i) {
return PackedRow(numCols, mp+i*(numCols+1));
return PackedRow(numCols, mp + i * (numCols + 1));
}
inline PackedRow operator[](const unsigned i) const {
return PackedRow(numCols, mp+i*(numCols+1));
return PackedRow(numCols, mp + i * (numCols + 1));
}
class iterator {
@ -497,7 +497,7 @@ namespace xr {
}
iterator& operator++() {
mp += (numCols+1);
mp += numCols + 1;
return *this;
}
@ -529,9 +529,17 @@ namespace xr {
}
inline iterator end() {
return iterator(mp+numRows*(numCols+1), numCols);
return iterator(mp+numRows* (numCols + 1), numCols);
}
inline unsigned num_rows() const {
return numRows;
}
inline unsigned num_cols() const {
return numCols;
}
private:
int64_t* mp = nullptr;

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

@ -71,7 +71,7 @@ namespace xr {
lastlit_added = to_add;
}
// TODO: Implement the following function. Unfortunately, it is needed
// TODO: Implement the following function. Unfortunately, it is needed (every xor constraint is also present as an ordinary CNF; e.g., if there is only a single xor constraint no GJ elimination will be performed)
// add_xor_clause_inter_cleaned_cut(xorlits, attach);
if (s().inconsistent())
break;
@ -109,12 +109,16 @@ namespace xr {
if (rhs)
ps[0].neg();
add_every_combination_xor(ps, attach);
//add_every_combination_xor(ps, attach); TODO: Blasts xors; ignored for now
if (ps.size() > 2) {
m_xor_clauses_updated = true;
m_xorclauses.push_back(xor_clause(ps, rhs, m_tmp_xor_clash_vars));
m_xorclauses_orig.push_back(xor_clause(ps, rhs, m_tmp_xor_clash_vars));
}
else {
// TODO: This completely ignore xors of size <= 2. The case of 2 has to be treated with more care
add_simple_xor_constraint(xor_clause(ps, rhs, m_tmp_xor_clash_vars));
}
}
void solver::asserted(sat::literal l) {
@ -170,7 +174,7 @@ namespace xr {
}
else {
confl_in_gauss = true;
i++; // TODO: That's strange, but this is really written this was in CMS
i++;
break;
}
}
@ -280,7 +284,8 @@ namespace xr {
std::ostream& solver::display(std::ostream& out) const {
return out;
}
// simplify xors by triggering (unit)propagation until nothing changes anymore
bool solver::clean_xor_clauses(vector<xor_clause>& xors) {
SASSERT(!inconsistent());
@ -313,7 +318,51 @@ namespace xr {
return !inconsistent();
}
// Adds xor constraints of size 0, 1 and 2. In case the constraint is larger the function returns true
bool solver::add_simple_xor_constraint(const xor_clause& constraint) {
SASSERT(!inconsistent());
switch (constraint.size()) {
case 0:
if (constraint.m_rhs)
s().set_conflict();
return false;
case 1: {
s().assign_scoped(sat::literal(constraint[0], !constraint.m_rhs));
s().propagate(false);
return false;
}
case 2: {
/*literal_vector vec(constraint.size());
for (const auto& v : constraint.m_vars)
vec.push_back(literal(v));
add_xor_clause(vec, constraint.m_rhs, true);*/
/*m_ctx->e_internalize(m_ctx->bool_var2expr(constraint[0]));
m_ctx->e_internalize(m_ctx->bool_var2expr(constraint[1]));
expr* e = m_ctx->mk_eq(m_ctx->bool_var2enode(constraint[0]), m_ctx->bool_var2enode(constraint[1]));
literal l = m_ctx->expr2literal(e);
if (constraint.m_rhs)
l.neg();
s().add_clause(l, sat::status::th(false, get_id()));*/
literal l1(constraint[0]);
literal l2(constraint[1]);
if (constraint.m_rhs) { // not equal
s().add_clause(l1, l2, sat::status::th(false, get_id()));
s().add_clause(~l1, ~l2, sat::status::th(false, get_id()));
}
else { // equal
s().add_clause(l1, ~l2, sat::status::th(false, get_id()));
s().add_clause(~l1, l2, sat::status::th(false, get_id()));
}
return false;
}
default:
return true;
}
}
// throw away all assigned clash-variables and simplify xor-clause with respect to current assignment
// may add conflict or propagate
bool solver::clean_one_xor(xor_clause& x) {
unsigned j = 0;
@ -331,29 +380,10 @@ namespace xr {
x[j++] = v;
}
x.shrink(j);
SASSERT(!inconsistent());
switch (x.size()) {
case 0:
if (x.m_rhs)
s().set_conflict();
return false;
case 1: {
s().assign_scoped(sat::literal(x[0], !x.m_rhs));
s().propagate(false);
return false;
}
case 2: {
literal_vector vec(x.size());
for (const auto& v : x.m_vars)
vec.push_back(literal(v));
add_xor_clause(vec, x.m_rhs, true);
return false;
}
default:
return true;
}
return add_simple_xor_constraint(x);
}
// reset all data-structures. Resets m_xorclauses from m_xorclauses_orig
bool solver::clear_gauss_matrices(const bool destruct) {
// TODO: Include; ignored for now. Maybe we can ignore the detached clauses
/*if (!destruct) {
@ -483,7 +513,8 @@ namespace xr {
m_xorclauses = cleaned;
}
// As the name suggests: Checks if there are (syntactically) equivalent xors and removes all these duplicates
void solver::clean_equivalent_xors(vector<xor_clause>& txors){
if (!txors.empty()) {
for (xor_clause& x: txors)
@ -495,8 +526,8 @@ namespace xr {
unsigned sz = 1;
unsigned j = 0;
for (unsigned i = 1; i < txors.size(); i++) {
auto& jd = txors[j];
auto& id = txors[i];
xor_clause& jd = txors[j];
xor_clause& id = txors[i];
if (jd.m_vars == id.m_vars && jd.m_rhs == id.m_rhs) {
jd.merge_clash(id, m_visited, s().num_vars());
jd.m_detached |= id.m_detached;
@ -518,6 +549,7 @@ namespace xr {
return sat::justification::mk_ext_justification(level, constraint->to_index());
}
// sort xors, eliminate duplicates, and eliminate negations by flipping rhs
void solver::clean_xor_no_prop(sat::literal_vector & ps, bool & rhs) {
std::sort(ps.begin(), ps.end());
sat::literal p_last = sat::null_literal;
@ -728,7 +760,7 @@ namespace xr {
// Remove all watches coming from xor solver
// TODO: Differentiate if the watch came from another theory (not xor)!!
void solver::clean_occur_from_idx(const literal l) {
vector<sat::watched>& ws = s().get_wlist(~l); // the same polarity that was added
vector<sat::watched>& ws = s().get_wlist(l); // the same polarity that was added
unsigned i = 0, j = 0;
const unsigned end = ws.size();
for (; i < end; i++) {

25
src/sat/smt/xor_solver.h
View file

@ -75,6 +75,8 @@ namespace xr {
void clean_xors_from_empty(vector<xor_clause>& thisxors);
unsigned xor_two(xor_clause const* x1_p, xor_clause const* x2_p, bool_var& clash_var);
bool add_simple_xor_constraint(const xor_clause& constraint);
bool inconsistent() const { return s().inconsistent(); }
// TODO: CMS watches the literals directly; Z3 their negation. "_neg_" just for now to avoid confusion
@ -83,11 +85,11 @@ namespace xr {
}
bool is_neg_watched(literal lit, size_t idx) const {
return s().get_wlist(~lit).contains(sat::watched((sat::ext_constraint_idx)idx));
return s().get_wlist(lit).contains(sat::watched((sat::ext_constraint_idx)idx));
}
void unwatch_neg_literal(literal lit, size_t idx) {
s().get_wlist(~lit).erase(sat::watched(idx));
s().get_wlist(lit).erase(sat::watched(idx));
SASSERT(!is_neg_watched(lit, idx));
}
@ -97,10 +99,25 @@ namespace xr {
}
void watch_neg_literal(literal lit, size_t idx) {
watch_neg_literal(s().get_wlist(~lit), idx);
watch_neg_literal(s().get_wlist(lit), idx);
}
static std::string toString(literal l) {
return (std::stringstream() << l).str();
}
static std::string toString(const literal& l) {
return (std::stringstream() << l).str();
}
static std::string toString(const literal_vector& l) {
return (std::stringstream() << l).str();
}
static std::string toString(const bool_var_vector & l) {
return (std::stringstream() << l).str();
}
public:
solver(euf::solver& ctx);
solver(ast_manager& m, euf::theory_id id);