3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-09-10 15:15:00 -07:00
parent a37d05d54b
commit e818b7bd27
4 changed files with 51 additions and 4 deletions

View file

@ -1656,6 +1656,12 @@ bool ast_manager::are_distinct(expr* a, expr* b) const {
return false;
}
func_decl* ast_manager::get_rec_fun_decl(quantifier* q) const {
SASSERT(is_rec_fun_def(q));
return to_app(to_app(q->get_pattern(0))->get_arg(0))->get_decl();
}
void ast_manager::register_plugin(family_id id, decl_plugin * plugin) {
SASSERT(m_plugins.get(id, 0) == 0);
m_plugins.setx(id, plugin, 0);

View file

@ -1632,6 +1632,7 @@ public:
bool is_rec_fun_def(quantifier* q) const { return q->get_qid() == m_rec_fun; }
bool is_lambda_def(quantifier* q) const { return q->get_qid() == m_lambda_def; }
func_decl* get_rec_fun_decl(quantifier* q) const;
symbol const& rec_fun_qid() const { return m_rec_fun; }

View file

@ -47,6 +47,7 @@ namespace smt {
m_model_finder(mf),
m_max_cexs(1),
m_iteration_idx(0),
m_has_rec_fun(false),
m_curr_model(nullptr),
m_pinned_exprs(m) {
}
@ -351,9 +352,7 @@ namespace smt {
bool model_checker::check_rec_fun(quantifier* q, bool strict_rec_fun) {
TRACE("model_checker", tout << mk_pp(q, m) << "\n";);
SASSERT(q->get_num_patterns() == 2); // first pattern is the function, second is the body.
expr* fn = to_app(q->get_pattern(0))->get_arg(0);
SASSERT(is_app(fn));
func_decl* f = to_app(fn)->get_decl();
func_decl* f = m.get_rec_fun_decl(q);
expr_ref_vector args(m);
unsigned num_decls = q->get_num_decls();
@ -433,7 +432,7 @@ namespace smt {
TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);
m_max_cexs += m_params.m_mbqi_max_cexs;
if (num_failures == 0 && !m_context->validate_model()) {
if (num_failures == 0 && (!m_context->validate_model() || has_rec_under_quantifiers())) {
num_failures = 1;
// this time force expanding recursive function definitions
// that are not forced true in the current model.
@ -450,6 +449,43 @@ namespace smt {
return num_failures == 0;
}
struct has_rec_fun_proc {
obj_hashtable<func_decl>& m_rec_funs;
bool m_has_rec_fun;
bool has_rec_fun() const { return m_has_rec_fun; }
has_rec_fun_proc(obj_hashtable<func_decl>& rec_funs):
m_rec_funs(rec_funs),
m_has_rec_fun(false) {}
void operator()(app* fn) {
m_has_rec_fun |= m_rec_funs.contains(fn->get_decl());
}
void operator()(expr*) {}
};
bool model_checker::has_rec_under_quantifiers() {
if (!m_has_rec_fun) {
return false;
}
obj_hashtable<func_decl> rec_funs;
for (quantifier * q : *m_qm) {
if (m.is_rec_fun_def(q)) {
rec_funs.insert(m.get_rec_fun_decl(q));
}
}
expr_fast_mark1 visited;
has_rec_fun_proc proc(rec_funs);
for (quantifier * q : *m_qm) {
if (!m.is_rec_fun_def(q)) {
quick_for_each_expr(proc, visited, q);
if (proc.has_rec_fun()) return true;
}
}
return false;
}
//
// (repeated from defined_names.cpp)
// NB. The pattern for lambdas is incomplete.
@ -479,6 +515,7 @@ namespace smt {
}
found_relevant = true;
if (m.is_rec_fun_def(q)) {
m_has_rec_fun = true;
if (!check_rec_fun(q, strict_rec_fun)) {
TRACE("model_checker", tout << "checking recursive function failed\n";);
num_failures++;

View file

@ -51,8 +51,10 @@ namespace smt {
scoped_ptr<context> m_aux_context; // Auxiliary context used for model checking quantifiers.
unsigned m_max_cexs;
unsigned m_iteration_idx;
bool m_has_rec_fun;
proto_model * m_curr_model;
obj_map<expr, expr *> m_value2expr;
friend class instantiation_set;
void init_aux_context();
@ -64,6 +66,7 @@ namespace smt {
bool add_blocking_clause(model * cex, expr_ref_vector & sks);
bool check(quantifier * q);
bool check_rec_fun(quantifier* q, bool strict_rec_fun);
bool has_rec_under_quantifiers();
void check_quantifiers(bool strict_rec_fun, bool& found_relevant, unsigned& num_failures);
struct instance {