mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

fix hidden tautology bug on non-learned clauses

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-01-21 23:18:41 -08:00
parent ece5ad90e0
commit 3b1810d893
7 changed files with 22 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/sat/sat_asymm_branch.cpp
View file

@ -399,13 +399,11 @@ namespace sat {
bool asymm_branch::process_sampled(big& big, clause & c) {
scoped_detach scoped_d(s, c);
sort(big, c);
#if 1
if (uhte(big, c)) {
if (c.is_learned() && uhte(big, c)) {
++m_hidden_tautologies;
scoped_d.del_clause();
return false;
}
#endif
return uhle(scoped_d, big, c);
}

3
src/sat/sat_elim_vars.cpp
View file

@ -88,6 +88,7 @@ namespace sat{
simp.collect_clauses(pos_l, simp.m_pos_cls);
simp.collect_clauses(neg_l, simp.m_neg_cls);
VERIFY(!simp.is_external(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_neg_cls);
@ -100,7 +101,7 @@ namespace sat{
pos_occs.reset();
neg_occs.reset();
literal_vector lits;
add_clauses(b, lits);
add_clauses(b, lits);
return true;
}

9
src/sat/sat_model_converter.cpp
View file

@ -275,14 +275,7 @@ namespace sat {
}
std::ostream& model_converter::display(std::ostream& out, entry const& entry) const {
out << " (";
switch (entry.get_kind()) {
case ELIM_VAR: out << "elim"; break;
case BLOCK_LIT: out << "blocked"; break;
case CCE: out << "cce"; break;
case ACCE: out << "acce"; break;
}
out << " " << entry.var();
out << " (" << entry.get_kind() << " " << entry.var();
bool start = true;
unsigned index = 0;
for (literal l : entry.m_clauses) {

10
src/sat/sat_model_converter.h
View file

@ -134,6 +134,16 @@ namespace sat {
void expand(literal_vector& update_stack);
};
inline std::ostream& operator<<(std::ostream& out, model_converter::kind k) {
switch (k) {
case model_converter::ELIM_VAR: out << "elim"; break;
case model_converter::BLOCK_LIT: out << "blocked"; break;
case model_converter::CCE: out << "cce"; break;
case model_converter::ACCE: out << "acce"; break;
}
return out;
}
};
#endif

2
src/sat/sat_simplifier.cpp
View file

@ -1818,6 +1818,7 @@ namespace sat {
if (s.m_config.m_drat) s.m_drat.add(*new_c, true);
s.m_clauses.push_back(new_c);
m_use_list.insert(*new_c);
if (m_sub_counter > 0)
back_subsumption1(*new_c);
@ -1829,6 +1830,7 @@ namespace sat {
return true;
}
}
return true;
}

4
src/sat/sat_solver.cpp
View file

@ -3225,7 +3225,9 @@ namespace sat {
literal l2 = w.get_literal();
if (l.index() > l2.index())
continue;
out << "(" << l << " " << l2 << ")\n";
out << "(" << l << " " << l2 << ")";
if (w.is_learned()) out << "*";
out << "\n";
}
}
}

3
src/sat/tactic/goal2sat.cpp
View file

@ -142,6 +142,7 @@ struct goal2sat::imp {
sat::bool_var v = m_solver.mk_var(ext);
m_map.insert(t, v);
l = sat::literal(v, sign);
// if (to_app(t)->get_decl()->get_name() == "XX") IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(t, m) << ": " << "v" << v << "\n";);
TRACE("sat", tout << "new_var: " << v << ": " << mk_ismt2_pp(t, m) << "\n";);
if (ext && !is_uninterp_const(t)) {
m_interpreted_atoms.push_back(t);
@ -1025,6 +1026,7 @@ void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) {
expr_ref sat2goal::mc::lit2expr(sat::literal l) {
if (!m_var2expr.get(l.var())) {
app* aux = m.mk_fresh_const(0, m.mk_bool_sort());
// if (aux->get_decl()->get_name() == "k!81740") IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(aux, m) << ": " << "v" << l.var() << "\n";);
m_var2expr.set(l.var(), aux);
}
VERIFY(m_var2expr.get(l.var()));
@ -1067,6 +1069,7 @@ struct sat2goal::imp {
app* aux = mc ? mc->var2expr(l.var()) : nullptr;
if (!aux) {
aux = m.mk_fresh_const(0, m.mk_bool_sort());
// if (aux->get_decl()->get_name() == "k!81740") IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(aux, m) << ": " << "v" << l.var() << "\n";);
if (mc)
mc->insert(l.var(), aux, true);
}