mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

comments, minor

Browse source
This commit is contained in:
Jakob Rath 2023-03-29 15:53:22 +02:00
parent 1f58a906ed
commit 67a4480410
1 changed files with 5 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/math/polysat/solver.cpp
View file

@ -1054,7 +1054,7 @@ namespace polysat {
unsigned max_level = 0; // highest level in lemma
unsigned lits_at_max_level = 0; // how many literals at the highest level in lemma
unsigned snd_level = 0; // second-highest level in lemma
unsigned num_undef = 0; // whether there is an unassigned literal (at most one)
unsigned num_undef = 0; // number of unassigned literals
for (sat::literal lit : lemma) {
switch (m_bvars.value(lit)) {
case l_true:
@ -1062,6 +1062,8 @@ namespace polysat {
case l_false:
break;
default:
// TODO: Entering this case means we used clause_builder::insert at some point where it should have been clause_builder::insert_eval?
// Maybe we should just get rid of the insert/insert_eval distinction and evaluate everything here.
switch (lit2cnstr(lit).eval(*this)) {
case l_true:
return std::nullopt;
@ -1070,15 +1072,11 @@ namespace polysat {
break;
case l_undef:
++num_undef;
// NSB: we used to not return null here.
// Lemmas that were not false under evaluation are now skipped
// with this change.
if (num_undef > 1)
return std::nullopt;
continue;
}
}
unsigned const lit_level = m_bvars.level(lit);
if (lit_level > max_level) {
snd_level = max_level;
@ -1103,8 +1101,8 @@ namespace polysat {
// backjump to max_level so we can propagate
unsigned jump_level;
unsigned branching_factor = lits_at_max_level;
if (num_undef == 1)
jump_level = max_level, branching_factor = 1;
if (num_undef >= 1)
jump_level = max_level, branching_factor = num_undef;
else if (lits_at_max_level <= 1)
jump_level = snd_level;
else
@ -1316,12 +1314,6 @@ namespace polysat {
return lit;
}
/**
* Activate constraint immediately
* Activation and de-activation of constraints follows the scope controlled by push/pop.
* constraints activated within the linear solver are de-activated when the linear
* solver is popped.
*/
void solver::activate_constraint(signed_constraint c) {
SASSERT(c);
LOG("Activating constraint: " << c);