mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

Fix subsumption for unilinear case

Browse source
This commit is contained in:
Jakob Rath 2022-09-27 17:53:45 +02:00
parent 1df749ad33
commit 74d8497ed9
1 changed files with 9 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -67,12 +67,18 @@ namespace polysat {
* \param[out] v Body * \param[out] v Body
*/ */
pdd simplify_clause::abstract(pdd const& p, pdd& v) { pdd simplify_clause::abstract(pdd const& p, pdd& v) {
if (p.is_val()) if (p.is_val()) {
SASSERT(v.is_zero());
return p; return p;
}
if (p.is_unilinear()) { if (p.is_unilinear()) {
// we need an interval with coeff == 1 to be able to compare intervals easily
auto const& coeff = p.hi().val();
if (coeff.is_one() || coeff == p.manager().max_value()) {
v = p.manager().mk_var(p.var()); v = p.manager().mk_var(p.var());
return p; return p;
} }
}
unsigned max_var = p.var(); unsigned max_var = p.var();
auto& m = p.manager(); auto& m = p.manager();
pdd r(m); pdd r(m);