mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 04:13:38 +00:00
Code Activity

fix #1510 by reintroducing automatic declaration of recognizers

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-02 23:02:20 +09:00
parent a738f5af12
commit 8e09a78c26
11 changed files with 35 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/api/api_datatype.cpp
View file

@ -137,7 +137,7 @@ extern "C" {
func_decl* decl = (decls)[i]; func_decl* decl = (decls)[i];
mk_c(c)->save_multiple_ast_trail(decl); mk_c(c)->save_multiple_ast_trail(decl);
enum_consts[i] = of_func_decl(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); mk_c(c)->save_multiple_ast_trail(decl);
enum_testers[i] = of_func_decl(decl); enum_testers[i] = of_func_decl(decl);
} }
@ -196,7 +196,7 @@ extern "C" {
*nil_decl = of_func_decl(f); *nil_decl = of_func_decl(f);
} }
if (is_nil_decl) { 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); mk_c(c)->save_multiple_ast_trail(f);
*is_nil_decl = of_func_decl(f); *is_nil_decl = of_func_decl(f);
} }
@ -206,7 +206,7 @@ extern "C" {
*cons_decl = of_func_decl(f); *cons_decl = of_func_decl(f);
} }
if (is_cons_decl) { 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); mk_c(c)->save_multiple_ast_trail(f);
*is_cons_decl = of_func_decl(f); *is_cons_decl = of_func_decl(f);
} }
@ -290,7 +290,7 @@ extern "C" {
*constructor_decl = of_func_decl(f); *constructor_decl = of_func_decl(f);
} }
if (tester) { 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); mk_c(c)->save_multiple_ast_trail(f2);
*tester = of_func_decl(f2); *tester = of_func_decl(f2);
} }
@ -497,7 +497,7 @@ extern "C" {
RETURN_Z3(nullptr); RETURN_Z3(nullptr);
} }
func_decl* decl = (decls)[idx]; 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); mk_c(c)->save_ast_trail(decl);
RETURN_Z3(of_func_decl(decl)); RETURN_Z3(of_func_decl(decl));
Z3_CATCH_RETURN(nullptr); Z3_CATCH_RETURN(nullptr);

27
src/ast/datatype_decl_plugin.cpp
View file

