From 493a3a63125230cc567380543d6679c749334e15 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 20 Jun 2017 23:39:38 -0400 Subject: [PATCH] (mev) call expand_value only at the end There is no need to expand array values throughout evaluation. They are expanded during array equality checking (if requested), and can be expanded at the very end of evaluation (if needed). --- src/model/model_evaluator.cpp | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index f88beba4c..279cfde3b 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -125,7 +125,6 @@ struct evaluator_cfg : public default_rewriter_cfg { expr * val = m_model.get_const_interp(f); if (val != 0) { result = val; - expand_value(result); return BR_DONE; } @@ -274,7 +273,6 @@ struct evaluator_cfg : public default_rewriter_cfg { return BR_FAILED; } - // disabled until made more efficient vector stores1, stores2; bool args_are_unique1, args_are_unique2; expr_ref else1(m()), else2(m()); @@ -489,6 +487,10 @@ struct model_evaluator::imp : public rewriter_tpl { m_cfg(md.get_manager(), md, p) { set_cancel_check(false); } + + void expand_value (expr_ref &val) { + m_cfg.expand_value (val); + } }; model_evaluator::model_evaluator(model_core & md, params_ref const & p) { @@ -537,14 +539,12 @@ void model_evaluator::reset(params_ref const & p) { void model_evaluator::operator()(expr * t, expr_ref & result) { TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";); m_imp->operator()(t, result); + m_imp->expand_value(result); } expr_ref model_evaluator::operator()(expr * t) { TRACE("model_evaluator", tout << mk_ismt2_pp(t, m()) << "\n";); expr_ref result(m()); - m_imp->operator()(t, result); + this->operator()(t, result); return result; } - - -