mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fix #4938

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-02-26 02:06:15 -08:00
parent 56e4ee3273
commit ea1089e980
5 changed files with 27 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/ast/datatype_decl_plugin.cpp
View file

@ -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));

2
src/ast/datatype_decl_plugin.h
View file

@ -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);

8
src/model/model_evaluator.cpp
View file

@ -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;

5
src/sat/smt/dt_solver.cpp
View file

@ -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));

8
src/smt/theory_datatype.cpp
View file

@ -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;
}