mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

Fixed justification

Browse source 
(justification may not contain consequence)
This commit is contained in:
Clemens Eisenhofer 2022-12-10 22:29:31 +01:00
parent ed5ce1ce5f
commit 8855163ccf
2 changed files with 6 additions and 6 deletions

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

@ -69,8 +69,8 @@ void PackedRow::get_reason(literal_vector& antecedents, const unsigned_vector& c
SASSERT((*this)[col] == 1);
unsigned var = column_to_var[col];
if (var == prop.var()) {
antecedents.push_back(prop);
std::swap(antecedents[0], antecedents.back());
// In Z3 we should not have the antecedents in the justification
//antecedents.push_back(prop);
}
else
antecedents.push_back(literal(var, !tmp_col2[col]));
@ -373,7 +373,7 @@ std::ostream& EGaussian::display(std::ostream& out) const {
if (m_mat.num_rows() == 0)
return out;
for (auto const& row : m_mat) {
bool first = true;
bool first = true;
for (int i = 0; i < row.get_size() * 64; ++i) {
if (row[i]) {
if (first)

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

@ -127,7 +127,7 @@ namespace xr {
}
}
void solver::asserted(sat::literal l) {
void solver::asserted(literal l) {
TRACE("xor", tout << "asserted: " << l << "\n";);
force_push();
m_prop_queue.push_back(l);
@ -699,7 +699,7 @@ namespace xr {
while (!m_interesting.empty()) {
// Pop and check if it can be XOR-ed together
const unsigned v = m_interesting.back();
bool_var v = m_interesting.back();
m_interesting.pop_back();
if (m_occ_cnt[v] != 2)
continue;
@ -707,7 +707,7 @@ namespace xr {
unsigned indexes[2];
unsigned at = 0;
unsigned_vector& ws = occurs[v];
for (unsigned i : ws)
for (bool_var i : ws)
if (!xors[i].empty())
indexes[at++] = i;
SASSERT(at == 2);