mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

#5422

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-21 07:14:54 -07:00
parent 8a4b292f3e
commit e5e7c510d5
2 changed files with 95 additions and 94 deletions
Download patch file Download diff file Expand all files Collapse all files

64
src/qe/mbp/mbp_plugin.cpp
View file

@ -95,52 +95,40 @@ namespace mbp {
lits.push_back(e); lits.push_back(e);
} }
void project_plugin::extract_literals(model& model, app_ref_vector const& vars, expr_ref_vector& fmls) { bool project_plugin::reduce(model_evaluator& eval, model& model, expr* fml, expr_ref_vector& fmls) {
m_cache.reset(); expr* nfml, * f1, * f2, * f3;
m_bool_visited.reset();
expr_ref val(m); expr_ref val(m);
model_evaluator eval(model);
eval.set_expand_array_equalities(true);
TRACE("qe", tout << fmls << "\n";);
DEBUG_CODE(for (expr* fml : fmls) { CTRACE("qe", m.is_false(eval(fml)), tout << mk_pp(fml, m) << " is false\n" << model;); SASSERT(!m.is_false(eval(fml))); });
for (unsigned i = 0; i < fmls.size(); ++i) {
expr* fml = fmls.get(i), * nfml, * f1, * f2, * f3;
SASSERT(m.is_bool(fml));
if (m.is_not(fml, nfml) && m.is_distinct(nfml)) if (m.is_not(fml, nfml) && m.is_distinct(nfml))
fmls[i--] = pick_equality(m, model, nfml); push_back(fmls, pick_equality(m, model, nfml));
else if (m.is_or(fml)) { else if (m.is_or(fml)) {
for (expr* arg : *to_app(fml)) { for (expr* arg : *to_app(fml)) {
val = eval(arg); val = eval(arg);
if (m.is_true(val)) { if (m.is_true(val)) {
fmls[i] = arg; fmls.push_back(arg);
--i;
break; break;
} }
} }
} }
else if (m.is_and(fml)) { else if (m.is_and(fml)) {
fmls.append(to_app(fml)->get_num_args(), to_app(fml)->get_args()); fmls.append(to_app(fml)->get_num_args(), to_app(fml)->get_args());
erase(fmls, i);
} }
else if (m.is_iff(fml, f1, f2) || (m.is_not(fml, nfml) && m.is_xor(nfml, f1, f2))) { else if (m.is_iff(fml, f1, f2) || (m.is_not(fml, nfml) && m.is_xor(nfml, f1, f2))) {
val = eval(f1); val = eval(f1);
if (m.is_false(val)) { if (m.is_false(val)) {
f1 = mk_not(m, f1); push_back(fmls, mk_not(m, f1));
f2 = mk_not(m, f2); push_back(fmls, mk_not(m, f2));
} }
fmls[i--] = f1; else {
push_back(fmls, f1);
push_back(fmls, f2); push_back(fmls, f2);
} }
}
else if (m.is_implies(fml, f1, f2)) { else if (m.is_implies(fml, f1, f2)) {
val = eval(f2); val = eval(f2);
if (m.is_true(val)) { if (m.is_true(val))
fmls[i] = f2; push_back(fmls, f2);
} else
else { push_back(fmls, mk_not(m, f1));
fmls[i] = mk_not(m, f1);
}
--i;
} }
else if (m.is_ite(fml, f1, f2, f3)) { else if (m.is_ite(fml, f1, f2, f3)) {
val = eval(f1); val = eval(f1);
@ -152,17 +140,15 @@ namespace mbp {
push_back(fmls, mk_not(m, f1)); push_back(fmls, mk_not(m, f1));
push_back(fmls, f3); push_back(fmls, f3);
} }
erase(fmls, i);
} }
else if (m.is_not(fml, nfml) && m.is_not(nfml, nfml)) { else if (m.is_not(fml, nfml) && m.is_not(nfml, nfml)) {
push_back(fmls, nfml); push_back(fmls, nfml);
erase(fmls, i);
} }
else if (m.is_not(fml, nfml) && m.is_and(nfml)) { else if (m.is_not(fml, nfml) && m.is_and(nfml)) {
for (expr* arg : *to_app(nfml)) { for (expr* arg : *to_app(nfml)) {
val = eval(arg); val = eval(arg);
if (m.is_false(val)) { if (m.is_false(val)) {
fmls[i--] = mk_not(m, arg); push_back(fmls, mk_not(m, arg));
break; break;
} }
} }
@ -170,7 +156,6 @@ namespace mbp {
else if (m.is_not(fml, nfml) && m.is_or(nfml)) { else if (m.is_not(fml, nfml) && m.is_or(nfml)) {
for (expr* arg : *to_app(nfml)) for (expr* arg : *to_app(nfml))
push_back(fmls, mk_not(m, arg)); push_back(fmls, mk_not(m, arg));
erase(fmls, i);
} }
else if ((m.is_not(fml, nfml) && m.is_iff(nfml, f1, f2)) || m.is_xor(fml, f1, f2)) { else if ((m.is_not(fml, nfml) && m.is_iff(nfml, f1, f2)) || m.is_xor(fml, f1, f2)) {
val = eval(f1); val = eval(f1);
@ -180,12 +165,10 @@ namespace mbp {
f1 = mk_not(m, f1); f1 = mk_not(m, f1);
push_back(fmls, f1); push_back(fmls, f1);
push_back(fmls, f2); push_back(fmls, f2);
erase(fmls, i);
} }
else if (m.is_not(fml, nfml) && m.is_implies(nfml, f1, f2)) { else if (m.is_not(fml, nfml) && m.is_implies(nfml, f1, f2)) {
push_back(fmls, f1); push_back(fmls, f1);
push_back(fmls, mk_not(m, f2)); push_back(fmls, mk_not(m, f2));
erase(fmls, i);
} }
else if (m.is_not(fml, nfml) && m.is_ite(nfml, f1, f2, f3)) { else if (m.is_not(fml, nfml) && m.is_ite(nfml, f1, f2, f3)) {
val = eval(f1); val = eval(f1);
@ -197,8 +180,25 @@ namespace mbp {
push_back(fmls, mk_not(m, f1)); push_back(fmls, mk_not(m, f1));
push_back(fmls, mk_not(m, f3)); push_back(fmls, mk_not(m, f3));
} }
erase(fmls, i);
} }
else
return false;
return true;
}
void project_plugin::extract_literals(model& model, app_ref_vector const& vars, expr_ref_vector& fmls) {
m_cache.reset();
m_bool_visited.reset();
expr_ref val(m);
model_evaluator eval(model);
eval.set_expand_array_equalities(true);
TRACE("qe", tout << fmls << "\n";);
DEBUG_CODE(for (expr* fml : fmls) { CTRACE("qe", m.is_false(eval(fml)), tout << mk_pp(fml, m) << " is false\n" << model;); SASSERT(!m.is_false(eval(fml))); });
for (unsigned i = 0; i < fmls.size(); ++i) {
expr* nfml, * fml = fmls.get(i);
if (reduce(eval, model, fml, fmls))
erase(fmls, i);
else if (m.is_not(fml, nfml)) else if (m.is_not(fml, nfml))
extract_bools(eval, fmls, i, nfml, false); extract_bools(eval, fmls, i, nfml, false);
else else

1
src/qe/mbp/mbp_plugin.h
View file

@ -43,6 +43,7 @@ namespace mbp {
expr_mark m_non_ground; expr_mark m_non_ground;
expr_ref_vector m_cache, m_args, m_pure_eqs; expr_ref_vector m_cache, m_args, m_pure_eqs;
bool reduce(model_evaluator& eval, model& model, expr* fml, expr_ref_vector& fmls);
void extract_bools(model_evaluator& eval, expr_ref_vector& fmls, unsigned i, expr* fml, bool is_true); void extract_bools(model_evaluator& eval, expr_ref_vector& fmls, unsigned i, expr* fml, bool is_true);
void visit_app(expr* e); void visit_app(expr* e);
bool visit_ite(model_evaluator& eval, expr* e, expr_ref_vector& fmls); bool visit_ite(model_evaluator& eval, expr* e, expr_ref_vector& fmls);