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

remove const qualifiers from value types, add code review comment

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-11-15 09:35:50 -08:00
parent fbd775e5f0
commit 8ee3ca1d7c
4 changed files with 41 additions and 41 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -76,7 +76,7 @@ void PackedRow::get_reason(
while (at != 0) {
unsigned col = extra + at - 1 + i * 64;
SASSERT(operator[](col) == 1);
const unsigned var = col_to_var[col];
unsigned var = col_to_var[col];
if (var == prop.var()) {
tmp_clause.push_back(prop);
std::swap(tmp_clause[0], tmp_clause.back());
@ -117,7 +117,7 @@ gret PackedRow::propGause(
int extra = 0;
while (at != 0) {
unsigned col = extra + at-1 + i*64;
const unsigned var = col_to_var[col];
unsigned var = col_to_var[col];
// found new non-basic variable, let's watch it
if (!var_has_resp_row[var]) {
new_resp_var = var;
@ -136,7 +136,7 @@ gret PackedRow::propGause(
//Calc value of row
tmp_col2.set_and(*this, cols_vals);
const unsigned pop_t = tmp_col2.popcnt() + (unsigned)rhs();
unsigned pop_t = tmp_col2.popcnt() + (unsigned)rhs();
SASSERT(pop == 1 || pop == 0);
@ -162,7 +162,7 @@ gret PackedRow::propGause(
return gret::nothing_satisfied;
}
EGaussian::EGaussian(xr::solver& _solver, const unsigned _matrix_no, const vector<xor_clause>& _xorclauses) :
EGaussian::EGaussian(xr::solver& _solver, unsigned _matrix_no, const vector<xor_clause>& _xorclauses) :
m_xorclauses(_xorclauses), m_solver(_solver), matrix_no(_matrix_no) { }
EGaussian::~EGaussian() {
@ -201,7 +201,7 @@ public:
}
}
bool operator()(const unsigned a, const unsigned b) {
bool operator()(unsigned a, unsigned b) {
SASSERT(m_solver.seen.size() > a);
SASSERT(m_solver.seen.size() > b);
if (m_solver.seen[b] && !m_solver.seen[a])
@ -299,7 +299,7 @@ void EGaussian::delete_gauss_watch_this_matrix() {
clear_gwatches(i);
}
void EGaussian::clear_gwatches(const unsigned var) {
void EGaussian::clear_gwatches(unsigned var) {
//if there is only one matrix, don't check, just empty it
if (m_solver.m_gmatrices.empty()) {
m_solver.m_gwatches[var].clear();
@ -391,7 +391,7 @@ bool EGaussian::full_init(bool& created) {
void EGaussian::eliminate() {
// TODO: Why twice? gauss_jordan_elim
const unsigned end_row = num_rows;
unsigned end_row = num_rows;
unsigned rowI = 0;
unsigned row_i = 0;
unsigned col = 0;
@ -431,7 +431,7 @@ void EGaussian::eliminate() {
}
}
literal_vector* EGaussian::get_reason(const unsigned row, int& out_ID) {
literal_vector* EGaussian::get_reason(unsigned row, int& out_ID) {
if (!xor_reasons[row].m_must_recalc) {
out_ID = xor_reasons[row].m_ID;
return &(xor_reasons[row].m_reason);
@ -466,7 +466,7 @@ gret EGaussian::init_adjust_matrix() {
if (row_i >= num_rows)
break;
unsigned non_resp_var;
const unsigned popcnt = row.find_watchVar(tmp_clause, col_to_var, var_has_resp_row, non_resp_var);
unsigned popcnt = row.find_watchVar(tmp_clause, col_to_var, var_has_resp_row, non_resp_var);
switch (popcnt) {
@ -555,7 +555,7 @@ gret EGaussian::init_adjust_matrix() {
}
// Delete this row because we have already add to xor clause, nothing to do anymore
void EGaussian::delete_gausswatch(const unsigned row_n) {
void EGaussian::delete_gausswatch(unsigned row_n) {
// clear nonbasic value watch list
svector<gauss_watched>& ws_t = m_solver.m_gwatches[row_to_var_non_resp[row_n]];
@ -569,7 +569,7 @@ void EGaussian::delete_gausswatch(const unsigned row_n) {
UNREACHABLE();
}
unsigned EGaussian::get_max_level(const gauss_data& gqd, const unsigned row_n) {
unsigned EGaussian::get_max_level(const gauss_data& gqd, unsigned row_n) {
int ID;
literal_vector* cl = get_reason(row_n, ID);
unsigned nMaxLevel = gqd.currLevel;
@ -595,8 +595,8 @@ bool EGaussian::find_truths(
svector<gauss_watched>& ws,
unsigned& i,
unsigned& j,
const unsigned var,
const unsigned row_n,
unsigned var,
unsigned row_n,
gauss_data& gqd) {
SASSERT(gqd.status != gauss_res::confl);
SASSERT(initialized);
@ -800,7 +800,7 @@ void EGaussian::update_cols_vals_set(bool force) {
last_val_update = m_solver.s().trail_size();
}
void EGaussian::prop_lit(const gauss_data& gqd, const unsigned row_i, const literal ret_lit_prop) {
void EGaussian::prop_lit(const gauss_data& gqd, unsigned row_i, const literal ret_lit_prop) {
unsigned level;
if (gqd.currLevel == m_solver.m_num_scopes)
level = gqd.currLevel;
@ -815,10 +815,10 @@ bool EGaussian::inconsistent() const {
}
void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) {
const unsigned new_resp_row_n = gqd.new_resp_row;
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 new_resp_col = var_to_col[gqd.new_resp_var];
unsigned row_i = 0;
elim_called++;
@ -964,7 +964,7 @@ void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) {
// Checking functions below
//////////////////
void EGaussian::check_row_not_in_watch(const unsigned v, const unsigned row_num) const {
void EGaussian::check_row_not_in_watch(unsigned v, unsigned row_num) const {
for (const auto& x: m_solver.m_gwatches[v])
SASSERT(!(x.matrix_num == matrix_no && x.row_n == row_num));
}

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

@ -475,11 +475,11 @@ namespace xr {
return *this;
}
inline PackedRow operator[](const unsigned i) {
inline PackedRow operator[](unsigned i) {
return PackedRow(numCols, mp+i*(numCols+1));
}
inline PackedRow operator[](const unsigned i) const {
inline PackedRow operator[](unsigned i) const {
return PackedRow(numCols, mp+i*(numCols+1));
}
@ -487,7 +487,7 @@ namespace xr {
int64_t* mp;
const unsigned numCols;
iterator(int64_t* _mp, const unsigned _numCols) : mp(_mp), numCols(_numCols) { }
iterator(int64_t* _mp, unsigned _numCols) : mp(_mp), numCols(_numCols) { }
public:
friend class PackedMatrix;
@ -501,7 +501,7 @@ namespace xr {
return *this;
}
iterator operator+(const unsigned num) const {
iterator operator+(unsigned num) const {
iterator ret(*this);
ret.mp += (numCols + 1) * num;
return ret;
@ -511,7 +511,7 @@ namespace xr {
return (unsigned)(mp - b.mp) / (numCols + 1);
}
void operator+=(const unsigned num) {
void operator+=(unsigned num) {
mp += (numCols + 1) * num; // add by f4
}
@ -543,7 +543,7 @@ namespace xr {
public:
EGaussian(
solver& solver,
const unsigned matrix_no,
unsigned matrix_no,
const vector<xor_clause>& xorclauses
);
~EGaussian();
@ -554,12 +554,12 @@ namespace xr {
svector<gauss_watched>& ws,
unsigned& i,
unsigned& j,
const unsigned var,
const unsigned row_n,
unsigned var,
unsigned row_n,
gauss_data& gqd
);
literal_vector* get_reason(const unsigned row, int& out_ID);
literal_vector* get_reason(unsigned row, int& out_ID);
// when basic variable is touched , eliminate one col
void eliminate_col(
@ -581,20 +581,20 @@ namespace xr {
xr::solver& m_solver; // original sat solver
//Cleanup
void clear_gwatches(const unsigned var);
void clear_gwatches(unsigned var);
void delete_gauss_watch_this_matrix();
void delete_gausswatch(const unsigned row_n);
void delete_gausswatch(unsigned row_n);
//Invariant checks, debug
void check_no_prop_or_unsat_rows();
void check_tracked_cols_only_one_set();
bool check_row_satisfied(const unsigned row);
void check_row_not_in_watch(const unsigned v, const unsigned row_num) const;
bool check_row_satisfied(unsigned row);
void check_row_not_in_watch(unsigned v, unsigned row_num) const;
//Reason generation
vector<reason> xor_reasons;
sat::literal_vector tmp_clause;
unsigned get_max_level(const gauss_data& gqd, const unsigned row_n);
unsigned get_max_level(const gauss_data& gqd, unsigned row_n);
//Initialisation
void eliminate();
@ -604,7 +604,7 @@ namespace xr {
double get_density();
//Helper functions
void prop_lit(const gauss_data& gqd, const unsigned row_i, const sat::literal ret_lit_prop);
void prop_lit(const gauss_data& gqd, unsigned row_i, const sat::literal ret_lit_prop);
bool inconsistent() const;
///////////////

7
src/sat/smt/xor_matrix_finder.cpp
View file

@ -94,7 +94,7 @@ namespace xr {
newSet.push_back(v);
}
if (tomerge.size() == 1) {
const unsigned into = *tomerge.begin();
unsigned into = *tomerge.begin();
unsigned_vector& intoReverse = m_reverseTable.find(into);
for (unsigned i = 0; i < newSet.size(); i++) {
intoReverse.push_back(newSet[i]);
@ -104,9 +104,8 @@ namespace xr {
}
for (unsigned v: tomerge) {
for (const auto& v2 : m_reverseTable[v]) {
for (const auto& v2 : m_reverseTable[v])
newSet.insert(v2);
}
m_reverseTable.erase(v);
}
for (auto j : newSet)
@ -133,7 +132,7 @@ namespace xr {
for (xor_clause& x : m_xor.m_xorclauses) {
// take 1st variable to check which matrix it's in.
const unsigned matrix = m_table[x[0]];
unsigned matrix = m_table[x[0]];
SASSERT(matrix < m_matrix_no);
//for stats

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

@ -606,11 +606,9 @@ namespace xr {
while (changed) {
changed = false;
m_interesting.clear();
for (const bool_var l : m_occurrences) {
if (m_occ_cnt[l] == 2 && !s().is_visited(l)) {
for (const bool_var l : m_occurrences)
if (m_occ_cnt[l] == 2 && !s().is_visited(l))
m_interesting.push_back(l);
}
}
while (!m_interesting.empty()) {
@ -622,7 +620,7 @@ namespace xr {
unsigned indexes[2];
unsigned at = 0;
size_t i2 = 0;
unsigned i2 = 0;
sat::watch_list& ws = s().get_wlist(literal(v, false));
//Remove the 2 indexes from the watchlist
@ -632,6 +630,9 @@ namespace xr {
// TODO: Check!!! Is this fine?
ws[i2++] = ws[i];
}
// NSB code review get_ext_constraint_idx() is a pointer.
// If it corresponds to an index in the watch list, use a helper function
// to convert it.
else if (!xors[w.get_ext_constraint_idx()].empty()) {
SASSERT(at < 2);
indexes[at] = w.get_ext_constraint_idx();