From fcda4cee9fde8fa129637d87a261d683ff3ca3a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 9 Mar 2017 05:29:56 +0100 Subject: [PATCH] ensure evaluation of array equalities is enabled for external facing evaluator. Issue #917 Signed-off-by: Nikolaj Bjorner --- src/model/model_evaluator.cpp | 11 ++++++++++- src/model/model_evaluator.h | 1 + src/model/model_evaluator_params.pyg | 3 ++- src/smt/proto_model/proto_model.cpp | 1 + src/smt/smt_model_checker.cpp | 7 +++++-- src/tactic/extension_model_converter.cpp | 1 + 6 files changed, 20 insertions(+), 4 deletions(-) diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index af2253801..61da4b3a0 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -50,6 +50,7 @@ struct evaluator_cfg : public default_rewriter_cfg { unsigned m_max_steps; bool m_model_completion; bool m_cache; + bool m_array_equalities; evaluator_cfg(ast_manager & m, model_core & md, params_ref const & p): m_model(md), @@ -81,6 +82,7 @@ struct evaluator_cfg : public default_rewriter_cfg { m_max_steps = p.max_steps(); m_model_completion = p.completion(); m_cache = p.cache(); + m_array_equalities = p.array_equalities(); } ast_manager & m() const { return m_model.get_manager(); } @@ -264,11 +266,14 @@ struct evaluator_cfg : public default_rewriter_cfg { br_status mk_array_eq(expr* a, expr* b, expr_ref& result) { - return BR_FAILED; if (a == b) { result = m().mk_true(); return BR_DONE; } + if (!m_array_equalities) { + return BR_FAILED; + } + // disabled until made more efficient vector stores1, stores2; bool args_are_unique1, args_are_unique2; @@ -508,6 +513,10 @@ void model_evaluator::set_model_completion(bool f) { m_imp->cfg().m_model_completion = f; } +void model_evaluator::set_expand_array_equalities(bool f) { + m_imp->cfg().m_array_equalities = f; +} + unsigned model_evaluator::get_num_steps() const { return m_imp->get_num_steps(); } diff --git a/src/model/model_evaluator.h b/src/model/model_evaluator.h index 3f4da5c96..ba55e96ba 100644 --- a/src/model/model_evaluator.h +++ b/src/model/model_evaluator.h @@ -35,6 +35,7 @@ public: ast_manager & m () const; void set_model_completion(bool f); + void set_expand_array_equalities(bool f); void updt_params(params_ref const & p); static void get_param_descrs(param_descrs & r); diff --git a/src/model/model_evaluator_params.pyg b/src/model/model_evaluator_params.pyg index b68d5c3ad..b6417f7fc 100644 --- a/src/model/model_evaluator_params.pyg +++ b/src/model/model_evaluator_params.pyg @@ -3,6 +3,7 @@ def_module_params('model_evaluator', params=(max_memory_param(), max_steps_param(), ('completion', BOOL, False, 'assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model'), - ('cache', BOOL, True, 'cache intermediate results in the model evaluator') + ('cache', BOOL, True, 'cache intermediate results in the model evaluator'), + ('array_equalities', BOOL, True, 'evaluate array equalities') )) diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index a7875e99e..129bed87e 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -93,6 +93,7 @@ bool proto_model::is_select_of_model_value(expr* e) const { bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { m_eval.set_model_completion(model_completion); + m_eval.set_expand_array_equalities(false); try { m_eval(e, result); #if 0 diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 5329cd80f..093d215b6 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -290,7 +290,7 @@ namespace smt { while (true) { lbool r = m_aux_context->check(); - TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";); + TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";); if (r != l_true) break; model_ref cex; @@ -300,7 +300,7 @@ namespace smt { } num_new_instances++; if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) { - TRACE("model_checker", tout << "Add blocking clause failed\n";); + TRACE("model_checker", tout << "Add blocking clause failed new-instances: " << num_new_instances << " max-cex: " << m_max_cexs << "\n";); // add_blocking_clause failed... stop the search for new counter-examples... break; } @@ -407,6 +407,7 @@ namespace smt { found_relevant = true; if (m.is_rec_fun_def(q)) { if (!check_rec_fun(q)) { + TRACE("model_checker", tout << "checking recursive function failed\n";); num_failures++; } } @@ -414,6 +415,7 @@ namespace smt { if (m_params.m_mbqi_trace || get_verbosity_level() >= 5) { verbose_stream() << "(smt.mbqi :failed " << q->get_qid() << ")\n"; } + TRACE("model_checker", tout << "checking quantifier " << mk_pp(q, m) << " failed\n";); num_failures++; } } @@ -452,6 +454,7 @@ namespace smt { } bool model_checker::has_new_instances() { + TRACE("model_checker", tout << "instances: " << m_new_instances.size() << "\n";); return !m_new_instances.empty(); } diff --git a/src/tactic/extension_model_converter.cpp b/src/tactic/extension_model_converter.cpp index ee6b8f691..18b5b6288 100644 --- a/src/tactic/extension_model_converter.cpp +++ b/src/tactic/extension_model_converter.cpp @@ -49,6 +49,7 @@ void extension_model_converter::operator()(model_ref & md, unsigned goal_idx) { TRACE("extension_mc", model_v2_pp(tout, *md); display_decls_info(tout, md);); model_evaluator ev(*(md.get())); ev.set_model_completion(true); + ev.set_expand_array_equalities(false); expr_ref val(m()); unsigned i = m_vars.size(); while (i > 0) {