From ea1089e98016e33807bd9314af07285a03d5d482 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 26 Feb 2021 02:06:15 -0800 Subject: [PATCH] fix #4938 --- src/ast/datatype_decl_plugin.cpp | 10 ++++++++++ src/ast/datatype_decl_plugin.h | 2 ++ src/model/model_evaluator.cpp | 8 +++++--- src/sat/smt/dt_solver.cpp | 5 ++--- src/smt/theory_datatype.cpp | 8 ++++++++ 5 files changed, 27 insertions(+), 6 deletions(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 9d1a1c437..4fe6df396 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -640,6 +640,16 @@ namespace datatype { return result; } + bool util::is_considered_uninterpreted(func_decl * f, unsigned n, expr* const* args) { + if (is_accessor(f)) { + func_decl* c = get_accessor_constructor(f); + SASSERT(n == 1); + if (is_constructor(args[0])) + return to_app(args[0])->get_decl() != c; + return false; + } + return false; + } bool util::is_fully_interp(sort * s) const { SASSERT(is_datatype(s)); diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index b06141365..8b609073d 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -345,6 +345,8 @@ namespace datatype { bool is_is(app const * f) const { return is_app_of(f, fid(), OP_DT_IS);} bool is_is(expr const * e) const { return is_app(e) && is_is(to_app(e)); } bool is_recognizer(expr const * f) const { return is_app(f) && (is_recognizer0(to_app(f)) || is_is(to_app(f))); } + bool is_considered_uninterpreted(func_decl * f, unsigned n, expr* const* args); + MATCH_UNARY(is_recognizer); bool is_accessor(expr const* e) const { return is_app(e) && is_app_of(to_app(e), fid(), OP_DT_ACCESSOR); } MATCH_UNARY(is_accessor); diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index c5c310cca..2235a005d 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -54,6 +54,7 @@ struct evaluator_cfg : public default_rewriter_cfg { array_util m_ar; arith_util m_au; fpa_util m_fpau; + datatype::util m_dt; unsigned long long m_max_memory; unsigned m_max_steps; bool m_model_completion; @@ -80,6 +81,7 @@ struct evaluator_cfg : public default_rewriter_cfg { m_ar(m), m_au(m), m_fpau(m), + m_dt(m), m_pinned(m) { bool flat = true; m_b_rw.set_flat(flat); @@ -147,9 +149,8 @@ struct evaluator_cfg : public default_rewriter_cfg { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { auto st = reduce_app_core(f, num, args, result, result_pr); CTRACE("model_evaluator", st != BR_FAILED, - tout << f->get_name() << " "; - for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m) << " "; - tout << "\n"; + tout << f->get_name() << "\n"; + for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m) << "\n"; tout << result << "\n";); return st; @@ -352,6 +353,7 @@ struct evaluator_cfg : public default_rewriter_cfg { if (f_ui) { fi = m_model.get_func_interp(f_ui); } + if (!fi) { result = m_au.mk_numeral(rational(0), f->get_range()); return BR_DONE; diff --git a/src/sat/smt/dt_solver.cpp b/src/sat/smt/dt_solver.cpp index 9bf80e5b0..b0f7f0789 100644 --- a/src/sat/smt/dt_solver.cpp +++ b/src/sat/smt/dt_solver.cpp @@ -693,7 +693,7 @@ namespace dt { enode* con = m_var_data[v]->m_constructor; func_decl* c_decl = con->get_decl(); m_args.reset(); - for (enode* arg : euf::enode_args(m_var_data[v]->m_constructor)) + for (enode* arg : euf::enode_args(con)) m_args.push_back(values.get(arg->get_root_id())); values.set(n->get_root_id(), m.mk_app(c_decl, m_args)); } @@ -765,8 +765,7 @@ namespace dt { mk_var(n); enode* arg = n->get_arg(0); theory_var v = mk_var(arg); - add_recognizer(v, n); - + add_recognizer(v, n); } else { SASSERT(is_accessor(term)); diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index e8169e21b..7fc40a4cc 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -736,6 +736,14 @@ namespace smt { } bool theory_datatype::include_func_interp(func_decl* f) { + if (!m_util.is_accessor(f)) + return false; + func_decl* con = m_util.get_accessor_constructor(f); + for (enode* app : ctx.enodes_of(f)) { + enode* arg = app->get_arg(0)->get_root(); + if (is_constructor(arg) && arg->get_decl() != con) + return true; + } return false; }