mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 01:16:15 +00:00
Code Activity

remove 'change' just return

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-09-21 08:53:00 -07:00
parent 1020f38e1a
commit 0888f92efd
2 changed files with 6 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -157,6 +157,8 @@ namespace polysat {
UNREACHABLE(); // we don't follow the regular loop when backjumping UNREACHABLE(); // we don't follow the regular loop when backjumping
return false; return false;
} }
UNREACHABLE();
return false;
} }
bool conflict::is_relevant(sat::literal lit) const { bool conflict::is_relevant(sat::literal lit) const {

8
src/math/polysat/simplify_clause.cpp
View file

@ -22,10 +22,9 @@ namespace polysat {
{} {}
bool simplify_clause::apply(clause& cl) { bool simplify_clause::apply(clause& cl) {
bool changed = false; if (try_constant_subsumptions(cl))
if (try_unilinear_subsumption(cl)) return true;
changed = true; return false;
return changed;
} }
pdd simplify_clause::abstract(pdd const& p, pdd& v) { pdd simplify_clause::abstract(pdd const& p, pdd& v) {
@ -80,6 +79,7 @@ namespace polysat {
entry.valid = true; entry.valid = true;
} }
/** /**
* Test simple subsumption between univariate and linear literals, i.e., * Test simple subsumption between univariate and linear literals, i.e.,
* the case where both literals can be represented by a single contiguous forbidden interval. * the case where both literals can be represented by a single contiguous forbidden interval.