diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 28a456b22..7be434477 100644 --- a/src/muz/base/dl_context.cpp +++ b/src/muz/base/dl_context.cpp @@ -229,6 +229,7 @@ namespace datalog { m_enable_bind_variables(true), m_last_status(OK), m_last_answer(m), + m_last_ground_answer(m), m_engine_type(LAST_ENGINE) { re.set_context(this); updt_params(pa); @@ -306,6 +307,8 @@ namespace datalog { bool context::compress_unbound() const { return m_params->xform_compress_unbound(); } bool context::quantify_arrays() const { return m_params->xform_quantify_arrays(); } bool context::instantiate_quantifiers() const { return m_params->xform_instantiate_quantifiers(); } + bool context::array_blast() const { return m_params->xform_array_blast(); } + bool context::array_blast_full() const { return m_params->xform_array_blast_full(); } void context::register_finite_sort(sort * s, sort_kind k) { @@ -546,10 +549,20 @@ namespace datalog { return m_engine->get_cover_delta(level, pred); } + expr_ref context::get_reachable(func_decl *pred) { + ensure_engine(); + return m_engine->get_reachable(pred); + } void context::add_cover(int level, func_decl* pred, expr* property) { ensure_engine(); m_engine->add_cover(level, pred, property); } + + void context::add_invariant(func_decl* pred, expr *property) + { + ensure_engine(); + m_engine->add_invariant(pred, property); + } void context::check_rules(rule_set& r) { m_rule_properties.set_generate_proof(generate_proof_trace()); @@ -561,6 +574,7 @@ namespace datalog { m_rule_properties.check_nested_free(); m_rule_properties.check_infinite_sorts(); break; + case SPACER_ENGINE: case PDR_ENGINE: m_rule_properties.collect(r); m_rule_properties.check_existential_tail(); @@ -792,6 +806,9 @@ namespace datalog { if (e == symbol("datalog")) { m_engine_type = DATALOG_ENGINE; } + else if (e == symbol("spacer")) { + m_engine_type = SPACER_ENGINE; + } else if (e == symbol("pdr")) { m_engine_type = PDR_ENGINE; } @@ -844,8 +861,10 @@ namespace datalog { m_mc = mk_skip_model_converter(); m_last_status = OK; m_last_answer = 0; + m_last_ground_answer = 0; switch (get_engine()) { case DATALOG_ENGINE: + case SPACER_ENGINE: case PDR_ENGINE: case QPDR_ENGINE: case BMC_ENGINE: @@ -867,6 +886,28 @@ namespace datalog { return m_engine->query(query); } + lbool context::query_from_lvl (expr* query, unsigned lvl) { + m_mc = mk_skip_model_converter(); + m_last_status = OK; + m_last_answer = 0; + m_last_ground_answer = 0; + switch (get_engine()) { + case DATALOG_ENGINE: + case SPACER_ENGINE: + case PDR_ENGINE: + case QPDR_ENGINE: + case BMC_ENGINE: + case QBMC_ENGINE: + case TAB_ENGINE: + case CLP_ENGINE: + flush_add_rules(); + break; + default: + UNREACHABLE(); + } + ensure_engine(); + return m_engine->query_from_lvl (query, lvl); + } model_ref context::get_model() { ensure_engine(); return m_engine->get_model(); @@ -905,6 +946,42 @@ namespace datalog { return m_last_answer.get(); } + expr* context::get_ground_sat_answer () { + if (m_last_ground_answer) { + return m_last_ground_answer; + } + ensure_engine (); + m_last_ground_answer = m_engine->get_ground_sat_answer (); + return m_last_ground_answer; + } + + void context::get_rules_along_trace (rule_ref_vector& rules) { + ensure_engine (); + m_engine->get_rules_along_trace (rules); + } + + void context::get_rules_along_trace_as_formulas (expr_ref_vector& rules, svector& names) { + rule_manager& rm = get_rule_manager (); + rule_ref_vector rv (rm); + get_rules_along_trace (rv); + expr_ref fml (m); + rule_ref_vector::iterator it = rv.begin (), end = rv.end (); + for (; it != end; it++) { + m_rule_manager.to_formula (**it, fml); + rules.push_back (fml); + // The concatenated names are already stored last-first, so do not need to be reversed here + const symbol& rule_name = (*it)->name(); + names.push_back (rule_name); + + TRACE ("dl", + if (rule_name == symbol::null) { + tout << "Encountered unnamed rule: "; + (*it)->display(*this, tout); + tout << "\n"; + }); + } + } + void context::display_certificate(std::ostream& out) { ensure_engine(); m_engine->display_certificate(out); diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 0e1d47609..738c2559e 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -207,6 +207,7 @@ namespace datalog { bool m_enable_bind_variables; execution_result m_last_status; expr_ref m_last_answer; + expr_ref m_last_ground_answer; DL_ENGINE m_engine_type; @@ -277,6 +278,8 @@ namespace datalog { bool xform_bit_blast() const; bool xform_slice() const; bool xform_coi() const; + bool array_blast() const; + bool array_blast_full() const; void register_finite_sort(sort * s, sort_kind k); @@ -407,6 +410,10 @@ namespace datalog { */ unsigned get_num_levels(func_decl* pred); + /** + Retrieve reachable facts of 'pred'. + */ + expr_ref get_reachable(func_decl *pred); /** Retrieve the current cover of 'pred' up to 'level' unfoldings. Return just the delta that is known at 'level'. To @@ -421,6 +428,11 @@ namespace datalog { */ void add_cover(int level, func_decl* pred, expr* property); + /** + Add an invariant of predicate 'pred'. + */ + void add_invariant (func_decl *pred, expr *property); + /** \brief Check rule subsumption. */ @@ -509,6 +521,7 @@ namespace datalog { lbool query(expr* q); + lbool query_from_lvl (expr* q, unsigned lvl); /** \brief retrieve model from inductive invariant that shows query is unsat. @@ -545,6 +558,18 @@ namespace datalog { in the query that are derivable. */ expr* get_answer_as_formula(); + /** + * get bottom-up (from query) sequence of ground predicate instances + * (for e.g. P(0,1,0,0,3)) that together form a ground derivation to query + */ + expr* get_ground_sat_answer (); + + /** + * \brief obtain the sequence of rules along the counterexample trace + */ + void get_rules_along_trace (rule_ref_vector& rules); + + void get_rules_along_trace_as_formulas (expr_ref_vector& rules, svector& names); void collect_statistics(statistics& st) const;