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

more

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-10-28 20:18:20 -07:00
parent ca74f696b5
commit 47fd9d8e18
1 changed files with 20 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -9,6 +9,9 @@ Abstract:
Based on CMS (crypto minisat by Mate Soos). Based on CMS (crypto minisat by Mate Soos).
Notes:
- if use-matrices is false, maybe just disable xor? That is don't support dual approach
--*/ --*/
@ -48,25 +51,28 @@ namespace xr {
XorFinder finder(NULL, solver); XorFinder finder(NULL, solver);
for(auto& x: m_solver->xorclauses_unused) m_solver->xorclauses.push_back(std::move(x)); for (auto& x: m_solver->xorclauses_unused)
m_solver->xorclauses_unused.clear(); m_xor.xorclauses.push_back(std::move(x));
m_solver->clauseCleaner->clean_xor_clauses(solver->xorclauses); m_xor.xorclauses_unused.clear();
m_xor.clauseCleaner->clean_xor_clauses(solver->xorclauses);
finder.grab_mem(); finder.grab_mem();
finder.move_xors_without_connecting_vars_to_unused(); finder.move_xors_without_connecting_vars_to_unused();
if (!finder.xor_together_xors(m_solver->xorclauses)) return false; if (!finder.xor_together_xors(m_solver->xorclauses))
return false;
finder.move_xors_without_connecting_vars_to_unused(); finder.move_xors_without_connecting_vars_to_unused();
finder.clean_equivalent_xors(m_solver->xorclauses); finder.clean_equivalent_xors(m_solver->xorclauses);
for(const auto& x: m_solver->xorclauses_unused) for(const auto& x: m_xor.xorclauses_unused)
clash_vars_unused.insert(x.clash_vars.begin(), x.clash_vars.end()); clash_vars_unused.insert(x.clash_vars.begin(), x.clash_vars.end());
if (m_solver->xorclauses.size() < m_solver->conf.gaussconf.min_gauss_xor_clauses) { if (m_xor.xorclauses.size() < m_sat.get_config().m_min_gauss_xor_clauses) {
can_detach = false; can_detach = false;
return true; return true;
} }
//Just one giant matrix. //Just one giant matrix.
// if (m_sat.get_config().m_xor_gauss_do_matrix_find)
if (!m_solver->conf.gaussconf.doMatrixFind) { if (!m_solver->conf.gaussconf.doMatrixFind) {
m_solver->gmatrices.push_back(new EGaussian(m_solver, 0, m_solver->xorclauses)); m_solver->gmatrices.push_back(new EGaussian(m_solver, 0, m_solver->xorclauses));
m_solver->gqueuedata.resize(m_solver->gmatrices.size()); m_solver->gqueuedata.resize(m_solver->gmatrices.size());
@ -74,8 +80,8 @@ namespace xr {
} }
std::vector<uint32_t> newSet; std::vector<uint32_t> newSet;
set<uint32_t> tomerge; uint_set tomerge;
for (const constraint& x : m_solver->m_constraints) { for (const constraint& x : m_xor.m_constraints) {
if (belong_same_matrix(x)) if (belong_same_matrix(x))
continue; continue;
@ -101,19 +107,16 @@ namespace xr {
newSet.insert(newSet.end(), m_reverseTable[v].begin(), m_reverseTable[v].end()); newSet.insert(newSet.end(), m_reverseTable[v].begin(), m_reverseTable[v].end());
m_reverseTable.erase(v); m_reverseTable.erase(v);
} }
for (uint32_t i = 0; i < newSet.size(); i++) for (auto j : newSet)
m_table[newSet[i]] = m_matrix_no; m_table[j] = m_matrix_no;
m_reverseTable[m_matrix_no] = newSet; m_reverseTable[m_matrix_no] = newSet;
m_matrix_no++; m_matrix_no++;
} }
uint32_t numMatrixes = set_matrixes(); set_matrixes();
const bool time_out = false; #endif
return !m_sat.inconsistent();
return !m_solver->inconsistent();
#endif
return false;
} }
unsigned xor_matrix_finder::set_matrixes() { unsigned xor_matrix_finder::set_matrixes() {