diff --git a/src/muz_qe/dl_mk_slice.h b/src/muz_qe/dl_mk_slice.h index cf6d8ad62..d798430d5 100644 --- a/src/muz_qe/dl_mk_slice.h +++ b/src/muz_qe/dl_mk_slice.h @@ -97,10 +97,14 @@ namespace datalog { the \c goal must be present in the \c rule_set that is being transformed. */ mk_slice(context & ctx); + + virtual ~mk_slice() { } rule_set * operator()(rule_set const & source, model_converter_ref& mc, proof_converter_ref& pc); func_decl* get_predicate(func_decl* p) { func_decl* q = p; m_predicates.find(p, q); return q; } + + obj_map const& get_predicates() { return m_predicates; } }; }; diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp index 922a09448..13c2c0f6d 100644 --- a/src/muz_qe/pdr_context.cpp +++ b/src/muz_qe/pdr_context.cpp @@ -20,6 +20,9 @@ Revision History: Notes: + TODO: + - fix the slicing with covers. + - --*/ @@ -350,7 +353,7 @@ namespace pdr { } } - expr_ref pred_transformer::get_cover_delta(int level) { + expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level) { expr_ref result(m.mk_true(), m), v(m), c(m); if (level == -1) { result = pm.mk_and(m_invariants); @@ -368,6 +371,25 @@ namespace pdr { scoped_ptr rep = mk_default_expr_replacer(m); rep->set_substitution(&sub); (*rep)(result); + + // adjust result according to model converter. + unsigned arity = m_head->get_arity(); + model_ref md = alloc(model, m); + if (arity == 0) { + md->register_decl(m_head, result); + } + else { + func_interp* fi = alloc(func_interp, m, arity); + fi->set_else(result); + md->register_decl(m_head, fi); + } + apply(ctx.get_model_converter(), md, 0); + if (p_orig->get_arity() == 0) { + result = md->get_const_interp(p_orig); + } + else { + result = md->get_func_interp(p_orig)->get_interp(); + } return result; } @@ -1181,10 +1203,10 @@ namespace pdr { } } - expr_ref context::get_cover_delta(int level, func_decl* p) { + expr_ref context::get_cover_delta(int level, func_decl* p_orig, func_decl* p) { pred_transformer* pt = 0; if (m_rels.find(p, pt)) { - return pt->get_cover_delta(level); + return pt->get_cover_delta(p_orig, level); } else { IF_VERBOSE(10, verbose_stream() << "did not find predicate " << p->get_name() << "\n";); diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h index 19b1a6570..0f9af5649 100644 --- a/src/muz_qe/pdr_context.h +++ b/src/muz_qe/pdr_context.h @@ -126,7 +126,7 @@ namespace pdr { qinst* get_quantifiers(datalog::rule const* r) const { qinst* q = 0; m_rule2qinst.find(r, q); return q; } expr* rule2tag(datalog::rule const* r) { return m_rule2tag.find(r); } unsigned get_num_levels() { return m_levels.size(); } - expr_ref get_cover_delta(int level); + expr_ref get_cover_delta(func_decl* p_orig, int level); void add_cover(unsigned level, expr* property); std::ostream& display(std::ostream& strm) const; @@ -385,6 +385,8 @@ namespace pdr { void set_model_converter(model_converter_ref& mc) { m_mc = mc; } + model_converter_ref get_model_converter() { return m_mc; } + void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; } void update_rules(datalog::rule_set& rules); @@ -395,7 +397,7 @@ namespace pdr { unsigned get_num_levels(func_decl* p); - expr_ref get_cover_delta(int level, func_decl* p); + expr_ref get_cover_delta(int level, func_decl* p_orig, func_decl* p); void add_cover(int level, func_decl* pred, expr* property); diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp index 1e7ba27c7..098fd0c56 100644 --- a/src/muz_qe/pdr_dl_interface.cpp +++ b/src/muz_qe/pdr_dl_interface.cpp @@ -39,7 +39,8 @@ dl_interface::dl_interface(datalog::context& ctx) : m_ctx(ctx), m_pdr_rules(ctx), m_old_rules(ctx), - m_context(0) { + m_context(0), + m_refs(ctx.get_manager()) { m_context = alloc(pdr::context, ctx.get_fparams(), ctx.get_params(), ctx.get_manager()); } @@ -78,6 +79,8 @@ lbool dl_interface::query(expr * query) { //we restore the initial state in the datalog context m_ctx.ensure_opened(); m_pdr_rules.reset(); + m_refs.reset(); + m_pred2slice.reset(); m_ctx.get_rmanager().reset_relations(); ast_manager& m = m_ctx.get_manager(); datalog::rule_manager& rule_manager = m_ctx.get_rule_manager(); @@ -116,10 +119,20 @@ lbool dl_interface::query(expr * query) { m_ctx.transform_rules(transformer, mc, pc); query_pred = slice->get_predicate(query_pred.get()); m_ctx.set_output_predicate(query_pred); + + // track sliced predicates. + obj_map const& preds = slice->get_predicates(); + obj_map::iterator it = preds.begin(); + obj_map::iterator end = preds.end(); + for (; it != end; ++it) { + m_pred2slice.insert(it->m_key, it->m_value); + m_refs.push_back(it->m_key); + m_refs.push_back(it->m_value); + } } if (m_ctx.get_params().get_uint(":unfold-rules",0) > 0) { - unsigned num_unfolds = m_ctx.get_params().get_uint(":unfold-rules",0); + unsigned num_unfolds = m_ctx.get_params().get_uint(":unfold-rules", 0); datalog::rule_transformer transformer1(m_ctx), transformer2(m_ctx); if (m_ctx.get_params().get_uint(":coalesce-rules", false)) { transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx)); @@ -160,15 +173,23 @@ lbool dl_interface::query(expr * query) { } } -expr_ref dl_interface::get_cover_delta(int level, func_decl* pred) { - return m_context->get_cover_delta(level, pred); +expr_ref dl_interface::get_cover_delta(int level, func_decl* pred_orig) { + func_decl* pred = pred_orig; + m_pred2slice.find(pred_orig, pred); + SASSERT(pred); + return m_context->get_cover_delta(level, pred_orig, pred); } void dl_interface::add_cover(int level, func_decl* pred, expr* property) { + if (m_ctx.get_params().get_bool(":slice", true)) { + throw default_exception("Covers are incompatible with slicing. Disable slicing before using covers"); + } m_context->add_cover(level, pred, property); } unsigned dl_interface::get_num_levels(func_decl* pred) { + m_pred2slice.find(pred, pred); + SASSERT(pred); return m_context->get_num_levels(pred); } diff --git a/src/muz_qe/pdr_dl_interface.h b/src/muz_qe/pdr_dl_interface.h index 994f4da07..096583a70 100644 --- a/src/muz_qe/pdr_dl_interface.h +++ b/src/muz_qe/pdr_dl_interface.h @@ -37,7 +37,9 @@ namespace pdr { datalog::context& m_ctx; datalog::rule_set m_pdr_rules; datalog::rule_set m_old_rules; - context* m_context; + context* m_context; + obj_map m_pred2slice; + ast_ref_vector m_refs; void check_reset(); diff --git a/src/muz_qe/pdr_manager.cpp b/src/muz_qe/pdr_manager.cpp index 87edbc618..ad53f45db 100644 --- a/src/muz_qe/pdr_manager.cpp +++ b/src/muz_qe/pdr_manager.cpp @@ -58,24 +58,20 @@ namespace pdr { expr_ref inductive_property::fixup_clause(expr* fml) const { expr_ref_vector disjs(m); datalog::flatten_or(fml, disjs); - switch(disjs.size()) { - case 0: return expr_ref(m.mk_false(), m); - case 1: return expr_ref(disjs[0].get(), m); - default: return expr_ref(m.mk_or(disjs.size(), disjs.c_ptr()), m); - } + expr_ref result(m); + bool_rewriter(m).mk_or(disjs.size(), disjs.c_ptr(), result); + return result; } expr_ref inductive_property::fixup_clauses(expr* fml) const { expr_ref_vector conjs(m); + expr_ref result(m); datalog::flatten_and(fml, conjs); for (unsigned i = 0; i < conjs.size(); ++i) { conjs[i] = fixup_clause(conjs[i].get()); } - switch(conjs.size()) { - case 0: return expr_ref(m.mk_true(), m); - case 1: return expr_ref(conjs[0].get(), m); - default: return expr_ref(m.mk_and(conjs.size(), conjs.c_ptr()), m); - } + bool_rewriter(m).mk_and(conjs.size(), conjs.c_ptr(), result); + return result; } std::string inductive_property::to_string() const {