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

pre-merge commit

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-13 10:09:44 -08:00
parent 7ab042763b
commit bffa0facee
4 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/sat_elim_vars.cpp
View file

@ -87,7 +87,7 @@ namespace sat{
simp.m_neg_cls.reset(); simp.m_neg_cls.reset();
simp.collect_clauses(pos_l, simp.m_pos_cls, false); simp.collect_clauses(pos_l, simp.m_pos_cls, false);
simp.collect_clauses(neg_l, simp.m_neg_cls, false); simp.collect_clauses(neg_l, simp.m_neg_cls, false);
VERIFY(!s.is_external(v)); //VERIFY(!s.is_external(v));
model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
simp.save_clauses(mc_entry, simp.m_pos_cls); simp.save_clauses(mc_entry, simp.m_pos_cls);
simp.save_clauses(mc_entry, simp.m_neg_cls); simp.save_clauses(mc_entry, simp.m_neg_cls);

6
src/sat/sat_simplifier.cpp
View file

@ -1356,7 +1356,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);
@ -1382,7 +1382,7 @@ namespace sat {
void prepare_block_binary(watch_list::iterator it, literal l1, literal blocked, model_converter::entry*& new_entry, model_converter::kind k) { void prepare_block_binary(watch_list::iterator it, literal l1, literal blocked, model_converter::entry*& new_entry, model_converter::kind k) {
SASSERT(!s.is_external(blocked)); SASSERT(!s.is_external(blocked));
VERIFY(!s.is_external(blocked)); //VERIFY(!s.is_external(blocked));
if (new_entry == 0) if (new_entry == 0)
new_entry = &(mc.mk(k, blocked.var())); new_entry = &(mc.mk(k, blocked.var()));
literal l2 = it->get_literal(); literal l2 = it->get_literal();
@ -1782,7 +1782,7 @@ namespace sat {
// eliminate variable // eliminate variable
++s.m_stats.m_elim_var_res; ++s.m_stats.m_elim_var_res;
VERIFY(!is_external(v)); //VERIFY(!is_external(v));
model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v); model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
save_clauses(mc_entry, m_pos_cls); save_clauses(mc_entry, m_pos_cls);
save_clauses(mc_entry, m_neg_cls); save_clauses(mc_entry, m_neg_cls);

2
src/sat/sat_solver.cpp
View file

@ -1331,7 +1331,7 @@ namespace sat {
void solver::add_assumption(literal lit) { void solver::add_assumption(literal lit) {
m_assumption_set.insert(lit); m_assumption_set.insert(lit);
m_assumptions.push_back(lit); m_assumptions.push_back(lit);
VERIFY(is_external(lit.var())); set_external(lit.var());
} }
void solver::pop_assumption() { void solver::pop_assumption() {

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

@ -94,7 +94,7 @@ public:
bool override_incremental() const { bool override_incremental() const {
sat_simplifier_params p(m_params); sat_simplifier_params p(m_params);
std::cout << "override: " << p.override_incremental() << "\n"; //std::cout << "override: " << p.override_incremental() << "\n";
return p.override_incremental(); return p.override_incremental();
} }