@ -791,13 +791,20 @@ namespace datatype {
return res; 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) { func_decl * util::get_constructor_recognizer(func_decl * con) {
SASSERT(is_constructor(con)); SASSERT(is_constructor(con));
func_decl * d = nullptr; func_decl * d = nullptr;
if (m_constructor2recognizer.find(con, d)) if (m_constructor2recognizer.find(con, d))
return d; return d;
sort * datatype = con->get_range(); sort * datatype = con->get_range();
#if 0
def const& dd = get_def(datatype); def const& dd = get_def(datatype);
symbol r; symbol r;
for (constructor const* c : dd) { for (constructor const* c : dd) {
@ -812,14 +819,6 @@ namespace datatype {
m_asts.push_back(d); m_asts.push_back(d);
m_constructor2recognizer.insert(con, d); m_constructor2recognizer.insert(con, d);
return 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 { func_decl * util::get_recognizer_constructor(func_decl * recognizer) const {
@ -1049,15 +1048,11 @@ namespace datatype {
sort* s = todo.back(); sort* s = todo.back();
todo.pop_back(); todo.pop_back();
out << s->get_name() << " =\n"; out << s->get_name() << " =\n";
ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s); ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s);
for (unsigned i = 0; i < cnstrs.size(); ++i) { for (func_decl * cns : cnstrs) {
func_decl* cns = cnstrs[i]; out << " " << cns->get_name() << " :: ";
func_decl* rec = get_constructor_recognizer(cns);
out << " " << cns->get_name() << " :: " << rec->get_name() << " :: ";
ptr_vector<func_decl> const & accs = *get_constructor_accessors(cns); ptr_vector<func_decl> const & accs = *get_constructor_accessors(cns);
for (unsigned j = 0; j < accs.size(); ++j) { for (func_decl* acc : accs) {
func_decl* acc = accs[j];
sort* s1 = acc->get_range(); sort* s1 = acc->get_range();
out << "(" << acc->get_name() << ": " << s1->get_name() << ") "; out << "(" << acc->get_name() << ": " << s1->get_name() << ") ";
if (is_datatype(s1) && are_siblings(s1, s0) && !mark.is_marked(s1)) { if (is_datatype(s1) && are_siblings(s1, s0) && !mark.is_marked(s1)) {

1
src/ast/datatype_decl_plugin.h
View file

@ -368,6 +368,7 @@ namespace datatype {
sort* get_datatype_parameter_sort(sort * ty, unsigned idx); sort* get_datatype_parameter_sort(sort * ty, unsigned idx);
func_decl * get_non_rec_constructor(sort * ty); func_decl * get_non_rec_constructor(sort * ty);
func_decl * get_constructor_recognizer(func_decl * constructor); func_decl * get_constructor_recognizer(func_decl * constructor);
func_decl * get_constructor_is(func_decl * constructor);
ptr_vector<func_decl> const * get_constructor_accessors(func_decl * constructor); ptr_vector<func_decl> const * get_constructor_accessors(func_decl * constructor);
func_decl * get_accessor_constructor(func_decl * accessor); func_decl * get_accessor_constructor(func_decl * accessor);
func_decl * get_recognizer_constructor(func_decl * recognizer) const; func_decl * get_recognizer_constructor(func_decl * recognizer) const;

5
src/cmd_context/cmd_context.cpp
View file

@ -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)) { for (func_decl * c : *m_dt_util.get_datatype_constructors(dt)) {
TRACE("new_dt_eh", tout << "new constructor: " << c->get_name() << "\n";); TRACE("new_dt_eh", tout << "new constructor: " << c->get_name() << "\n";);
m_owner.insert(c); 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);
// func_decl * r = m_dt_util.get_constructor_recognizer(c); m_owner.insert(r);
// m_owner.insert(r);
// TRACE("new_dt_eh", tout << "new recognizer: " << r->get_name() << "\n";); // TRACE("new_dt_eh", tout << "new recognizer: " << r->get_name() << "\n";);
for (func_decl * a : *m_dt_util.get_constructor_accessors(c)) { for (func_decl * a : *m_dt_util.get_constructor_accessors(c)) {
TRACE("new_dt_eh", tout << "new accessor: " << a->get_name() << "\n";); TRACE("new_dt_eh", tout << "new accessor: " << a->get_name() << "\n";);

2
src/muz/pdr/pdr_prop_solver.cpp
View file

@ -133,7 +133,7 @@ namespace pdr {
else if ((m.is_eq(e, c, val) && is_app(val) && dt.is_constructor(to_app(val))) || 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)))){ (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* 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); conjs[i] = m.mk_app(r, c);
ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(f); ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(f);
for (unsigned j = 0; j < acc.size(); ++j) { for (unsigned j = 0; j < acc.size(); ++j) {

2
src/muz/spacer/spacer_util.cpp
View file

@ -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))) || } 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)))){ (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* 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); conjs[i] = m.mk_app(r, c);
ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(f); ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(f);
for (unsigned j = 0; j < acc.size(); ++j) { for (unsigned j = 0; j < acc.size(); ++j) {

2
src/parsers/smt2/smt2parser.cpp
View file

@ -1414,7 +1414,7 @@ namespace smt2 {
else { else {
SASSERT(is_app(pattern)); SASSERT(is_app(pattern));
func_decl * f = to_app(pattern)->get_decl(); 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<func_decl> const * acc = dtutil().get_constructor_accessors(f); ptr_vector<func_decl> const * acc = dtutil().get_constructor_accessors(f);
shifter()(t, acc->size(), tsh); shifter()(t, acc->size(), tsh);
for (func_decl* a : *acc) { for (func_decl* a : *acc) {

10
src/qe/qe_datatype_plugin.cpp
View file

@ -261,7 +261,7 @@ namespace qe {
return false; return false;
} }
func_decl* c = a->get_decl(); 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<func_decl> const & acc = *m_util.get_constructor_accessors(c); ptr_vector<func_decl> const & acc = *m_util.get_constructor_accessors(c);
SASSERT(acc.size() == a->get_num_args()); SASSERT(acc.size() == a->get_num_args());
// //
@ -380,7 +380,7 @@ namespace qe {
} }
func_decl* c = l->get_decl(); func_decl* c = l->get_decl();
ptr_vector<func_decl> const& acc = *m_util.get_constructor_accessors(c); ptr_vector<func_decl> 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); expr_ref_vector conj(m);
conj.push_back(m.mk_app(rec, r)); conj.push_back(m.mk_app(rec, r));
for (unsigned i = 0; i < acc.size(); ++i) { for (unsigned i = 0; i < acc.size(); ++i) {
@ -627,7 +627,7 @@ namespace qe {
// //
if (!has_recognizer(x, fml, r, c)) { if (!has_recognizer(x, fml, r, c)) {
c = m_datatype_util.get_datatype_constructors(s)->get(vl.get_unsigned()); 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); app* is_c = m.mk_app(r, x);
// assert v => r(x) // assert v => r(x)
m_ctx.add_constraint(true, is_c); m_ctx.add_constraint(true, is_c);
@ -674,7 +674,7 @@ namespace qe {
// //
if (!has_recognizer(x, fml, r, c)) { if (!has_recognizer(x, fml, r, c)) {
c = m_datatype_util.get_datatype_constructors(s)->get(vl.get_unsigned()); 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); app* is_c = m.mk_app(r, x);
fml = m.mk_and(is_c, fml); fml = m.mk_and(is_c, fml);
app_ref fresh_x(m.mk_fresh_const("x", s), m); 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()); 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); app* is_c = m.mk_app(r, x);
// assert v => r(x) // assert v => r(x)

4
src/qe/qe_datatypes.cpp
View file

@ -151,7 +151,7 @@ namespace qe {
return false; return false;
} }
func_decl* c = a->get_decl(); 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<func_decl> const & acc = *dt.get_constructor_accessors(c); ptr_vector<func_decl> const & acc = *dt.get_constructor_accessors(c);
SASSERT(acc.size() == a->get_num_args()); SASSERT(acc.size() == a->get_num_args());
// //
@ -232,7 +232,7 @@ namespace qe {
func_decl* c = to_app(l)->get_decl(); func_decl* c = to_app(l)->get_decl();
ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(c); ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(c);
if (!is_app_of(r, 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) { 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))); lits.push_back(m.mk_eq(to_app(l)->get_arg(i), access(c, i, acc, r)));

2
src/qe/qe_lite.cpp
View file

@ -692,7 +692,7 @@ namespace eq {
} }
} }
else { 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)); conjs.push_back(m.mk_app(rec, r));
ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(d); ptr_vector<func_decl> const& acc = *dt.get_constructor_accessors(d);
for (unsigned i = 0; i < acc.size(); ++i) { for (unsigned i = 0; i < acc.size(); ++i) {

10
src/smt/theory_datatype.cpp
View file

@ -167,7 +167,7 @@ namespace smt {
func_decl * upd = n->get_decl(); func_decl * upd = n->get_decl();
func_decl * acc = to_func_decl(upd->get_parameter(0).get_ast()); func_decl * acc = to_func_decl(upd->get_parameter(0).get_ast());
func_decl * con = m_util.get_accessor_constructor(acc); 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<func_decl> const & accessors = *m_util.get_constructor_accessors(con); ptr_vector<func_decl> const & accessors = *m_util.get_constructor_accessors(con);
app_ref rec_app(m.mk_app(rec, arg1), m); app_ref rec_app(m.mk_app(rec, arg1), m);
ctx.internalize(rec_app, false); ctx.internalize(rec_app, false);
@ -710,7 +710,7 @@ namespace smt {
literal consequent; literal consequent;
if (!r) { if (!r) {
ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(dt); ptr_vector<func_decl> 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()); app * rec_app = get_manager().mk_app(rec, n->get_owner());
ctx.internalize(rec_app, false); ctx.internalize(rec_app, false);
consequent = literal(ctx.get_bool_var(rec_app)); consequent = literal(ctx.get_bool_var(rec_app));
@ -751,12 +751,12 @@ namespace smt {
m_stats.m_splits++; m_stats.m_splits++;
if (d->m_recognizers.empty()) { if (d->m_recognizers.empty()) {
r = m_util.get_constructor_recognizer(non_rec_c); r = m_util.get_constructor_is(non_rec_c);
} }
else { else {
enode * recognizer = d->m_recognizers[non_rec_idx]; enode * recognizer = d->m_recognizers[non_rec_idx];
if (recognizer == nullptr) { 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)) { else if (!ctx.is_relevant(recognizer)) {
ctx.mark_as_relevant(recognizer); ctx.mark_as_relevant(recognizer);
@ -776,7 +776,7 @@ namespace smt {
if (curr == nullptr) { if (curr == nullptr) {
ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(s); ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(s);
// found empty slot... // found empty slot...
r = m_util.get_constructor_recognizer(constructors[idx]); r = m_util.get_constructor_is(constructors[idx]);
break; break;
} }
else if (!ctx.is_relevant(curr)) { else if (!ctx.is_relevant(curr)) {