mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-06 03:10:25 +00:00
Code Activity

Fix refutation generation

Browse source
This commit is contained in:
Arie Gurfinkel 2018-06-08 09:45:19 -07:00
parent 18e3c7b13d
commit 4099f31f4f
1 changed files with 19 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/muz/spacer/spacer_sat_answer.cpp
View file

@ -53,7 +53,7 @@ ground_sat_answer_op::ground_sat_answer_op(context &ctx) :
proof_ref ground_sat_answer_op::operator()(pred_transformer &query) { proof_ref ground_sat_answer_op::operator()(pred_transformer &query) {
vector<frame> todo; vector<frame> todo, new_todo;
// -- find substitution for a query if query is not nullary // -- find substitution for a query if query is not nullary
expr_ref_vector qsubst(m); expr_ref_vector qsubst(m);
@ -73,29 +73,32 @@ proof_ref ground_sat_answer_op::operator()(pred_transformer &query) {
} }
} }
frame root(query.get_last_rf(), query, qsubst); todo.push_back(frame(query.get_last_rf(), query, qsubst));
todo.push_back(root); expr_ref root_fact(m);
root_fact = todo.back().fact();
while (!todo.empty()) { while (!todo.empty()) {
frame &curr = todo.back(); frame &curr = todo.back();
if (m_cache.contains(curr.fact())) if (m_cache.contains(curr.fact())) {
{
todo.pop_back(); todo.pop_back();
continue; continue;
} }
if (curr.m_visit == 0) { if (curr.m_visit == 0) {
mk_children(curr, todo); new_todo.reset();
mk_children(curr, new_todo);
curr.m_visit = 1; curr.m_visit = 1;
// curr becomes invalid
todo.append(new_todo);
} }
else { else {
proof* pf = mk_proof_step(curr); proof* pf = mk_proof_step(curr);
m_pinned.push_back(curr.fact());
m_cache.insert(curr.fact(), pf); m_cache.insert(curr.fact(), pf);
todo.pop_back(); todo.pop_back();
} }
} }
return proof_ref(m_cache.find(root.fact()), m); return proof_ref(m_cache.find(root_fact), m);
} }
@ -120,7 +123,7 @@ void ground_sat_answer_op::mk_children(frame &fr, vector<frame> &todo) {
lbool res = m_solver->check_sat(0, nullptr); lbool res = m_solver->check_sat(0, nullptr);
(void)res; (void)res;
SASSERT(res == l_true); VERIFY(res == l_true);
model_ref mdl; model_ref mdl;
m_solver->get_model(mdl); m_solver->get_model(mdl);
@ -155,9 +158,16 @@ proof *ground_sat_answer_op::mk_proof_step(frame &fr) {
datalog::rule_manager &rm = m_ctx.get_datalog_context().get_rule_manager(); datalog::rule_manager &rm = m_ctx.get_datalog_context().get_rule_manager();
expr_ref rule_fml(m); expr_ref rule_fml(m);
rm.to_formula(fr.rule(), rule_fml); rm.to_formula(fr.rule(), rule_fml);
// premises.push_back(fr.rule().get_proof());
premises.push_back(m.mk_asserted(rule_fml)); premises.push_back(m.mk_asserted(rule_fml));
for (auto &k : fr.m_kids) {premises.push_back(m_cache.find(k));} for (auto &k : fr.m_kids) {premises.push_back(m_cache.find(k));}
for (unsigned i = 0; i < premises.size(); i++) {
positions.push_back(std::make_pair(0,i));
}
for (unsigned i = 0; i <= premises.size(); i++) {
substs.push_back(expr_ref_vector(m));
}
m_pinned.push_back(m.mk_hyper_resolve(premises.size(), m_pinned.push_back(m.mk_hyper_resolve(premises.size(),
premises.c_ptr(), premises.c_ptr(),
fr.fact(), fr.fact(),