diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 04f5834aa..05e8eeb70 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -2938,7 +2938,7 @@ expr_ref context::mk_unsat_answer() const } -proof_ref context::get_ground_refutation() { +proof_ref context::get_ground_refutation() const { if (m_last_result != l_true) { IF_VERBOSE(0, verbose_stream() << "Sat answer unavailable when result is false\n";); @@ -2948,142 +2948,45 @@ proof_ref context::get_ground_refutation() { ground_sat_answer_op op(*this); return op(*m_query); } -expr_ref context::get_ground_sat_answer() { + +expr_ref context::get_ground_sat_answer() const { if (m_last_result != l_true) { IF_VERBOSE(0, verbose_stream() << "Sat answer unavailable when result is false\n";); return expr_ref(m); } - // treat the following as queues: read from left to right and insert at the right - reach_fact_ref_vector reach_facts; - ptr_vector preds; - ptr_vector pts; - expr_ref_vector cex (m); // pre-order list of ground instances of predicates - expr_ref_vector cex_facts (m); // equalities for the ground cex using signature constants + // convert a ground refutation into a linear counterexample + // only works for linear CHC systems + expr_ref_vector cex(m); + proof_ref pf = get_ground_refutation(); - // temporary - reach_fact *reach_fact; - pred_transformer* pt; - expr_ref cex_fact (m); - datalog::rule const* r; - - // get and discard query rule - reach_fact = m_query->get_last_rf (); - r = &reach_fact->get_rule (); - - // initialize queues - reach_facts.append (reach_fact->get_justifications ()); - if (reach_facts.size() != 1) { - // XXX Escape if an assertion is about to fail - IF_VERBOSE(1, - verbose_stream () << - "Warning: counterexample is trivial or non-existent\n";); - return expr_ref(m.mk_true(), m); + proof_ref_vector premises(m); + expr_ref conclusion(m); + svector> positions; + vector substs; + unsigned count = 0; + while (m.is_hyper_resolve(pf, premises, conclusion, positions, substs)) { + // skip the first fact since it is query!X introduced by the encoding + // and not a user-visible predicate + if (count++ > 0) + cex.push_back(m.get_fact(pf)); + if (premises.size() > 1) { + SASSERT(premises.size() == 2 && "Non linear CHC detected"); + pf = premises.get(1); + } else { + pf.reset(); + break; } - m_query->find_predecessors (*r, preds); - SASSERT (preds.size () == 1); - pts.push_back (&(get_pred_transformer (preds[0]))); - cex_facts.push_back (m.mk_true ()); - // XXX a hack to avoid assertion when query predicate is not nullary - if (preds[0]->get_arity () == 0) - { cex.push_back(m.mk_const(preds[0])); } - - // smt context to obtain local cexes - ref cex_ctx = - mk_smt_solver(m, params_ref::get_empty(), symbol::null); - - bool first = true; - // preorder traversal of the query derivation tree - for (unsigned curr = 0; curr < pts.size (); curr++) { - // pick next pt, fact, and cex_fact - pt = pts.get (curr); - reach_fact = reach_facts[curr]; - - cex_fact = cex_facts.get (curr); - - ptr_vector child_pts; - - // get justifying rule and child facts for the derivation of reach_fact at pt - r = &reach_fact->get_rule (); - const reach_fact_ref_vector &child_reach_facts = - reach_fact->get_justifications (); - // get child pts - preds.reset(); - pt->find_predecessors(*r, preds); - - for (unsigned j = 0; j < preds.size (); j++) { - child_pts.push_back (&(get_pred_transformer (preds[j]))); - } - // update the queues - reach_facts.append (child_reach_facts); - pts.append (child_pts); - - // update cex and cex_facts by making a local sat check: - // check consistency of reach facts of children, rule body, and cex_fact - cex_ctx->push (); - cex_ctx->assert_expr (cex_fact); - unsigned u_tail_sz = r->get_uninterpreted_tail_size (); - SASSERT (child_reach_facts.size () == u_tail_sz); - for (unsigned i = 0; i < u_tail_sz; i++) { - expr_ref ofml (m); - m_pm.formula_n2o(child_reach_facts[i]->get(), ofml, i); - cex_ctx->assert_expr (ofml); - } - cex_ctx->assert_expr(pt->transition()); - cex_ctx->assert_expr(pt->rule2tag(r)); - TRACE("cex", cex_ctx->display(tout);); - lbool res = cex_ctx->check_sat(0, nullptr); - CTRACE("cex", res == l_false, - tout << "Cex fact: " << mk_pp(cex_fact, m) << "\n"; - for (unsigned i = 0; i < u_tail_sz; i++) - tout << "Pre" << i << " " - << mk_pp(child_reach_facts[i]->get(), m) << "\n"; - tout << "Rule: "; - get_datalog_context().get_rule_manager().display_smt2(*r, tout) << "\n"; - ); - VERIFY (res == l_true); - model_ref local_mdl; - cex_ctx->get_model (local_mdl); - cex_ctx->pop (1); - local_mdl->set_model_completion(true); - if (first) { - unsigned sig_size = pt->sig_size(); - expr_ref_vector ground_fact_conjs(m); - expr_ref_vector ground_arg_vals(m); - for (unsigned j = 0; j < sig_size; j++) { - expr_ref sig_arg(m), sig_val(m); - sig_arg = m.mk_const (m_pm.o2n(pt->sig(j), 0)); - sig_val = (*local_mdl)(sig_arg); - ground_arg_vals.push_back(sig_val); - } - cex.push_back(m.mk_app(pt->head(), sig_size, ground_arg_vals.c_ptr())); - first = false; - } - for (unsigned i = 0; i < child_pts.size(); i++) { - pred_transformer& ch_pt = *(child_pts.get(i)); - unsigned sig_size = ch_pt.sig_size(); - expr_ref_vector ground_fact_conjs(m); - expr_ref_vector ground_arg_vals(m); - for (unsigned j = 0; j < sig_size; j++) { - expr_ref sig_arg(m), sig_val(m); - sig_arg = m.mk_const (m_pm.o2o(ch_pt.sig(j), 0, i)); - sig_val = (*local_mdl)(sig_arg); - ground_fact_conjs.push_back(m.mk_eq(sig_arg, sig_val)); - ground_arg_vals.push_back(sig_val); - } - if (!ground_fact_conjs.empty()) { - expr_ref ground_fact(m); - ground_fact = mk_and(ground_fact_conjs); - m_pm.formula_o2n(ground_fact, ground_fact, i); - cex_facts.push_back (ground_fact); - } else { - cex_facts.push_back (m.mk_true ()); - } - cex.push_back(m.mk_app(ch_pt.head(), - sig_size, ground_arg_vals.c_ptr())); + premises.reset(); + conclusion.reset(); + positions.reset(); + substs.reset(); } + SASSERT(!pf || !m.is_hyper_resolve(pf)); + if (pf) { + cex.push_back(m.get_fact(pf)); } TRACE ("spacer", tout << "ground cex\n" << cex << "\n";); @@ -3091,7 +2994,7 @@ expr_ref context::get_ground_sat_answer() { return mk_and(cex); } -void context::display_certificate(std::ostream &out) { +void context::display_certificate(std::ostream &out) const { switch(m_last_result) { case l_false: out << mk_pp(mk_unsat_answer(), m); diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index cb9063c52..76813895c 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -1006,7 +1006,7 @@ class context { /** \brief Retrieve satisfying assignment with explanation. */ - expr_ref mk_sat_answer() {return get_ground_sat_answer();} + expr_ref mk_sat_answer() const {return get_ground_sat_answer();} expr_ref mk_unsat_answer() const; unsigned get_cex_depth (); @@ -1065,6 +1065,7 @@ public: ast_manager& get_ast_manager() const {return m;} manager& get_manager() {return m_pm;} + const manager & get_manager() const {return m_pm;} decl2rel const& get_pred_transformers() const {return m_rels;} pred_transformer& get_pred_transformer(func_decl* p) const {return *m_rels.find(p);} @@ -1082,8 +1083,8 @@ public: * 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_ref get_ground_sat_answer (); - proof_ref get_ground_refutation(); + expr_ref get_ground_sat_answer () const; + proof_ref get_ground_refutation() const; void get_rules_along_trace (datalog::rule_ref_vector& rules); void collect_statistics(statistics& st) const; @@ -1091,7 +1092,7 @@ public: void reset(); std::ostream& display(std::ostream& out) const; - void display_certificate(std::ostream& out); + void display_certificate(std::ostream& out) const; pob& get_root() const {return m_pob_queue.get_root();} void set_query(func_decl* q) {m_query_pred = q;} diff --git a/src/muz/spacer/spacer_sat_answer.cpp b/src/muz/spacer/spacer_sat_answer.cpp index 30241230f..7b54260f5 100644 --- a/src/muz/spacer/spacer_sat_answer.cpp +++ b/src/muz/spacer/spacer_sat_answer.cpp @@ -1,7 +1,7 @@ #include "muz/spacer/spacer_sat_answer.h" #include "muz/base/dl_context.h" #include "muz/base/dl_rule.h" - +#include "ast/scoped_proof.h" #include "smt/smt_solver.h" namespace spacer { @@ -44,15 +44,16 @@ struct ground_sat_answer_op::frame { pred_transformer &pt() {return m_pt;} }; -ground_sat_answer_op::ground_sat_answer_op(context &ctx) : +ground_sat_answer_op::ground_sat_answer_op(const context &ctx) : m_ctx(ctx), m(m_ctx.get_ast_manager()), m_pm(m_ctx.get_manager()), m_pinned(m) { - m_solver = mk_smt_solver(m, params_ref::get_empty(), symbol::null); } proof_ref ground_sat_answer_op::operator()(pred_transformer &query) { + // -- turn on proof mode so that proof constructing API in ast_manager work correctly + scoped_proof _pf(m); - + m_solver = mk_smt_solver(m, params_ref::get_empty(), symbol::null); vector todo, new_todo; // -- find substitution for a query if query is not nullary diff --git a/src/muz/spacer/spacer_sat_answer.h b/src/muz/spacer/spacer_sat_answer.h index 6cfd3b14c..daf2e5da0 100644 --- a/src/muz/spacer/spacer_sat_answer.h +++ b/src/muz/spacer/spacer_sat_answer.h @@ -29,9 +29,9 @@ Revision History: namespace spacer { class ground_sat_answer_op { - context &m_ctx; + const context &m_ctx; ast_manager &m; - manager &m_pm; + const manager &m_pm; expr_ref_vector m_pinned; obj_map m_cache; @@ -46,7 +46,7 @@ class ground_sat_answer_op { model_ref &mdl, expr_ref_vector &subst); public: - ground_sat_answer_op(context &ctx); + ground_sat_answer_op(const context &ctx); proof_ref operator() (pred_transformer &query); };