From 8e09a78c269d9c0a25f784dc0cc898ab24b1182d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 2 Mar 2018 23:02:20 +0900 Subject: [PATCH] fix #1510 by reintroducing automatic declaration of recognizers Signed-off-by: Nikolaj Bjorner --- src/api/api_datatype.cpp | 10 +++++----- src/ast/datatype_decl_plugin.cpp | 27 +++++++++++---------------- src/ast/datatype_decl_plugin.h | 1 + src/cmd_context/cmd_context.cpp | 5 ++--- src/muz/pdr/pdr_prop_solver.cpp | 2 +- src/muz/spacer/spacer_util.cpp | 2 +- src/parsers/smt2/smt2parser.cpp | 2 +- src/qe/qe_datatype_plugin.cpp | 10 +++++----- src/qe/qe_datatypes.cpp | 4 ++-- src/qe/qe_lite.cpp | 2 +- src/smt/theory_datatype.cpp | 10 +++++----- 11 files changed, 35 insertions(+), 40 deletions(-) diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index df0b2317f..799e537ea 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -137,7 +137,7 @@ extern "C" { func_decl* decl = (decls)[i]; mk_c(c)->save_multiple_ast_trail(decl); enum_consts[i] = of_func_decl(decl); - decl = dt_util.get_constructor_recognizer(decl); + decl = dt_util.get_constructor_is(decl); mk_c(c)->save_multiple_ast_trail(decl); enum_testers[i] = of_func_decl(decl); } @@ -196,7 +196,7 @@ extern "C" { *nil_decl = of_func_decl(f); } if (is_nil_decl) { - f = data_util.get_constructor_recognizer(cnstrs[0]); + f = data_util.get_constructor_is(cnstrs[0]); mk_c(c)->save_multiple_ast_trail(f); *is_nil_decl = of_func_decl(f); } @@ -206,7 +206,7 @@ extern "C" { *cons_decl = of_func_decl(f); } if (is_cons_decl) { - f = data_util.get_constructor_recognizer(cnstrs[1]); + f = data_util.get_constructor_is(cnstrs[1]); mk_c(c)->save_multiple_ast_trail(f); *is_cons_decl = of_func_decl(f); } @@ -290,7 +290,7 @@ extern "C" { *constructor_decl = of_func_decl(f); } if (tester) { - func_decl* f2 = data_util.get_constructor_recognizer(f); + func_decl* f2 = data_util.get_constructor_is(f); mk_c(c)->save_multiple_ast_trail(f2); *tester = of_func_decl(f2); } @@ -497,7 +497,7 @@ extern "C" { RETURN_Z3(nullptr); } func_decl* decl = (decls)[idx]; - decl = dt_util.get_constructor_recognizer(decl); + decl = dt_util.get_constructor_is(decl); mk_c(c)->save_ast_trail(decl); RETURN_Z3(of_func_decl(decl)); Z3_CATCH_RETURN(nullptr); diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 722cb22b5..44f824959 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -791,13 +791,20 @@ namespace datatype { return res; } + + func_decl * util::get_constructor_is(func_decl * con) { + SASSERT(is_constructor(con)); + sort * datatype = con->get_range(); + parameter ps[1] = { parameter(con)}; + return m.mk_func_decl(m_family_id, OP_DT_IS, 1, ps, 1, &datatype); + } + func_decl * util::get_constructor_recognizer(func_decl * con) { SASSERT(is_constructor(con)); func_decl * d = nullptr; if (m_constructor2recognizer.find(con, d)) return d; sort * datatype = con->get_range(); -#if 0 def const& dd = get_def(datatype); symbol r; for (constructor const* c : dd) { @@ -812,14 +819,6 @@ namespace datatype { m_asts.push_back(d); m_constructor2recognizer.insert(con, d); return d; -#else - parameter ps[1] = { parameter(con)}; - d = m.mk_func_decl(m_family_id, OP_DT_IS, 1, ps, 1, &datatype); - m_constructor2recognizer.insert(con, d); - m_asts.push_back(d); - m_asts.push_back(con); - return d; -#endif } func_decl * util::get_recognizer_constructor(func_decl * recognizer) const { @@ -1049,15 +1048,11 @@ namespace datatype { sort* s = todo.back(); todo.pop_back(); out << s->get_name() << " =\n"; - ptr_vector const& cnstrs = *get_datatype_constructors(s); - for (unsigned i = 0; i < cnstrs.size(); ++i) { - func_decl* cns = cnstrs[i]; - func_decl* rec = get_constructor_recognizer(cns); - out << " " << cns->get_name() << " :: " << rec->get_name() << " :: "; + for (func_decl * cns : cnstrs) { + out << " " << cns->get_name() << " :: "; ptr_vector const & accs = *get_constructor_accessors(cns); - for (unsigned j = 0; j < accs.size(); ++j) { - func_decl* acc = accs[j]; + for (func_decl* acc : accs) { sort* s1 = acc->get_range(); out << "(" << acc->get_name() << ": " << s1->get_name() << ") "; if (is_datatype(s1) && are_siblings(s1, s0) && !mark.is_marked(s1)) { diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index 81c2d09a5..e644ccbda 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -368,6 +368,7 @@ namespace datatype { sort* get_datatype_parameter_sort(sort * ty, unsigned idx); func_decl * get_non_rec_constructor(sort * ty); func_decl * get_constructor_recognizer(func_decl * constructor); + func_decl * get_constructor_is(func_decl * constructor); ptr_vector const * get_constructor_accessors(func_decl * constructor); func_decl * get_accessor_constructor(func_decl * accessor); func_decl * get_recognizer_constructor(func_decl * recognizer) const; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 0be458b4a..aabe43110 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -2015,9 +2015,8 @@ void cmd_context::dt_eh::operator()(sort * dt, pdecl* pd) { for (func_decl * c : *m_dt_util.get_datatype_constructors(dt)) { TRACE("new_dt_eh", tout << "new constructor: " << c->get_name() << "\n";); m_owner.insert(c); - // Don't insert recognizer any longer. It is a built-in function. - // func_decl * r = m_dt_util.get_constructor_recognizer(c); - // m_owner.insert(r); + func_decl * r = m_dt_util.get_constructor_recognizer(c); + m_owner.insert(r); // TRACE("new_dt_eh", tout << "new recognizer: " << r->get_name() << "\n";); for (func_decl * a : *m_dt_util.get_constructor_accessors(c)) { TRACE("new_dt_eh", tout << "new accessor: " << a->get_name() << "\n";); diff --git a/src/muz/pdr/pdr_prop_solver.cpp b/src/muz/pdr/pdr_prop_solver.cpp index 801d06e50..8ebc9b9cb 100644 --- a/src/muz/pdr/pdr_prop_solver.cpp +++ b/src/muz/pdr/pdr_prop_solver.cpp @@ -133,7 +133,7 @@ namespace pdr { else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) || (m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))){ func_decl* f = to_app(val)->get_decl(); - func_decl* r = dt.get_constructor_recognizer(f); + func_decl* r = dt.get_constructor_is(f); conjs[i] = m.mk_app(r, c); ptr_vector const& acc = *dt.get_constructor_accessors(f); for (unsigned j = 0; j < acc.size(); ++j) { diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index cdec5d7eb..625ac4b7b 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -694,7 +694,7 @@ void expand_literals(ast_manager &m, expr_ref_vector& conjs) } else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) || (m.is_eq(e, val, c) && is_app(val) && dt.is_constructor(to_app(val)))){ func_decl* f = to_app(val)->get_decl(); - func_decl* r = dt.get_constructor_recognizer(f); + func_decl* r = dt.get_constructor_is(f); conjs[i] = m.mk_app(r, c); ptr_vector const& acc = *dt.get_constructor_accessors(f); for (unsigned j = 0; j < acc.size(); ++j) { diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 347cbbd68..9265312d4 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -1414,7 +1414,7 @@ namespace smt2 { else { SASSERT(is_app(pattern)); func_decl * f = to_app(pattern)->get_decl(); - func_decl * r = dtutil().get_constructor_recognizer(f); + func_decl * r = dtutil().get_constructor_is(f); ptr_vector const * acc = dtutil().get_constructor_accessors(f); shifter()(t, acc->size(), tsh); for (func_decl* a : *acc) { diff --git a/src/qe/qe_datatype_plugin.cpp b/src/qe/qe_datatype_plugin.cpp index 58878d067..81a402ba4 100644 --- a/src/qe/qe_datatype_plugin.cpp +++ b/src/qe/qe_datatype_plugin.cpp @@ -261,7 +261,7 @@ namespace qe { return false; } func_decl* c = a->get_decl(); - func_decl* r = m_util.get_constructor_recognizer(c); + func_decl_ref r(m_util.get_constructor_is(c), m); ptr_vector const & acc = *m_util.get_constructor_accessors(c); SASSERT(acc.size() == a->get_num_args()); // @@ -380,7 +380,7 @@ namespace qe { } func_decl* c = l->get_decl(); ptr_vector const& acc = *m_util.get_constructor_accessors(c); - func_decl* rec = m_util.get_constructor_recognizer(c); + func_decl* rec = m_util.get_constructor_is(c); expr_ref_vector conj(m); conj.push_back(m.mk_app(rec, r)); for (unsigned i = 0; i < acc.size(); ++i) { @@ -627,7 +627,7 @@ namespace qe { // if (!has_recognizer(x, fml, r, c)) { c = m_datatype_util.get_datatype_constructors(s)->get(vl.get_unsigned()); - r = m_datatype_util.get_constructor_recognizer(c); + r = m_datatype_util.get_constructor_is(c); app* is_c = m.mk_app(r, x); // assert v => r(x) m_ctx.add_constraint(true, is_c); @@ -674,7 +674,7 @@ namespace qe { // if (!has_recognizer(x, fml, r, c)) { c = m_datatype_util.get_datatype_constructors(s)->get(vl.get_unsigned()); - r = m_datatype_util.get_constructor_recognizer(c); + r = m_datatype_util.get_constructor_is(c); app* is_c = m.mk_app(r, x); fml = m.mk_and(is_c, fml); app_ref fresh_x(m.mk_fresh_const("x", s), m); @@ -775,7 +775,7 @@ namespace qe { } c = m_datatype_util.get_datatype_constructors(s)->get(vl.get_unsigned()); - r = m_datatype_util.get_constructor_recognizer(c); + r = m_datatype_util.get_constructor_is(c); app* is_c = m.mk_app(r, x); // assert v => r(x) diff --git a/src/qe/qe_datatypes.cpp b/src/qe/qe_datatypes.cpp index db1e6ec85..770beb59d 100644 --- a/src/qe/qe_datatypes.cpp +++ b/src/qe/qe_datatypes.cpp @@ -151,7 +151,7 @@ namespace qe { return false; } func_decl* c = a->get_decl(); - func_decl* rec = dt.get_constructor_recognizer(c); + func_decl_ref rec(dt.get_constructor_is(c), m); ptr_vector const & acc = *dt.get_constructor_accessors(c); SASSERT(acc.size() == a->get_num_args()); // @@ -232,7 +232,7 @@ namespace qe { func_decl* c = to_app(l)->get_decl(); ptr_vector const& acc = *dt.get_constructor_accessors(c); if (!is_app_of(r, c)) { - lits.push_back(m.mk_app(dt.get_constructor_recognizer(c), r)); + lits.push_back(m.mk_app(dt.get_constructor_is(c), r)); } for (unsigned i = 0; i < acc.size(); ++i) { lits.push_back(m.mk_eq(to_app(l)->get_arg(i), access(c, i, acc, r))); diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index 8cbf6c70f..e96626479 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -692,7 +692,7 @@ namespace eq { } } else { - func_decl* rec = dt.get_constructor_recognizer(d); + func_decl* rec = dt.get_constructor_is(d); conjs.push_back(m.mk_app(rec, r)); ptr_vector const& acc = *dt.get_constructor_accessors(d); for (unsigned i = 0; i < acc.size(); ++i) { diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 695d479f4..3d3d56055 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -167,7 +167,7 @@ namespace smt { func_decl * upd = n->get_decl(); func_decl * acc = to_func_decl(upd->get_parameter(0).get_ast()); func_decl * con = m_util.get_accessor_constructor(acc); - func_decl * rec = m_util.get_constructor_recognizer(con); + func_decl * rec = m_util.get_constructor_is(con); ptr_vector const & accessors = *m_util.get_constructor_accessors(con); app_ref rec_app(m.mk_app(rec, arg1), m); ctx.internalize(rec_app, false); @@ -710,7 +710,7 @@ namespace smt { literal consequent; if (!r) { ptr_vector const & constructors = *m_util.get_datatype_constructors(dt); - func_decl * rec = m_util.get_constructor_recognizer(constructors[unassigned_idx]); + func_decl * rec = m_util.get_constructor_is(constructors[unassigned_idx]); app * rec_app = get_manager().mk_app(rec, n->get_owner()); ctx.internalize(rec_app, false); consequent = literal(ctx.get_bool_var(rec_app)); @@ -751,12 +751,12 @@ namespace smt { m_stats.m_splits++; if (d->m_recognizers.empty()) { - r = m_util.get_constructor_recognizer(non_rec_c); + r = m_util.get_constructor_is(non_rec_c); } else { enode * recognizer = d->m_recognizers[non_rec_idx]; if (recognizer == nullptr) { - r = m_util.get_constructor_recognizer(non_rec_c); + r = m_util.get_constructor_is(non_rec_c); } else if (!ctx.is_relevant(recognizer)) { ctx.mark_as_relevant(recognizer); @@ -776,7 +776,7 @@ namespace smt { if (curr == nullptr) { ptr_vector const & constructors = *m_util.get_datatype_constructors(s); // found empty slot... - r = m_util.get_constructor_recognizer(constructors[idx]); + r = m_util.get_constructor_is(constructors[idx]); break; } else if (!ctx.is_relevant(curr)) {