From 3d486c4c98b2a6d07ca397f4fd2d2d5257d19e95 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Apr 2013 15:28:45 -0700 Subject: [PATCH 1/5] add abstraction and instantiation Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/expr_safe_replace.cpp | 6 + src/ast/rewriter/expr_safe_replace.h | 2 + src/muz_qe/dl_context.cpp | 4 + src/muz_qe/dl_mk_quantifier_abstraction.cpp | 206 ++++++++++++ src/muz_qe/dl_mk_quantifier_abstraction.h | 61 ++++ src/muz_qe/dl_mk_quantifier_instantiation.cpp | 295 ++++++++++++++++++ src/muz_qe/dl_mk_quantifier_instantiation.h | 120 +++++++ src/muz_qe/fixedpoint_params.pyg | 2 + 8 files changed, 696 insertions(+) create mode 100644 src/muz_qe/dl_mk_quantifier_abstraction.cpp create mode 100644 src/muz_qe/dl_mk_quantifier_abstraction.h create mode 100644 src/muz_qe/dl_mk_quantifier_instantiation.cpp create mode 100644 src/muz_qe/dl_mk_quantifier_instantiation.h diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp index b3b4d5138..1ec810414 100644 --- a/src/ast/rewriter/expr_safe_replace.cpp +++ b/src/ast/rewriter/expr_safe_replace.cpp @@ -100,3 +100,9 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) { } res = cache.find(e); } + +void expr_safe_replace::reset() { + m_src.reset(); + m_dst.reset(); + m_subst.reset(); +} diff --git a/src/ast/rewriter/expr_safe_replace.h b/src/ast/rewriter/expr_safe_replace.h index 6af819596..b6131906a 100644 --- a/src/ast/rewriter/expr_safe_replace.h +++ b/src/ast/rewriter/expr_safe_replace.h @@ -38,6 +38,8 @@ public: void operator()(expr_ref& e) { (*this)(e.get(), e); } void operator()(expr* src, expr_ref& e); + + void reset(); }; #endif /* __EXPR_SAFE_REPLACE_H__ */ diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index c667c7775..9207fbe61 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -46,6 +46,7 @@ Revision History: #include"dl_mk_bit_blast.h" #include"dl_mk_array_blast.h" #include"dl_mk_karr_invariants.h" +#include"dl_mk_quantifier_abstraction.h" #include"datatype_decl_plugin.h" #include"expr_abstract.h" @@ -905,6 +906,9 @@ namespace datalog { m_transf.register_plugin(alloc(datalog::mk_rule_inliner, *this, 34890)); m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34880)); + + m_transf.register_plugin(alloc(datalog::mk_quantifier_abstraction, *this, 33000)); + m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000)); m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000)); m_transf.register_plugin(alloc(datalog::mk_karr_invariants, *this, 36010)); diff --git a/src/muz_qe/dl_mk_quantifier_abstraction.cpp b/src/muz_qe/dl_mk_quantifier_abstraction.cpp new file mode 100644 index 000000000..511ab7b9a --- /dev/null +++ b/src/muz_qe/dl_mk_quantifier_abstraction.cpp @@ -0,0 +1,206 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_mk_quantifier_abstraction.cpp + +Abstract: + + Create quantified Horn clauses from benchmarks with arrays. + +Author: + + Ken McMillan + Andrey Rybalchenko + Nikolaj Bjorner (nbjorner) 2013-04-02 + +Revision History: + +--*/ + +#include "dl_mk_quantifier_abstraction.h" +#include "dl_context.h" + +namespace datalog { + + mk_quantifier_abstraction::mk_quantifier_abstraction( + context & ctx, unsigned priority): + plugin(priority), + m(ctx.get_manager()), + m_ctx(ctx), + a(m), + m_refs(m) { + } + + mk_quantifier_abstraction::~mk_quantifier_abstraction() { + + } + + func_decl* mk_quantifier_abstraction::declare_pred(func_decl* old_p) { + + unsigned sz = old_p->get_arity(); + unsigned num_arrays = 0; + for (unsigned i = 0; i < sz; ++i) { + if (a.is_array(old_p->get_domain(i))) { + num_arrays++; + } + } + if (num_arrays == 0) { + return 0; + } + + func_decl* new_p = 0; + if (!m_old2new.find(old_p, new_p)) { + sort_ref_vector domain(m); + for (unsigned i = 0; i < sz; ++i) { + sort* s = old_p->get_domain(i); + while (a.is_array(s)) { + unsigned arity = get_array_arity(s); + for (unsigned j = 0; j < arity; ++j) { + domain.push_back(get_array_domain(s, j)); + } + s = get_array_range(s); + } + domain.push_back(s); + } + SASSERT(old_p->get_range() == m.mk_bool_sort()); + new_p = m.mk_func_decl(old_p->get_name(), domain.size(), domain.c_ptr(), old_p->get_range()); + m_refs.push_back(new_p); + m_ctx.register_predicate(new_p); + } + return new_p; + } + + app_ref mk_quantifier_abstraction::mk_head(app* p, unsigned idx) { + func_decl* new_p = declare_pred(p->get_decl()); + if (!new_p) { + return app_ref(p, m); + } + expr_ref_vector args(m); + expr_ref arg(m); + unsigned sz = p->get_num_args(); + for (unsigned i = 0; i < sz; ++i) { + arg = p->get_arg(i); + sort* s = m.get_sort(arg); + while (a.is_array(s)) { + unsigned arity = get_array_arity(s); + for (unsigned j = 0; j < arity; ++j) { + args.push_back(m.mk_var(idx++, get_array_domain(s, j))); + } + ptr_vector args2; + args2.push_back(arg); + args2.append(arity, args.c_ptr()-arity); + arg = a.mk_select(args2.size(), args2.c_ptr()); + s = get_array_range(s); + } + args.push_back(arg); + } + return app_ref(m.mk_app(new_p, args.size(), args.c_ptr()), m); + } + + app_ref mk_quantifier_abstraction::mk_tail(app* p) { + func_decl* old_p = p->get_decl(); + func_decl* new_p = declare_pred(old_p); + if (!new_p) { + return app_ref(p, m); + } + SASSERT(new_p->get_arity() > old_p->get_arity()); + unsigned num_extra_args = new_p->get_arity() - old_p->get_arity(); + var_shifter shift(m); + expr_ref p_shifted(m); + shift(p, num_extra_args, p_shifted); + app* ps = to_app(p_shifted); + expr_ref_vector args(m); + app_ref_vector pats(m); + sort_ref_vector vars(m); + svector names; + expr_ref arg(m); + unsigned idx = 0; + unsigned sz = p->get_num_args(); + for (unsigned i = 0; i < sz; ++i) { + arg = ps->get_arg(i); + sort* s = m.get_sort(arg); + bool is_pattern = false; + while (a.is_array(s)) { + is_pattern = true; + unsigned arity = get_array_arity(s); + for (unsigned j = 0; j < arity; ++j) { + vars.push_back(get_array_domain(s, j)); + names.push_back(symbol(idx)); + args.push_back(m.mk_var(idx++, vars.back())); + } + ptr_vector args2; + args2.push_back(arg); + args2.append(arity, args.c_ptr()-arity); + arg = a.mk_select(args2.size(), args2.c_ptr()); + s = get_array_range(s); + } + if (is_pattern) { + pats.push_back(to_app(arg)); + } + args.push_back(arg); + } + expr* pat = 0; + expr_ref pattern(m); + pattern = m.mk_pattern(pats.size(), pats.c_ptr()); + pat = pattern.get(); + app_ref result(m); + symbol qid, skid; + result = m.mk_app(new_p, args.size(), args.c_ptr()); + result = m.mk_eq(m.mk_forall(vars.size(), vars.c_ptr(), names.c_ptr(), result, 1, qid, skid, 1, &pat), m.mk_true()); + return result; + } + + rule_set * mk_quantifier_abstraction::operator()(rule_set const & source) { + if (!m_ctx.get_params().quantify_arrays()) { + return 0; + } + m_refs.reset(); + m_old2new.reset(); + m_new2old.reset(); + rule_manager& rm = source.get_rule_manager(); + rule_set * result = alloc(rule_set, m_ctx); + unsigned sz = source.get_num_rules(); + rule_ref new_rule(rm); + app_ref_vector tail(m); + app_ref head(m); + svector neg; + rule_counter& vc = rm.get_counter(); + + for (unsigned i = 0; i < sz; ++i) { + tail.reset(); + neg.reset(); + rule & r = *source.get_rule(i); + unsigned cnt = vc.get_max_rule_var(r)+1; + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned tsz = r.get_tail_size(); + for (unsigned j = 0; j < utsz; ++j) { + tail.push_back(mk_tail(r.get_tail(j))); + neg.push_back(r.is_neg_tail(j)); + } + for (unsigned j = utsz; j < tsz; ++j) { + tail.push_back(r.get_tail(j)); + neg.push_back(false); + } + head = mk_head(r.get_head(), cnt); + + new_rule = rm.mk(head, tail.size(), tail.c_ptr(), neg.c_ptr(), r.name(), true); + result->add_rule(new_rule); + + } + + // model converter: TBD. + // proof converter: TBD. + + if (m_old2new.empty()) { + dealloc(result); + result = 0; + } + return result; + } + + +}; + + diff --git a/src/muz_qe/dl_mk_quantifier_abstraction.h b/src/muz_qe/dl_mk_quantifier_abstraction.h new file mode 100644 index 000000000..8c26e277a --- /dev/null +++ b/src/muz_qe/dl_mk_quantifier_abstraction.h @@ -0,0 +1,61 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_mk_quantifier_abstraction.h + +Abstract: + + Convert clauses with array arguments to predicates + into Quantified Horn clauses. + +Author: + + Ken McMillan + Andrey Rybalchenko + Nikolaj Bjorner (nbjorner) 2013-04-02 + +Revision History: + + Based on approach suggested in SAS 2013 paper + "On Solving Universally Quantified Horn Clauses" + +--*/ +#ifndef _DL_MK_QUANTIFIER_ABSTRACTION_H_ +#define _DL_MK_QUANTIFIER_ABSTRACTION_H_ + + +#include"dl_rule_transformer.h" +#include"array_decl_plugin.h" + +namespace datalog { + + class context; + + class mk_quantifier_abstraction : public rule_transformer::plugin { + ast_manager& m; + context& m_ctx; + array_util a; + func_decl_ref_vector m_refs; + obj_map m_new2old; + obj_map m_old2new; + + func_decl* declare_pred(func_decl* old_p); + app_ref mk_head(app* p, unsigned idx); + app_ref mk_tail(app* p); + + public: + mk_quantifier_abstraction(context & ctx, unsigned priority); + + virtual ~mk_quantifier_abstraction(); + + rule_set * operator()(rule_set const & source); + }; + + + +}; + +#endif /* _DL_MK_QUANTIFIER_ABSTRACTION_H_ */ + diff --git a/src/muz_qe/dl_mk_quantifier_instantiation.cpp b/src/muz_qe/dl_mk_quantifier_instantiation.cpp new file mode 100644 index 000000000..a5b80af4f --- /dev/null +++ b/src/muz_qe/dl_mk_quantifier_instantiation.cpp @@ -0,0 +1,295 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_mk_quantifier_instantiation.cpp + +Abstract: + + Convert Quantified Horn clauses into non-quantified clauses using + instantiation. + +Author: + + Ken McMillan + Andrey Rybalchenko + Nikolaj Bjorner (nbjorner) 2013-04-02 + +Revision History: + + Based on approach suggested in SAS 2013 paper + "On Solving Universally Quantified Horn Clauses" + +--*/ + +#include "dl_mk_quantifier_instantiation.h" +#include "dl_context.h" + +namespace datalog { + + mk_quantifier_instantiation::mk_quantifier_instantiation( + context & ctx, unsigned priority): + plugin(priority), + m(ctx.get_manager()), + m_ctx(ctx), + m_var2cnst(m), + m_cnst2var(m), + a(m) { + } + + mk_quantifier_instantiation::~mk_quantifier_instantiation() { + + } + + void mk_quantifier_instantiation::extract_quantifiers(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs) { + conjs.reset(); + qs.reset(); + unsigned tsz = r.get_tail_size(); + for (unsigned j = 0; j < tsz; ++j) { + conjs.push_back(r.get_tail(j)); + + } + datalog::flatten_and(conjs); + for (unsigned j = 0; j < conjs.size(); ++j) { + expr* e = conjs[j].get(); + quantifier* q; + if (rule_manager::is_forall(m, e, q)) { + qs.push_back(q); + conjs[j] = conjs.back(); + conjs.pop_back(); + --j; + } + } + } + + void mk_quantifier_instantiation::instantiate_quantifier(quantifier* q, expr_ref_vector & conjs) { + expr_ref qe(m); + qe = q; + m_var2cnst(qe); + q = to_quantifier(qe); + unsigned num_patterns = q->get_num_patterns(); + for (unsigned i = 0; i < num_patterns; ++i) { + expr * pat = q->get_pattern(i); + SASSERT(m.is_pattern(pat)); + instantiate_quantifier(q, to_app(pat), conjs); + } + } + + + void mk_quantifier_instantiation::instantiate_quantifier(quantifier* q, app* pat, expr_ref_vector & conjs) { + unsigned sz = pat->get_num_args(); + m_binding.reset(); + m_binding.resize(q->get_num_decls()); + term_pairs todo; + match(0, pat, 0, todo, q, conjs); + } + + void mk_quantifier_instantiation::match(unsigned i, app* pat, unsigned j, term_pairs& todo, quantifier* q, expr_ref_vector& conjs) { + while (j < todo.size()) { + expr* p = todo[j].first; + expr* t = todo[j].second; + if (is_var(p)) { + unsigned idx = to_var(p)->get_idx(); + expr* t2 = m_binding[idx]; + if (!t2) { + m_binding[idx] = t; + match(i, pat, j + 1, todo, q, conjs); + m_binding[idx] = 0; + return; + } + else if (m_uf.find(t2->get_id()) != m_uf.find(t->get_id())) { + // matching failed. + return; + } + j += 1; + continue; + } + if (!is_app(p)) { + return; + } + app* a1 = to_app(p); + unsigned id = t->get_id(); + unsigned next_id = id; + unsigned sz = todo.size(); + do { + expr* t2 = m_terms[next_id]; + if (is_app(t2)) { + app* a2 = to_app(t2); + if (a1->get_decl() == a2->get_decl() && + a1->get_num_args() == a2->get_num_args()) { + for (unsigned k = 0; k < a1->get_num_args(); ++k) { + todo.push_back(std::make_pair(a1->get_arg(k), a2->get_arg(k))); + } + match(i, pat, j + 1, todo, q, conjs); + todo.resize(sz); + } + } + next_id = m_uf.next(id); + } + while (next_id != id); + return; + } + + if (i == pat->get_num_args()) { + yield_binding(q, conjs); + return; + } + expr* arg = pat->get_arg(i); + ptr_vector* terms = 0; + + if (m_funs.find(to_app(arg)->get_decl(), terms)) { + for (unsigned k = 0; k < terms->size(); ++k) { + todo.push_back(std::make_pair(arg, (*terms)[k])); + match(i + 1, pat, j, todo, q, conjs); + todo.pop_back(); + } + } + } + + void mk_quantifier_instantiation::yield_binding(quantifier* q, expr_ref_vector& conjs) { + DEBUG_CODE( + for (unsigned i = 0; i < m_binding.size(); ++i) { + SASSERT(m_binding[i]); + }); + m_binding.reverse(); + expr_ref res(m); + instantiate(m, q, m_binding.c_ptr(), res); + m_binding.reverse(); + conjs.push_back(res); + } + + void mk_quantifier_instantiation::merge(expr* e1, expr* e2) { + unsigned i1 = e1->get_id(); + unsigned i2 = e2->get_id(); + unsigned n = std::max(i1, i2); + while (n >= m_uf.get_num_vars()) { + m_uf.mk_var(); + } + m_uf.merge(i1, i2); + } + + void mk_quantifier_instantiation::collect_egraph(expr* e) { + expr* e1, *e2; + m_todo.push_back(e); + expr_fast_mark1 visited; + while (!m_todo.empty()) { + e = m_todo.back(); + m_todo.pop_back(); + if (visited.is_marked(e)) { + continue; + } + if (e->get_id() >= m_terms.size()) { + m_terms.resize(e->get_id()+1); + } + m_terms[e->get_id()] = e; + visited.mark(e); + if (m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) { + merge(e1, e2); + } + if (is_app(e)) { + app* ap = to_app(e); + ptr_vector* terms = 0; + if (m_funs.find(ap->get_decl(), terms)) { + terms = alloc(ptr_vector); + m_funs.insert(ap->get_decl(), terms); + } + terms->push_back(e); + m_todo.append(ap->get_num_args(), ap->get_args()); + } + } + } + + void mk_quantifier_instantiation::instantiate_rule(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs, rule_set& rules) { + rule_manager& rm = m_ctx.get_rule_manager(); + expr_ref fml(m), cnst(m); + var_ref var(m); + ptr_vector sorts; + r.get_vars(sorts); + m_uf.reset(); + m_terms.reset(); + m_var2cnst.reset(); + m_cnst2var.reset(); + fml = m.mk_and(conjs.size(), conjs.c_ptr()); + + for (unsigned i = 0; i < sorts.size(); ++i) { + if (!sorts[i]) { + sorts[i] = m.mk_bool_sort(); + } + var = m.mk_var(i, sorts[i]); + cnst = m.mk_fresh_const("C", sorts[i]); + m_var2cnst.insert(var, cnst); + m_cnst2var.insert(cnst, var); + } + + fml = m.mk_and(conjs.size(), conjs.c_ptr()); + m_var2cnst(fml); + collect_egraph(fml); + + for (unsigned i = 0; i < qs.size(); ++i) { + instantiate_quantifier(qs[i].get(), conjs); + } + obj_map*>::iterator it = m_funs.begin(), end = m_funs.end(); + for (; it != end; ++it) { + dealloc(it->m_value); + } + m_funs.reset(); + + fml = m.mk_and(conjs.size(), conjs.c_ptr()); + fml = m.mk_implies(fml, r.get_head()); + + rule_ref_vector added_rules(rm); + proof_ref pr(m); // proofs are TBD. + rm.mk_rule(fml, pr, added_rules); + rules.add_rules(added_rules.size(), added_rules.c_ptr()); + } + + rule_set * mk_quantifier_instantiation::operator()(rule_set const & source) { + if (!m_ctx.get_params().instantiate_quantifiers()) { + return 0; + } + bool has_quantifiers = false; + unsigned sz = source.get_num_rules(); + for (unsigned i = 0; !has_quantifiers && i < sz; ++i) { + rule& r = *source.get_rule(i); + has_quantifiers = has_quantifiers || r.has_quantifiers(); + if (r.has_negation()) { + return 0; + } + } + if (!has_quantifiers) { + return 0; + } + + expr_ref_vector conjs(m); + quantifier_ref_vector qs(m); + rule_set * result = alloc(rule_set, m_ctx); + + bool instantiated = false; + + for (unsigned i = 0; i < sz; ++i) { + rule * r = source.get_rule(i); + extract_quantifiers(*r, conjs, qs); + if (qs.empty()) { + result->add_rule(r); + } + else { + instantiate_rule(*r, conjs, qs, *result); + instantiated = true; + } + } + + // model converter: TBD. + // proof converter: TBD. + + if (!instantiated) { + dealloc(result); + result = 0; + } + return result; + } + + +}; + + diff --git a/src/muz_qe/dl_mk_quantifier_instantiation.h b/src/muz_qe/dl_mk_quantifier_instantiation.h new file mode 100644 index 000000000..81a77e86a --- /dev/null +++ b/src/muz_qe/dl_mk_quantifier_instantiation.h @@ -0,0 +1,120 @@ +/*++ +Copyright (c) 2013 Microsoft Corporation + +Module Name: + + dl_mk_quantifier_instantiation.h + +Abstract: + + Convert Quantified Horn clauses into non-quantified clauses using + instantiation. + +Author: + + Ken McMillan + Andrey Rybalchenko + Nikolaj Bjorner (nbjorner) 2013-04-02 + +Revision History: + + Based on approach suggested in SAS 2013 paper + "On Solving Universally Quantified Horn Clauses" + +--*/ +#ifndef _DL_MK_QUANTIFIER_INSTANTIATION_H_ +#define _DL_MK_QUANTIFIER_INSTANTIATION_H_ + + +#include"dl_rule_transformer.h" +#include"array_decl_plugin.h" +#include"expr_safe_replace.h" + + +namespace datalog { + + class context; + + class mk_quantifier_instantiation : public rule_transformer::plugin { + typedef svector > term_pairs; + + class union_find { + unsigned_vector m_find; + unsigned_vector m_size; + unsigned_vector m_next; + public: + unsigned mk_var() { + unsigned r = m_find.size(); + m_find.push_back(r); + m_size.push_back(1); + m_next.push_back(r); + return r; + } + unsigned get_num_vars() const { return m_find.size(); } + + unsigned find(unsigned v) const { + while (true) { + unsigned new_v = m_find[v]; + if (new_v == v) + return v; + v = new_v; + } + } + + unsigned next(unsigned v) const { return m_next[v]; } + + bool is_root(unsigned v) const { return m_find[v] == v; } + + void merge(unsigned v1, unsigned v2) { + unsigned r1 = find(v1); + unsigned r2 = find(v2); + if (r1 == r2) + return; + if (m_size[r1] > m_size[r2]) + std::swap(r1, r2); + m_find[r1] = r2; + m_size[r2] += m_size[r1]; + std::swap(m_next[r1], m_next[r2]); + } + + void reset() { + m_find.reset(); + m_next.reset(); + m_size.reset(); + } + }; + ast_manager& m; + context& m_ctx; + expr_safe_replace m_var2cnst; + expr_safe_replace m_cnst2var; + array_util a; + union_find m_uf; + ptr_vector m_todo; + ptr_vector m_terms; + ptr_vector m_binding; + obj_map*> m_funs; + + + void merge(expr* e1, expr* e2); + void extract_quantifiers(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs); + void collect_egraph(expr* e); + void instantiate_rule(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs, rule_set& rules); + void instantiate_quantifier(quantifier* q, expr_ref_vector & conjs); + void mk_quantifier_instantiation::instantiate_quantifier(quantifier* q, app* pat, expr_ref_vector & conjs); + void mk_quantifier_instantiation::match(unsigned i, app* pat, unsigned j, term_pairs& todo, quantifier* q, expr_ref_vector& conjs); + void mk_quantifier_instantiation::yield_binding(quantifier* q, expr_ref_vector& conjs); + + public: + mk_quantifier_instantiation(context & ctx, unsigned priority); + + virtual ~mk_quantifier_instantiation(); + + rule_set * operator()(rule_set const & source); + }; + + + +}; + +#endif /* _DL_MK_QUANTIFIER_INSTANTIATION_H_ */ + diff --git a/src/muz_qe/fixedpoint_params.pyg b/src/muz_qe/fixedpoint_params.pyg index 7a3316c56..774559cdb 100644 --- a/src/muz_qe/fixedpoint_params.pyg +++ b/src/muz_qe/fixedpoint_params.pyg @@ -42,6 +42,8 @@ def_module_params('fixedpoint', ('simplify_formulas_post', BOOL, False, "PDR: simplify derived formulas after inductive propagation"), ('slice', BOOL, True, "PDR: simplify clause set using slicing"), ('karr', BOOL, False, "Add linear invariants to clauses using Karr's method"), + ('quantify_arrays', BOOL, False, "create quantified Horn clauses from clauses with arrays"), + ('instantiate_quantifiers', BOOL, False, "instantiate quantified Horn clauses using E-matching heuristic"), ('coalesce_rules', BOOL, False, "BMC: coalesce rules"), ('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"), ('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"), From cda29bc03b8e0e64099a4f7b95792fc181471a46 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Apr 2013 15:29:52 -0700 Subject: [PATCH 2/5] add abstraction and instantiation Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_context.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 9207fbe61..44852a52f 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -47,6 +47,7 @@ Revision History: #include"dl_mk_array_blast.h" #include"dl_mk_karr_invariants.h" #include"dl_mk_quantifier_abstraction.h" +#include"dl_mk_quantifier_instantiation.h" #include"datatype_decl_plugin.h" #include"expr_abstract.h" @@ -908,6 +909,7 @@ namespace datalog { m_transf.register_plugin(alloc(datalog::mk_quantifier_abstraction, *this, 33000)); + m_transf.register_plugin(alloc(datalog::mk_quantifier_instantiation, *this, 32000)); m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000)); m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000)); From 477e8cc46a10c61a211aba23acbdcd77b337dcf1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Apr 2013 20:33:22 -0700 Subject: [PATCH 3/5] debugging quantifier instantiation Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_mk_quantifier_instantiation.cpp | 35 +++++++++------ src/muz_qe/dl_mk_quantifier_instantiation.h | 45 +++++++++++++------ 2 files changed, 52 insertions(+), 28 deletions(-) diff --git a/src/muz_qe/dl_mk_quantifier_instantiation.cpp b/src/muz_qe/dl_mk_quantifier_instantiation.cpp index a5b80af4f..11c039bf8 100644 --- a/src/muz_qe/dl_mk_quantifier_instantiation.cpp +++ b/src/muz_qe/dl_mk_quantifier_instantiation.cpp @@ -18,13 +18,14 @@ Author: Revision History: - Based on approach suggested in SAS 2013 paper + Based on approach suggested in the SAS 2013 paper "On Solving Universally Quantified Horn Clauses" --*/ #include "dl_mk_quantifier_instantiation.h" #include "dl_context.h" +#include "pattern_inference.h" namespace datalog { @@ -34,12 +35,10 @@ namespace datalog { m(ctx.get_manager()), m_ctx(ctx), m_var2cnst(m), - m_cnst2var(m), - a(m) { + m_cnst2var(m) { } - mk_quantifier_instantiation::~mk_quantifier_instantiation() { - + mk_quantifier_instantiation::~mk_quantifier_instantiation() { } void mk_quantifier_instantiation::extract_quantifiers(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs) { @@ -66,8 +65,15 @@ namespace datalog { void mk_quantifier_instantiation::instantiate_quantifier(quantifier* q, expr_ref_vector & conjs) { expr_ref qe(m); qe = q; - m_var2cnst(qe); + m_var2cnst(qe); q = to_quantifier(qe); + if (q->get_num_patterns() == 0) { + proof_ref new_pr(m); + pattern_inference_params params; + pattern_inference infer(m, params); + infer(q, qe, new_pr); + q = to_quantifier(qe); + } unsigned num_patterns = q->get_num_patterns(); for (unsigned i = 0; i < num_patterns; ++i) { expr * pat = q->get_pattern(i); @@ -86,6 +92,7 @@ namespace datalog { } void mk_quantifier_instantiation::match(unsigned i, app* pat, unsigned j, term_pairs& todo, quantifier* q, expr_ref_vector& conjs) { + TRACE("dl", tout << "match" << mk_pp(pat, m) << "\n";); while (j < todo.size()) { expr* p = todo[j].first; expr* t = todo[j].second; @@ -102,7 +109,7 @@ namespace datalog { // matching failed. return; } - j += 1; + ++j; continue; } if (!is_app(p)) { @@ -125,7 +132,7 @@ namespace datalog { todo.resize(sz); } } - next_id = m_uf.next(id); + next_id = m_uf.next(next_id); } while (next_id != id); return; @@ -156,16 +163,14 @@ namespace datalog { expr_ref res(m); instantiate(m, q, m_binding.c_ptr(), res); m_binding.reverse(); + m_cnst2var(res); conjs.push_back(res); + TRACE("dl", tout << mk_pp(q, m) << "\n==>\n" << mk_pp(res, m) << "\n";); } void mk_quantifier_instantiation::merge(expr* e1, expr* e2) { unsigned i1 = e1->get_id(); unsigned i2 = e2->get_id(); - unsigned n = std::max(i1, i2); - while (n >= m_uf.get_num_vars()) { - m_uf.mk_var(); - } m_uf.merge(i1, i2); } @@ -179,7 +184,8 @@ namespace datalog { if (visited.is_marked(e)) { continue; } - if (e->get_id() >= m_terms.size()) { + unsigned n = e->get_id(); + if (n >= m_terms.size()) { m_terms.resize(e->get_id()+1); } m_terms[e->get_id()] = e; @@ -190,7 +196,7 @@ namespace datalog { if (is_app(e)) { app* ap = to_app(e); ptr_vector* terms = 0; - if (m_funs.find(ap->get_decl(), terms)) { + if (!m_funs.find(ap->get_decl(), terms)) { terms = alloc(ptr_vector); m_funs.insert(ap->get_decl(), terms); } @@ -237,6 +243,7 @@ namespace datalog { fml = m.mk_and(conjs.size(), conjs.c_ptr()); fml = m.mk_implies(fml, r.get_head()); + TRACE("dl", r.display(m_ctx, tout); tout << mk_pp(fml, m) << "\n";); rule_ref_vector added_rules(rm); proof_ref pr(m); // proofs are TBD. diff --git a/src/muz_qe/dl_mk_quantifier_instantiation.h b/src/muz_qe/dl_mk_quantifier_instantiation.h index 81a77e86a..969a0bf23 100644 --- a/src/muz_qe/dl_mk_quantifier_instantiation.h +++ b/src/muz_qe/dl_mk_quantifier_instantiation.h @@ -18,7 +18,7 @@ Author: Revision History: - Based on approach suggested in SAS 2013 paper + Based on approach suggested in the SAS 2013 paper "On Solving Universally Quantified Horn Clauses" --*/ @@ -27,7 +27,6 @@ Revision History: #include"dl_rule_transformer.h" -#include"array_decl_plugin.h" #include"expr_safe_replace.h" @@ -42,6 +41,12 @@ namespace datalog { unsigned_vector m_find; unsigned_vector m_size; unsigned_vector m_next; + + void ensure_size(unsigned v) { + while (v >= get_num_vars()) { + mk_var(); + } + } public: unsigned mk_var() { unsigned r = m_find.size(); @@ -53,6 +58,9 @@ namespace datalog { unsigned get_num_vars() const { return m_find.size(); } unsigned find(unsigned v) const { + if (v >= get_num_vars()) { + return v; + } while (true) { unsigned new_v = m_find[v]; if (new_v == v) @@ -61,15 +69,24 @@ namespace datalog { } } - unsigned next(unsigned v) const { return m_next[v]; } + unsigned next(unsigned v) const { + if (v >= get_num_vars()) { + return v; + } + return m_next[v]; + } - bool is_root(unsigned v) const { return m_find[v] == v; } + bool is_root(unsigned v) const { + return v >= get_num_vars() || m_find[v] == v; + } void merge(unsigned v1, unsigned v2) { unsigned r1 = find(v1); unsigned r2 = find(v2); if (r1 == r2) return; + ensure_size(v1); + ensure_size(v2); if (m_size[r1] > m_size[r2]) std::swap(r1, r2); m_find[r1] = r2; @@ -83,15 +100,15 @@ namespace datalog { m_size.reset(); } }; - ast_manager& m; - context& m_ctx; + + ast_manager& m; + context& m_ctx; expr_safe_replace m_var2cnst; expr_safe_replace m_cnst2var; - array_util a; - union_find m_uf; - ptr_vector m_todo; - ptr_vector m_terms; - ptr_vector m_binding; + union_find m_uf; + ptr_vector m_todo; + ptr_vector m_terms; + ptr_vector m_binding; obj_map*> m_funs; @@ -100,9 +117,9 @@ namespace datalog { void collect_egraph(expr* e); void instantiate_rule(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs, rule_set& rules); void instantiate_quantifier(quantifier* q, expr_ref_vector & conjs); - void mk_quantifier_instantiation::instantiate_quantifier(quantifier* q, app* pat, expr_ref_vector & conjs); - void mk_quantifier_instantiation::match(unsigned i, app* pat, unsigned j, term_pairs& todo, quantifier* q, expr_ref_vector& conjs); - void mk_quantifier_instantiation::yield_binding(quantifier* q, expr_ref_vector& conjs); + void instantiate_quantifier(quantifier* q, app* pat, expr_ref_vector & conjs); + void match(unsigned i, app* pat, unsigned j, term_pairs& todo, quantifier* q, expr_ref_vector& conjs); + void yield_binding(quantifier* q, expr_ref_vector& conjs); public: mk_quantifier_instantiation(context & ctx, unsigned priority); From 2a745d5224c416ce81bcf8f5d586cdc24a879d1e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Apr 2013 14:46:58 -0700 Subject: [PATCH 4/5] adding model convertion to quantifier transformation Signed-off-by: Nikolaj Bjorner --- src/api/api_datalog.cpp | 4 +- src/muz_qe/datalog_parser.cpp | 4 +- src/muz_qe/dl_cmds.cpp | 1 + src/muz_qe/dl_context.cpp | 11 +- src/muz_qe/dl_context.h | 14 +- src/muz_qe/dl_mk_karr_invariants.cpp | 2 +- src/muz_qe/dl_mk_loop_counter.cpp | 4 +- src/muz_qe/dl_mk_quantifier_abstraction.cpp | 160 ++++++++++++++++-- src/muz_qe/dl_mk_quantifier_abstraction.h | 5 +- src/muz_qe/dl_mk_quantifier_instantiation.cpp | 38 ++--- src/muz_qe/dl_mk_quantifier_instantiation.h | 1 - src/muz_qe/dl_rule.cpp | 2 +- src/muz_qe/horn_tactic.cpp | 2 +- 13 files changed, 188 insertions(+), 60 deletions(-) diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 0f100e747..f6eadfea0 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -358,7 +358,7 @@ extern "C" { v->m_ast_vector.push_back(coll.m_queries[i].get()); } for (unsigned i = 0; i < coll.m_rels.size(); ++i) { - to_fixedpoint_ref(d)->ctx().register_predicate(coll.m_rels[i].get()); + to_fixedpoint_ref(d)->ctx().register_predicate(coll.m_rels[i].get(), true); } for (unsigned i = 0; i < coll.m_rules.size(); ++i) { to_fixedpoint_ref(d)->add_rule(coll.m_rules[i].get(), coll.m_names[i]); @@ -415,7 +415,7 @@ extern "C" { void Z3_API Z3_fixedpoint_register_relation(Z3_context c,Z3_fixedpoint d, Z3_func_decl f) { Z3_TRY; LOG_Z3_fixedpoint_register_relation(c, d, f); - to_fixedpoint_ref(d)->ctx().register_predicate(to_func_decl(f)); + to_fixedpoint_ref(d)->ctx().register_predicate(to_func_decl(f), true); Z3_CATCH; } diff --git a/src/muz_qe/datalog_parser.cpp b/src/muz_qe/datalog_parser.cpp index cfe283410..545f3e14a 100644 --- a/src/muz_qe/datalog_parser.cpp +++ b/src/muz_qe/datalog_parser.cpp @@ -441,6 +441,7 @@ protected: unsigned m_sym_idx; std::string m_path; str2sort m_sort_dict; + // true if an error occured during the current call to the parse_stream // function @@ -812,7 +813,8 @@ protected: } f = m_manager.mk_func_decl(s, domain.size(), domain.c_ptr(), m_manager.mk_bool_sort()); - m_context.register_predicate(f); + m_context.register_predicate(f, true); + while (tok == TK_ID) { char const* pred_pragma = m_lexer->get_token_data(); if(strcmp(pred_pragma, "printtuples")==0 || strcmp(pred_pragma, "outputtuples")==0) { diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp index aef14e051..c1e3f85f9 100644 --- a/src/muz_qe/dl_cmds.cpp +++ b/src/muz_qe/dl_cmds.cpp @@ -229,6 +229,7 @@ public: status = dlctx.query(m_target); } catch (z3_error & ex) { + ctx.regular_stream() << "(error \"query failed: " << ex.msg() << "\")" << std::endl; throw ex; } catch (z3_exception& ex) { diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 44852a52f..a928d7ba7 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -302,14 +302,6 @@ namespace datalog { return m_preds.contains(pred); } - func_decl * context::try_get_predicate_decl(symbol pred_name) const { - func_decl * res; - if (!m_preds_by_name.find(pred_name, res)) { - return 0; - } - return res; - } - void context::register_variable(func_decl* var) { m_vars.push_back(m.mk_const(var)); } @@ -361,7 +353,6 @@ namespace datalog { m_pinned.push_back(decl); m_preds.insert(decl); if (named) { - SASSERT(!m_preds_by_name.contains(decl->get_name())); m_preds_by_name.insert(decl->get_name(), decl); } } @@ -448,7 +439,7 @@ namespace datalog { func_decl* new_pred = m.mk_fresh_func_decl(prefix, suffix, arity, domain, m.mk_bool_sort()); - register_predicate(new_pred); + register_predicate(new_pred, true); if (m_rel.get()) { m_rel->inherit_predicate_kind(new_pred, orig_pred); diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index 0c4558a28..cb432d4e9 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -183,18 +183,22 @@ namespace datalog { retrieved by the try_get_predicate_decl() function. Auxiliary predicates introduced e.g. by rule transformations do not need to be named. */ - void register_predicate(func_decl * pred, bool named = true); + void register_predicate(func_decl * pred, bool named); bool is_predicate(func_decl * pred) const; - + /** \brief If a predicate name has a \c func_decl object assigned, return pointer to it; otherwise return 0. - + Not all \c func_decl object used as relation identifiers need to be assigned to their names. Generally, the names coming from the parses are registered here. - */ - func_decl * try_get_predicate_decl(symbol pred_name) const; + */ + func_decl * try_get_predicate_decl(symbol const& pred_name) const { + func_decl * res = 0; + m_preds_by_name.find(pred_name, res); + return res; + } /** \brief Create a fresh head predicate declaration. diff --git a/src/muz_qe/dl_mk_karr_invariants.cpp b/src/muz_qe/dl_mk_karr_invariants.cpp index 2596a7337..7932735fe 100644 --- a/src/muz_qe/dl_mk_karr_invariants.cpp +++ b/src/muz_qe/dl_mk_karr_invariants.cpp @@ -206,7 +206,7 @@ namespace datalog { for (; it != end; ++it) { rule_ref r(*it, m_inner_ctx.get_rule_manager()); m_inner_ctx.add_rule(r); - m_inner_ctx.register_predicate(r->get_decl()); + m_inner_ctx.register_predicate(r->get_decl(), false); } m_inner_ctx.close(); rule_set::decl2rules::iterator dit = source.begin_grouped_rules(); diff --git a/src/muz_qe/dl_mk_loop_counter.cpp b/src/muz_qe/dl_mk_loop_counter.cpp index 172198746..6b95671f2 100644 --- a/src/muz_qe/dl_mk_loop_counter.cpp +++ b/src/muz_qe/dl_mk_loop_counter.cpp @@ -72,14 +72,14 @@ namespace datalog { for (unsigned j = 0; j < utsz; ++j, ++cnt) { tail.push_back(add_arg(r.get_tail(j), cnt)); neg.push_back(r.is_neg_tail(j)); - ctx.register_predicate(tail.back()->get_decl()); + ctx.register_predicate(tail.back()->get_decl(), false); } for (unsigned j = utsz; j < tsz; ++j) { tail.push_back(r.get_tail(j)); neg.push_back(false); } head = add_arg(r.get_head(), cnt); - ctx.register_predicate(head->get_decl()); + ctx.register_predicate(head->get_decl(), false); // set the loop counter to be an increment of the previous bool found = false; unsigned last = head->get_num_args()-1; diff --git a/src/muz_qe/dl_mk_quantifier_abstraction.cpp b/src/muz_qe/dl_mk_quantifier_abstraction.cpp index 511ab7b9a..0dd48ef53 100644 --- a/src/muz_qe/dl_mk_quantifier_abstraction.cpp +++ b/src/muz_qe/dl_mk_quantifier_abstraction.cpp @@ -21,9 +21,110 @@ Revision History: #include "dl_mk_quantifier_abstraction.h" #include "dl_context.h" +#include "expr_safe_replace.h" +#include "expr_abstract.h" namespace datalog { + + // model converter: + // Given model for P^(x, y, i, a[i]) + // create model: P(x,y,a) == forall i . P^(x,y,i,a[i]) + // requires substitution and list of bound variables. + + class mk_quantifier_abstraction::qa_model_converter : public model_converter { + ast_manager& m; + func_decl_ref_vector m_old_funcs; + func_decl_ref_vector m_new_funcs; + vector m_subst; + vector > m_bound; + + public: + + qa_model_converter(ast_manager& m): + m(m), m_old_funcs(m), m_new_funcs(m) {} + + virtual ~qa_model_converter() {} + + virtual model_converter * translate(ast_translation & translator) { + return alloc(qa_model_converter, m); + } + + void insert(func_decl* old_p, func_decl* new_p, expr_ref_vector& sub, svector const& bound) { + m_old_funcs.push_back(old_p); + m_new_funcs.push_back(new_p); + m_subst.push_back(sub); + m_bound.push_back(bound); + } + + virtual void operator()(model_ref & model) { + for (unsigned i = 0; i < m_new_funcs.size(); ++i) { + func_decl* p = m_new_funcs[i].get(); + func_decl* q = m_old_funcs[i].get(); + expr_ref_vector const& s = m_subst[i]; + svector const& is_bound = m_bound[i]; + func_interp* f = model->get_func_interp(p); + expr_ref body(m); + unsigned arity_p = p->get_arity(); + unsigned arity_q = q->get_arity(); + SASSERT(0 < arity_p); + model->register_decl(p, f); + func_interp* g = alloc(func_interp, m, arity_q); + + if (f) { + body = f->get_interp(); + SASSERT(!f->is_partial()); + SASSERT(body); + } + else { + body = m.mk_false(); + } + // TBD. create quantifier wrapper around body. + + // 1. replace variables by the compound terms from + // the original predicate. + expr_safe_replace sub(m); + for (unsigned i = 0; i < s.size(); ++i) { + sub.insert(m.mk_var(i, m.get_sort(s[i])), s[i]); + } + sub(body); + sub.reset(); + + // 2. replace bound variables by constants. + expr_ref_vector consts(m), bound(m), free(m); + ptr_vector sorts; + svector names; + for (unsigned i = 0; i < q->get_arity(); ++i) { + sort* s = q->get_domain(i); + consts.push_back(m.mk_fresh_const("C", s)); + sub.insert(m.mk_var(i, s), consts.back()); + if (is_bound[i]) { + bound.push_back(consts.back()); + names.push_back(symbol(i)); + sorts.push_back(s); + } + else { + free.push_back(consts.back()); + } + } + sub(body); + sub.reset(); + + // 3. abstract and quantify those variables that should be bound. + expr_abstract(m, 0, bound.size(), bound.c_ptr(), body, body); + body = m.mk_forall(names.size(), sorts.c_ptr(), names.c_ptr(), body); + + // 4. replace remaining constants by variables. + for (unsigned i = 0; i < free.size(); ++i) { + sub.insert(free[i].get(), m.mk_var(i, m.get_sort(free[i].get()))); + } + sub(body); + g->set_else(body); + model->register_decl(q, g); + } + } + }; + mk_quantifier_abstraction::mk_quantifier_abstraction( context & ctx, unsigned priority): plugin(priority), @@ -33,8 +134,7 @@ namespace datalog { m_refs(m) { } - mk_quantifier_abstraction::~mk_quantifier_abstraction() { - + mk_quantifier_abstraction::~mk_quantifier_abstraction() { } func_decl* mk_quantifier_abstraction::declare_pred(func_decl* old_p) { @@ -52,22 +152,41 @@ namespace datalog { func_decl* new_p = 0; if (!m_old2new.find(old_p, new_p)) { + expr_ref_vector sub(m); + svector bound; sort_ref_vector domain(m); + expr_ref arg(m); for (unsigned i = 0; i < sz; ++i) { sort* s = old_p->get_domain(i); + unsigned lookahead = 0; + sort* s0 = s; + while (a.is_array(s0)) { + lookahead += get_array_arity(s0); + s0 = get_array_range(s0); + } + arg = m.mk_var(bound.size() + lookahead, s); while (a.is_array(s)) { unsigned arity = get_array_arity(s); + expr_ref_vector args(m); for (unsigned j = 0; j < arity; ++j) { domain.push_back(get_array_domain(s, j)); + args.push_back(m.mk_var(bound.size(), domain.back())); + bound.push_back(true); } + arg = mk_select(arg, args.size(), args.c_ptr()); s = get_array_range(s); } domain.push_back(s); + bound.push_back(false); + sub.push_back(arg); } SASSERT(old_p->get_range() == m.mk_bool_sort()); new_p = m.mk_func_decl(old_p->get_name(), domain.size(), domain.c_ptr(), old_p->get_range()); m_refs.push_back(new_p); - m_ctx.register_predicate(new_p); + m_ctx.register_predicate(new_p, false); + if (m_mc) { + m_mc->insert(old_p, new_p, sub, bound); + } } return new_p; } @@ -88,10 +207,7 @@ namespace datalog { for (unsigned j = 0; j < arity; ++j) { args.push_back(m.mk_var(idx++, get_array_domain(s, j))); } - ptr_vector args2; - args2.push_back(arg); - args2.append(arity, args.c_ptr()-arity); - arg = a.mk_select(args2.size(), args2.c_ptr()); + arg = mk_select(arg, arity, args.c_ptr()+args.size()-arity); s = get_array_range(s); } args.push_back(arg); @@ -130,10 +246,7 @@ namespace datalog { names.push_back(symbol(idx)); args.push_back(m.mk_var(idx++, vars.back())); } - ptr_vector args2; - args2.push_back(arg); - args2.append(arity, args.c_ptr()-arity); - arg = a.mk_select(args2.size(), args2.c_ptr()); + arg = mk_select(arg, arity, args.c_ptr()+args.size()-arity); s = get_array_range(s); } if (is_pattern) { @@ -151,8 +264,16 @@ namespace datalog { result = m.mk_eq(m.mk_forall(vars.size(), vars.c_ptr(), names.c_ptr(), result, 1, qid, skid, 1, &pat), m.mk_true()); return result; } + + expr * mk_quantifier_abstraction::mk_select(expr* arg, unsigned num_args, expr* const* args) { + ptr_vector args2; + args2.push_back(arg); + args2.append(num_args, args); + return a.mk_select(args2.size(), args2.c_ptr()); + } rule_set * mk_quantifier_abstraction::operator()(rule_set const & source) { + TRACE("dl", tout << "quantify " << source.get_num_rules() << " " << m_ctx.get_params().quantify_arrays() << "\n";); if (!m_ctx.get_params().quantify_arrays()) { return 0; } @@ -168,6 +289,10 @@ namespace datalog { svector neg; rule_counter& vc = rm.get_counter(); + if (m_ctx.get_model_converter()) { + m_mc = alloc(qa_model_converter, m); + } + for (unsigned i = 0; i < sz; ++i) { tail.reset(); neg.reset(); @@ -186,17 +311,22 @@ namespace datalog { head = mk_head(r.get_head(), cnt); new_rule = rm.mk(head, tail.size(), tail.c_ptr(), neg.c_ptr(), r.name(), true); + TRACE("dl", r.display(m_ctx, tout); new_rule->display(m_ctx, tout);); result->add_rule(new_rule); - } - - // model converter: TBD. - // proof converter: TBD. + + // proof converter: proofs are not necessarily preserved using this transformation. if (m_old2new.empty()) { dealloc(result); + dealloc(m_mc); result = 0; } + else { + m_ctx.add_model_converter(m_mc); + } + m_mc = 0; + return result; } diff --git a/src/muz_qe/dl_mk_quantifier_abstraction.h b/src/muz_qe/dl_mk_quantifier_abstraction.h index 8c26e277a..c7e6c6bb4 100644 --- a/src/muz_qe/dl_mk_quantifier_abstraction.h +++ b/src/muz_qe/dl_mk_quantifier_abstraction.h @@ -34,16 +34,19 @@ namespace datalog { class context; class mk_quantifier_abstraction : public rule_transformer::plugin { + class qa_model_converter; ast_manager& m; context& m_ctx; array_util a; - func_decl_ref_vector m_refs; + func_decl_ref_vector m_refs; obj_map m_new2old; obj_map m_old2new; + qa_model_converter* m_mc; func_decl* declare_pred(func_decl* old_p); app_ref mk_head(app* p, unsigned idx); app_ref mk_tail(app* p); + expr* mk_select(expr* a, unsigned num_args, expr* const* args); public: mk_quantifier_abstraction(context & ctx, unsigned priority); diff --git a/src/muz_qe/dl_mk_quantifier_instantiation.cpp b/src/muz_qe/dl_mk_quantifier_instantiation.cpp index 11c039bf8..993e5ada5 100644 --- a/src/muz_qe/dl_mk_quantifier_instantiation.cpp +++ b/src/muz_qe/dl_mk_quantifier_instantiation.cpp @@ -46,8 +46,7 @@ namespace datalog { qs.reset(); unsigned tsz = r.get_tail_size(); for (unsigned j = 0; j < tsz; ++j) { - conjs.push_back(r.get_tail(j)); - + conjs.push_back(r.get_tail(j)); } datalog::flatten_and(conjs); for (unsigned j = 0; j < conjs.size(); ++j) { @@ -98,17 +97,12 @@ namespace datalog { expr* t = todo[j].second; if (is_var(p)) { unsigned idx = to_var(p)->get_idx(); - expr* t2 = m_binding[idx]; - if (!t2) { + if (!m_binding[idx]) { m_binding[idx] = t; match(i, pat, j + 1, todo, q, conjs); m_binding[idx] = 0; return; } - else if (m_uf.find(t2->get_id()) != m_uf.find(t->get_id())) { - // matching failed. - return; - } ++j; continue; } @@ -168,12 +162,6 @@ namespace datalog { TRACE("dl", tout << mk_pp(q, m) << "\n==>\n" << mk_pp(res, m) << "\n";); } - void mk_quantifier_instantiation::merge(expr* e1, expr* e2) { - unsigned i1 = e1->get_id(); - unsigned i2 = e2->get_id(); - m_uf.merge(i1, i2); - } - void mk_quantifier_instantiation::collect_egraph(expr* e) { expr* e1, *e2; m_todo.push_back(e); @@ -186,12 +174,12 @@ namespace datalog { } unsigned n = e->get_id(); if (n >= m_terms.size()) { - m_terms.resize(e->get_id()+1); + m_terms.resize(n+1); } - m_terms[e->get_id()] = e; + m_terms[n] = e; visited.mark(e); if (m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) { - merge(e1, e2); + m_uf.merge(e1->get_id(), e2->get_id()); } if (is_app(e)) { app* ap = to_app(e); @@ -246,12 +234,23 @@ namespace datalog { TRACE("dl", r.display(m_ctx, tout); tout << mk_pp(fml, m) << "\n";); rule_ref_vector added_rules(rm); - proof_ref pr(m); // proofs are TBD. + proof_ref pr(m); rm.mk_rule(fml, pr, added_rules); + if (r.get_proof()) { + // use def-axiom to encode that new rule is a weakening of the original. + proof* p1 = r.get_proof(); + for (unsigned i = 0; i < added_rules.size(); ++i) { + rule* r2 = added_rules[i].get(); + r2->to_formula(fml); + pr = m.mk_modus_ponens(m.mk_def_axiom(m.mk_implies(m.get_fact(p1), fml)), p1); + r2->set_proof(m, pr); + } + } rules.add_rules(added_rules.size(), added_rules.c_ptr()); } rule_set * mk_quantifier_instantiation::operator()(rule_set const & source) { + TRACE("dl", tout << m_ctx.get_params().instantiate_quantifiers() << "\n";); if (!m_ctx.get_params().instantiate_quantifiers()) { return 0; } @@ -286,8 +285,7 @@ namespace datalog { } } - // model converter: TBD. - // proof converter: TBD. + // model convertion: identity function. if (!instantiated) { dealloc(result); diff --git a/src/muz_qe/dl_mk_quantifier_instantiation.h b/src/muz_qe/dl_mk_quantifier_instantiation.h index 969a0bf23..138d5abee 100644 --- a/src/muz_qe/dl_mk_quantifier_instantiation.h +++ b/src/muz_qe/dl_mk_quantifier_instantiation.h @@ -112,7 +112,6 @@ namespace datalog { obj_map*> m_funs; - void merge(expr* e1, expr* e2); void extract_quantifiers(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs); void collect_egraph(expr* e); void instantiate_rule(rule& r, expr_ref_vector& conjs, quantifier_ref_vector& qs, rule_set& rules); diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp index 14a316e48..b7d6d9fae 100644 --- a/src/muz_qe/dl_rule.cpp +++ b/src/muz_qe/dl_rule.cpp @@ -135,7 +135,7 @@ namespace datalog { h.set_name(name); h(fml, p, fmls, prs); for (unsigned i = 0; i < h.get_fresh_predicates().size(); ++i) { - m_ctx.register_predicate(h.get_fresh_predicates()[i]); + m_ctx.register_predicate(h.get_fresh_predicates()[i], false); } for (unsigned i = 0; i < fmls.size(); ++i) { mk_rule_core2(fmls[i].get(), prs[i].get(), rules, name); diff --git a/src/muz_qe/horn_tactic.cpp b/src/muz_qe/horn_tactic.cpp index 02c41c091..1a8f562d9 100644 --- a/src/muz_qe/horn_tactic.cpp +++ b/src/muz_qe/horn_tactic.cpp @@ -92,7 +92,7 @@ class horn_tactic : public tactic { void register_predicate(expr* a) { SASSERT(is_predicate(a)); - m_ctx.register_predicate(to_app(a)->get_decl(), true); + m_ctx.register_predicate(to_app(a)->get_decl(), false); } void check_predicate(ast_mark& mark, expr* a) { From 0b7a270883dc8b66070b88ed2ca132aa5a6d5b48 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Apr 2013 16:53:09 -0700 Subject: [PATCH 5/5] debug quantifier transforms Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_context.cpp | 5 +- src/muz_qe/dl_mk_quantifier_abstraction.cpp | 125 ++++++++++++-------- src/muz_qe/dl_rule_set.h | 1 - 3 files changed, 82 insertions(+), 49 deletions(-) diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index a928d7ba7..852d8f847 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -899,7 +899,10 @@ namespace datalog { m_transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34880)); - m_transf.register_plugin(alloc(datalog::mk_quantifier_abstraction, *this, 33000)); + if (get_params().quantify_arrays()) { + m_transf.register_plugin(alloc(datalog::mk_quantifier_abstraction, *this, 33000)); + m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 32500)); + } m_transf.register_plugin(alloc(datalog::mk_quantifier_instantiation, *this, 32000)); m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000)); diff --git a/src/muz_qe/dl_mk_quantifier_abstraction.cpp b/src/muz_qe/dl_mk_quantifier_abstraction.cpp index 0dd48ef53..d4abb1ffc 100644 --- a/src/muz_qe/dl_mk_quantifier_abstraction.cpp +++ b/src/muz_qe/dl_mk_quantifier_abstraction.cpp @@ -37,6 +37,7 @@ namespace datalog { func_decl_ref_vector m_old_funcs; func_decl_ref_vector m_new_funcs; vector m_subst; + vector m_sorts; vector > m_bound; public: @@ -50,25 +51,27 @@ namespace datalog { return alloc(qa_model_converter, m); } - void insert(func_decl* old_p, func_decl* new_p, expr_ref_vector& sub, svector const& bound) { + void insert(func_decl* old_p, func_decl* new_p, expr_ref_vector& sub, sort_ref_vector& sorts, svector const& bound) { m_old_funcs.push_back(old_p); m_new_funcs.push_back(new_p); m_subst.push_back(sub); m_bound.push_back(bound); + m_sorts.push_back(sorts); } - virtual void operator()(model_ref & model) { + virtual void operator()(model_ref & old_model) { + model_ref new_model = alloc(model, m); for (unsigned i = 0; i < m_new_funcs.size(); ++i) { func_decl* p = m_new_funcs[i].get(); func_decl* q = m_old_funcs[i].get(); - expr_ref_vector const& s = m_subst[i]; + expr_ref_vector const& sub = m_subst[i]; + sort_ref_vector const& sorts = m_sorts[i]; svector const& is_bound = m_bound[i]; - func_interp* f = model->get_func_interp(p); + func_interp* f = old_model->get_func_interp(p); expr_ref body(m); unsigned arity_p = p->get_arity(); unsigned arity_q = q->get_arity(); SASSERT(0 < arity_p); - model->register_decl(p, f); func_interp* g = alloc(func_interp, m, arity_q); if (f) { @@ -79,49 +82,56 @@ namespace datalog { else { body = m.mk_false(); } - // TBD. create quantifier wrapper around body. + // Create quantifier wrapper around body. + TRACE("dl", tout << mk_pp(body, m) << "\n";); // 1. replace variables by the compound terms from // the original predicate. - expr_safe_replace sub(m); - for (unsigned i = 0; i < s.size(); ++i) { - sub.insert(m.mk_var(i, m.get_sort(s[i])), s[i]); + expr_safe_replace rep(m); + for (unsigned i = 0; i < sub.size(); ++i) { + rep.insert(m.mk_var(i, m.get_sort(sub[i])), sub[i]); } - sub(body); - sub.reset(); + rep(body); + rep.reset(); + TRACE("dl", tout << mk_pp(body, m) << "\n";); // 2. replace bound variables by constants. expr_ref_vector consts(m), bound(m), free(m); - ptr_vector sorts; svector names; - for (unsigned i = 0; i < q->get_arity(); ++i) { - sort* s = q->get_domain(i); + ptr_vector bound_sorts; + for (unsigned i = 0; i < sorts.size(); ++i) { + sort* s = sorts[i]; consts.push_back(m.mk_fresh_const("C", s)); - sub.insert(m.mk_var(i, s), consts.back()); + rep.insert(m.mk_var(i, s), consts.back()); if (is_bound[i]) { bound.push_back(consts.back()); names.push_back(symbol(i)); - sorts.push_back(s); + bound_sorts.push_back(s); } else { free.push_back(consts.back()); } } - sub(body); - sub.reset(); + rep(body); + rep.reset(); + TRACE("dl", tout << mk_pp(body, m) << "\n";); // 3. abstract and quantify those variables that should be bound. expr_abstract(m, 0, bound.size(), bound.c_ptr(), body, body); - body = m.mk_forall(names.size(), sorts.c_ptr(), names.c_ptr(), body); + body = m.mk_forall(names.size(), bound_sorts.c_ptr(), names.c_ptr(), body); + TRACE("dl", tout << mk_pp(body, m) << "\n";); // 4. replace remaining constants by variables. for (unsigned i = 0; i < free.size(); ++i) { - sub.insert(free[i].get(), m.mk_var(i, m.get_sort(free[i].get()))); + rep.insert(free[i].get(), m.mk_var(i, m.get_sort(free[i].get()))); } - sub(body); + rep(body); g->set_else(body); - model->register_decl(q, g); + TRACE("dl", tout << mk_pp(body, m) << "\n";); + + new_model->register_decl(q, g); } + old_model = new_model; } }; @@ -139,6 +149,10 @@ namespace datalog { func_decl* mk_quantifier_abstraction::declare_pred(func_decl* old_p) { + if (m_ctx.is_output_predicate(old_p)) { + return 0; + } + unsigned sz = old_p->get_arity(); unsigned num_arrays = 0; for (unsigned i = 0; i < sz; ++i) { @@ -152,26 +166,29 @@ namespace datalog { func_decl* new_p = 0; if (!m_old2new.find(old_p, new_p)) { - expr_ref_vector sub(m); - svector bound; - sort_ref_vector domain(m); + expr_ref_vector sub(m), vars(m); + svector bound; + sort_ref_vector domain(m), sorts(m); expr_ref arg(m); for (unsigned i = 0; i < sz; ++i) { - sort* s = old_p->get_domain(i); + sort* s0 = old_p->get_domain(i); unsigned lookahead = 0; - sort* s0 = s; - while (a.is_array(s0)) { - lookahead += get_array_arity(s0); - s0 = get_array_range(s0); + sort* s = s0; + while (a.is_array(s)) { + lookahead += get_array_arity(s); + s = get_array_range(s); } - arg = m.mk_var(bound.size() + lookahead, s); + arg = m.mk_var(bound.size() + lookahead, s0); + s = s0; while (a.is_array(s)) { unsigned arity = get_array_arity(s); expr_ref_vector args(m); for (unsigned j = 0; j < arity; ++j) { - domain.push_back(get_array_domain(s, j)); - args.push_back(m.mk_var(bound.size(), domain.back())); + sort* s1 = get_array_domain(s, j); + domain.push_back(s1); + args.push_back(m.mk_var(bound.size(), s1)); bound.push_back(true); + sorts.push_back(s1); } arg = mk_select(arg, args.size(), args.c_ptr()); s = get_array_range(s); @@ -179,14 +196,16 @@ namespace datalog { domain.push_back(s); bound.push_back(false); sub.push_back(arg); + sorts.push_back(s0); } SASSERT(old_p->get_range() == m.mk_bool_sort()); new_p = m.mk_func_decl(old_p->get_name(), domain.size(), domain.c_ptr(), old_p->get_range()); m_refs.push_back(new_p); m_ctx.register_predicate(new_p, false); if (m_mc) { - m_mc->insert(old_p, new_p, sub, bound); + m_mc->insert(old_p, new_p, sub, sorts, bound); } + m_old2new.insert(old_p, new_p); } return new_p; } @@ -212,6 +231,11 @@ namespace datalog { } args.push_back(arg); } + TRACE("dl", + tout << mk_pp(new_p, m) << "\n"; + for (unsigned i = 0; i < args.size(); ++i) { + tout << mk_pp(args[i].get(), m) << "\n"; + }); return app_ref(m.mk_app(new_p, args.size(), args.c_ptr()), m); } @@ -237,7 +261,7 @@ namespace datalog { for (unsigned i = 0; i < sz; ++i) { arg = ps->get_arg(i); sort* s = m.get_sort(arg); - bool is_pattern = false; + bool is_pattern = false; while (a.is_array(s)) { is_pattern = true; unsigned arity = get_array_arity(s); @@ -277,42 +301,49 @@ namespace datalog { if (!m_ctx.get_params().quantify_arrays()) { return 0; } + unsigned sz = source.get_num_rules(); + for (unsigned i = 0; i < sz; ++i) { + rule& r = *source.get_rule(i); + if (r.has_negation()) { + return 0; + } + } + m_refs.reset(); m_old2new.reset(); m_new2old.reset(); rule_manager& rm = source.get_rule_manager(); - rule_set * result = alloc(rule_set, m_ctx); - unsigned sz = source.get_num_rules(); rule_ref new_rule(rm); - app_ref_vector tail(m); + expr_ref_vector tail(m); app_ref head(m); - svector neg; + expr_ref fml(m); rule_counter& vc = rm.get_counter(); if (m_ctx.get_model_converter()) { m_mc = alloc(qa_model_converter, m); } + rule_set * result = alloc(rule_set, m_ctx); - for (unsigned i = 0; i < sz; ++i) { + for (unsigned i = 0; i < sz; ++i) { tail.reset(); - neg.reset(); rule & r = *source.get_rule(i); + TRACE("dl", r.display(m_ctx, tout); ); unsigned cnt = vc.get_max_rule_var(r)+1; unsigned utsz = r.get_uninterpreted_tail_size(); unsigned tsz = r.get_tail_size(); for (unsigned j = 0; j < utsz; ++j) { tail.push_back(mk_tail(r.get_tail(j))); - neg.push_back(r.is_neg_tail(j)); } for (unsigned j = utsz; j < tsz; ++j) { tail.push_back(r.get_tail(j)); - neg.push_back(false); } head = mk_head(r.get_head(), cnt); - - new_rule = rm.mk(head, tail.size(), tail.c_ptr(), neg.c_ptr(), r.name(), true); - TRACE("dl", r.display(m_ctx, tout); new_rule->display(m_ctx, tout);); - result->add_rule(new_rule); + fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), head); + rule_ref_vector added_rules(rm); + proof_ref pr(m); + rm.mk_rule(fml, pr, added_rules); + result->add_rules(added_rules.size(), added_rules.c_ptr()); + TRACE("dl", added_rules.back()->display(m_ctx, tout);); } // proof converter: proofs are not necessarily preserved using this transformation. diff --git a/src/muz_qe/dl_rule_set.h b/src/muz_qe/dl_rule_set.h index 9aa64425c..58427ca87 100644 --- a/src/muz_qe/dl_rule_set.h +++ b/src/muz_qe/dl_rule_set.h @@ -20,7 +20,6 @@ Revision History: #define _DL_RULE_SET_H_ #include"obj_hashtable.h" - #include"dl_rule.h" namespace datalog {