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

restored commented out code

Browse source 
Signed-off-by: Miguel Angelo Da Terra Neves <t-mineve@microsoft.com>
This commit is contained in:
Miguel Angelo Da Terra Neves 2017-12-15 14:00:20 -08:00
parent b731d02adc
commit 0f1286adae
5 changed files with 7 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/sat/sat_asymm_branch.cpp
View file

@ -76,12 +76,12 @@ namespace sat {
s.propagate(false); s.propagate(false);
if (s.m_inconsistent) if (s.m_inconsistent)
break; break;
//std::cout << "elim: " << m_elim_literals - elim << "\n"; std::cout << "elim: " << m_elim_literals - elim << "\n";
if (m_elim_literals == elim) if (m_elim_literals == elim)
break; break;
} }
//std::cout << "elim-literals: " << m_elim_literals - elim0 << "\n"; std::cout << "elim-literals: " << m_elim_literals - elim0 << "\n";
//std::cout << "elim-learned-literals: " << m_elim_learned_literals - eliml0 << "\n"; std::cout << "elim-learned-literals: " << m_elim_learned_literals - eliml0 << "\n";
return m_elim_literals > elim0; return m_elim_literals > elim0;
} }

1
src/sat/sat_integrity_checker.cpp
View file

@ -155,7 +155,6 @@ namespace sat {
} }
bool integrity_checker::check_watches(literal l, watch_list const& wlist) const { bool integrity_checker::check_watches(literal l, watch_list const& wlist) const {
return true; // TODO: remove
for (watched const& w : wlist) { for (watched const& w : wlist) {
switch (w.get_kind()) { switch (w.get_kind()) {
case watched::BINARY: case watched::BINARY:

2
src/sat/sat_lookahead.cpp
View file

@ -2390,7 +2390,7 @@ namespace sat {
} }
} }
} }
//std::cout << candidates.size() << " -> " << k << "\n"; std::cout << candidates.size() << " -> " << k << "\n";
if (k == candidates.size()) break; if (k == candidates.size()) break;
candidates.shrink(k); candidates.shrink(k);
if (k == 0) break; if (k == 0) break;

2
src/sat/sat_simplifier.cpp
View file

@ -1360,7 +1360,7 @@ namespace sat {
void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry, model_converter::kind k) { void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry, model_converter::kind k) {
TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";); TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
//VERIFY(!s.is_external(l)); VERIFY(!s.is_external(l));
if (new_entry == 0) if (new_entry == 0)
new_entry = &(mc.mk(k, l.var())); new_entry = &(mc.mk(k, l.var()));
m_to_remove.push_back(&c); m_to_remove.push_back(&c);

4
src/sat/sat_solver.cpp
View file

@ -1546,8 +1546,8 @@ namespace sat {
if (!check_clauses(m_model)) { if (!check_clauses(m_model)) {
IF_VERBOSE(0, verbose_stream() << "failure checking clauses on transformed model\n";); IF_VERBOSE(0, verbose_stream() << "failure checking clauses on transformed model\n";);
//UNREACHABLE(); // TODO: uncomment UNREACHABLE();
//throw solver_exception("check model failed"); // TODO: uncomment throw solver_exception("check model failed");
} }
TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";); TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";);