From b8e8e090ad10b8557219ae6724ee215de7e7e76d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 10 Jun 2017 09:30:01 -0700 Subject: [PATCH] filter assumptions by membership in initial list #1065 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 16 +++++++--------- 1 file changed, 7 insertions(+), 9 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index b9ed925b0..e9302bb35 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -597,16 +597,14 @@ private: extract_asm2dep(dep2asm, asm2dep); sat::literal_vector const& core = m_solver.get_core(); TRACE("sat", - dep2asm_t::iterator it2 = dep2asm.begin(); - dep2asm_t::iterator end2 = dep2asm.end(); - for (; it2 != end2; ++it2) { - tout << mk_pp(it2->m_key, m) << " |-> " << sat::literal(it2->m_value) << "\n"; + for (auto kv : dep2asm) { + tout << mk_pp(kv.m_key, m) << " |-> " << sat::literal(kv.m_value) << "\n"; } - tout << "core: "; - for (unsigned i = 0; i < core.size(); ++i) { - tout << core[i] << " "; + tout << "asm2fml: "; + for (auto kv : asm2fml) { + tout << mk_pp(kv.m_key, m) << " |-> " << mk_pp(kv.m_value, m) << "\n"; } - tout << "\n"; + tout << "core: "; for (auto c : core) tout << c << " "; tout << "\n"; ); m_core.reset(); @@ -615,8 +613,8 @@ private: VERIFY(asm2dep.find(core[i].index(), e)); if (asm2fml.contains(e)) { e = asm2fml.find(e); + m_core.push_back(e); } - m_core.push_back(e); } }