ground sat refutation from spacer (wip)

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

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<func_decl> preds;
     ptr_vector<pred_transformer> 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

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;

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<frame> 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<frame> &todo) {
+    const datalog::rule &r = fr.rule();
+    ptr_vector<func_decl> 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<std::pair<unsigned, unsigned>> positions;
+    vector<expr_ref_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());
+}
+
+}

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<expr, proof*> m_cache;
+
+    ref<solver> m_solver;
+
+    struct frame;
+
+    proof *mk_proof_step(frame &fr);
+    void mk_children(frame &fr, vector<frame> &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