diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp index 1e75b1590..6c4490d42 100644 --- a/src/cmd_context/extra_cmds/proof_cmds.cpp +++ b/src/cmd_context/extra_cmds/proof_cmds.cpp @@ -258,7 +258,7 @@ public: trim.assume(m_clauses.size()); clause1.push_back(hint); m_clauses.push_back(clause1); - m_is_infer.push_back(false); + m_is_infer.push_back(true); mk_clause(clause); trim.infer(m_clauses.size()); m_clauses.push_back(clause); @@ -278,7 +278,7 @@ public: m_clauses.push_back(clause); if (hint) m_clauses.back().push_back(hint); - m_is_infer.push_back(is_rup(hint)); + m_is_infer.push_back(true); if (clause.empty()) do_trim(std::cout); } @@ -295,16 +295,23 @@ public: bool is_infer = m_is_infer[id]; for (expr* e : clause) pp.collect(e); + pp.display_decls(out); - for (expr* e : clause) + for (expr* e : clause) { + m.is_not(e, e); pp.define_expr(out, e); + } if (!is_infer) out << "(assume"; else out << "(infer"; - for (expr* e : clause) - pp.display_expr_def(out << " ", e); + for (expr* e : clause) { + if (m.is_not(e, e)) + pp.display_expr_def(out << " (not ", e) << ")"; + else + pp.display_expr_def(out << " ", e); + } out << ")\n"; } } diff --git a/src/sat/sat_proof_trim.cpp b/src/sat/sat_proof_trim.cpp index 9e1ab7c06..8e3c14f94 100644 --- a/src/sat/sat_proof_trim.cpp +++ b/src/sat/sat_proof_trim.cpp @@ -171,34 +171,28 @@ namespace sat { void proof_trim::conflict_analysis_core(literal_vector const& cl, clause* cp) { IF_VERBOSE(3, verbose_stream() << "core " << cl << "\n"); - if (cl.empty()) { - add_core(~s.m_not_l, s.m_conflict); - add_core(s.m_not_l, s.get_justification(s.m_not_l)); - return; - } - SASSERT(!s.inconsistent()); - s.push(); - unsigned lvl = s.scope_lvl(); - for (auto lit : cl) - s.assign(~lit, justification(lvl)); unsigned trail_size0 = s.m_trail.size(); - s.propagate(false); - if (!s.inconsistent()) { - s.m_qhead = 0; + if (!cl.empty()) { + SASSERT(!s.inconsistent()); + s.push(); + unsigned lvl = s.scope_lvl(); + for (auto lit : cl) + s.assign(~lit, justification(lvl)); + trail_size0 = s.m_trail.size(); s.propagate(false); + if (!s.inconsistent()) { + s.m_qhead = 0; + s.propagate(false); + } + if (!s.inconsistent()) + IF_VERBOSE(0, s.display(verbose_stream())); + for (unsigned i = trail_size0; i < s.m_trail.size(); ++i) + m_propagated[s.m_trail[i].var()] = true; } - if (!s.inconsistent()) - IF_VERBOSE(0, s.display(verbose_stream())); - - SASSERT(s.inconsistent()); - for (unsigned i = trail_size0; i < s.m_trail.size(); ++i) - m_propagated[s.m_trail[i].var()] = true; - SASSERT(s.inconsistent()); IF_VERBOSE(3, verbose_stream() << s.m_not_l << " " << s.m_conflict << "\n"); if (s.m_not_l != null_literal) { - if (s.lvl(s.m_not_l) == 0) - add_core(~s.m_not_l, s.m_conflict); + add_core(~s.m_not_l, s.m_conflict); add_dependency(s.m_not_l); } add_dependency(s.m_conflict); @@ -208,22 +202,21 @@ namespace sat { m_propagated[v] = false; if (!s.is_marked(v)) continue; + add_core(v); s.reset_mark(v); add_dependency(s.get_justification(v)); } - s.pop(1); + if (!cl.empty()) + s.pop(1); } void proof_trim::add_dependency(literal lit) { bool_var v = lit.var(); if (m_propagated[v]) // literal was propagated after assuming ~C s.mark(v); - else if (s.lvl(v) == 0) { // literal depends on level 0, it is not assumed by ~C + else if (s.lvl(v) == 0) // literal depends on level 0, it is not assumed by ~C // inefficient for repeated insertions ? - auto j = s.get_justification(v); - literal lit = literal(v, s.value(v) == l_false); - add_core(lit, j); - } + add_core(v); } void proof_trim::add_dependency(justification j) { @@ -248,6 +241,12 @@ namespace sat { } } + void proof_trim::add_core(bool_var v) { + auto j = s.get_justification(v); + literal lit = literal(v, s.value(v) == l_false); + add_core(lit, j); + } + void proof_trim::add_core(literal l, justification j) { m_clause.reset(); @@ -275,6 +274,11 @@ namespace sat { std::sort(m_clause.begin(), m_clause.end()); IF_VERBOSE(3, verbose_stream() << "add core " << m_clause << "\n"); m_core_literals.insert(m_clause); + if (s.lvl(l) == 0) { + m_clause.reset(); + m_clause.push_back(l); + m_core_literals.insert(m_clause); + } } bool proof_trim::in_core(literal_vector const& cl, clause* cp) const { @@ -326,12 +330,29 @@ namespace sat { void proof_trim::assume(unsigned id, bool is_initial) { std::sort(m_clause.begin(), m_clause.end()); + if (unit_or_binary_occurs()) + return; IF_VERBOSE(3, verbose_stream() << (is_initial?"assume ":"rup ") << m_clause << "\n"); auto* cl = s.mk_clause(m_clause, status::redundant()); m_trail.push_back({ id, m_clause, cl, true, is_initial }); s.propagate(false); save(m_clause, cl); } + + /** + * Unit clauses (and binary clause) do not have multi-set semantics in the solver. + * So they should only be represented once. + */ + bool proof_trim::unit_or_binary_occurs() { + if (m_clause.size() == 1) { + literal lit = m_clause[0]; + if (m_units.contains(lit.index())) + return true; + m_units.insert(lit.index()); + } + // todo: binary? + return false; + } void proof_trim::del() { std::sort(m_clause.begin(), m_clause.end()); diff --git a/src/sat/sat_proof_trim.h b/src/sat/sat_proof_trim.h index bf0468bc9..6d996ad6e 100644 --- a/src/sat/sat_proof_trim.h +++ b/src/sat/sat_proof_trim.h @@ -58,14 +58,18 @@ namespace sat { void prune_trail(literal_vector const& cl, clause* cp); void conflict_analysis_core(literal_vector const& cl, clause* cp); + void add_dependency(literal lit); void add_dependency(justification j); + void add_core(bool_var v); void add_core(literal l, justification j); bool in_core(literal_vector const& cl, clause* cp) const; void revive(literal_vector const& cl, clause* cp); clause* del(literal_vector const& cl); void save(literal_vector const& lits, clause* cl); + uint_set m_units; + bool unit_or_binary_occurs(); public: