mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-08 15:13:23 +00:00
Code Activity

vector -> set

Browse source
This commit is contained in:
Clemens Eisenhofer 2022-11-30 12:35:12 +01:00
parent 0b46b61dc3
commit add66973c5
1 changed files with 3 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -19,9 +19,6 @@ 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 {
xor_matrix_finder::xor_matrix_finder(solver& s) : m_xor(s), m_sat(s.s()) { } xor_matrix_finder::xor_matrix_finder(solver& s) : m_xor(s), m_sat(s.s()) { }
@ -81,7 +78,7 @@ namespace xr {
// Separate xor constraints in multiple gaussian matrixes // Separate xor constraints in multiple gaussian matrixes
// Two xor clauses have to belong to the same matrix if they share at least one variable // Two xor clauses have to belong to the same matrix if they share at least one variable
bool_var_vector newSet; bool_var_vector newSet;
unsigned_vector to_merge; uint_set to_merge;
unsigned matrix_no = 0; unsigned matrix_no = 0;
m_table.clear(); m_table.clear();
@ -89,7 +86,6 @@ namespace xr {
m_reverseTable.reset(); 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;
@ -98,11 +94,11 @@ namespace xr {
newSet.clear(); newSet.clear();
for (bool_var v : x) { for (bool_var v : x) {
if (m_table[v] != (unsigned)-1) if (m_table[v] != (unsigned)-1)
to_merge.push_back(m_table[v]); to_merge.insert(m_table[v]);
else else
newSet.push_back(v); newSet.push_back(v);
} }
if (to_merge.size() == 1) { if (to_merge.num_elems() == 1) {
const unsigned into = *to_merge.begin(); const unsigned into = *to_merge.begin();
unsigned_vector& intoReverse = m_reverseTable[into]; unsigned_vector& intoReverse = m_reverseTable[into];
for (unsigned i = 0; i < newSet.size(); i++) { for (unsigned i = 0; i < newSet.size(); i++) {