mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-01 08:53:18 +00:00
Code Activity

fixes to asserts

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-03-16 11:55:23 +01:00
parent 1ba86c8ce3
commit 93360318b2
3 changed files with 21 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/polysat/conflict.cpp
View file

@ -318,6 +318,7 @@ namespace polysat {
} }
void conflict::restore_lemma(clause_ref lemma) { void conflict::restore_lemma(clause_ref lemma) {
LOG_H3("Restore Lemma: " << ": " << show_deref(lemma));
m_lemmas.push_back(std::move(lemma)); m_lemmas.push_back(std::move(lemma));
} }

2
src/math/polysat/saturation.cpp
View file

@ -1605,7 +1605,7 @@ namespace polysat {
// ==> ax <= y + c if int(y) + int(c) <= 2^N, y <= int(y), c <= int(c) // ==> ax <= y + c if int(y) + int(c) <= 2^N, y <= int(y), c <= int(c)
// ==> a not in [-floor(-int(y+c) / int(x), 0[ // ==> a not in [-floor(-int(y+c) / int(x), 0[
// ==> -a >= floor(-int(y+c) / int(x) // ==> -a >= floor(-int(y+c) / int(x)
if (c_val + y_val <= m.max_value()) { if (c_val + y_val <= m.max_value() && x_bound != 0) {
auto bound = floor((m.two_to_N() - y_val - c_val) / x_bound); auto bound = floor((m.two_to_N() - y_val - c_val) / x_bound);
m_lemma.reset(); m_lemma.reset();
for (auto c : x_le_bound) for (auto c : x_le_bound)

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

@ -1032,18 +1032,26 @@ namespace polysat {
unsigned max_level = 0; // highest level in lemma unsigned max_level = 0; // highest level in lemma
unsigned lits_at_max_level = 0; // how many literals at the 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 snd_level = 0; // second-highest level in lemma
bool is_propagation = false; // whether there is an unassigned literal (at most one) unsigned num_undef = 0; // whether there is an unassigned literal (at most one)
for (sat::literal lit : lemma) { for (sat::literal lit : lemma) {
if (m_bvars.is_true(lit)) // may happen if we only use the clause to justify a new constraint; it is not a real lemma switch (m_bvars.value(lit)) {
case l_true:
return std::nullopt; return std::nullopt;
if (!m_bvars.is_assigned(lit)) { case l_false:
DEBUG_CODE({ break;
if (lit2cnstr(lit).eval(*this) != l_undef) default:
LOG("WARNING: missed evaluation of literal: " << lit_pp(*this, lit)); switch (lit2cnstr(lit).eval(*this)) {
}); case l_true:
SASSERT(!is_propagation); return std::nullopt;
is_propagation = true; case l_false:
continue; assign_eval(~lit);
break;
case l_undef:
++num_undef;
if (num_undef > 1)
return std::nullopt;
continue;
}
} }
unsigned const lit_level = m_bvars.level(lit); unsigned const lit_level = m_bvars.level(lit);
@ -1070,7 +1078,7 @@ namespace polysat {
// backjump to max_level so we can propagate // backjump to max_level so we can propagate
unsigned jump_level; unsigned jump_level;
unsigned branching_factor = lits_at_max_level; unsigned branching_factor = lits_at_max_level;
if (is_propagation) if (num_undef == 1)
jump_level = max_level, branching_factor = 1; jump_level = max_level, branching_factor = 1;
else if (lits_at_max_level <= 1) else if (lits_at_max_level <= 1)
jump_level = snd_level; jump_level = snd_level;