mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

fix #2155

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-03 22:32:50 -08:00
parent 5c13acbf9f
commit 26921d1c9c
2 changed files with 22 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/muz/spacer/spacer_context.cpp
View file

@ -2948,7 +2948,7 @@ proof_ref context::get_ground_refutation() {
ground_sat_answer_op op(*this); ground_sat_answer_op op(*this);
return op(*m_query); 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 (m_last_result != l_true) {
IF_VERBOSE(0, verbose_stream() IF_VERBOSE(0, verbose_stream()
<< "Sat answer unavailable when result is false\n";); << "Sat answer unavailable when result is false\n";);
@ -2994,6 +2994,7 @@ expr_ref context::get_ground_sat_answer() const {
ref<solver> cex_ctx = ref<solver> cex_ctx =
mk_smt_solver(m, params_ref::get_empty(), symbol::null); mk_smt_solver(m, params_ref::get_empty(), symbol::null);
bool first = true;
// preorder traversal of the query derivation tree // preorder traversal of the query derivation tree
for (unsigned curr = 0; curr < pts.size (); curr++) { for (unsigned curr = 0; curr < pts.size (); curr++) {
// pick next pt, fact, and cex_fact // 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->transition());
cex_ctx->assert_expr(pt->rule2tag(r)); cex_ctx->assert_expr(pt->rule2tag(r));
TRACE("cex", cex_ctx->display(tout););
lbool res = cex_ctx->check_sat(0, nullptr); lbool res = cex_ctx->check_sat(0, nullptr);
CTRACE("cex", res == l_false, CTRACE("cex", res == l_false,
tout << "Cex fact: " << mk_pp(cex_fact, m) << "\n"; 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->get_model (local_mdl);
cex_ctx->pop (1); cex_ctx->pop (1);
local_mdl->set_model_completion(true); 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++) { for (unsigned i = 0; i < child_pts.size(); i++) {
pred_transformer& ch_pt = *(child_pts.get(i)); pred_transformer& ch_pt = *(child_pts.get(i));
unsigned sig_size = ch_pt.sig_size(); 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";); 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) { switch(m_last_result) {
case l_false: case l_false:
out << mk_pp(mk_unsat_answer(), m); out << mk_pp(mk_unsat_answer(), m);

6
src/muz/spacer/spacer_context.h
View file

@ -1010,7 +1010,7 @@ class context {
/** /**
\brief Retrieve satisfying assignment with explanation. \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; expr_ref mk_unsat_answer() const;
unsigned get_cex_depth (); unsigned get_cex_depth ();
@ -1086,7 +1086,7 @@ public:
* get bottom-up (from query) sequence of ground predicate instances * 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 * (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(); proof_ref get_ground_refutation();
void get_rules_along_trace (datalog::rule_ref_vector& rules); void get_rules_along_trace (datalog::rule_ref_vector& rules);
@ -1095,7 +1095,7 @@ public:
void reset(); void reset();
std::ostream& display(std::ostream& out) const; 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();} pob& get_root() const {return m_pob_queue.get_root();}
void set_query(func_decl* q) {m_query_pred = q;} void set_query(func_decl* q) {m_query_pred = q;}