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

fingers starting on xor_gaussian.cpp

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-11-10 13:53:08 -08:00
parent 574f897f93
commit 303fd664c5
3 changed files with 39 additions and 41 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/xor_gaussian.cpp
View file

@ -18,7 +18,7 @@ Abstract:
#include <set> #include <set>
#include <iterator> #include <iterator>
#include "xor_solver.h" #include "sat/smt/xor_solver.h"
using std::ostream; using std::ostream;
using std::set; using std::set;

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

@ -13,11 +13,10 @@ Abstract:
#pragma once #pragma once
#include "sat/smt/euf_solver.h"
#include "util/debug.h" #include "util/debug.h"
#include "util/sat_literal.h" #include "util/sat_literal.h"
#include "util/trace.h" #include "util/trace.h"
#include "sat/smt/euf_solver.h"
namespace xr { namespace xr {

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

@ -166,7 +166,8 @@ namespace xr {
if (m_gmatrices[i->matrix_num]->find_truths(i, j, p.var(), i->row_n, m_gqueuedata[i->matrix_num])) { if (m_gmatrices[i->matrix_num]->find_truths(i, j, p.var(), i->row_n, m_gqueuedata[i->matrix_num])) {
continue; continue;
} else { }
else {
confl_in_gauss = true; confl_in_gauss = true;
i++; i++;
break; break;
@ -227,9 +228,8 @@ namespace xr {
// TODO: we should separate this parts from the euf_solver. Other non-euf theories might need it as well // TODO: we should separate this parts from the euf_solver. Other non-euf theories might need it as well
// Similar: Attaching "theory_var"s in non-euf/enode cases // Similar: Attaching "theory_var"s in non-euf/enode cases
void solver::force_push() { void solver::force_push() {
for (; m_num_scopes > 0; --m_num_scopes) { for (; m_num_scopes > 0; --m_num_scopes)
push_core(); push_core();
}
} }
void solver::push_core() { void solver::push_core() {
@ -299,13 +299,13 @@ namespace xr {
xors[j++] = x; xors[j++] = x;
} }
else { else {
for (const auto& v : x.m_clash_vars) { for (const auto& v : x.m_clash_vars)
m_removed_xorclauses_clash_vars.insert(v); m_removed_xorclauses_clash_vars.insert(v);
}
} }
} }
xors.shrink(j); xors.shrink(j);
if (inconsistent()) break; if (inconsistent())
break;
s().propagate(false); s().propagate(false);
} }
@ -472,21 +472,21 @@ namespace xr {
vector<xor_clause> cleaned; vector<xor_clause> cleaned;
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 (unsigned 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) {
if (xor_has_interesting_var(x) || x.m_detached) { bool has_connecting_var = xor_has_interesting_var(x) || x.m_detached;
TRACE("xor", tout << "XOR has connecting var: " << x << "\n";); TRACE("xor", tout << "XOR " << (has_connecting_var?"":"has no") << "connecting var : " << x << ")\n");
if (has_connecting_var)
cleaned.push_back(x); cleaned.push_back(x);
} else { else
TRACE("xor", tout << "XOR has no connecting var: " << x << "\n";);
m_xorclauses_unused.push_back(x); m_xorclauses_unused.push_back(x);
}
} }
m_xorclauses = cleaned; m_xorclauses = cleaned;
@ -495,9 +495,8 @@ namespace xr {
void solver::clean_equivalent_xors(vector<xor_clause>& txors){ void solver::clean_equivalent_xors(vector<xor_clause>& txors){
if (!txors.empty()) { if (!txors.empty()) {
size_t orig_size = txors.size(); size_t orig_size = txors.size();
for (xor_clause& x: txors) { for (xor_clause& x: txors)
std::sort(x.begin(), x.end()); std::sort(x.begin(), x.end());
}
std::sort(txors.begin(), txors.end()); std::sort(txors.begin(), txors.end());
unsigned sz = 1; unsigned sz = 1;
@ -508,7 +507,8 @@ namespace xr {
if (jd.m_vars == id.m_vars && jd.m_rhs == id.m_rhs) { if (jd.m_vars == id.m_vars && jd.m_rhs == id.m_rhs) {
jd.merge_clash(id, m_visited); jd.merge_clash(id, m_visited);
jd.m_detached |= id.m_detached; jd.m_detached |= id.m_detached;
} else { }
else {
j++; j++;
j = i; j = i;
sz++; sz++;
@ -527,27 +527,26 @@ namespace xr {
void solver::clean_xor_no_prop(sat::literal_vector & ps, bool & rhs) { void solver::clean_xor_no_prop(sat::literal_vector & ps, bool & rhs) {
std::sort(ps.begin(), ps.end()); std::sort(ps.begin(), ps.end());
sat::literal p = sat::null_literal; sat::literal p_last = sat::null_literal;
unsigned i = 0, j = 0; unsigned j = 0;
for (; i != ps.size(); i++) { for (auto p : ps) {
SASSERT(!ps[i].sign()); SASSERT(!p.sign());
if (ps[i].var() == p.var()) { if (p.var() == p_last.var()) {
//added, but easily removed // added, but easily removed
j--; j--;
p = sat::null_literal; p_last = sat::null_literal;
//Flip rhs if necessary // Flip rhs if necessary
if (s().value(ps[i]) != l_undef) { if (s().value(p) != l_undef)
rhs ^= s().value(ps[i]) == l_true; rhs ^= s().value(p) == l_true;
} }
} else if (s().value(ps[i]) == l_undef) { else if (s().value(p) == l_undef)
//Add and remember as last one to have been added // Add and remember as last one to have been added
ps[j++] = p = ps[i]; ps[j++] = p_last = p;
} else { else
//modify rhs instead of adding // modify rhs instead of adding
rhs ^= s().value(ps[i]) == l_true; rhs ^= s().value(p) == l_true;
}
} }
ps.resize(ps.size() - (i - j)); ps.shrink(j);
} }
bool solver::xor_together_xors(vector<xor_clause>& xors) { bool solver::xor_together_xors(vector<xor_clause>& xors) {