mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

local debug update

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-27 09:58:43 -07:00
parent 9cea3a1c02
commit 1392dc020f
2 changed files with 13 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/muz/rel/udoc_relation.cpp
View file

@ -1118,7 +1118,7 @@ namespace datalog {
unsigned idx_dst = dstt.column_idx(col_dst);
unsigned idx_src = srct.column_idx(col_src);
unsigned num_tbits = dstt.column_num_bits(col_dst);
SASSERT(num_bits == srct.column_num_bits(col_src));
SASSERT(num_tbits == srct.column_num_bits(col_src));
IF_VERBOSE(3, verbose_stream() << "copy column " << idx_src
<< " to " << idx_dst << " " << num_tbits << "\n";);
for (unsigned i = 0; i < num_tbits; ++i) {

24
src/opt/inc_sat_solver.cpp
View file

@ -318,6 +318,18 @@ private:
asm2dep.insert(it->m_value.index(), it->m_key);
}
sat::literal_vector const& core = m_solver.get_core();
TRACE("opt",
dep2asm_t::iterator it = dep2asm.begin();
dep2asm_t::iterator end = dep2asm.end();
for (; it != end; ++it) {
tout << mk_pp(it->m_key, m) << " |-> " << sat::literal(it->m_value) << "\n";
}
tout << "core: ";
for (unsigned i = 0; i < core.size(); ++i) {
tout << core[i] << " ";
}
tout << "\n";
);
m_core.reset();
for (unsigned i = 0; i < core.size(); ++i) {
@ -325,18 +337,6 @@ private:
VERIFY (asm2dep.find(core[i].index(), e));
m_core.push_back(e);
}
TRACE("opt",
dep2asm_t::iterator it = dep2asm.begin();
dep2asm_t::iterator end = dep2asm.end();
for (; it != end; ++it) {
tout << mk_pp(it->m_key, m) << " |-> " << it->m_value << "\n";
}
tout << "core: ";
for (unsigned i = 0; i < core.size(); ++i) {
tout << core[i] << ": " << mk_pp(m_core[i].get(), m) << " ";
}
tout << "\n";
);
}