From 15a5c979437a20370baa3fa720d5fb0603854b5c Mon Sep 17 00:00:00 2001 From: Clemens Eisenhofer Date: Wed, 30 Nov 2022 12:05:42 +0100 Subject: [PATCH] Bugfix hashmap insertion --- src/sat/smt/xor_matrix_finder.cpp | 41 +++++++++++++++++-------------- src/sat/smt/xor_matrix_finder.h | 3 +-- src/sat/smt/xor_solver.cpp | 7 +++--- 3 files changed, 27 insertions(+), 24 deletions(-) diff --git a/src/sat/smt/xor_matrix_finder.cpp b/src/sat/smt/xor_matrix_finder.cpp index ecc9a77a0..dd35e2c55 100644 --- a/src/sat/smt/xor_matrix_finder.cpp +++ b/src/sat/smt/xor_matrix_finder.cpp @@ -34,6 +34,7 @@ namespace xr { else if (comp_num != m_table[v]) // Another var in this XOR belongs to another component return false; } + // All variables in the xor clause belongs to the same matrix return true; } @@ -48,7 +49,6 @@ namespace xr { m_table.resize(m_sat.num_vars(), l_undef); m_reverseTable.reset(); clash_vars_unused.reset(); - m_matrix_no = 0; for (auto& x: m_xor.m_xorclauses_unused) m_xor.m_xorclauses.push_back(x); @@ -79,23 +79,27 @@ namespace xr { return true; } - unsigned_vector newSet; - unsigned_vector tomerge; + // Separate xor constraints in multiple gaussian matrixes + // 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) { if (belong_same_matrix(x)) continue; - tomerge.reset(); + to_merge.reset(); newSet.clear(); - for (unsigned v : x) { + for (bool_var v : x) { if (m_table[v] != l_undef) - tomerge.push_back(m_table[v]); + to_merge.push_back(m_table[v]); else newSet.push_back(v); } - if (tomerge.size() == 1) { - const unsigned into = *tomerge.begin(); - unsigned_vector& intoReverse = m_reverseTable.find(into); + if (to_merge.size() == 1) { + const unsigned into = *to_merge.begin(); + unsigned_vector& intoReverse = m_reverseTable[into]; for (unsigned i = 0; i < newSet.size(); i++) { intoReverse.push_back(newSet[i]); m_table[newSet[i]] = into; @@ -103,29 +107,28 @@ namespace xr { continue; } - for (unsigned v: tomerge) { + for (unsigned v: to_merge) { for (const auto& v2 : m_reverseTable[v]) { newSet.insert(v2); } m_reverseTable.erase(v); } for (auto j : newSet) - m_table[j] = m_matrix_no; - m_reverseTable[m_matrix_no] = newSet; - m_matrix_no++; + m_table[j] = matrix_no; + m_reverseTable.insert(matrix_no++, newSet); } - set_matrixes(); + set_matrixes(matrix_no); return !m_sat.inconsistent(); } - unsigned xor_matrix_finder::set_matrixes() { + unsigned xor_matrix_finder::set_matrixes(unsigned matrix_no) { svector matrix_shapes; - vector> xors_in_matrix(m_matrix_no); + vector> 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[i].m_num = i; matrix_shapes[i].m_cols = m_reverseTable[i].size(); @@ -134,7 +137,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]]; - SASSERT(matrix < m_matrix_no); + SASSERT(matrix < matrix_no); //for stats matrix_shapes[matrix].m_rows ++; @@ -155,7 +158,7 @@ namespace xr { unsigned unusedMatrix = 0; unsigned too_few_rows_matrix = 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]; unsigned i = m.m_num; if (m.m_rows == 0) diff --git a/src/sat/smt/xor_matrix_finder.h b/src/sat/smt/xor_matrix_finder.h index 6e1095dab..99165b563 100644 --- a/src/sat/smt/xor_matrix_finder.h +++ b/src/sat/smt/xor_matrix_finder.h @@ -51,13 +51,12 @@ namespace xr { u_map m_reverseTable; //matrix -> vars unsigned_vector m_table; //var -> matrix - unsigned m_matrix_no = 0; sorter m_sorter; solver& m_xor; sat::solver& m_sat; - unsigned set_matrixes(); + unsigned set_matrixes(unsigned matrix_no); inline bool belong_same_matrix(const xor_clause& x); diff --git a/src/sat/smt/xor_solver.cpp b/src/sat/smt/xor_solver.cpp index 7c1b66477..a605efcb0 100644 --- a/src/sat/smt/xor_solver.cpp +++ b/src/sat/smt/xor_solver.cpp @@ -489,6 +489,7 @@ namespace xr { 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() { if (m_xorclauses.empty()) return; @@ -497,13 +498,13 @@ namespace xr { s().init_visited(2); for (const xor_clause& x: m_xorclauses) - for (unsigned v : x) + for (bool_var v : x) s().inc_visited(v); //has at least 1 var with occur of 2 for (const xor_clause& x: m_xorclauses) { - bool has_connecting_var = xor_has_interesting_var(x) || x.m_detached; - TRACE("xor", tout << "XOR " << (has_connecting_var?"":"has no") << "connecting var : " << x << ")\n"); + 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"); if (has_connecting_var) cleaned.push_back(x);