mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix core extraction for QF_BV theory/inc_sat_solver based on regressions pointed out by Matthias Heizmann and Tjark Weber

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-07-09 12:35:11 -07:00
parent d7d22cad02
commit 8f862f8fed
2 changed files with 13 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/cmd_context/cmd_context.cpp
View file

@ -1476,7 +1476,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
if (produce_unsat_cores()) { if (produce_unsat_cores()) {
expr_ref_vector asms(m()); expr_ref_vector asms(m());
asms.append(num_assumptions, assumptions); asms.append(num_assumptions, assumptions);
for (unsigned i = 0; i < m_assertion_names.size(); ++i) { for (unsigned i = 0; false && i < m_assertion_names.size(); ++i) {
if (m_assertion_names[i]) { if (m_assertion_names[i]) {
asms.push_back(m_assertion_names[i]); asms.push_back(m_assertion_names[i]);
} }

15
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -135,7 +135,6 @@ public:
lbool r = internalize_formulas(); lbool r = internalize_formulas();
if (r != l_true) return r; if (r != l_true) return r;
r = internalize_assumptions(sz, assumptions, dep2asm); r = internalize_assumptions(sz, assumptions, dep2asm);
SASSERT(sz == m_asms.size());
if (r != l_true) return r; if (r != l_true) return r;
r = m_solver.check(m_asms.size(), m_asms.c_ptr(), m_weights.c_ptr(), max_weight); r = m_solver.check(m_asms.size(), m_asms.c_ptr(), m_weights.c_ptr(), max_weight);
@ -147,7 +146,7 @@ public:
break; break;
case l_false: case l_false:
// TBD: expr_dependency core is not accounted for. // TBD: expr_dependency core is not accounted for.
if (sz > 0) { if (!m_asms.empty()) {
extract_core(dep2asm); extract_core(dep2asm);
} }
break; break;
@ -314,7 +313,7 @@ private:
} }
lbool internalize_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) { lbool internalize_assumptions(unsigned sz, expr* const* asms, dep2asm_t& dep2asm) {
if (sz == 0) { if (sz == 0 && get_num_assumptions() == 0) {
m_asms.shrink(0); m_asms.shrink(0);
return l_true; return l_true;
} }
@ -322,6 +321,9 @@ private:
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
g->assert_expr(asms[i], m.mk_leaf(asms[i])); g->assert_expr(asms[i], m.mk_leaf(asms[i]));
} }
for (unsigned i = 0; i < get_num_assumptions(); ++i) {
g->assert_expr(get_assumption(i), m.mk_leaf(get_assumption(i)));
}
lbool res = internalize_goal(g, dep2asm); lbool res = internalize_goal(g, dep2asm);
if (res == l_true) { if (res == l_true) {
extract_assumptions(sz, asms, dep2asm); extract_assumptions(sz, asms, dep2asm);
@ -355,6 +357,13 @@ private:
++j; ++j;
} }
} }
for (unsigned i = 0; i < get_num_assumptions(); ++i) {
if (dep2asm.find(get_assumption(i), lit)) {
SASSERT(lit.var() <= m_solver.num_vars());
m_asms.push_back(lit);
}
}
SASSERT(dep2asm.size() == m_asms.size()); SASSERT(dep2asm.size() == m_asms.size());
} }