mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

#6418 - add best-effort for nested and/or (from ite literals)

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-10-23 11:03:51 -07:00
parent 071a1447e3
commit 4a1d76cf49
1 changed files with 29 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/qe/mbp/mbp_arith.cpp
View file

@ -155,6 +155,35 @@ namespace mbp {
} }
SASSERT(found_eq); SASSERT(found_eq);
} }
else if (m.is_and(lit) && !is_not) {
fmls.append(to_app(lit)->get_num_args(), to_app(lit)->get_args());
return true;
}
else if (m.is_or(lit) && is_not) {
for (expr* arg : *to_app(lit))
fmls.push_back(mk_not(m, arg));
return true;
}
else if (m.is_or(lit) && !is_not) {
for (expr* arg : *to_app(lit)) {
if (eval.is_true(arg)) {
fmls.push_back(arg);
return true;
}
}
TRACE("qe", tout << "Skipping " << mk_pp(lit, m) << "\n";);
return false;
}
else if (m.is_and(lit) && is_not) {
for (expr* arg : *to_app(lit)) {
if (eval.is_false(arg)) {
fmls.push_back(mk_not(m, arg));
return true;
}
}
TRACE("qe", tout << "Skipping " << mk_pp(lit, m) << "\n";);
return false;
}
else { else {
TRACE("qe", tout << "Skipping " << mk_pp(lit, m) << "\n";); TRACE("qe", tout << "Skipping " << mk_pp(lit, m) << "\n";);
return false; return false;