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

#5532 remove unsound rewrite rule that was recently added

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-07 06:42:24 +02:00
parent 72f6271d82
commit be4df46f6f
3 changed files with 14 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/rewriter/array_rewriter.cpp
View file

@ -693,12 +693,6 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result)
if (m_util.is_const(rhs) && m_util.is_store(lhs)) { if (m_util.is_const(rhs) && m_util.is_store(lhs)) {
std::swap(lhs, rhs); std::swap(lhs, rhs);
} }
if (m_util.is_const(lhs, v) && m_util.is_store(rhs)) {
unsigned n = to_app(rhs)->get_num_args();
result = m().mk_and(m().mk_eq(lhs, to_app(rhs)->get_arg(0)),
m().mk_eq(v, to_app(rhs)->get_arg(n - 1)));
return BR_REWRITE2;
}
if (m_util.is_const(lhs, v) && m_util.is_const(rhs, w)) { if (m_util.is_const(lhs, v) && m_util.is_const(rhs, w)) {
result = m().mk_eq(v, w); result = m().mk_eq(v, w);
return BR_REWRITE1; return BR_REWRITE1;

3
src/model/model_evaluator.cpp
View file

@ -710,11 +710,10 @@ void model_evaluator::operator()(expr * t, expr_ref & result) {
TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";); TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";);
m_imp->operator()(t, result); m_imp->operator()(t, result);
m_imp->expand_stores(result); m_imp->expand_stores(result);
TRACE("model_evaluator", tout << result << "\n";); TRACE("model_evaluator", tout << "eval: " << mk_ismt2_pp(t, m()) << " --> " << result << "\n";);
} }
expr_ref model_evaluator::operator()(expr * t) { expr_ref model_evaluator::operator()(expr * t) {
TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";);
expr_ref result(m()); expr_ref result(m());
this->operator()(t, result); this->operator()(t, result);
return result; return result;

12
src/sat/smt/euf_model.cpp
View file

@ -291,6 +291,18 @@ namespace euf {
} }
void solver::validate_model(model& mdl) { void solver::validate_model(model& mdl) {
model_evaluator ev(mdl);
ev.set_model_completion(true);
TRACE("model",
for (enode* n : m_egraph.nodes()) {
unsigned id = n->get_root_id();
expr* val = m_values.get(id, nullptr);
if (!val)
continue;
expr_ref mval = ev(n->get_expr());
if (m.is_value(mval) && val != mval)
tout << "#" << bpp(n) << " := " << mk_pp(val, m) << " ~ " << mval << "\n";
});
bool first = true; bool first = true;
for (enode* n : m_egraph.nodes()) { for (enode* n : m_egraph.nodes()) {
expr* e = n->get_expr(); expr* e = n->get_expr();