mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

z3str3: check relevancy of subformulas for negated non-relevant formulas in bitvector model construction

Browse source
This commit is contained in:
Murphy Berzish 2020-02-27 18:56:58 -05:00 • committed by Nikolaj Bjorner
parent f18bd7bf08
commit 01299dacbf
1 changed files with 12 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/theory_str_mc.cpp
View file

@ -882,9 +882,19 @@ namespace smt {
for (expr * f : formulas) { for (expr * f : formulas) {
if (!get_context().is_relevant(f)) { if (!get_context().is_relevant(f)) {
expr * subformula = nullptr;
if (m.is_not(f, subformula)) {
if (!get_context().is_relevant(subformula)) {
TRACE("str_fl", tout << "skip reducing formula " << mk_pp(f, m) << ", not relevant (and neither is its subformula)" << std::endl;);
continue;
} else {
TRACE("str_fl", tout << "considering formula " << mk_pp(f, m) << ", its subformula is relevant but it is not" << std::endl;);
}
} else {
TRACE("str_fl", tout << "skip reducing formula " << mk_pp(f, m) << ", not relevant" << std::endl;); TRACE("str_fl", tout << "skip reducing formula " << mk_pp(f, m) << ", not relevant" << std::endl;);
continue; continue;
} }
}
// reduce string formulas only. ignore others // reduce string formulas only. ignore others
sort * fSort = m.get_sort(f); sort * fSort = m.get_sort(f);
if (fSort == bool_sort && !is_quantifier(f)) { if (fSort == bool_sort && !is_quantifier(f)) {