mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

filter assumptions by membership in initial list #1065

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-06-10 09:30:01 -07:00
parent d5f646929e
commit b8e8e090ad
1 changed files with 7 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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);
}
}