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

Bugfix hashmap insertion

Browse source
This commit is contained in:
Clemens Eisenhofer 2022-11-30 12:05:42 +01:00
parent dc9069641c
commit 15a5c97943
3 changed files with 27 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -34,6 +34,7 @@ namespace xr {
else if (comp_num != m_table[v]) // Another var in this XOR belongs to another component else if (comp_num != m_table[v]) // Another var in this XOR belongs to another component
return false; return false;
} }
// All variables in the xor clause belongs to the same matrix
return true; return true;
} }
@ -48,7 +49,6 @@ namespace xr {
m_table.resize(m_sat.num_vars(), l_undef); m_table.resize(m_sat.num_vars(), l_undef);
m_reverseTable.reset(); m_reverseTable.reset();
clash_vars_unused.reset(); clash_vars_unused.reset();
m_matrix_no = 0;
for (auto& x: m_xor.m_xorclauses_unused) for (auto& x: m_xor.m_xorclauses_unused)
m_xor.m_xorclauses.push_back(x); m_xor.m_xorclauses.push_back(x);
@ -79,23 +79,27 @@ namespace xr {
return true; return true;
} }
unsigned_vector newSet; // Separate xor constraints in multiple gaussian matrixes
unsigned_vector tomerge; // Two xor clauses have to belong to the same matrix if they share at least one variable
bool_var_vector newSet;
unsigned_vector to_merge;
unsigned matrix_no = 0;
for (const xor_clause& x : m_xor.m_xorclauses) { for (const xor_clause& x : m_xor.m_xorclauses) {
if (belong_same_matrix(x)) if (belong_same_matrix(x))
continue; continue;
tomerge.reset(); to_merge.reset();
newSet.clear(); newSet.clear();
for (unsigned v : x) { for (bool_var v : x) {
if (m_table[v] != l_undef) if (m_table[v] != l_undef)
tomerge.push_back(m_table[v]); to_merge.push_back(m_table[v]);
else else
newSet.push_back(v); newSet.push_back(v);
} }
if (tomerge.size() == 1) { if (to_merge.size() == 1) {
const unsigned into = *tomerge.begin(); const unsigned into = *to_merge.begin();
unsigned_vector& intoReverse = m_reverseTable.find(into); unsigned_vector& intoReverse = m_reverseTable[into];
for (unsigned i = 0; i < newSet.size(); i++) { for (unsigned i = 0; i < newSet.size(); i++) {
intoReverse.push_back(newSet[i]); intoReverse.push_back(newSet[i]);
m_table[newSet[i]] = into; m_table[newSet[i]] = into;
@ -103,29 +107,28 @@ namespace xr {
continue; continue;
} }
for (unsigned v: tomerge) { for (unsigned v: to_merge) {
for (const auto& v2 : m_reverseTable[v]) { for (const auto& v2 : m_reverseTable[v]) {
newSet.insert(v2); newSet.insert(v2);
} }
m_reverseTable.erase(v); m_reverseTable.erase(v);
} }
for (auto j : newSet) for (auto j : newSet)
m_table[j] = m_matrix_no; m_table[j] = matrix_no;
m_reverseTable[m_matrix_no] = newSet; m_reverseTable.insert(matrix_no++, newSet);
m_matrix_no++;
} }
set_matrixes(); set_matrixes(matrix_no);
return !m_sat.inconsistent(); return !m_sat.inconsistent();
} }
unsigned xor_matrix_finder::set_matrixes() { unsigned xor_matrix_finder::set_matrixes(unsigned matrix_no) {
svector<matrix_shape> matrix_shapes; svector<matrix_shape> matrix_shapes;
vector<vector<xor_clause>> xors_in_matrix(m_matrix_no); vector<vector<xor_clause>> xors_in_matrix(matrix_no);
for (unsigned i = 0; i < m_matrix_no; i++) { for (unsigned i = 0; i < matrix_no; i++) {
matrix_shapes.push_back(matrix_shape(i)); matrix_shapes.push_back(matrix_shape(i));
matrix_shapes[i].m_num = i; matrix_shapes[i].m_num = i;
matrix_shapes[i].m_cols = m_reverseTable[i].size(); matrix_shapes[i].m_cols = m_reverseTable[i].size();
@ -134,7 +137,7 @@ namespace xr {
for (xor_clause& x : m_xor.m_xorclauses) { for (xor_clause& x : m_xor.m_xorclauses) {
// take 1st variable to check which matrix it's in. // take 1st variable to check which matrix it's in.
const unsigned matrix = m_table[x[0]]; const unsigned matrix = m_table[x[0]];
SASSERT(matrix < m_matrix_no); SASSERT(matrix < matrix_no);
//for stats //for stats
matrix_shapes[matrix].m_rows ++; matrix_shapes[matrix].m_rows ++;
@ -155,7 +158,7 @@ namespace xr {
unsigned unusedMatrix = 0; unsigned unusedMatrix = 0;
unsigned too_few_rows_matrix = 0; unsigned too_few_rows_matrix = 0;
unsigned unused_matrix_printed = 0; unsigned unused_matrix_printed = 0;
for (unsigned a = m_matrix_no; a-- > 0; ) { for (unsigned a = matrix_no; a-- > 0; ) {
matrix_shape& m = matrix_shapes[a]; matrix_shape& m = matrix_shapes[a];
unsigned i = m.m_num; unsigned i = m.m_num;
if (m.m_rows == 0) if (m.m_rows == 0)

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

@ -51,13 +51,12 @@ namespace xr {
u_map<unsigned_vector> m_reverseTable; //matrix -> vars u_map<unsigned_vector> m_reverseTable; //matrix -> vars
unsigned_vector m_table; //var -> matrix unsigned_vector m_table; //var -> matrix
unsigned m_matrix_no = 0;
sorter m_sorter; sorter m_sorter;
solver& m_xor; solver& m_xor;
sat::solver& m_sat; sat::solver& m_sat;
unsigned set_matrixes(); unsigned set_matrixes(unsigned matrix_no);
inline bool belong_same_matrix(const xor_clause& x); inline bool belong_same_matrix(const xor_clause& x);

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

@ -489,6 +489,7 @@ namespace xr {
return std::any_of(x.begin(), x.end(), [&](bool_var v) { return s().num_visited(v) > 1; }); return std::any_of(x.begin(), x.end(), [&](bool_var v) { return s().num_visited(v) > 1; });
} }
// moves all non-detached (as those are anyway relevant) xor clauses which variables occur in no other xor clause to unused
void solver::move_xors_without_connecting_vars_to_unused() { void solver::move_xors_without_connecting_vars_to_unused() {
if (m_xorclauses.empty()) if (m_xorclauses.empty())
return; return;
@ -497,12 +498,12 @@ namespace xr {
s().init_visited(2); s().init_visited(2);
for (const xor_clause& x: m_xorclauses) for (const xor_clause& x: m_xorclauses)
for (unsigned v : x) for (bool_var v : x)
s().inc_visited(v); s().inc_visited(v);
//has at least 1 var with occur of 2 //has at least 1 var with occur of 2
for (const xor_clause& x: m_xorclauses) { for (const xor_clause& x: m_xorclauses) {
bool has_connecting_var = xor_has_interesting_var(x) || x.m_detached; bool has_connecting_var = x.m_detached || xor_has_interesting_var(x);
TRACE("xor", tout << "XOR " << (has_connecting_var ? "" : "has no") << "connecting var : " << x << ")\n"); TRACE("xor", tout << "XOR " << (has_connecting_var ? "" : "has no") << "connecting var : " << x << ")\n");
if (has_connecting_var) if (has_connecting_var)