mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-18 20:03:38 +00:00
Code Activity

fix unsat core extraction code in smt_context

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-07-30 11:22:34 -07:00
parent d32019f4c9
commit 7346098895
3 changed files with 19 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/smt/smt_conflict_resolution.cpp
View file

@ -1334,8 +1334,9 @@ namespace smt {
if (!m_ctx.is_marked(var)) { if (!m_ctx.is_marked(var)) {
m_ctx.set_mark(var); m_ctx.set_mark(var);
m_unmark.push_back(var); m_unmark.push_back(var);
if (m_ctx.is_assumption(var)) }
m_assumptions.push_back(antecedent); if (m_ctx.is_assumption(var)) {
m_assumptions.push_back(antecedent);
} }
} }
@ -1373,7 +1374,7 @@ namespace smt {
} }
while (true) { while (true) {
TRACE("unsat_core_bug", tout << "js.get_kind(): " << js.get_kind() << ", idx: " << idx << "\n";); TRACE("unsat_core_bug", tout << consequent << " js.get_kind(): " << js.get_kind() << ", idx: " << idx << "\n";);
switch (js.get_kind()) { switch (js.get_kind()) {
case b_justification::CLAUSE: { case b_justification::CLAUSE: {
clause * cls = js.get_clause(); clause * cls = js.get_clause();
@ -1411,17 +1412,21 @@ namespace smt {
UNREACHABLE(); UNREACHABLE();
} }
while (true) { if (m_ctx.is_assumption(consequent.var())) {
if (idx < 0) m_assumptions.push_back(consequent);
goto end_unsat_core; }
while (idx >= 0) {
literal l = m_assigned_literals[idx]; literal l = m_assigned_literals[idx];
TRACE("unsat_core_bug", tout << "l: " << l << ", get_assign_level(l): " << m_ctx.get_assign_level(l) << ", is_marked(l): " << m_ctx.is_marked(l.var()) << "\n";); TRACE("unsat_core_bug", tout << "l: " << l << ", get_assign_level(l): " << m_ctx.get_assign_level(l) << ", is_marked(l): " << m_ctx.is_marked(l.var()) << "\n";);
if (m_ctx.get_assign_level(l) < search_lvl || idx == 0) if (m_ctx.get_assign_level(l) < search_lvl)
goto end_unsat_core; goto end_unsat_core;
if (m_ctx.is_marked(l.var())) if (m_ctx.is_marked(l.var()))
break; break;
idx--; idx--;
} }
if (idx < 0) {
goto end_unsat_core;
}
SASSERT(idx >= 0); SASSERT(idx >= 0);
consequent = m_assigned_literals[idx]; consequent = m_assigned_literals[idx];

9
src/smt/smt_context.cpp
View file

@ -3044,7 +3044,7 @@ namespace smt {
SASSERT(m_assumptions.empty()); SASSERT(m_assumptions.empty());
return; return;
} }
obj_hashtable<expr> already_found_assumptions; uint_set already_found_assumptions;
literal_vector::const_iterator it = m_conflict_resolution->begin_unsat_core(); literal_vector::const_iterator it = m_conflict_resolution->begin_unsat_core();
literal_vector::const_iterator end = m_conflict_resolution->end_unsat_core(); literal_vector::const_iterator end = m_conflict_resolution->end_unsat_core();
for (; it != end; ++it) { for (; it != end; ++it) {
@ -3053,10 +3053,9 @@ namespace smt {
SASSERT(get_bdata(l.var()).m_assumption); SASSERT(get_bdata(l.var()).m_assumption);
if (!m_literal2assumption.contains(l.index())) l.neg(); if (!m_literal2assumption.contains(l.index())) l.neg();
SASSERT(m_literal2assumption.contains(l.index())); SASSERT(m_literal2assumption.contains(l.index()));
expr * a = m_literal2assumption[l.index()]; if (!already_found_assumptions.contains(l.index())) {
if (!already_found_assumptions.contains(a)) { already_found_assumptions.insert(l.index());
already_found_assumptions.insert(a); m_unsat_core.push_back(m_literal2assumption[l.index()]);
m_unsat_core.push_back(a);
} }
} }
reset_assumptions(); reset_assumptions();

1
src/solver/solver.cpp
View file

@ -19,6 +19,7 @@ Notes:
#include"solver.h" #include"solver.h"
#include"model_evaluator.h" #include"model_evaluator.h"
#include"ast_util.h" #include"ast_util.h"
#include"ast_pp.h"
unsigned solver::get_num_assertions() const { unsigned solver::get_num_assertions() const {
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();