mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-12 11:54:07 +00:00
Code Activity

fix #8552

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-02-10 17:21:14 -08:00
parent 71bf76e76c
commit 9f35314188
1 changed files with 23 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1335,12 +1335,10 @@ namespace pb {
solver::~solver() {
m_stats.reset();
for (constraint* c : m_constraints) {
c->deallocate(m_allocator);
}
for (constraint* c : m_learned) {
c->deallocate(m_allocator);
}
for (constraint* c : m_constraints)
c->deallocate(m_allocator);
for (constraint* c : m_learned)
c->deallocate(m_allocator);
}
void solver::add_at_least(bool_var v, literal_vector const& lits, unsigned k) {
@ -1372,6 +1370,17 @@ namespace pb {
if (!learned && clausify(lit, lits.size(), lits.data(), k)) {
return nullptr;
}
init_visited();
for (literal l : lits) {
auto v = l.var();
if (is_visited(v)) {
svector<wliteral> wlits;
for (literal l : lits)
wlits.push_back(wliteral(1, l));
return add_pb_ge(lit, wlits, k, learned);
}
mark_visited(v);
}
void * mem = m_allocator.allocate(card::get_obj_size(lits.size()));
sat::constraint_base::initialize(mem, this);
card* c = new (sat::constraint_base::ptr2mem(mem)) card(next_id(), lit, lits, k);
@ -1450,6 +1459,14 @@ namespace pb {
s().add_clause(~lit, sat::status::th(false, get_id()));
return nullptr;
}
init_visited();
for (auto const&[w, l] : wlits) {
auto v = l.var();
if (is_visited(v)) {
throw default_exception("malformed constraint: variable appears more than once - is pre-processing disabled?");
}
mark_visited(v);
}
if (!learned) {
for (auto [w, l] : wlits)
s().set_external(l.var());