mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-12 17:06:14 +00:00
Code Activity

Fix vector initialization

Browse source
This commit is contained in:
Clemens Eisenhofer 2022-11-30 12:27:19 +01:00
parent 15a5c97943
commit 0b46b61dc3
1 changed files with 11 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -19,6 +19,8 @@ Notes:
#include "sat/smt/xor_matrix_finder.h" #include "sat/smt/xor_matrix_finder.h"
#include "sat/smt/xor_solver.h" #include "sat/smt/xor_solver.h"
#include <iostream>
namespace xr { namespace xr {
@ -27,7 +29,7 @@ namespace xr {
inline bool xor_matrix_finder::belong_same_matrix(const xor_clause& x) { inline bool xor_matrix_finder::belong_same_matrix(const xor_clause& x) {
unsigned comp_num = -1; unsigned comp_num = -1;
for (sat::bool_var v : x) { for (sat::bool_var v : x) {
if (m_table[v] == l_undef) // Belongs to none, abort if (m_table[v] == (unsigned)-1) // Belongs to none, abort
return false; return false;
if (comp_num == -1) // Belongs to this one if (comp_num == -1) // Belongs to this one
comp_num = m_table[v]; comp_num = m_table[v];
@ -44,10 +46,7 @@ namespace xr {
SASSERT(m_xor.m_gmatrices.empty()); SASSERT(m_xor.m_gmatrices.empty());
can_detach = true; can_detach = true;
m_table.clear();
m_table.resize(m_sat.num_vars(), l_undef);
m_reverseTable.reset();
clash_vars_unused.reset(); clash_vars_unused.reset();
for (auto& x: m_xor.m_xorclauses_unused) for (auto& x: m_xor.m_xorclauses_unused)
@ -85,14 +84,20 @@ namespace xr {
unsigned_vector to_merge; unsigned_vector to_merge;
unsigned matrix_no = 0; unsigned matrix_no = 0;
m_table.clear();
m_table.resize(m_sat.num_vars(), (unsigned)-1);
m_reverseTable.reset();
for (const xor_clause& x : m_xor.m_xorclauses) { for (const xor_clause& x : m_xor.m_xorclauses) {
std::cout << x << std::endl;
if (belong_same_matrix(x)) if (belong_same_matrix(x))
continue; continue;
to_merge.reset(); to_merge.reset();
newSet.clear(); newSet.clear();
for (bool_var v : x) { for (bool_var v : x) {
if (m_table[v] != l_undef) if (m_table[v] != (unsigned)-1)
to_merge.push_back(m_table[v]); to_merge.push_back(m_table[v]);
else else
newSet.push_back(v); newSet.push_back(v);