diff --git a/src/muz/spacer/CMakeLists.txt b/src/muz/spacer/CMakeLists.txt index 8e41d5ae7..22218f25f 100644 --- a/src/muz/spacer/CMakeLists.txt +++ b/src/muz/spacer/CMakeLists.txt @@ -27,6 +27,7 @@ z3_add_component(spacer spacer_iuc_proof.cpp spacer_mbc.cpp spacer_pdr.cpp + spacer_sat_answer.cpp COMPONENT_DEPENDENCIES arith_tactics core_tactics diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 6726bb15d..2e199c6e4 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -36,6 +36,7 @@ Notes: #include "muz/base/dl_rule_set.h" #include "smt/tactic/unit_subsumption_tactic.h" #include "model/model_smt2_pp.h" +#include "model/model_evaluator.h" #include "muz/transforms/dl_mk_rule_inliner.h" #include "ast/ast_smt2_pp.h" #include "ast/ast_ll_pp.h" @@ -52,6 +53,9 @@ Notes: #include "ast/expr_abstract.h" #include "smt/smt_solver.h" + +#include "muz/spacer/spacer_sat_answer.h" + namespace spacer { /// pob -- proof obligation @@ -2857,19 +2861,31 @@ expr_ref context::mk_unsat_answer() const return ex.to_expr(); } + +proof_ref context::get_ground_refutation() { + if (m_last_result != l_true) { + IF_VERBOSE(0, verbose_stream() + << "Sat answer unavailable when result is false\n";); + return proof_ref(m); + } + + ground_sat_answer_op op(*this); + return op(*m_query); +} expr_ref context::get_ground_sat_answer() { if (m_last_result != l_true) { - verbose_stream () << "Sat answer unavailable when result is false\n"; - return expr_ref (m); + 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 - cex_facts (m); // equalities for the ground cex using signature constants + 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 // temporary reach_fact *reach_fact; @@ -2921,6 +2937,7 @@ expr_ref context::get_ground_sat_answer() // 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]))); } @@ -2936,12 +2953,11 @@ expr_ref context::get_ground_sat_answer() SASSERT (child_reach_facts.size () == u_tail_sz); for (unsigned i = 0; i < u_tail_sz; i++) { expr_ref ofml (m); - child_pts.get (i)->get_manager ().formula_n2o - (child_reach_facts[i]->get (), ofml, i); + 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)); + cex_ctx->assert_expr(pt->transition()); + cex_ctx->assert_expr(pt->rule2tag(r)); lbool res = cex_ctx->check_sat(0, nullptr); CTRACE("cex", res == l_false, tout << "Cex fact: " << mk_pp(cex_fact, m) << "\n"; @@ -2956,40 +2972,35 @@ expr_ref context::get_ground_sat_answer() cex_ctx->get_model (local_mdl); cex_ctx->pop (1); - model_evaluator_util mev (m); - mev.set_model (*local_mdl); - 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); + model_evaluator mev(*local_mdl); + 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 (ch_pt.get_manager ().o2o (ch_pt.sig (j), 0, i)); + expr_ref sig_arg(m), sig_val(m); + sig_arg = m.mk_const (m_pm.o2o(ch_pt.sig(j), 0, i)); VERIFY(mev.eval (sig_arg, sig_val, true)); - ground_fact_conjs.push_back (m.mk_eq (sig_arg, sig_val)); - ground_arg_vals.push_back (sig_val); + ground_fact_conjs.push_back(m.mk_eq(sig_arg, sig_val)); + ground_arg_vals.push_back(sig_val); } if (ground_fact_conjs.size () > 0) { - expr_ref ground_fact (m); - ground_fact = m.mk_and (ground_fact_conjs.size (), ground_fact_conjs.c_ptr ()); - ch_pt.get_manager ().formula_o2n (ground_fact, ground_fact, i); + 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 ())); + cex.push_back(m.mk_app(ch_pt.head(), + sig_size, ground_arg_vals.c_ptr())); } } - TRACE ("spacer", - tout << "ground cex\n"; - for (unsigned i = 0; i < cex.size (); i++) { - tout << mk_pp (cex.get (i), m) << "\n"; - } - ); + TRACE ("spacer", tout << "ground cex\n" << cex << "\n";); - return expr_ref (m.mk_and (cex.size (), cex.c_ptr ()), m); + return expr_ref(m.mk_and(cex.size(), cex.c_ptr()), m); } ///this is where everything starts diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h index 34c04d596..e95ddc8ec 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -970,7 +970,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 (); + expr_ref get_ground_sat_answer (); + proof_ref get_ground_refutation(); void get_rules_along_trace (datalog::rule_ref_vector& rules); void collect_statistics(statistics& st) const; diff --git a/src/muz/spacer/spacer_sat_answer.cpp b/src/muz/spacer/spacer_sat_answer.cpp new file mode 100644 index 000000000..8382133d8 --- /dev/null +++ b/src/muz/spacer/spacer_sat_answer.cpp @@ -0,0 +1,168 @@ +#include "muz/spacer/spacer_sat_answer.h" +#include "muz/base/dl_context.h" +#include "muz/base/dl_rule.h" + +#include "smt/smt_solver.h" + +namespace spacer { + +struct ground_sat_answer_op::frame { + reach_fact *m_rf; + pred_transformer &m_pt; + expr_ref_vector m_gnd_subst; + expr_ref m_gnd_eq; + expr_ref m_fact; + unsigned m_visit; + expr_ref_vector m_kids; + + frame(reach_fact *rf, pred_transformer &pt, const expr_ref_vector &gnd_subst) : + m_rf(rf), m_pt(pt), + m_gnd_subst(gnd_subst), + m_gnd_eq(pt.get_ast_manager()), + m_fact(pt.get_ast_manager()), + m_visit(0), + m_kids(pt.get_ast_manager()) { + + ast_manager &m = pt.get_ast_manager(); + spacer::manager &pm = pt.get_manager(); + + m_fact = m.mk_app(head(), m_gnd_subst.size(), m_gnd_subst.c_ptr()); + if (pt.head()->get_arity() == 0) + m_gnd_eq = m.mk_true(); + else { + SASSERT(m_gnd_subst.size() == pt.head()->get_arity()); + for (unsigned i = 0, sz = pt.sig_size(); i < sz; ++i) { + m_gnd_eq = m.mk_eq(m.mk_const(pm.o2n(pt.sig(i), 0)), + m_gnd_subst.get(i)); + } + } + } + + func_decl* head() {return m_pt.head();} + expr* fact() {return m_fact;} + const datalog::rule &rule() {return m_rf->get_rule();} + pred_transformer &pt() {return m_pt;} +}; + +ground_sat_answer_op::ground_sat_answer_op(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) { + + + vector todo; + + // -- find substitution for a query if query is not nullary + expr_ref_vector qsubst(m); + if (query.head()->get_arity() > 0) { + solver::scoped_push _s_(*m_solver); + m_solver->assert_expr(query.get_last_rf()->get()); + lbool res = m_solver->check_sat(0, nullptr); + (void)res; + SASSERT(res == l_true); + model_ref mdl; + m_solver->get_model(mdl); + for (unsigned i = 0, sz = query.sig_size(); i < sz; ++i) { + expr_ref arg(m), val(m); + arg = m.mk_const(m_pm.o2n(query.sig(i), 0)); + mdl->eval(arg, val, true); + qsubst.push_back(val); + } + } + + frame root(query.get_last_rf(), query, qsubst); + todo.push_back(root); + + while (!todo.empty()) { + frame &curr = todo.back(); + if (m_cache.contains(curr.fact())) + { + todo.pop_back(); + continue; + } + + if (curr.m_visit == 0) { + mk_children(curr, todo); + curr.m_visit = 1; + } + else { + proof* pf = mk_proof_step(curr); + m_cache.insert(curr.fact(), pf); + todo.pop_back(); + } + + } + return proof_ref(m_cache.find(root.fact()), m); +} + + +void ground_sat_answer_op::mk_children(frame &fr, vector &todo) { + const datalog::rule &r = fr.rule(); + ptr_vector preds; + fr.pt().find_predecessors(r, preds); + + if (preds.empty()) return; + + const reach_fact_ref_vector &kid_rfs = fr.m_rf->get_justifications(); + solver::scoped_push _s_(*m_solver); + m_solver->assert_expr(fr.m_gnd_eq); + unsigned ut_sz = r.get_uninterpreted_tail_size(); + for (unsigned i = 0; i < ut_sz; ++i) { + expr_ref f(m); + m_pm.formula_n2o(kid_rfs.get(i)->get(), f, i); + m_solver->assert_expr(f); + } + m_solver->assert_expr(fr.pt().transition()); + m_solver->assert_expr(fr.pt().rule2tag(&r)); + + lbool res = m_solver->check_sat(0, nullptr); + (void)res; + SASSERT(res == l_true); + + model_ref mdl; + m_solver->get_model(mdl); + expr_ref_vector subst(m); + for (unsigned i = 0, sz = preds.size(); i < sz; ++i) { + subst.reset(); + mk_child_subst_from_model(preds.get(i), i, mdl, subst); + todo.push_back(frame(kid_rfs.get(i), + m_ctx.get_pred_transformer(preds.get(i)), subst)); + fr.m_kids.push_back(todo.back().fact()); + } +} + + +void ground_sat_answer_op::mk_child_subst_from_model(func_decl *pred, + unsigned j, model_ref &mdl, + expr_ref_vector &subst) { + pred_transformer &pt = m_ctx.get_pred_transformer(pred); + for (unsigned i = 0, sz = pt.sig_size(); i < sz; ++i) { + expr_ref arg(m), val(m); + arg = m.mk_const(m_pm.o2o(pt.sig(i), 0, j)); + mdl->eval(arg, val, true); + subst.push_back(val); + } +} + +proof *ground_sat_answer_op::mk_proof_step(frame &fr) { + svector> positions; + vector substs; + + proof_ref_vector premises(m); + datalog::rule_manager &rm = m_ctx.get_datalog_context().get_rule_manager(); + expr_ref rule_fml(m); + rm.to_formula(fr.rule(), rule_fml); + premises.push_back(m.mk_asserted(rule_fml)); + for (auto &k : fr.m_kids) {premises.push_back(m_cache.find(k));} + + m_pinned.push_back(m.mk_hyper_resolve(premises.size(), + premises.c_ptr(), + fr.fact(), + positions, substs)); + return to_app(m_pinned.back()); +} + +} diff --git a/src/muz/spacer/spacer_sat_answer.h b/src/muz/spacer/spacer_sat_answer.h new file mode 100644 index 000000000..6cfd3b14c --- /dev/null +++ b/src/muz/spacer/spacer_sat_answer.h @@ -0,0 +1,55 @@ +/*++ +Copyright (c) 2018 Arie Gurfinkel + +Module Name: + + spacer_sat_answer.h + +Abstract: + + Compute refutation proof for CHC + +Author: + + Arie Gurfinkel + +Revision History: + +--*/ + +#ifndef _SPACER_SAT_ANSWER_H_ +#define _SPACER_SAT_ANSWER_H_ + +#include "muz/spacer/spacer_context.h" +#include "ast/ast.h" +#include "util/obj_hashtable.h" +#include "model/model.h" +#include "solver/solver.h" + +namespace spacer { + +class ground_sat_answer_op { + context &m_ctx; + ast_manager &m; + manager &m_pm; + + expr_ref_vector m_pinned; + obj_map m_cache; + + ref m_solver; + + struct frame; + + proof *mk_proof_step(frame &fr); + void mk_children(frame &fr, vector &todo); + void mk_child_subst_from_model(func_decl *pred, unsigned i, + model_ref &mdl, expr_ref_vector &subst); + +public: + ground_sat_answer_op(context &ctx); + + proof_ref operator() (pred_transformer &query); +}; +} + +#endif