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

fixes to literal propagation exposed by bitwise and unit test

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-12-19 15:21:12 -08:00
parent 2afc58cc08
commit adb3d68743
4 changed files with 18 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -596,10 +596,8 @@ namespace polysat {
case l_false:
break;
case l_undef:
if (lit2cnstr(lit).is_currently_false(*this)) {
unsigned level = m_level; // TODO
assign_eval(level, lit);
}
if (lit2cnstr(lit).is_currently_false(*this))
assign_eval(lit);
else {
num_choices++;
choice = lit;
@ -732,7 +730,10 @@ namespace polysat {
m_search.push_boolean(lit);
}
void solver::assign_eval(unsigned level, sat::literal lit) {
void solver::assign_eval(sat::literal lit) {
unsigned level = 0;
for (auto v : lit2cnstr(lit)->vars())
level = std::max(get_level(v), level);
m_bvars.eval(lit, level);
m_trail.push_back(trail_instr_t::assign_bool_i);
m_search.push_boolean(lit);