From 93ad91d2f97f8c2077cb1fb2b2cfa15b5a57b005 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 25 Nov 2012 12:08:49 -0800 Subject: [PATCH] preparing handling of arrays/quantifiers, fix cover-related bugs reported by Arie Signed-off-by: Nikolaj Bjorner --- src/ast/array_decl_plugin.h | 14 + src/ast/dl_decl_plugin.cpp | 3 +- src/ast/dl_decl_plugin.h | 2 - src/model/model_evaluator.cpp | 2 +- src/muz_qe/dl_context.cpp | 2 + src/muz_qe/dl_mk_array_blast.cpp | 139 +++ src/muz_qe/dl_mk_array_blast.h | 61 + src/muz_qe/dl_mk_extract_quantifiers.cpp | 28 +- src/muz_qe/dl_util.h | 6 + src/muz_qe/equiv_proof_converter.h | 58 + src/muz_qe/pdr_context.cpp | 14 +- src/muz_qe/pdr_context.h | 1 + src/muz_qe/pdr_dl_interface.cpp | 18 +- src/muz_qe/pdr_quantifiers.cpp | 94 +- src/muz_qe/pdr_util.cpp | 1381 ++++++++++++---------- src/muz_qe/pdr_util.h | 16 +- 16 files changed, 1134 insertions(+), 705 deletions(-) create mode 100644 src/muz_qe/dl_mk_array_blast.cpp create mode 100644 src/muz_qe/dl_mk_array_blast.h create mode 100644 src/muz_qe/equiv_proof_converter.h diff --git a/src/ast/array_decl_plugin.h b/src/ast/array_decl_plugin.h index bd1e123e3..68c473560 100644 --- a/src/ast/array_decl_plugin.h +++ b/src/ast/array_decl_plugin.h @@ -144,7 +144,21 @@ public: bool is_map(expr* n) const { return is_app_of(n, m_fid, OP_ARRAY_MAP); } bool is_as_array(expr * n) const { return is_app_of(n, m_fid, OP_AS_ARRAY); } bool is_as_array_tree(expr * n); + bool is_select(func_decl* f) const { return is_decl_of(f, m_fid, OP_SELECT); } + bool is_store(func_decl* f) const { return is_decl_of(f, m_fid, OP_STORE); } + bool is_const(func_decl* f) const { return is_decl_of(f, m_fid, OP_CONST_ARRAY); } + bool is_map(func_decl* f) const { return is_decl_of(f, m_fid, OP_ARRAY_MAP); } + bool is_as_array(func_decl* f) const { return is_decl_of(f, m_fid, OP_AS_ARRAY); } func_decl * get_as_array_func_decl(app * n) const { SASSERT(is_as_array(n)); return to_func_decl(n->get_decl()->get_parameter(0).get_ast()); } + + app * mk_store(unsigned num_args, expr * const * args) { + return m_manager.mk_app(m_fid, OP_STORE, 0, 0, num_args, args); + } + + app * mk_select(unsigned num_args, expr * const * args) { + return m_manager.mk_app(m_fid, OP_SELECT, 0, 0, num_args, args); + } + app * mk_map(func_decl * f, unsigned num_args, expr * const * args) { parameter p(f); return m_manager.mk_app(m_fid, OP_ARRAY_MAP, 1, &p, num_args, args); diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index 76f34f316..5b73f944a 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -44,8 +44,7 @@ namespace datalog { m_num_sym("N"), m_lt_sym("<"), m_le_sym("<="), - m_rule_sym("R"), - m_hyper_resolve_sym("hyper-res") + m_rule_sym("R") { } diff --git a/src/ast/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h index 6e824b639..32e3c6da9 100644 --- a/src/ast/dl_decl_plugin.h +++ b/src/ast/dl_decl_plugin.h @@ -69,7 +69,6 @@ namespace datalog { symbol m_lt_sym; symbol m_le_sym; symbol m_rule_sym; - symbol m_hyper_resolve_sym; bool check_bounds(char const* msg, unsigned low, unsigned up, unsigned val) const; bool check_domain(unsigned low, unsigned up, unsigned val) const; @@ -93,7 +92,6 @@ namespace datalog { func_decl * mk_compare(decl_kind k, symbol const& sym, sort*const* domain); func_decl * mk_clone(sort* r); func_decl * mk_rule(unsigned arity); - func_decl * mk_hyper_res(unsigned num_params, parameter const* params, unsigned arity, sort *const* domain); sort * mk_finite_sort(unsigned num_params, parameter const* params); sort * mk_relation_sort(unsigned num_params, parameter const* params); diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index bccade304..258590121 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -147,7 +147,7 @@ struct evaluator_cfg : public default_rewriter_cfg { return m_a_rw.mk_app_core(f, num, args, result); if (fid == m_bv_rw.get_fid()) return m_bv_rw.mk_app_core(f, num, args, result); - if (fid == m_ar_rw.get_fid()) + if (fid == m_ar_rw.get_fid()) return m_ar_rw.mk_app_core(f, num, args, result); if (fid == m_dt_rw.get_fid()) return m_dt_rw.mk_app_core(f, num, args, result); diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 91e396671..12c12c75a 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -54,6 +54,7 @@ Revision History: #include"expr_functors.h" #include"dl_mk_partial_equiv.h" #include"dl_mk_bit_blast.h" +#include"dl_mk_array_blast.h" #include"datatype_decl_plugin.h" #include"expr_abstract.h" @@ -944,6 +945,7 @@ namespace datalog { transf.register_plugin(alloc(datalog::mk_subsumption_checker, *this, 34880)); transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000)); + transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000)); transform_rules(transf, mc, pc); } diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp new file mode 100644 index 000000000..39223264c --- /dev/null +++ b/src/muz_qe/dl_mk_array_blast.cpp @@ -0,0 +1,139 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + dl_mk_array_blast.cpp + +Abstract: + + Remove array variables from rules. + +Author: + + Nikolaj Bjorner (nbjorner) 2012-11-23 + +Revision History: + +--*/ + +#include "dl_mk_array_blast.h" +#include "expr_replacer.h" + +namespace datalog { + + + mk_array_blast::mk_array_blast(context & ctx, unsigned priority) : + rule_transformer::plugin(priority, false), + m_ctx(ctx), + m(ctx.get_manager()), + a(m), + rm(ctx.get_rule_manager()), + m_rewriter(m, m_params){ + m_params.set_bool(":expand-select-store",true); + m_rewriter.updt_params(m_params); + } + + mk_array_blast::~mk_array_blast() { + } + + bool mk_array_blast::is_store_def(expr* e, expr*& x, expr*& y) { + if (m.is_iff(e, x, y) || m.is_eq(e, x, y)) { + if (!a.is_store(y)) { + std::swap(x,y); + } + if (is_var(x) && a.is_store(y)) { + return true; + } + } + return false; + } + + bool mk_array_blast::blast(rule& r, rule_set& rules) { + unsigned utsz = r.get_uninterpreted_tail_size(); + unsigned tsz = r.get_tail_size(); + expr_ref_vector conjs(m), new_conjs(m); + for (unsigned i = 0; i < utsz; ++i) { + new_conjs.push_back(r.get_tail(i)); + } + for (unsigned i = utsz; i < tsz; ++i) { + conjs.push_back(r.get_tail(i)); + } + flatten_and(conjs); + expr_substitution sub(m); + uint_set lhs_vars, rhs_vars; + for (unsigned i = 0; i < conjs.size(); ++i) { + expr* x, *y; + if (is_store_def(conjs[i].get(), x, y)) { + // enforce topological order consistency: + uint_set lhs; + collect_vars(m, x, lhs_vars); + collect_vars(m, y, rhs_vars); + lhs = lhs_vars; + lhs &= rhs_vars; + if (!lhs.empty()) { + new_conjs.push_back(conjs[i].get()); + } + else { + sub.insert(x, y); + } + } + else { + new_conjs.push_back(conjs[i].get()); + } + } + if (sub.empty()) { + rules.add_rule(&r); + return false; + } + + rule_ref_vector new_rules(rm); + expr_ref fml1(m), fml2(m), body(m), head(m); + r.to_formula(fml1); + body = m.mk_and(new_conjs.size(), new_conjs.c_ptr()); + head = r.get_head(); + scoped_ptr replace = mk_default_expr_replacer(m); + replace->set_substitution(&sub); + (*replace)(body); + m_rewriter(body); + (*replace)(head); + m_rewriter(head); + fml2 = m.mk_implies(body, head); + rm.mk_rule(fml2, new_rules, r.name()); + SASSERT(new_rules.size() == 1); + + rules.add_rule(new_rules[0].get()); + if (m_pc) { + new_rules[0]->to_formula(fml2); + m_pc->insert(fml1, fml2); + } + return true; + } + + rule_set * mk_array_blast::operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc) { + ref epc; + if (pc) { + epc = alloc(equiv_proof_converter, m); + } + m_pc = epc.get(); + + rule_set* rules = alloc(rule_set, m_ctx); + rule_set::iterator it = source.begin(), end = source.end(); + bool change = false; + for (; it != end; ++it) { + change = blast(**it, *rules) || change; + } + if (!change) { + dealloc(rules); + rules = 0; + } + if (pc) { + pc = concat(pc.get(), epc.get()); + } + return rules; + + } + +}; + + diff --git a/src/muz_qe/dl_mk_array_blast.h b/src/muz_qe/dl_mk_array_blast.h new file mode 100644 index 000000000..858b9c778 --- /dev/null +++ b/src/muz_qe/dl_mk_array_blast.h @@ -0,0 +1,61 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + dl_mk_array_blast.h + +Abstract: + + Remove array variables from rules. + +Author: + + Nikolaj Bjorner (nbjorner) 2012-11-23 + +Revision History: + +--*/ +#ifndef _DL_MK_ARRAY_BLAST_H_ +#define _DL_MK_ARRAY_BLAST_H_ + +#include"dl_context.h" +#include"dl_rule_set.h" +#include"dl_rule_transformer.h" +#include "equiv_proof_converter.h" +#include "array_decl_plugin.h" + +namespace datalog { + + /** + \brief Blast occurrences of arrays in rules + */ + class mk_array_blast : public rule_transformer::plugin { + context& m_ctx; + ast_manager& m; + array_util a; + rule_manager& rm; + params_ref m_params; + th_rewriter m_rewriter; + equiv_proof_converter* m_pc; + + bool blast(rule& r, rule_set& new_rules); + + bool is_store_def(expr* e, expr*& x, expr*& y); + + public: + /** + \brief Create rule transformer that extracts universal quantifiers (over recursive predicates). + */ + mk_array_blast(context & ctx, unsigned priority); + + virtual ~mk_array_blast(); + + rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); + + }; + +}; + +#endif /* _DL_MK_ARRAY_BLAST_H_ */ + diff --git a/src/muz_qe/dl_mk_extract_quantifiers.cpp b/src/muz_qe/dl_mk_extract_quantifiers.cpp index 614e9dbc8..f6755bb4f 100644 --- a/src/muz_qe/dl_mk_extract_quantifiers.cpp +++ b/src/muz_qe/dl_mk_extract_quantifiers.cpp @@ -40,29 +40,32 @@ namespace datalog { void mk_extract_quantifiers::extract(rule& r, rule_set& new_rules) { - app_ref_vector tail(m); - svector neg_tail; + expr_ref_vector tail(m); quantifier_ref_vector quantifiers(m); unsigned utsz = r.get_uninterpreted_tail_size(); unsigned tsz = r.get_tail_size(); for (unsigned i = 0; i < utsz; ++i) { tail.push_back(r.get_tail(i)); - neg_tail.push_back(r.is_neg_tail(i)); + if (r.is_neg_tail(i)) { + new_rules.add_rule(&r); + return; + } } for (unsigned i = utsz; i < tsz; ++i) { - SASSERT(!r.is_neg_tail(i)); app* t = r.get_tail(i); expr_ref_vector conjs(m); datalog::flatten_and(t, conjs); + quantifier_ref qe(m); + quantifier* q = 0; for (unsigned j = 0; j < conjs.size(); ++j) { expr* e = conjs[j].get(); - quantifier* q = 0; if (rule_manager::is_forall(m, e, q)) { quantifiers.push_back(q); + qe = m.mk_exists(q->get_num_decls(), q->get_decl_sorts(), q->get_decl_names(), q->get_expr()); + tail.push_back(qe); } else { - tail.push_back(is_app(e)?to_app(e):m.mk_eq(e, m.mk_true())); - neg_tail.push_back(false); + tail.push_back(e); } } } @@ -70,11 +73,16 @@ namespace datalog { new_rules.add_rule(&r); } else { - rule* new_rule = rm.mk(r.get_head(), tail.size(), tail.c_ptr(), neg_tail.c_ptr(), r.name(), false); - new_rules.add_rule(new_rule); + expr_ref fml(m); + rule_ref_vector rules(rm); + fml = m.mk_implies(m.mk_and(tail.size(), tail.c_ptr()), r.get_head()); + rm.mk_rule(fml, rules, r.name()); quantifier_ref_vector* qs = alloc(quantifier_ref_vector, quantifiers); - m_quantifiers.insert(new_rule, qs); m_refs.push_back(qs); + for (unsigned i = 0; i < rules.size(); ++i) { + m_quantifiers.insert(rules[i].get(), qs); + new_rules.add_rule(rules[i].get()); + } } } diff --git a/src/muz_qe/dl_util.h b/src/muz_qe/dl_util.h index 1685bec9c..f314b691d 100644 --- a/src/muz_qe/dl_util.h +++ b/src/muz_qe/dl_util.h @@ -196,6 +196,12 @@ namespace datalog { scoped_no_proof(ast_manager& m): scoped_proof_mode(m, PGM_DISABLED) {} }; + class scoped_restore_proof : public scoped_proof_mode { + public: + scoped_restore_proof(ast_manager& m): scoped_proof_mode(m, m.proof_mode()) {} + }; + + class variable_intersection diff --git a/src/muz_qe/equiv_proof_converter.h b/src/muz_qe/equiv_proof_converter.h new file mode 100644 index 000000000..94d6f4e04 --- /dev/null +++ b/src/muz_qe/equiv_proof_converter.h @@ -0,0 +1,58 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + equiv_proof_converter.h + +Abstract: + + Proof converter that applies equivalence rule to leaves. + + Given a proof P with occurrences of [asserted fml] + replace [asserted fml] by a proof of the form + [mp [asserted fml'] [~ fml fml']] + +Author: + + Nikolaj Bjorner (nbjorner) 2012-11-23 + +Revision History: + +--*/ + +#ifndef _EQUIV_PROOF_CONVERTER_H_ +#define _EQUIV_PROOF_CONVERTER_H_ + +#include "replace_proof_converter.h" + +class equiv_proof_converter : public proof_converter { + ast_manager& m; + replace_proof_converter m_replace; +public: + + equiv_proof_converter(ast_manager& m): m(m), m_replace(m) {} + + virtual ~equiv_proof_converter() {} + + virtual void operator()(ast_manager & m, unsigned num_source, proof * const * source, proof_ref & result) { + m_replace(m, num_source, source, result); + } + + virtual proof_converter * translate(ast_translation & translator) { + return m_replace.translate(translator); + } + + void insert(expr* fml1, expr* fml2) { + proof_ref p1(m), p2(m), p3(m); + p1 = m.mk_asserted(fml1); + p2 = m.mk_rewrite(fml1, fml2); + p3 = m.mk_modus_ponens(p1, p2); + m_replace.insert(p3); + } + + ast_manager& get_manager() { return m; } + +}; + +#endif diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index f056342a2..909a42625 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -35,7 +35,6 @@ Notes: #include "pdr_generalizers.h" #include "datatype_decl_plugin.h" #include "for_each_expr.h" -#include "model_v2_pp.h" #include "dl_rule_set.h" #include "unit_subsumption_tactic.h" #include "model_smt2_pp.h" @@ -146,7 +145,6 @@ namespace pdr { expr_ref vl(m); for (; it != end; ++it) { expr* pred = it->m_key; - TRACE("pdr", tout << mk_pp(pred, m) << "\n";); if (model.eval(to_app(pred)->get_decl(), vl) && m.is_true(vl)) { return *it->m_value; } @@ -362,7 +360,7 @@ namespace pdr { } // replace local constants by bound variables. expr_substitution sub(m); - for (unsigned i = 0; i < m_sig.size(); ++i) { + for (unsigned i = 0; i < sig_size(); ++i) { c = m.mk_const(pm.o2n(sig(i), 0)); v = m.mk_var(i, sig(i)->get_range()); sub.insert(c, v); @@ -397,7 +395,7 @@ namespace pdr { // replace bound variables by local constants. expr_ref result(property, m), v(m), c(m); expr_substitution sub(m); - for (unsigned i = 0; i < m_sig.size(); ++i) { + for (unsigned i = 0; i < sig_size(); ++i) { c = m.mk_const(pm.o2n(sig(i), 0)); v = m.mk_var(i, sig(i)->get_range()); sub.insert(v, c); @@ -602,6 +600,12 @@ namespace pdr { } m_rule2inst.insert(&rule,&var_reprs); m_rule2vars.insert(&rule, aux_vars); + TRACE("pdr", + tout << rule.get_decl()->get_name() << "\n"; + for (unsigned i = 0; i < var_reprs.size(); ++i) { + tout << mk_pp(var_reprs[i].get(), m) << " "; + } + tout << "\n";); } bool pred_transformer::check_filled(app_ref_vector const& v) const { @@ -723,7 +727,7 @@ namespace pdr { pred_transformer& p = pt(); ast_manager& m = p.get_manager(); manager& pm = p.get_pdr_manager(); - TRACE("pdr", model_v2_pp(tout, get_model());); + TRACE("pdr", model_smt2_pp(tout, m, get_model(), 0);); func_decl* f = p.head(); unsigned arity = f->get_arity(); expr_ref_vector args(m); diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h index 4b578a188..c7f53752a 100644 --- a/src/muz_qe/pdr_context.h +++ b/src/muz_qe/pdr_context.h @@ -116,6 +116,7 @@ namespace pdr { ptr_vector const& rules() const { return m_rules; } func_decl* sig(unsigned i) { init_sig(); return m_sig[i].get(); } // signature func_decl* const* sig() { init_sig(); return m_sig.c_ptr(); } + unsigned sig_size() { init_sig(); return m_sig.size(); } expr* transition() const { return m_transition; } expr* initial_state() const { return m_initial_state; } expr* rule2tag(datalog::rule const* r) { return m_rule2tag.find(r); } diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index be31f4724..b047aaae0 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -58,18 +58,18 @@ dl_interface::~dl_interface() { // void dl_interface::check_reset() { datalog::rule_ref_vector const& new_rules = m_ctx.get_rules().get_rules(); - datalog::rule_ref_vector const& old_rules = m_old_rules.get_rules(); - for (unsigned i = 0; i < new_rules.size(); ++i) { - bool found = false; - for (unsigned j = 0; !found && j < old_rules.size(); ++j) { + datalog::rule_ref_vector const& old_rules = m_old_rules.get_rules(); + bool is_subsumed = !old_rules.empty(); + for (unsigned i = 0; is_subsumed && i < new_rules.size(); ++i) { + is_subsumed = false; + for (unsigned j = 0; !is_subsumed && j < old_rules.size(); ++j) { if (m_ctx.check_subsumes(*old_rules[j], *new_rules[i])) { - found = true; + is_subsumed = true; } } - if (!found) { - CTRACE("pdr", (old_rules.size() > 0), new_rules[i]->display(m_ctx, tout << "Fresh rule ");); + if (!is_subsumed) { + TRACE("pdr", new_rules[i]->display(m_ctx, tout << "Fresh rule ");); m_context->reset(); - break; } } m_old_rules.reset(); @@ -160,6 +160,8 @@ lbool dl_interface::query(expr * query) { m_ctx.replace_rules(old_rules); quantifier_model_checker quantifier_mc(*m_context, m, extract_quantifiers->quantifiers(), m_pdr_rules); + + datalog::scoped_restore_proof _sc(m); // update_rules may overwrite the proof mode. m_context->set_proof_converter(pc); m_context->set_model_converter(mc); diff --git a/src/muz_qe/pdr_quantifiers.cpp b/src/muz_qe/pdr_quantifiers.cpp index d52a0bf07..8b5f6fa1e 100644 --- a/src/muz_qe/pdr_quantifiers.cpp +++ b/src/muz_qe/pdr_quantifiers.cpp @@ -24,6 +24,7 @@ Revision History: #include "qe.h" #include "var_subst.h" #include "dl_rule_set.h" +#include "model_smt2_pp.h" namespace pdr { @@ -181,25 +182,21 @@ namespace pdr { bool found_instance = false; TRACE("pdr", tout << mk_pp(m_A,m) << "\n";); - ast_manager mp(PGM_COARSE); - ast_translation tr(m, mp); - ast_translation rev_tr(mp, m); - expr_ref_vector fmls(mp); + datalog::scoped_coarse_proof _scp(m); + + expr_ref_vector fmls(m); front_end_params fparams; fparams.m_proof_mode = PGM_COARSE; // TBD: does not work on integers: fparams.m_mbqi = true; - expr_ref C(m); - fmls.push_back(tr(m_A.get())); - for (unsigned i = 0; i < m_Bs.size(); ++i) { - C = m.update_quantifier(qs[i], m_Bs[i].get()); - fmls.push_back(tr(C.get())); - } + + fmls.push_back(m_A.get()); + fmls.append(m_Bs); TRACE("pdr", tout << "assert\n"; for (unsigned i = 0; i < fmls.size(); ++i) { - tout << mk_pp(fmls[i].get(), mp) << "\n"; + tout << mk_pp(fmls[i].get(), m) << "\n"; }); - smt::kernel solver(mp, fparams); + smt::kernel solver(m, fparams); for (unsigned i = 0; i < fmls.size(); ++i) { solver.assert_expr(fmls[i].get()); } @@ -216,8 +213,8 @@ namespace pdr { } proof* p = solver.get_proof(); - TRACE("pdr", tout << mk_ismt2_pp(p, mp) << "\n";); - collect_insts collector(mp); + TRACE("pdr", tout << mk_ismt2_pp(p, m) << "\n";); + collect_insts collector(m); for_each_expr(collector, p); ptr_vector const& quants = collector.quantifiers(); @@ -225,20 +222,20 @@ namespace pdr { symbol qid = quants[i]->get_qid(); if (!qid_map.find(qid, q)) { TRACE("pdr", tout << "Could not find quantifier " - << mk_pp(quants[i], mp) << "\n";); + << mk_pp(quants[i], m) << "\n";); continue; } expr_ref_vector const& binding = collector.bindings()[i]; - TRACE("pdr", tout << "Instantiating:\n" << mk_pp(quants[i], mp) << "\n"; + TRACE("pdr", tout << "Instantiating:\n" << mk_pp(quants[i], m) << "\n"; for (unsigned j = 0; j < binding.size(); ++j) { - tout << mk_pp(binding[j], mp) << " "; + tout << mk_pp(binding[j], m) << " "; } tout << "\n";); expr_ref_vector new_binding(m); for (unsigned j = 0; j < binding.size(); ++j) { - new_binding.push_back(rev_tr(binding[j])); + new_binding.push_back(binding[j]); } add_binding(q, new_binding); found_instance = true; @@ -258,11 +255,32 @@ namespace pdr { return found_instance; } + /** + Given node: + + - pt - predicate transformer for rule: + P(x) :- Body1(x,y) || Body2(x,z) & (Fa u . Q(u,x,z)). + - rule - P(x) :- Body2(x,z) + + - qis - Fa u . Q(u,x,z) + + - A := node.state(x) && Body2(x,y) + + - Bs := array of Bs of the form: + . Fa u . Q(u, P_x, P_y) - instantiate quantifier to P variables. + . B := inv(Q_0,Q_1,Q_2) + . B := inv(u, P_x, P_y) := B[u/Q_0, P_x/Q_1, P_y/Q_2] + . B := Fa u . inv(u, P_x, P_y) + + + */ + + void quantifier_model_checker::model_check_node(model_node& node) { TRACE("pdr", node.display(tout, 0);); pred_transformer& pt = node.pt(); manager& pm = pt.get_pdr_manager(); - expr_ref A(m), B(m), C(m); + expr_ref A(m), B(m), C(m), v(m); expr_ref_vector As(m); m_Bs.reset(); // @@ -285,8 +303,12 @@ namespace pdr { return; } unsigned level = node.level(); - unsigned previous_level = (level == 0)?0:(level-1); + if (level == 0) { + return; + } + unsigned previous_level = level - 1; + As.push_back(pt.get_propagation_formula(m_ctx.get_pred_transformers(), level)); As.push_back(node.state()); As.push_back(pt.rule2tag(m_current_rule)); @@ -296,28 +318,42 @@ namespace pdr { { datalog::scoped_no_proof _no_proof(m); + quantifier_ref q(m); scoped_ptr rep = mk_default_expr_replacer(m); for (unsigned j = 0; j < qis->size(); ++j) { - quantifier* q = (*qis)[j].get(); + q = (*qis)[j].get(); + app_ref_vector& inst = pt.get_inst(m_current_rule); + ptr_vector& aux_vars = pt.get_aux_vars(*m_current_rule); + TRACE("pdr", + tout << "q:\n" << mk_pp(q, m) << "\n"; + tout << "level: " << level << "\n"; + model_smt2_pp(tout, m, node.get_model(), 0); + m_current_rule->display(m_ctx.get_context(), tout << "rule:\n"); + + ); + + var_subst vs(m, false); + vs(q, inst.size(), (expr*const*)inst.c_ptr(), B); + q = to_quantifier(B); + TRACE("pdr", tout << "q instantiated:\n" << mk_pp(q, m) << "\n";); + app* a = to_app(q->get_expr()); func_decl* f = a->get_decl(); pred_transformer& pt2 = m_ctx.get_pred_transformer(f); B = pt2.get_formulas(previous_level, true); + TRACE("pdr", tout << "B:\n" << mk_pp(B, m) << "\n";); + expr_substitution sub(m); - expr_ref_vector refs(m); for (unsigned i = 0; i < a->get_num_args(); ++i) { - expr* v = m.mk_const(pm.o2n(pt2.sig(i),0)); + v = m.mk_const(pm.o2n(pt2.sig(i),0)); sub.insert(v, a->get_arg(i)); - refs.push_back(v); } rep->set_substitution(&sub); (*rep)(B); - app_ref_vector& inst = pt.get_inst(m_current_rule); - ptr_vector& aux_vars = pt.get_aux_vars(*m_current_rule); - pt.ground_free_vars(B, inst, aux_vars); - var_subst vs(m, false); - vs(B, inst.size(), (expr*const*)inst.c_ptr(), B); + TRACE("pdr", tout << "B substituted:\n" << mk_pp(B, m) << "\n";); + + B = m.update_quantifier(q, B); m_Bs.push_back(B); } } diff --git a/src/muz_qe/pdr_util.cpp b/src/muz_qe/pdr_util.cpp index 512d94956..0840f1d73 100644 --- a/src/muz_qe/pdr_util.cpp +++ b/src/muz_qe/pdr_util.cpp @@ -86,559 +86,599 @@ namespace pdr { return res.str(); } + ///////////////////////// + // select elimination rewriter + // -///////////////////////// -// model_evaluator -// + class select_elim { + ast_manager& m; + array_util a; + model_ref m_model; + public: + select_elim(ast_manager& m, model_ref& md): m(m), a(m), m_model(md) {} + + br_status mk_app_core(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result) { + if (a.is_select(f)) { + expr_ref tmp(m); + tmp = m.mk_app(f, num_args, args); + m_model->eval(tmp, result); + return BR_DONE; + } + else { + return BR_FAILED; + } + } + }; + + struct select_elim_cfg: public default_rewriter_cfg { + select_elim m_r; + bool rewrite_patterns() const { return false; } + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { + return m_r.mk_app_core(f, num, args, result); + } + select_elim_cfg(ast_manager & m, model_ref& md, params_ref const & p):m_r(m, md) {} + }; + + template class rewriter_tpl; + + class select_elim_star : public rewriter_tpl { + select_elim_cfg m_cfg; + public: + select_elim_star(ast_manager & m, model_ref& md, params_ref const & p = params_ref()): + rewriter_tpl(m, false, m_cfg), + m_cfg(m, md, p) {} + }; -void model_evaluator::assign_value(expr* e, expr* val) { - rational r; - if (m.is_true(val)) { - set_true(e); - } - else if (m.is_false(val)) { - set_false(e); - } - else if (m_arith.is_numeral(val, r)) { - set_number(e, r); - } - else if (m.is_value(val)) { - set_value(e, val); - } - else { - IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << "\n";); - TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << "\n";); - set_x(e); - } -} -void model_evaluator::setup_model(model_ref& model) { - m_numbers.reset(); - m_values.reset(); - m_model = model; - rational r; - unsigned sz = model->get_num_constants(); - for (unsigned i = 0; i < sz; i++) { - func_decl * d = model->get_constant(i); - expr* val = model->get_const_interp(d); - expr* e = m.mk_const(d); - m_refs.push_back(e); - assign_value(e, val); - } -} - -void model_evaluator::reset() { - m1.reset(); - m2.reset(); - m_values.reset(); - m_visited.reset(); - m_numbers.reset(); - m_refs.reset(); - m_model = 0; -} - -expr_ref_vector model_evaluator::minimize_model(ptr_vector const & formulas, model_ref& mdl) { - setup_model(mdl); - - TRACE("pdr_verbose", - tout << "formulas:\n"; - for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n"; - ); - - expr_ref_vector model = prune_by_cone_of_influence(formulas); - TRACE("pdr_verbose", - tout << "pruned model:\n"; - for (unsigned i = 0; i < model.size(); ++i) tout << mk_pp(model[i].get(), m) << "\n";); - - reset(); - - DEBUG_CODE( - setup_model(mdl); - VERIFY(check_model(formulas)); - reset();); - - return model; -} - -expr_ref_vector model_evaluator::minimize_literals(ptr_vector const& formulas, model_ref& mdl) { - - TRACE("pdr", - tout << "formulas:\n"; - for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n"; - ); - - expr_ref_vector result(m); - ptr_vector tocollect; + ///////////////////////// + // model_evaluator + // - setup_model(mdl); - collect(formulas, tocollect); - for (unsigned i = 0; i < tocollect.size(); ++i) { - expr* e = tocollect[i]; - SASSERT(m.is_bool(e)); - SASSERT(is_true(e) || is_false(e)); - if (is_true(e)) { - result.push_back(e); + + void model_evaluator::assign_value(expr* e, expr* val) { + rational r; + if (m.is_true(val)) { + set_true(e); + } + else if (m.is_false(val)) { + set_false(e); + } + else if (m_arith.is_numeral(val, r)) { + set_number(e, r); + } + else if (m.is_value(val)) { + set_value(e, val); } else { - result.push_back(m.mk_not(e)); + IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << "\n";); + TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << "\n";); + set_x(e); } } - reset(); - return result; -} -void model_evaluator::process_formula(app* e, ptr_vector& todo, ptr_vector& tocollect) { - SASSERT(m.is_bool(e)); - SASSERT(is_true(e) || is_false(e)); - unsigned v = is_true(e); - unsigned sz = e->get_num_args(); - expr* const* args = e->get_args(); - if (e->get_family_id() == m.get_basic_family_id()) { - switch(e->get_decl_kind()) { - case OP_TRUE: - break; - case OP_FALSE: - break; - case OP_EQ: - case OP_IFF: - if (args[0] == args[1]) { - SASSERT(v); - // no-op - } - else if (!m.is_bool(args[0])) { - tocollect.push_back(e); + void model_evaluator::setup_model(model_ref& model) { + m_numbers.reset(); + m_values.reset(); + m_model = model; + rational r; + unsigned sz = model->get_num_constants(); + for (unsigned i = 0; i < sz; i++) { + func_decl * d = model->get_constant(i); + expr* val = model->get_const_interp(d); + expr* e = m.mk_const(d); + m_refs.push_back(e); + assign_value(e, val); + } + } + + void model_evaluator::reset() { + m1.reset(); + m2.reset(); + m_values.reset(); + m_visited.reset(); + m_numbers.reset(); + m_refs.reset(); + m_model = 0; + } + + expr_ref_vector model_evaluator::minimize_model(ptr_vector const & formulas, model_ref& mdl) { + setup_model(mdl); + + TRACE("pdr_verbose", + tout << "formulas:\n"; + for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n"; + ); + + expr_ref_vector model = prune_by_cone_of_influence(formulas); + TRACE("pdr_verbose", + tout << "pruned model:\n"; + for (unsigned i = 0; i < model.size(); ++i) tout << mk_pp(model[i].get(), m) << "\n";); + + reset(); + + DEBUG_CODE( + setup_model(mdl); + VERIFY(check_model(formulas)); + reset();); + + return model; + } + + expr_ref_vector model_evaluator::minimize_literals(ptr_vector const& formulas, model_ref& mdl) { + + TRACE("pdr", + tout << "formulas:\n"; + for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n"; + ); + + expr_ref_vector result(m); + expr_ref tmp(m); + ptr_vector tocollect; + + setup_model(mdl); + collect(formulas, tocollect); + for (unsigned i = 0; i < tocollect.size(); ++i) { + expr* e = tocollect[i]; + SASSERT(m.is_bool(e)); + SASSERT(is_true(e) || is_false(e)); + if (is_true(e)) { + result.push_back(e); } else { - todo.append(sz, args); + result.push_back(m.mk_not(e)); } - break; - case OP_DISTINCT: - tocollect.push_back(e); - break; - case OP_ITE: - if (args[1] == args[2]) { - tocollect.push_back(args[1]); - } - else if (is_true(args[1]) && is_true(args[2])) { - todo.append(2, args+1); - } - else if (is_false(args[1]) && is_false(args[2])) { - todo.append(2, args+1); - } - else if (is_true(args[0])) { - todo.append(2, args); - } - else { - SASSERT(is_false(args[0])); - todo.push_back(args[0]); - todo.push_back(args[2]); - } - break; - case OP_AND: - if (v) { - todo.append(sz, args); - } - else { - unsigned i = 0; - for (; !is_false(args[i]) && i < sz; ++i); - if (i == sz) { - fatal_error(1); + } + select_elim_star select_elim(m, m_model); + for (unsigned i = 0; i < result.size(); ++i) { + select_elim(result[i].get(), tmp); + result[i] = tmp; + } + reset(); + TRACE("pdr", + tout << "minimized model:\n"; + for (unsigned i = 0; i < result.size(); ++i) tout << mk_pp(result[i].get(), m) << "\n"; + ); + + return result; + } + + void model_evaluator::process_formula(app* e, ptr_vector& todo, ptr_vector& tocollect) { + SASSERT(m.is_bool(e)); + SASSERT(is_true(e) || is_false(e)); + unsigned v = is_true(e); + unsigned sz = e->get_num_args(); + expr* const* args = e->get_args(); + if (e->get_family_id() == m.get_basic_family_id()) { + switch(e->get_decl_kind()) { + case OP_TRUE: + break; + case OP_FALSE: + break; + case OP_EQ: + case OP_IFF: + if (args[0] == args[1]) { + SASSERT(v); + // no-op } - VERIFY(i < sz); - todo.push_back(args[i]); - } - break; - case OP_OR: - if (v) { - unsigned i = 0; - for (; !is_true(args[i]) && i < sz; ++i); - if (i == sz) { - fatal_error(1); - } - VERIFY(i < sz); - todo.push_back(args[i]); - } - else { - todo.append(sz, args); - } - break; - case OP_XOR: - case OP_NOT: - todo.append(sz, args); - break; - case OP_IMPLIES: - if (v) { - if (is_true(args[1])) { - todo.push_back(args[1]); - } - else if (is_false(args[0])) { - todo.push_back(args[0]); + else if (!m.is_bool(args[0])) { + tocollect.push_back(e); } else { - IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); - UNREACHABLE(); + todo.append(sz, args); } + break; + case OP_DISTINCT: + tocollect.push_back(e); + break; + case OP_ITE: + if (args[1] == args[2]) { + tocollect.push_back(args[1]); + } + else if (is_true(args[1]) && is_true(args[2])) { + todo.append(2, args+1); + } + else if (is_false(args[1]) && is_false(args[2])) { + todo.append(2, args+1); + } + else if (is_true(args[0])) { + todo.append(2, args); + } + else { + SASSERT(is_false(args[0])); + todo.push_back(args[0]); + todo.push_back(args[2]); + } + break; + case OP_AND: + if (v) { + todo.append(sz, args); + } + else { + unsigned i = 0; + for (; !is_false(args[i]) && i < sz; ++i); + if (i == sz) { + fatal_error(1); + } + VERIFY(i < sz); + todo.push_back(args[i]); + } + break; + case OP_OR: + if (v) { + unsigned i = 0; + for (; !is_true(args[i]) && i < sz; ++i); + if (i == sz) { + fatal_error(1); + } + VERIFY(i < sz); + todo.push_back(args[i]); + } + else { + todo.append(sz, args); + } + break; + case OP_XOR: + case OP_NOT: + todo.append(sz, args); + break; + case OP_IMPLIES: + if (v) { + if (is_true(args[1])) { + todo.push_back(args[1]); + } + else if (is_false(args[0])) { + todo.push_back(args[0]); + } + else { + IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); + UNREACHABLE(); + } + } + else { + todo.append(sz, args); + } + break; + default: + IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); + UNREACHABLE(); + } + } + else { + tocollect.push_back(e); + } + } + + void model_evaluator::collect(ptr_vector const& formulas, ptr_vector& tocollect) { + ptr_vector todo; + todo.append(formulas); + m_visited.reset(); + + VERIFY(check_model(formulas)); + + while (!todo.empty()) { + app* e = to_app(todo.back()); + todo.pop_back(); + if (!m_visited.is_marked(e)) { + process_formula(e, todo, tocollect); + m_visited.mark(e, true); + } + } + m_visited.reset(); + } + + expr_ref_vector model_evaluator::prune_by_cone_of_influence(ptr_vector const & formulas) { + ptr_vector tocollect; + collect(formulas, tocollect); + m1.reset(); + m2.reset(); + for (unsigned i = 0; i < tocollect.size(); ++i) { + TRACE("pdr_verbose", tout << "collect: " << mk_pp(tocollect[i], m) << "\n";); + for_each_expr(*this, m_visited, tocollect[i]); + } + unsigned sz = m_model->get_num_constants(); + expr_ref e(m), eq(m); + expr_ref_vector model(m); + for (unsigned i = 0; i < sz; i++) { + func_decl * d = m_model->get_constant(i); + expr* val = m_model->get_const_interp(d); + e = m.mk_const(d); + if (m_visited.is_marked(e)) { + eq = m.mk_eq(e, val); + model.push_back(eq); + } + } + m_visited.reset(); + TRACE("pdr", tout << sz << " ==> " << model.size() << "\n";); + return model; + + } + + void model_evaluator::eval_arith(app* e) { + rational r, r2; + +#define ARG1 e->get_arg(0) +#define ARG2 e->get_arg(1) + + unsigned arity = e->get_num_args(); + for (unsigned i = 0; i < arity; ++i) { + expr* arg = e->get_arg(i); + if (is_x(arg)) { + set_x(e); + return; + } + SASSERT(!is_unknown(arg)); + } + switch(e->get_decl_kind()) { + case OP_NUM: + VERIFY(m_arith.is_numeral(e, r)); + set_number(e, r); + break; + case OP_IRRATIONAL_ALGEBRAIC_NUM: + set_x(e); + break; + case OP_LE: + set_bool(e, get_number(ARG1) <= get_number(ARG2)); + break; + case OP_GE: + set_bool(e, get_number(ARG1) >= get_number(ARG2)); + break; + case OP_LT: + set_bool(e, get_number(ARG1) < get_number(ARG2)); + break; + case OP_GT: + set_bool(e, get_number(ARG1) > get_number(ARG2)); + break; + case OP_ADD: + r = rational::zero(); + for (unsigned i = 0; i < arity; ++i) { + r += get_number(e->get_arg(i)); + } + set_number(e, r); + break; + case OP_SUB: + r = get_number(e->get_arg(0)); + for (unsigned i = 1; i < arity; ++i) { + r -= get_number(e->get_arg(i)); + } + set_number(e, r); + break; + case OP_UMINUS: + SASSERT(arity == 1); + set_number(e, get_number(e->get_arg(0))); + break; + case OP_MUL: + r = rational::one(); + for (unsigned i = 0; i < arity; ++i) { + r *= get_number(e->get_arg(i)); + } + set_number(e, r); + break; + case OP_DIV: + SASSERT(arity == 2); + r = get_number(ARG2); + if (r.is_zero()) { + set_x(e); } else { - todo.append(sz, args); + set_number(e, get_number(ARG1) / r); } + break; + case OP_IDIV: + SASSERT(arity == 2); + r = get_number(ARG2); + if (r.is_zero()) { + set_x(e); + } + else { + set_number(e, div(get_number(ARG1), r)); + } + break; + case OP_REM: + // rem(v1,v2) = if v2 >= 0 then mod(v1,v2) else -mod(v1,v2) + SASSERT(arity == 2); + r = get_number(ARG2); + if (r.is_zero()) { + set_x(e); + } + else { + r2 = mod(get_number(ARG1), r); + if (r.is_neg()) r2.neg(); + set_number(e, r2); + } + break; + case OP_MOD: + SASSERT(arity == 2); + r = get_number(ARG2); + if (r.is_zero()) { + set_x(e); + } + else { + set_number(e, mod(get_number(ARG1), r)); + } + break; + case OP_TO_REAL: + SASSERT(arity == 1); + set_number(e, get_number(ARG1)); + break; + case OP_TO_INT: + SASSERT(arity == 1); + set_number(e, floor(get_number(ARG1))); + break; + case OP_IS_INT: + SASSERT(arity == 1); + set_bool(e, get_number(ARG1).is_int()); + break; + case OP_POWER: + set_x(e); break; default: IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); UNREACHABLE(); + break; } } - else { - tocollect.push_back(e); - } -} - -void model_evaluator::collect(ptr_vector const& formulas, ptr_vector& tocollect) { - ptr_vector todo; - todo.append(formulas); - m_visited.reset(); - VERIFY(check_model(formulas)); - - while (!todo.empty()) { - app* e = to_app(todo.back()); - todo.pop_back(); - if (!m_visited.is_marked(e)) { - process_formula(e, todo, tocollect); - m_visited.mark(e, true); - } - } - m_visited.reset(); -} - -expr_ref_vector model_evaluator::prune_by_cone_of_influence(ptr_vector const & formulas) { - ptr_vector tocollect; - collect(formulas, tocollect); - m1.reset(); - m2.reset(); - for (unsigned i = 0; i < tocollect.size(); ++i) { - TRACE("pdr_verbose", tout << "collect: " << mk_pp(tocollect[i], m) << "\n";); - for_each_expr(*this, m_visited, tocollect[i]); - } - unsigned sz = m_model->get_num_constants(); - expr_ref e(m), eq(m); - expr_ref_vector model(m); - for (unsigned i = 0; i < sz; i++) { - func_decl * d = m_model->get_constant(i); - expr* val = m_model->get_const_interp(d); - e = m.mk_const(d); - if (m_visited.is_marked(e)) { - eq = m.mk_eq(e, val); - model.push_back(eq); - } - } - m_visited.reset(); - TRACE("pdr", tout << sz << " ==> " << model.size() << "\n";); - return model; - -} - -void model_evaluator::eval_arith(app* e) { - rational r, r2; - -#define ARG1 e->get_arg(0) -#define ARG2 e->get_arg(1) - - unsigned arity = e->get_num_args(); - for (unsigned i = 0; i < arity; ++i) { - expr* arg = e->get_arg(i); - if (is_x(arg)) { - set_x(e); - return; - } - SASSERT(!is_unknown(arg)); - } - switch(e->get_decl_kind()) { - case OP_NUM: - VERIFY(m_arith.is_numeral(e, r)); - set_number(e, r); - break; - case OP_IRRATIONAL_ALGEBRAIC_NUM: - set_x(e); - break; - case OP_LE: - set_bool(e, get_number(ARG1) <= get_number(ARG2)); - break; - case OP_GE: - set_bool(e, get_number(ARG1) >= get_number(ARG2)); - break; - case OP_LT: - set_bool(e, get_number(ARG1) < get_number(ARG2)); - break; - case OP_GT: - set_bool(e, get_number(ARG1) > get_number(ARG2)); - break; - case OP_ADD: - r = rational::zero(); - for (unsigned i = 0; i < arity; ++i) { - r += get_number(e->get_arg(i)); - } - set_number(e, r); - break; - case OP_SUB: - r = get_number(e->get_arg(0)); - for (unsigned i = 1; i < arity; ++i) { - r -= get_number(e->get_arg(i)); - } - set_number(e, r); - break; - case OP_UMINUS: - SASSERT(arity == 1); - set_number(e, get_number(e->get_arg(0))); - break; - case OP_MUL: - r = rational::one(); - for (unsigned i = 0; i < arity; ++i) { - r *= get_number(e->get_arg(i)); - } - set_number(e, r); - break; - case OP_DIV: - SASSERT(arity == 2); - r = get_number(ARG2); - if (r.is_zero()) { + void model_evaluator::inherit_value(expr* e, expr* v) { + expr* w; + SASSERT(!is_unknown(v)); + SASSERT(m.get_sort(e) == m.get_sort(v)); + if (is_x(v)) { set_x(e); } - else { - set_number(e, get_number(ARG1) / r); + else if (m.is_bool(e)) { + SASSERT(m.is_bool(v)); + if (is_true(v)) set_true(e); + else if (is_false(v)) set_false(e); + else { + TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";); + set_x(e); + } } - break; - case OP_IDIV: - SASSERT(arity == 2); - r = get_number(ARG2); - if (r.is_zero()) { - set_x(e); + else if (m_arith.is_int_real(e)) { + set_number(e, get_number(v)); } - else { - set_number(e, div(get_number(ARG1), r)); + else if (m.is_value(v)) { + set_value(e, v); } - break; - case OP_REM: - // rem(v1,v2) = if v2 >= 0 then mod(v1,v2) else -mod(v1,v2) - SASSERT(arity == 2); - r = get_number(ARG2); - if (r.is_zero()) { - set_x(e); + else if (m_values.find(v, w)) { + set_value(e, w); } - else { - r2 = mod(get_number(ARG1), r); - if (r.is_neg()) r2.neg(); - set_number(e, r2); - } - break; - case OP_MOD: - SASSERT(arity == 2); - r = get_number(ARG2); - if (r.is_zero()) { - set_x(e); - } - else { - set_number(e, mod(get_number(ARG1), r)); - } - break; - case OP_TO_REAL: - SASSERT(arity == 1); - set_number(e, get_number(ARG1)); - break; - case OP_TO_INT: - SASSERT(arity == 1); - set_number(e, floor(get_number(ARG1))); - break; - case OP_IS_INT: - SASSERT(arity == 1); - set_bool(e, get_number(ARG1).is_int()); - break; - case OP_POWER: - set_x(e); - break; - default: - IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); - UNREACHABLE(); - break; - } -} - -void model_evaluator::inherit_value(expr* e, expr* v) { - expr* w; - SASSERT(!is_unknown(v)); - SASSERT(m.get_sort(e) == m.get_sort(v)); - if (is_x(v)) { - set_x(e); - } - else if (m.is_bool(e)) { - SASSERT(m.is_bool(v)); - if (is_true(v)) set_true(e); - else if (is_false(v)) set_false(e); else { TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";); set_x(e); } } - else if (m_arith.is_int_real(e)) { - set_number(e, get_number(v)); - } - else if (m.is_value(v)) { - set_value(e, v); - } - else if (m_values.find(v, w)) { - set_value(e, w); - } - else { - TRACE("pdr", tout << "not inherited:\n" << mk_pp(e, m) << "\n" << mk_pp(v, m) << "\n";); - set_x(e); - } -} - -void model_evaluator::eval_iff(app* e, expr* arg1, expr* arg2) { - if (arg1 == arg2) { - set_true(e); - } - else if (is_x(arg1) || is_x(arg2)) { - set_x(e); - } - else { - bool val = is_true(arg1) == is_true(arg2); - SASSERT(val == (is_false(arg1) == is_false(arg2))); - if (val) { - set_true(e); + + bool model_evaluator::extract_array_func_interp(expr* a, vector& stores, expr_ref else_case) { + SASSERT(m_array.is_array(a)); + + while (m_array.is_store(a)) { + expr_ref_vector store(m); + store.append(to_app(a)->get_num_args()-1, to_app(a)->get_args()+1); + stores.push_back(store); + a = to_app(a)->get_arg(0); } - else { - set_false(e); - } - } -} - -void model_evaluator::eval_basic(app* e) { - expr* arg1, *arg2; - expr *argCond, *argThen, *argElse, *arg; - bool has_x = false; - unsigned arity = e->get_num_args(); - switch(e->get_decl_kind()) { - case OP_AND: - for (unsigned j = 0; j < arity; ++j) { - expr * arg = e->get_arg(j); - if (is_false(arg)) { - set_false(e); - return; + + if (m_array.is_const(a)) { + else_case = to_app(a)->get_arg(0); + return true; + } + + if (m_array.is_as_array(a)) { + func_decl* f = m_array.get_as_array_func_decl(to_app(a)); + func_interp* g = m_model->get_func_interp(f); + unsigned sz = g->num_entries(); + unsigned arity = f->get_arity(); + for (unsigned i = 0; i < sz; ++i) { + expr_ref_vector store(m); + func_entry const* fe = g->get_entry(i); + store.append(arity, fe->get_args()); + store.push_back(fe->get_result()); + for (unsigned j = 0; j < store.size(); ++j) { + if (!is_ground(store[j].get())) { + return false; + } + } + stores.push_back(store); + } + else_case = g->get_else(); + if (!is_ground(else_case)) { + return false; } - else if (is_x(arg)) { - has_x = true; + return true; + } + + return false; + } + + /** + best effort evaluator of extensional array equality. + */ + void model_evaluator::eval_array_eq(app* e, expr* arg1, expr* arg2) { + expr_ref v1(m), v2(m); + m_model->eval(arg1, v1); + m_model->eval(arg2, v2); + if (v1 == v2) { + set_true(e); + return; + } + sort* s = m.get_sort(arg1); + sort* r = get_array_range(s); + if (!r->is_infinite() && !r->is_very_big()) { + TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";); + set_x(e); + return; + } + vector store; + expr_ref else1(m), else2(m); + if (!extract_array_func_interp(v1, store, else1) || + !extract_array_func_interp(v2, store, else2)) { + TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";); + set_x(e); + return; + } + + if (else1 != else2) { + if (m.is_value(else1) && m.is_value(else2)) { + set_bool(e, false); } else { - SASSERT(is_true(arg)); - } - } - if (has_x) { - set_x(e); - } - else { - set_true(e); - } - break; - case OP_OR: - for (unsigned j = 0; j < arity; ++j) { - expr * arg = e->get_arg(j); - if (is_true(arg)) { - set_true(e); - return; - } - else if (is_x(arg)) { - has_x = true; - } - else { - SASSERT(is_false(arg)); - } - } - if (has_x) { - set_x(e); - } - else { - set_false(e); - } - break; - case OP_NOT: - VERIFY(m.is_not(e, arg)); - if (is_true(arg)) { - set_false(e); - } - else if (is_false(arg)) { - set_true(e); - } - else { - SASSERT(is_x(arg)); - set_x(e); - } - break; - case OP_IMPLIES: - VERIFY(m.is_implies(e, arg1, arg2)); - if (is_false(arg1) || is_true(arg2)) { - set_true(e); - } - else if (arg1 == arg2) { - set_true(e); - } - else if (is_true(arg1) && is_false(arg2)) { - set_false(e); - } - else { - SASSERT(is_x(arg1) || is_x(arg2)); - set_x(e); - } - break; - case OP_IFF: - VERIFY(m.is_iff(e, arg1, arg2)); - eval_iff(e, arg1, arg2); - break; - case OP_ITE: - VERIFY(m.is_ite(e, argCond, argThen, argElse)); - if (is_true(argCond)) { - inherit_value(e, argThen); - } - else if (is_false(argCond)) { - inherit_value(e, argElse); - } - else if (argThen == argElse) { - inherit_value(e, argThen); - } - else if (m.is_bool(e)) { - SASSERT(is_x(argCond)); - if (is_x(argThen) || is_x(argElse)) { + TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";); set_x(e); } - else if (is_true(argThen) == is_true(argElse)) { - inherit_value(e, argThen); + return; + } + + expr_ref s1(m), s2(m), w1(m), w2(m); + expr_ref_vector args1(m), args2(m); + args1.push_back(v1); + args2.push_back(v2); + for (unsigned i = 0; i < store.size(); ++i) { + args1.resize(1); + args2.resize(1); + args1.append(store[i].size()-1, store[i].c_ptr()); + args2.append(store[i].size()-1, store[i].c_ptr()); + s1 = m_array.mk_select(args1.size(), args1.c_ptr()); + s2 = m_array.mk_select(args2.size(), args2.c_ptr()); + m_model->eval(s1, w1); + m_model->eval(s2, w2); + if (w1 == w2) { + continue; + } + else if (m.is_value(w1) && m.is_value(w2)) { + set_bool(e, false); + return; } else { + TRACE("pdr", tout << "equality is unknown: " << mk_pp(e, m) << "\n";); set_x(e); + return; } } - else { - set_x(e); - } - break; - case OP_TRUE: - set_true(e); - break; - case OP_FALSE: - set_false(e); - break; - case OP_EQ: - VERIFY(m.is_eq(e, arg1, arg2)); - if (m.is_bool(arg1)) { - eval_iff(e, arg1, arg2); - } - else if (arg1 == arg2) { + set_bool(e, true); + } + + void model_evaluator::eval_eq(app* e, expr* arg1, expr* arg2) { + if (arg1 == arg2) { set_true(e); } + else if (m_array.is_array(arg1)) { + eval_array_eq(e, arg1, arg2); + } else if (is_x(arg1) || is_x(arg2)) { set_x(e); } + else if (m.is_bool(arg1)) { + bool val = is_true(arg1) == is_true(arg2); + SASSERT(val == (is_false(arg1) == is_false(arg2))); + if (val) { + set_true(e); + } + else { + set_false(e); + } + } else if (m_arith.is_int_real(arg1)) { set_bool(e, get_number(arg1) == get_number(arg2)); } @@ -648,164 +688,222 @@ void model_evaluator::eval_basic(app* e) { if (m.is_value(e1) && m.is_value(e2)) { set_bool(e, e1 == e2); } + else if (e1 == e2) { + set_bool(e, true); + } else { TRACE("pdr", tout << "not value equal:\n" << mk_pp(e1, m) << "\n" << mk_pp(e2, m) << "\n";); set_x(e); } } - break; - case OP_DISTINCT: { - vector values; - for (unsigned i = 0; i < arity; ++i) { - expr* arg = e->get_arg(i); - if (is_x(arg)) { + } + + void model_evaluator::eval_basic(app* e) { + expr* arg1, *arg2; + expr *argCond, *argThen, *argElse, *arg; + bool has_x = false; + unsigned arity = e->get_num_args(); + switch(e->get_decl_kind()) { + case OP_AND: + for (unsigned j = 0; j < arity; ++j) { + expr * arg = e->get_arg(j); + if (is_false(arg)) { + set_false(e); + return; + } + else if (is_x(arg)) { + has_x = true; + } + else { + SASSERT(is_true(arg)); + } + } + if (has_x) { set_x(e); - return; } - values.push_back(get_number(arg)); - } - std::sort(values.begin(), values.end()); - for (unsigned i = 0; i + 1 < values.size(); ++i) { - if (values[i] == values[i+1]) { + else { + set_true(e); + } + break; + case OP_OR: + for (unsigned j = 0; j < arity; ++j) { + expr * arg = e->get_arg(j); + if (is_true(arg)) { + set_true(e); + return; + } + else if (is_x(arg)) { + has_x = true; + } + else { + SASSERT(is_false(arg)); + } + } + if (has_x) { + set_x(e); + } + else { set_false(e); - return; } + break; + case OP_NOT: + VERIFY(m.is_not(e, arg)); + if (is_true(arg)) { + set_false(e); + } + else if (is_false(arg)) { + set_true(e); + } + else { + SASSERT(is_x(arg)); + set_x(e); + } + break; + case OP_IMPLIES: + VERIFY(m.is_implies(e, arg1, arg2)); + if (is_false(arg1) || is_true(arg2)) { + set_true(e); + } + else if (arg1 == arg2) { + set_true(e); + } + else if (is_true(arg1) && is_false(arg2)) { + set_false(e); + } + else { + SASSERT(is_x(arg1) || is_x(arg2)); + set_x(e); + } + break; + case OP_IFF: + VERIFY(m.is_iff(e, arg1, arg2)); + eval_eq(e, arg1, arg2); + break; + case OP_ITE: + VERIFY(m.is_ite(e, argCond, argThen, argElse)); + if (is_true(argCond)) { + inherit_value(e, argThen); + } + else if (is_false(argCond)) { + inherit_value(e, argElse); + } + else if (argThen == argElse) { + inherit_value(e, argThen); + } + else if (m.is_bool(e)) { + SASSERT(is_x(argCond)); + if (is_x(argThen) || is_x(argElse)) { + set_x(e); + } + else if (is_true(argThen) == is_true(argElse)) { + inherit_value(e, argThen); + } + else { + set_x(e); + } + } + else { + set_x(e); + } + break; + case OP_TRUE: + set_true(e); + break; + case OP_FALSE: + set_false(e); + break; + case OP_EQ: + VERIFY(m.is_eq(e, arg1, arg2)); + eval_eq(e, arg1, arg2); + break; + case OP_DISTINCT: { + vector values; + for (unsigned i = 0; i < arity; ++i) { + expr* arg = e->get_arg(i); + if (is_x(arg)) { + set_x(e); + return; + } + values.push_back(get_number(arg)); + } + std::sort(values.begin(), values.end()); + for (unsigned i = 0; i + 1 < values.size(); ++i) { + if (values[i] == values[i+1]) { + set_false(e); + return; + } + } + set_true(e); + break; + } + default: + IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); + UNREACHABLE(); } - set_true(e); - break; } - default: - IF_VERBOSE(0, verbose_stream() << "Term not handled " << mk_pp(e, m) << "\n";); - UNREACHABLE(); - } -} - -bool model_evaluator::check_model(ptr_vector const& formulas) { - ptr_vector todo(formulas); - - while (!todo.empty()) { - expr * curr_e = todo.back(); - - if (!is_app(curr_e)) { + + bool model_evaluator::check_model(ptr_vector const& formulas) { + ptr_vector todo(formulas); + + while (!todo.empty()) { + expr * curr_e = todo.back(); + + if (!is_app(curr_e)) { + todo.pop_back(); + continue; + } + app * curr = to_app(curr_e); + + if (!is_unknown(curr)) { + todo.pop_back(); + continue; + } + unsigned arity = curr->get_num_args(); + for (unsigned i = 0; i < arity; ++i) { + if (is_unknown(curr->get_arg(i))) { + todo.push_back(curr->get_arg(i)); + } + } + if (todo.back() != curr) { + continue; + } todo.pop_back(); - continue; + if (curr->get_family_id() == m_arith.get_family_id()) { + eval_arith(curr); + } + else if (curr->get_family_id() == m.get_basic_family_id()) { + eval_basic(curr); + } + else { + expr_ref vl(m); + m_model->eval(curr, vl); + assign_value(curr, vl); + } + + IF_VERBOSE(35,verbose_stream() << "assigned "<get_num_args(); - for (unsigned i = 0; i < arity; ++i) { - if (is_unknown(curr->get_arg(i))) { - todo.push_back(curr->get_arg(i)); + + bool has_x = false; + for (unsigned i = 0; i < formulas.size(); ++i) { + expr * form = formulas[i]; + SASSERT(!is_unknown(form)); + TRACE("pdr_verbose", + tout << "formula is " << (is_true(form) ? "true" : is_false(form) ? "false" : "unknown") << "\n" <get_family_id() == m_arith.get_family_id()) { - eval_arith(curr); - } - else if (curr->get_family_id() == m.get_basic_family_id()) { - eval_basic(curr); - } - else { - expr_ref vl(m); - m_model->eval(curr, vl); - assign_value(curr, vl); - } - - IF_VERBOSE(35,verbose_stream() << "assigned "<get_num_parameters(); - - ptr_vector domain; - domain.push_back(arr_sort); - - //we push params of the array as remaining arguments of the store. The first - //num_params-1 parameters are indices and the last one is the range of the array - for (unsigned i=0; iget_parameter(i).get_ast())); - } - - return m.mk_func_decl(array_fid, OP_STORE, - arr_sort->get_num_parameters(), arr_sort->get_parameters(), - domain.size(), domain.c_ptr(), arr_sort); + return !has_x; } - void get_as_array_value(const model_core & mdl, expr * arr_e, expr_ref& res) { - ast_manager& m = mdl.get_manager(); - array_util pl(m); - SASSERT(pl.is_as_array(arr_e)); - - app * arr = to_app(arr_e); - - unsigned sz = 0; - func_decl_ref f(pl.get_as_array_func_decl(arr), m); - sort * arr_sort = arr->get_decl()->get_range(); - func_interp* g = mdl.get_func_interp(f); - - res = pl.mk_const_array(arr_sort, g->get_else()); - - unsigned arity = f->get_arity(); - - sz = g->num_entries(); - if (sz) { - func_decl_ref store_fn(mk_store(m, arr_sort), m); - ptr_vector store_args; - for (unsigned i = 0; i < sz; ++i) { - const func_entry * fe = g->get_entry(i); - store_args.reset(); - store_args.push_back(res); - store_args.append(arity, fe->get_args()); - store_args.push_back(fe->get_result()); - res = m.mk_app(store_fn, store_args.size(), store_args.c_ptr()); - } - } - } - - void get_value_from_model(const model_core & mdl, func_decl * f, expr_ref& res) { - SASSERT(f->get_arity()==0); - ast_manager& m = mdl.get_manager(); - - res = mdl.get_const_interp(f); - - array_util pl(m); - - if (pl.is_as_array(res)) { - get_as_array_value(mdl, res, res); - } - } - void reduce_disequalities(model& model, unsigned threshold, expr_ref& fml) { ast_manager& m = fml.get_manager(); expr_ref_vector conjs(m); @@ -914,8 +1012,7 @@ bool model_evaluator::check_model(ptr_vector const& formulas) { br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { return m_r.mk_app_core(f, num, args, result); } - ite_hoister_cfg(ast_manager & m, params_ref const & p):m_r(m) {} - + ite_hoister_cfg(ast_manager & m, params_ref const & p):m_r(m) {} }; class ite_hoister_star : public rewriter_tpl { diff --git a/src/muz_qe/pdr_util.h b/src/muz_qe/pdr_util.h index 1d1e86262..bb9f74060 100644 --- a/src/muz_qe/pdr_util.h +++ b/src/muz_qe/pdr_util.h @@ -28,6 +28,7 @@ Revision History: #include "trace.h" #include "vector.h" #include "arith_decl_plugin.h" +#include "array_decl_plugin.h" #include "bv_decl_plugin.h" @@ -56,6 +57,7 @@ namespace pdr { class model_evaluator { ast_manager& m; arith_util m_arith; + array_util m_array; obj_map m_numbers; expr_ref_vector m_refs; obj_map m_values; @@ -78,7 +80,8 @@ namespace pdr { expr_ref_vector prune_by_cone_of_influence(ptr_vector const & formulas); void eval_arith(app* e); void eval_basic(app* e); - void eval_iff(app* e, expr* arg1, expr* arg2); + void eval_eq(app* e, expr* arg1, expr* arg2); + void eval_array_eq(app* e, expr* arg1, expr* arg2); void inherit_value(expr* e, expr* v); inline bool is_unknown(expr* x) { return !m1.is_marked(x) && !m2.is_marked(x); } @@ -99,9 +102,11 @@ namespace pdr { inline void set_value(expr* x, expr* v) { set_v(x); m_refs.push_back(v); m_values.insert(x, v); } bool check_model(ptr_vector const & formulas); + + bool extract_array_func_interp(expr* a, vector& stores, expr_ref else_case); public: - model_evaluator(ast_manager& m) : m(m), m_arith(m), m_refs(m) {} + model_evaluator(ast_manager& m) : m(m), m_arith(m), m_array(m), m_refs(m) {} /** \brief extract equalities from model that suffice to satisfy formula. @@ -118,13 +123,12 @@ namespace pdr { */ expr_ref_vector minimize_literals(ptr_vector const & formulas, model_ref& mdl); - - // for_each_expr visitor. + /** + for_each_expr visitor. + */ void operator()(expr* e) {} }; - void get_value_from_model(const model_core & mdl, func_decl * f, expr_ref& res); - /** \brief replace variables that are used in many disequalities by an equality using the model.