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

fix mux extraction to check for top-level assertion

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-31 11:57:16 -08:00
parent 62bb234251
commit 6422b783b2
1 changed files with 25 additions and 21 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
src/sat/smt/pb_solver.cpp
View file

@ -21,6 +21,7 @@ Author:
#include "sat/smt/pb_solver.h"
#include "sat/smt/euf_solver.h"
#include "sat/sat_simplifier_params.hpp"
#include "sat/sat_scc.h"
namespace pb {
@ -1422,7 +1423,7 @@ namespace pb {
c->watch_literal(*this, ~lit);
}
if (!c->well_formed())
std::cout << *c << "\n";
IF_VERBOSE(0, verbose_stream() << *c << "\n");
VERIFY(c->well_formed());
if (m_solver && m_solver->get_config().m_drat) {
std::function<void(std::ostream& out)> fn = [&](std::ostream& out) {
@ -3133,32 +3134,35 @@ namespace pb {
void solver::find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) {
sat::literal_set slits(lits);
bool change = false;
for (constraint* cp : m_constraints) {
if (!cp->is_card()) continue;
if (!cp->is_card())
continue;
if (cp->lit() != sat::null_literal)
continue;
card const& c = cp->to_card();
if (c.size() == c.k() + 1) {
literal_vector mux;
for (literal lit : c) {
if (slits.contains(~lit)) {
mux.push_back(~lit);
}
}
if (mux.size() <= 1) {
continue;
}
if (c.size() != c.k() + 1)
continue;
for (literal m : mux) {
slits.remove(m);
}
change = true;
mutexes.push_back(mux);
}
literal_vector mux;
for (literal lit : c)
if (slits.contains(~lit))
mux.push_back(~lit);
if (mux.size() <= 1)
continue;
for (literal m : mux)
slits.remove(m);
change = true;
mutexes.push_back(mux);
}
if (!change) return;
if (!change)
return;
lits.reset();
for (literal l : slits) {
for (literal l : slits)
lits.push_back(l);
}
}
void solver::display(std::ostream& out, ineq const& ineq, bool values) const {