From d318aab7d1abea500cf47b0fb410ae21b5d6126d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 2 Jan 2013 09:49:27 -0800 Subject: [PATCH] experiments wtih QHC Signed-off-by: Nikolaj Bjorner --- src/muz_qe/dl_context.cpp | 4 + src/muz_qe/dl_mk_extract_quantifiers.cpp | 370 +++++++++++++++++----- src/muz_qe/dl_mk_extract_quantifiers.h | 52 ++- src/muz_qe/dl_mk_extract_quantifiers2.cpp | 107 ------- src/muz_qe/dl_mk_extract_quantifiers2.h | 66 ---- src/muz_qe/pdr_dl_interface.cpp | 9 +- src/muz_qe/pdr_quantifiers.cpp | 45 +-- src/muz_qe/pdr_quantifiers.h | 15 +- src/muz_qe/proof_utils.cpp | 2 +- 9 files changed, 379 insertions(+), 291 deletions(-) delete mode 100644 src/muz_qe/dl_mk_extract_quantifiers2.cpp delete mode 100644 src/muz_qe/dl_mk_extract_quantifiers2.h diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 5581732c8..5784c7be2 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -1206,7 +1206,11 @@ namespace datalog { for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { ptr_vector sorts; get_free_vars(m_rule_fmls[i].get(), sorts); + while (!sorts.empty() && !sorts.back()) { + sorts.pop_back(); + } if (!sorts.empty()) { + std::cout << "has free vars " << mk_pp(m_rule_fmls[i].get(), m) << "\n"; rm.mk_rule(m_rule_fmls[i].get(), rule_refs, m_rule_names[i]); m_rule_fmls[i] = m_rule_fmls.back(); m_rule_names[i] = m_rule_names.back(); diff --git a/src/muz_qe/dl_mk_extract_quantifiers.cpp b/src/muz_qe/dl_mk_extract_quantifiers.cpp index d2b4f0cec..8a5aa52ec 100644 --- a/src/muz_qe/dl_mk_extract_quantifiers.cpp +++ b/src/muz_qe/dl_mk_extract_quantifiers.cpp @@ -19,6 +19,12 @@ Revision History: #include"dl_mk_extract_quantifiers.h" #include"ast_pp.h" +#include"dl_bmc_engine.h" +#include"smt_quantifier.h" +#include"smt_context.h" +#include"for_each_expr.h" +#include "expr_abstract.h" + namespace datalog { @@ -27,24 +33,16 @@ namespace datalog { rule_transformer::plugin(101, false), m_ctx(ctx), m(ctx.get_manager()), - rm(ctx.get_rule_manager()) + rm(ctx.get_rule_manager()), + m_query_pred(m) {} mk_extract_quantifiers::~mk_extract_quantifiers() { - for (unsigned i = 0; i < m_refs.size(); ++i) { - dealloc(m_refs[i]); - } - m_quantifiers.reset(); - m_refs.reset(); + reset(); } - app_ref mk_extract_quantifiers::ensure_app(expr* e) { - if (is_app(e)) { - return app_ref(to_app(e), m); - } - else { - return app_ref(m.mk_eq(e, m.mk_true()), m); - } + void mk_extract_quantifiers::set_query(func_decl* q) { + m_query_pred = q; } void mk_extract_quantifiers::ensure_predicate(expr* e, unsigned& max_var, app_ref_vector& tail) { @@ -67,85 +65,305 @@ namespace datalog { tail.push_back(m.mk_app(a->get_decl(), args.size(), args.c_ptr())); } + class mk_extract_quantifiers::collect_insts { + ast_manager& m; + ptr_vector m_binding; + vector m_bindings; + ptr_vector m_quantifiers; + public: + collect_insts(ast_manager& m): m(m) { } + void operator()(expr* n) { + expr* not_q_or_i, *e1, *e2, *e3; + if (m.is_quant_inst(n, not_q_or_i, m_binding)) { + VERIFY(m.is_or(not_q_or_i, e1, e2)); + VERIFY(m.is_not(e1, e3)); + SASSERT(is_quantifier(e3)); + m_quantifiers.push_back(to_quantifier(e3)); + m_bindings.push_back(expr_ref_vector(m,m_binding.size(), m_binding.c_ptr())); + m_binding.reset(); + } + else if ((m.is_rewrite(n, e1, e2) || + (m.is_rewrite_star(n) && + (e3 = to_app(n)->get_arg(to_app(n)->get_num_args()-1), + e1 = to_app(e3)->get_arg(0), + e2 = to_app(e3)->get_arg(1), + true))) && + is_quantifier(e1) && m.is_false(e2)) { + quantifier* q = to_quantifier(e1); + m_quantifiers.push_back(q); + m_bindings.push_back(expr_ref_vector(m)); + expr_ref_vector& b = m_bindings.back(); + for (unsigned i = 0; i < q->get_num_decls(); ++i) { + b.push_back(m.mk_fresh_const("V", q->get_decl_sort(i))); + } + } + } + + void reset() { + m_quantifiers.reset(); + m_bindings.reset(); + } + + unsigned size() const { return m_quantifiers.size(); } + ptr_vector const& quantifiers() const { return m_quantifiers; } + vector const& bindings() const { return m_bindings; } + }; + + + /* + * forall y . P1(x,y) & + * forall y . P2(x,y) & + * Body[x] & + * ~H[x] + * forall y . y != binding1 => ~ P1(x,y) + * forall y . y != binding2 => ~ P2(x,y) + */ void mk_extract_quantifiers::extract(rule& r, rule_set& new_rules) { - app_ref_vector tail(m); - quantifier_ref_vector quantifiers(m); unsigned utsz = r.get_uninterpreted_tail_size(); - unsigned tsz = r.get_tail_size(); - var_counter vc(true); - unsigned max_var = vc.get_max_var(r); - for (unsigned i = 0; i < utsz; ++i) { - tail.push_back(r.get_tail(i)); - if (r.is_neg_tail(i)) { - new_rules.add_rule(&r); - return; + expr_ref_vector conjs(m); + quantifier_ref_vector qs(m); + for (unsigned i = utsz; i < r.get_tail_size(); ++i) { + conjs.push_back(r.get_tail(i)); + } + 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; } } - var_subst vs(m, true); - for (unsigned i = utsz; i < tsz; ++i) { - app* t = r.get_tail(i); - expr_ref_vector conjs(m); - datalog::flatten_and(t, conjs); - expr_ref qe(m); - quantifier* q = 0; - for (unsigned j = 0; j < conjs.size(); ++j) { - expr* e = conjs[j].get(); - if (rule_manager::is_forall(m, e, q)) { - quantifiers.push_back(q); - expr_ref_vector sub(m); - ptr_vector fv; - unsigned num_decls = q->get_num_decls(); - get_free_vars(q, fv); - for (unsigned k = 0; k < fv.size(); ++k) { - unsigned idx = fv.size()-k-1; - if (!fv[idx]) { - fv[idx] = m.mk_bool_sort(); - } - sub.push_back(m.mk_var(idx, fv[idx])); - } - for (unsigned k = 0; k < num_decls; ++k) { - sub.push_back(m.mk_var(num_decls+max_var-k, q->get_decl_sort(k))); - } - max_var += num_decls; - vs(q->get_expr(), sub.size(), sub.c_ptr(), qe); - ensure_predicate(qe, max_var, tail); - } - else { - tail.push_back(ensure_app(e)); - } - } - } - if (quantifiers.empty()) { + if (qs.empty()) { new_rules.add_rule(&r); } else { - rule_ref new_rule(rm); - TRACE("dl", - tout << mk_pp(r.get_head(), m) << " :- \n"; - for (unsigned i = 0; i < tail.size(); ++i) { - tout << " " << mk_pp(tail[i].get(), m) << "\n"; - }); - new_rule = rm.mk(r.get_head(), tail.size(), tail.c_ptr(), 0, r.name(), false); - quantifier_ref_vector* qs = alloc(quantifier_ref_vector, quantifiers); - m_refs.push_back(qs); - new_rules.add_rule(new_rule); - m_quantifiers.insert(new_rule, qs); + expr_ref fml(m); + expr_ref_vector bindings(m); + obj_map insts; + for (unsigned i = 0; i < qs.size(); ++i) { + insts.insert(qs[i].get(), alloc(expr_ref_vector, m)); + } + + unsigned max_inst = 10; // TODO configuration. + + for (unsigned i = 0; i < max_inst; ++i) { + app_ref_vector sub(m); + rule2formula(r, insts, fml, sub); + bool new_binding = find_instantiations_proof_based(fml, sub, insts, bindings); + if (!new_binding) { + break; + } + } + + expr_ref_vector fmls(m); + for (unsigned i = 0; i < utsz; ++i) { + fmls.push_back(r.get_tail(i)); + } + fmls.append(bindings); + fmls.append(conjs); + fml = m.mk_implies(m.mk_and(fmls.size(), fmls.c_ptr()), r.get_head()); + TRACE("dl", tout << "new rule\n" << mk_pp(fml, m) << "\n";); + rule_ref_vector rules(rm); + rm.mk_rule(fml, rules, r.name()); + for (unsigned i = 0; i < rules.size(); ++i) { + new_rules.add_rule(rules[i].get()); + m_quantifiers.insert(rules[i].get(), alloc(quantifier_ref_vector, qs)); + } + obj_map::iterator it = insts.begin(), end = insts.end(); + for (; it != end; ++it) { + dealloc(it->m_value); + } } } + + void mk_extract_quantifiers::rule2formula( + rule& r, + obj_map const& insts, + expr_ref& fml, + app_ref_vector& sub) + { + expr_ref body(m); + expr_ref_vector fmls(m); + ptr_vector sorts; + var_subst vs(m, false); + obj_map::iterator it = insts.begin(), end = insts.end(); + for (; it != end; ++it) { + quantifier* q = it->m_key; + expr_ref_vector& eqs = *it->m_value; + expr_ref_vector disj(m); + disj.append(eqs); + disj.push_back(m.mk_not(q->get_expr())); + body = m.mk_or(disj.size(), disj.c_ptr()); + fml = m.update_quantifier(q, body); + fmls.push_back(fml); + } + fml = m.mk_or(fmls.size(), fmls.c_ptr()); + fmls.reset(); + fmls.push_back(fml); + for (unsigned i = 0; i < r.get_tail_size(); ++i) { + SASSERT(!r.is_neg_tail(i)); + fmls.push_back(r.get_tail(i)); + } + fmls.push_back(m.mk_not(r.get_head())); + fml = m.mk_and(fmls.size(), fmls.c_ptr()); + + get_free_vars(fml, sorts); + for (unsigned i = 0; i < sorts.size(); ++i) { + if (!sorts[i]) { + sorts[i] = m.mk_bool_sort(); + } + sub.push_back(m.mk_const(symbol(i), sorts[i])); + } + vs(fml, sub.size(), (expr*const*)sub.c_ptr(), fml); + } + + bool mk_extract_quantifiers::find_instantiations_proof_based( + expr* fml, + app_ref_vector const& var_inst, + obj_map& insts, + expr_ref_vector& bindings) + { + datalog::scoped_fine_proof _scp(m); + smt_params fparams; + fparams.m_mbqi = true; // false + fparams.m_soft_timeout = 1000; + smt::kernel solver(m, fparams); + solver.assert_expr(fml); + IF_VERBOSE(1, verbose_stream() << "check\n";); + lbool result = solver.check(); + IF_VERBOSE(1, verbose_stream() << "checked\n";); + TRACE("dl", tout << result << "\n";); + if (result != l_false) { + return false; + } + + map qid_map; + quantifier* q; + + obj_map::iterator it = insts.begin(), end = insts.end(); + for (; it != end; ++it) { + q = it->m_key; + qid_map.insert(q->get_qid(), q); + } + + proof* p = solver.get_proof(); + TRACE("dl", tout << mk_pp(p, m) << "\n";); + collect_insts collector(m); + for_each_expr(collector, p); + ptr_vector const& quants = collector.quantifiers(); + + for (unsigned i = 0; i < collector.size(); ++i) { + symbol qid = quants[i]->get_qid(); + if (!qid_map.find(qid, q)) { + TRACE("dl", tout << "Could not find quantifier " << mk_pp(quants[i], m) << "\n";); + continue; + } + expr_ref_vector const& binding = collector.bindings()[i]; + + TRACE("dl", tout << "Instantiating:\n" << mk_pp(quants[i], m) << "\n"; + for (unsigned j = 0; j < binding.size(); ++j) { + tout << mk_pp(binding[j], m) << " "; + } + tout << "\n";); + + expr_ref_vector instantiation(m); + for (unsigned j = 0; j < binding.size(); ++j) { + instantiation.push_back(binding[j]); + } + add_binding(var_inst, bindings, q, instantiation, insts); + } + + return collector.size() > 0; + } + + void mk_extract_quantifiers::add_binding( + app_ref_vector const& var_inst, + expr_ref_vector& bindings, + quantifier* q, + expr_ref_vector const& instantiation, + obj_map& insts) + { + if (instantiation.size() == q->get_num_decls()) { + // Full binding. + apply_binding(var_inst, bindings, q, instantiation, insts); + } + } + + void mk_extract_quantifiers::apply_binding( + app_ref_vector const& var_inst, + expr_ref_vector& bindings, + quantifier* q, + expr_ref_vector const& instantiation, + obj_map& insts) + { + datalog::scoped_no_proof _scp(m); + expr_ref e(m); + expr_ref_vector eqs(m); + var_subst vs(m, false); + inv_var_shifter invsh(m); + vs(q->get_expr(), instantiation.size(), instantiation.c_ptr(), e); + invsh(e, q->get_num_decls(), e); + expr_ref_vector inst(m); + inst.append(var_inst.size(), (expr*const*)var_inst.c_ptr()); + inst.reverse(); + expr_abstract(m, 0, inst.size(), inst.c_ptr(), e, e); + bindings.push_back(e); + for (unsigned i = 0; i < instantiation.size(); ++i) { + e = instantiation[i]; + e = m.mk_eq(m.mk_var(i, q->get_decl_sort(i)), e); + eqs.push_back(e); + } + e = m.mk_and(eqs.size(), eqs.c_ptr()); + insts.find(q)->push_back(e); + + TRACE("dl", tout << mk_pp(q, m) << "\n"; + tout << "instantiation: "; + for (unsigned i = 0; i < instantiation.size(); ++i) { + tout << mk_pp(instantiation[i], m) << " "; + } + tout << "\n"; + tout << "inst: "; + for (unsigned i = 0; i < var_inst.size(); ++i) { + tout << mk_pp(var_inst[i], m) << " "; + } + tout << "\n"; + tout << mk_pp(bindings.back(), m) << "\n"; + tout << "eqs: " << mk_pp(e, m) << "\n"; + ); + } + + + void mk_extract_quantifiers::reset() { + obj_map::iterator it = m_quantifiers.begin(), + end = m_quantifiers.end(); + for (; it != end; ++it) { + dealloc(it->m_value); + } + m_has_quantifiers = false; + m_quantifiers.reset(); + } rule_set * mk_extract_quantifiers::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { - m_quantifiers.reset(); - rule_set* rules = alloc(rule_set, m_ctx); + reset(); rule_set::iterator it = source.begin(), end = source.end(); + for (; !m_has_quantifiers && it != end; ++it) { + m_has_quantifiers = (*it)->has_quantifiers(); + } + if (!m_has_quantifiers) { + return 0; + } + + rule_set* rules = alloc(rule_set, m_ctx); + it = source.begin(); for (; it != end; ++it) { extract(**it, *rules); } - if (m_quantifiers.empty()) { - dealloc(rules); - rules = 0; - } - return rules; + + return rules; } }; diff --git a/src/muz_qe/dl_mk_extract_quantifiers.h b/src/muz_qe/dl_mk_extract_quantifiers.h index 5da5d59d7..b32dbc32d 100644 --- a/src/muz_qe/dl_mk_extract_quantifiers.h +++ b/src/muz_qe/dl_mk_extract_quantifiers.h @@ -7,7 +7,8 @@ Module Name: Abstract: - Remove universal quantifiers over interpreted predicates in the body. + Replace universal quantifiers over interpreted predicates in the body + by instantiations mined using bounded model checking search. Author: @@ -22,6 +23,7 @@ Revision History: #include"dl_context.h" #include"dl_rule_set.h" #include"dl_rule_transformer.h" +#include"obj_pair_hashtable.h" namespace datalog { @@ -29,15 +31,41 @@ namespace datalog { \brief Extract universal quantifiers from rules. */ class mk_extract_quantifiers : public rule_transformer::plugin { - context& m_ctx; - ast_manager& m; - rule_manager& rm; - ptr_vector m_refs; + + class collect_insts; + + context& m_ctx; + ast_manager& m; + rule_manager& rm; + func_decl_ref m_query_pred; + bool m_has_quantifiers; obj_map m_quantifiers; + void reset(); + void extract(rule& r, rule_set& new_rules); - app_ref ensure_app(expr* e); + void rule2formula( + rule& r, + obj_map const& insts, + expr_ref& fml, + app_ref_vector& sub); + + + void add_binding( + app_ref_vector const& var_inst, + expr_ref_vector& bindings, + quantifier* q, + expr_ref_vector const& instantiation, + obj_map& insts); + + void apply_binding( + app_ref_vector const& var_inst, + expr_ref_vector& bindings, + quantifier* q, + expr_ref_vector const& instantiation, + obj_map& insts); + public: /** @@ -46,15 +74,23 @@ namespace datalog { mk_extract_quantifiers(context & ctx); virtual ~mk_extract_quantifiers(); + + void set_query(func_decl* q); rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + bool has_quantifiers() { return m_has_quantifiers; } + obj_map& quantifiers() { return m_quantifiers; } - bool has_quantifiers() const { return !m_quantifiers.empty(); } - void ensure_predicate(expr* e, unsigned& max_var, app_ref_vector& tail); + bool find_instantiations_proof_based( + expr* fml, + app_ref_vector const& var_inst, + obj_map& insts, + expr_ref_vector& bindings); + }; }; diff --git a/src/muz_qe/dl_mk_extract_quantifiers2.cpp b/src/muz_qe/dl_mk_extract_quantifiers2.cpp deleted file mode 100644 index 5f320fffe..000000000 --- a/src/muz_qe/dl_mk_extract_quantifiers2.cpp +++ /dev/null @@ -1,107 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - dl_mk_extract_quantifiers2.cpp - -Abstract: - - Remove universal quantifiers over interpreted predicates in the body. - -Author: - - Nikolaj Bjorner (nbjorner) 2012-11-21 - -Revision History: - ---*/ - -#include"dl_mk_extract_quantifiers2.h" -#include"ast_pp.h" -#include"dl_bmc_engine.h" -#include"smt_quantifier.h" -#include"smt_context.h" - -namespace datalog { - - - mk_extract_quantifiers2::mk_extract_quantifiers2(context & ctx) : - rule_transformer::plugin(101, false), - m_ctx(ctx), - m(ctx.get_manager()), - rm(ctx.get_rule_manager()), - m_query_pred(m) - {} - - mk_extract_quantifiers2::~mk_extract_quantifiers2() { - reset(); - } - - void mk_extract_quantifiers2::set_query(func_decl* q) { - m_query_pred = q; - } - - - /* - * - * - */ - void mk_extract_quantifiers2::extract(rule& r, rule_set& new_rules) { - unsigned utsz = r.get_uninterpreted_tail_size(); - unsigned tsz = r.get_tail_size(); - expr_ref_vector conjs(m); - quantifier_ref_vector qs(m); - for (unsigned i = utsz; i < tsz; ++i) { - conjs.push_back(r.get_tail(i)); - } - 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); - } - } - if (qs.empty()) { - new_rules.add_rule(&r); - } - else { - m_quantifiers.insert(&r, new quantifier_ref_vector(qs)); - // TODO - } - } - - - void mk_extract_quantifiers2::reset() { - obj_map::iterator it = m_quantifiers.begin(), - end = m_quantifiers.end(); - for (; it != end; ++it) { - dealloc(it->m_value); - } - m_has_quantifiers = false; - m_quantifiers.reset(); - } - - rule_set * mk_extract_quantifiers2::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { - reset(); - rule_set::iterator it = source.begin(), end = source.end(); - for (; !m_has_quantifiers && it != end; ++it) { - m_has_quantifiers = (*it)->has_quantifiers(); - } - if (!m_has_quantifiers) { - return 0; - } - - rule_set* rules = alloc(rule_set, m_ctx); - it = source.begin(); - for (; it != end; ++it) { - extract(**it, *rules); - } - - return rules; - } - -}; - - diff --git a/src/muz_qe/dl_mk_extract_quantifiers2.h b/src/muz_qe/dl_mk_extract_quantifiers2.h deleted file mode 100644 index 320f94c95..000000000 --- a/src/muz_qe/dl_mk_extract_quantifiers2.h +++ /dev/null @@ -1,66 +0,0 @@ -/*++ -Copyright (c) 2012 Microsoft Corporation - -Module Name: - - dl_mk_extract_quantifiers2.h - -Abstract: - - Replace universal quantifiers over interpreted predicates in the body - by instantiations mined using bounded model checking search. - -Author: - - Nikolaj Bjorner (nbjorner) 2012-11-21 - -Revision History: - ---*/ -#ifndef _DL_MK_EXTRACT_QUANTIFIERS2_H_ -#define _DL_MK_EXTRACT_QUANTIFIERS2_H_ - -#include"dl_context.h" -#include"dl_rule_set.h" -#include"dl_rule_transformer.h" -#include"obj_pair_hashtable.h" - -namespace datalog { - - /** - \brief Extract universal quantifiers from rules. - */ - class mk_extract_quantifiers2 : public rule_transformer::plugin { - context& m_ctx; - ast_manager& m; - rule_manager& rm; - func_decl_ref m_query_pred; - bool m_has_quantifiers; - obj_map m_quantifiers; - - void reset(); - - void extract(rule& r, rule_set& new_rules); - - public: - /** - \brief Create rule transformer that extracts universal quantifiers (over recursive predicates). - */ - mk_extract_quantifiers2(context & ctx); - - virtual ~mk_extract_quantifiers2(); - - void set_query(func_decl* q); - - rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); - - bool has_quantifiers() { return m_has_quantifiers; } - - obj_map& quantifiers() { return m_quantifiers; } - - }; - -}; - -#endif /* _DL_MK_EXTRACT_QUANTIFIERS2_H_ */ - diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index ba975c8c1..54a40f8b8 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -25,7 +25,7 @@ Revision History: #include "dl_mk_rule_inliner.h" #include "dl_rule.h" #include "dl_rule_transformer.h" -#include "dl_mk_extract_quantifiers2.h" +#include "dl_mk_extract_quantifiers.h" #include "smt2parser.h" #include "pdr_context.h" #include "pdr_dl_interface.h" @@ -146,7 +146,7 @@ lbool dl_interface::query(expr * query) { } } // remove universal quantifiers from body. - datalog::mk_extract_quantifiers2* extract_quantifiers = alloc(datalog::mk_extract_quantifiers2, m_ctx); + datalog::mk_extract_quantifiers* extract_quantifiers = alloc(datalog::mk_extract_quantifiers, m_ctx); datalog::rule_transformer extract_q_tr(m_ctx); extract_q_tr.register_plugin(extract_quantifiers); m_ctx.transform_rules(extract_q_tr, mc, pc); @@ -177,8 +177,9 @@ lbool dl_interface::query(expr * query) { while (true) { result = m_context->solve(); if (result == l_true && extract_quantifiers->has_quantifiers()) { - if (quantifier_mc.check()) { - return l_true; + result = quantifier_mc.check(); + if (result != l_false) { + return result; } // else continue } diff --git a/src/muz_qe/pdr_quantifiers.cpp b/src/muz_qe/pdr_quantifiers.cpp index 9233f6314..23c204801 100644 --- a/src/muz_qe/pdr_quantifiers.cpp +++ b/src/muz_qe/pdr_quantifiers.cpp @@ -154,13 +154,10 @@ namespace pdr { // As & not Body_i is satisfiable // then instantiate with model for parameters to Body_i - bool quantifier_model_checker::find_instantiations(quantifier_ref_vector const& qs, unsigned level) { - return - find_instantiations_proof_based(qs, level); // || - // find_instantiations_qe_based(qs, level); + void quantifier_model_checker::find_instantiations(quantifier_ref_vector const& qs, unsigned level) { + find_instantiations_proof_based(qs, level); } - class collect_insts { ast_manager& m; ptr_vector m_binding; @@ -207,7 +204,7 @@ namespace pdr { }; - bool quantifier_model_checker::find_instantiations_proof_based(quantifier_ref_vector const& qs, unsigned level) { + void quantifier_model_checker::find_instantiations_proof_based(quantifier_ref_vector const& qs, unsigned level) { bool found_instance = false; datalog::scoped_fine_proof _scp(m); @@ -233,10 +230,13 @@ namespace pdr { TRACE("pdr", tout << result << "\n";); - if (result != l_false) { - return false; + if (m_rules_model_check != l_false) { + m_rules_model_check = result; + } + + if (result != l_false) { + return; } - m_rules_model_check = false; map qid_map; quantifier* q; @@ -272,7 +272,12 @@ namespace pdr { add_binding(q, new_binding); found_instance = true; } - return found_instance; + if (found_instance) { + m_rules_model_check = l_false; + } + else if (m_rules_model_check != l_false) { + m_rules_model_check = l_undef; + } } @@ -445,7 +450,7 @@ namespace pdr { qe_lite qe(m); r.get_vars(vars); -#if 1 + if (qis) { quantifier_ref_vector const& qi = *qis; for (unsigned i = 0; i < qi.size(); ++i) { @@ -471,7 +476,7 @@ namespace pdr { body.push_back(m.update_quantifier(q, fml)); } } -#endif + a = r.get_head(); for (unsigned i = 0; i < a->get_num_args(); ++i) { v = m.mk_var(vars.size()+i, m.get_sort(a->get_arg(i))); @@ -584,17 +589,17 @@ namespace pdr { find_instantiations(*qis, level); } - bool quantifier_model_checker::model_check(model_node& root) { + lbool quantifier_model_checker::model_check(model_node& root) { m_instantiations.reset(); m_instantiated_rules.reset(); - m_rules_model_check = true; + m_rules_model_check = l_true; ptr_vector nodes; get_nodes(root, nodes); for (unsigned i = nodes.size(); i > 0; ) { --i; model_check_node(*nodes[i]); } - if (!m_rules_model_check) { + if (m_rules_model_check == l_false) { weaken_under_approximation(); } return m_rules_model_check; @@ -644,12 +649,12 @@ namespace pdr { TRACE("pdr", m_rules.display(tout);); } - bool quantifier_model_checker::check() { - if (model_check(m_ctx.get_root())) { - return true; + lbool quantifier_model_checker::check() { + lbool result = model_check(m_ctx.get_root()); + if (result == l_false) { + refine(); } - refine(); - return false; + return result; } }; diff --git a/src/muz_qe/pdr_quantifiers.h b/src/muz_qe/pdr_quantifiers.h index 2a7dcaf2c..941fab3d9 100644 --- a/src/muz_qe/pdr_quantifiers.h +++ b/src/muz_qe/pdr_quantifiers.h @@ -21,6 +21,7 @@ Revision History: #define _PDR_QUANTIFIERS_H_ #include "ast.h" +#include "lbool.h" #include "dl_rule.h" #include "obj_pair_hashtable.h" @@ -46,7 +47,7 @@ namespace pdr { pred_transformer* m_current_pt; datalog::rule const* m_current_rule; model_node* m_current_node; - bool m_rules_model_check; + lbool m_rules_model_check; app_ref_vector m_instantiations; ptr_vector m_instantiated_rules; @@ -54,13 +55,9 @@ namespace pdr { void weaken_under_approximation(); - bool find_instantiations(quantifier_ref_vector const& qs, unsigned level); + void find_instantiations(quantifier_ref_vector const& qs, unsigned level); - bool find_instantiations_model_based(quantifier_ref_vector const& qs, unsigned level); - - bool find_instantiations_proof_based(quantifier_ref_vector const& qs, unsigned level); - - bool find_instantiations_qe_based(quantifier_ref_vector const& qs, unsigned level); + void find_instantiations_proof_based(quantifier_ref_vector const& qs, unsigned level); void add_binding(quantifier* q, expr_ref_vector& binding); @@ -80,7 +77,7 @@ namespace pdr { 'false' and a set of instantiations that contradict the current model. */ - bool model_check(model_node& root); + lbool model_check(model_node& root); void add_over_approximations(quantifier_ref_vector& qis, model_node& n); @@ -113,7 +110,7 @@ namespace pdr { ~quantifier_model_checker(); - bool check(); + lbool check(); }; }; diff --git a/src/muz_qe/proof_utils.cpp b/src/muz_qe/proof_utils.cpp index 038b08c5c..e699ee356 100644 --- a/src/muz_qe/proof_utils.cpp +++ b/src/muz_qe/proof_utils.cpp @@ -342,7 +342,7 @@ public: } app* cl = to_app(clause); for (unsigned i = 0; i < cl->get_num_args(); ++i) { - if (cl->get_argi(i) == fml) { + if (cl->get_arg(i) == fml) { return true; } }