mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

handling unsimplified input

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-13 14:40:46 -08:00
parent b259f46f85
commit e816946ddc
2 changed files with 3834 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

3806
enc_temp_folder/e6c4896a12a9fc61d88ea292bf2dca16/pb_solver.cpp Normal file
View file

File diff suppressed because it is too large Load diff

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

@ -1370,14 +1370,20 @@ namespace pb {
s().mk_clause(_lits.size(), _lits.data(), sat::status::th(learned, get_id()));
return nullptr;
}
if (k == 0 && lit == sat::null_literal)
return nullptr;
if (k == 0) {
s().assign_unit(lit);
if (lit != sat::null_literal)
s().add_clause(lit, sat::status::th(false, get_id()));
return nullptr;
}
if (k < lits.size()) {
if (lit == sat::null_literal)
s().add_clause(0, nullptr, sat::status::th(false, get_id()));
else
s().add_clause(~lit, sat::status::th(false, get_id()));
return nullptr;
}
if (!learned && clausify(lit, lits.size(), lits.data(), k)) {
return nullptr;
@ -1440,12 +1446,27 @@ namespace pb {
constraint* solver::add_pb_ge(literal lit, svector<wliteral> const& wlits, unsigned k, bool learned) {
bool units = true;
for (wliteral wl : wlits) units &= wl.first == 1;
if (k == 0 && lit == sat::null_literal) {
for (wliteral wl : wlits)
units &= wl.first == 1;
if (k == 0) {
if (lit != sat::null_literal)
s().add_clause(lit, sat::status::th(false, get_id()));
return nullptr;
}
rational weight(0);
for (auto const [w, l] : wlits)
weight += w;
if (weight < k) {
if (lit == sat::null_literal)
s().add_clause(0, nullptr, sat::status::th(false, get_id()));
else
s().add_clause(~lit, sat::status::th(false, get_id()));
return nullptr;
}
if (!learned) {
for (wliteral wl : wlits) s().set_external(wl.second.var());
for (wliteral wl : wlits)
s().set_external(wl.second.var());
}
if (units || k == 1) {
literal_vector lits;