From 26921d1c9cccf05f6cc3c5cc8d9448809bef7cf2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Mar 2019 22:32:50 -0800 Subject: [PATCH] fix #2155 Signed-off-by: Nikolaj Bjorner --- src/muz/spacer/spacer_context.cpp | 22 +++++++++++++++++++--- src/muz/spacer/spacer_context.h | 6 +++--- 2 files changed, 22 insertions(+), 6 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 76e7e24c6..a2fb70e63 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -2948,7 +2948,7 @@ proof_ref context::get_ground_refutation() { ground_sat_answer_op op(*this); return op(*m_query); } -expr_ref context::get_ground_sat_answer() const { +expr_ref context::get_ground_sat_answer() { if (m_last_result != l_true) { IF_VERBOSE(0, verbose_stream() << "Sat answer unavailable when result is false\n";); @@ -2994,6 +2994,7 @@ expr_ref context::get_ground_sat_answer() const { 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 @@ -3032,6 +3033,7 @@ expr_ref context::get_ground_sat_answer() const { } 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"; @@ -3046,6 +3048,20 @@ expr_ref context::get_ground_sat_answer() const { 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)); + std::cout << sig_arg << "\n"; + 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(); @@ -3073,10 +3089,10 @@ expr_ref context::get_ground_sat_answer() const { TRACE ("spacer", tout << "ground cex\n" << cex << "\n";); - return expr_ref(m.mk_and(cex.size(), cex.c_ptr()), m); + return mk_and(cex); } -void context::display_certificate(std::ostream &out) const { +void context::display_certificate(std::ostream &out) { 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 494de1c23..54eb1befa 100644 --- a/src/muz/spacer/spacer_context.h +++ b/src/muz/spacer/spacer_context.h @@ -1010,7 +1010,7 @@ class context { /** \brief Retrieve satisfying assignment with explanation. */ - expr_ref mk_sat_answer() const {return get_ground_sat_answer();} + expr_ref mk_sat_answer() {return get_ground_sat_answer();} expr_ref mk_unsat_answer() const; unsigned get_cex_depth (); @@ -1086,7 +1086,7 @@ 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 () const; + expr_ref get_ground_sat_answer (); proof_ref get_ground_refutation(); void get_rules_along_trace (datalog::rule_ref_vector& rules); @@ -1095,7 +1095,7 @@ public: void reset(); std::ostream& display(std::ostream& out) const; - void display_certificate(std::ostream& out) const; + void display_certificate(std::ostream& out); pob& get_root() const {return m_pob_queue.get_root();} void set_query(func_decl* q) {m_query_pred = q;}