From 4e780d0cc84570df7e711643d471677a80c3ecc2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 5 Oct 2022 05:43:48 +0200 Subject: [PATCH] trim Signed-off-by: Nikolaj Bjorner --- src/cmd_context/extra_cmds/proof_cmds.cpp | 48 ++++++-- src/sat/sat_proof_trim.cpp | 132 +++++++++++----------- src/sat/sat_proof_trim.h | 11 +- 3 files changed, 116 insertions(+), 75 deletions(-) diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp index e464e6ecb..1e675aecc 100644 --- a/src/cmd_context/extra_cmds/proof_cmds.cpp +++ b/src/cmd_context/extra_cmds/proof_cmds.cpp @@ -189,7 +189,9 @@ class proof_trim { cmd_context& ctx; ast_manager& m; sat::proof_trim trim; - + vector m_clauses; + bool_vector m_is_infer; + void mk_clause(expr_ref_vector const& clause) { trim.init_clause(); for (expr* arg: clause) @@ -214,9 +216,11 @@ public: trim(gparams::get_module("sat"), m.limit()) { } - void assume(expr_ref_vector const& _clause, bool is_initial = true) { - mk_clause(_clause); - trim.assume(true); + void assume(expr_ref_vector const& clause) { + mk_clause(clause); + trim.assume(m_clauses.size()); + m_clauses.push_back(clause); + m_is_infer.push_back(false); } void del(expr_ref_vector const& _clause) { @@ -224,14 +228,42 @@ public: trim.del(); } - void infer(expr_ref_vector const& _clause, app*) { - mk_clause(_clause); - trim.infer(); + void infer(expr_ref_vector const& clause, app* hint) { + mk_clause(clause); + trim.infer(m_clauses.size()); + m_clauses.push_back(clause); + if (hint) + m_clauses.back().push_back(hint); + m_is_infer.push_back(true); } void updt_params(params_ref const& p) { trim.updt_params(p); - } + } + + void do_trim(std::ostream& out) { + ast_pp_util pp(m); + auto ids = trim.trim(); + for (unsigned id : ids) { + auto const& clause = m_clauses[id]; + bool is_infer = m_is_infer[id]; + for (expr* e : clause) + pp.collect(e); + pp.display_decls(out); + for (expr* e : clause) + pp.define_expr(out, e); + + if (!is_infer) + out << "(assume "; + else + out << "(infer"; + for (expr* e : clause) + pp.display_expr_def(out << " ", e); + out << ")\n"; + } + } + + }; class proof_saver { diff --git a/src/sat/sat_proof_trim.cpp b/src/sat/sat_proof_trim.cpp index be581eec7..522b91cdc 100644 --- a/src/sat/sat_proof_trim.cpp +++ b/src/sat/sat_proof_trim.cpp @@ -29,12 +29,13 @@ namespace sat { Output: reduced trail - result */ - vector proof_trim::trim() { - vector result; + unsigned_vector proof_trim::trim() { + unsigned_vector result; m_core_literals.reset(); m_core_literals.insert(literal_vector()); + m_propagated.resize(num_vars(), false); for (unsigned i = m_trail.size(); i-- > 0; ) { - auto const& [cl, clp, is_add, is_initial] = m_trail[i]; + auto const& [id, cl, clp, is_add, is_initial] = m_trail[i]; if (!is_add) { revive(cl, clp); continue; @@ -43,7 +44,7 @@ namespace sat { del(cl, clp); if (!in_core(cl, clp)) continue; - result.push_back(cl); + result.push_back(id); if (is_initial) continue; conflict_analysis_core(cl, clp); @@ -73,15 +74,15 @@ namespace sat { (l1 == cl[2] && l2 == cl[0] && l3 == cl[1])); } - /** - * cl is on the trail if there is some literal l that is implied by cl - * Remove all clauses after cl that are in the cone of influence of cl. - * The coi is defined inductively: C is in coi of cl if it contains ~l - * or it contains ~l' where l' is implied by a clause in the coi of cl. - * Possible optimization: - * - check if clause contains a literal that is on implied on the trail - * if it doesn't contain any such literal, bypass the trail adjustment. - */ + /** + * cl is on the trail if there is some literal l that is implied by cl + * Remove all clauses after cl that are in the cone of influence of cl. + * The coi is defined inductively: C is in coi of cl if it contains ~l + * or it contains ~l' where l' is implied by a clause in the coi of cl. + * Possible optimization: + * - check if clause contains a literal that is on implied on the trail + * if it doesn't contain any such literal, bypass the trail adjustment. + */ void proof_trim::prune_trail(literal_vector const& cl, clause* cp) { m_in_clause.reset(); @@ -89,6 +90,12 @@ namespace sat { for (literal lit : cl) m_in_clause.insert(lit.index()); + + auto unassign_literal = [&](literal l) { + m_in_coi.insert((~l).index()); + s.m_assignment[l.index()] = l_undef; + s.m_assignment[(~l).index()] = l_undef; + }; bool on_trail = false; unsigned j = 0; @@ -97,9 +104,7 @@ namespace sat { if (m_in_clause.contains(l.index())) { SASSERT(!on_trail); on_trail = true; - m_in_coi.insert((~l).index()); - s.m_assignment[l.index()] = l_undef; - s.m_assignment[(~l).index()] = l_undef; + unassign_literal(l); continue; } if (!on_trail) { @@ -119,11 +124,8 @@ namespace sat { else UNREACHABLE(); // approach does not work for external justifications - if (in_coi) { - m_in_coi.insert((~l).index()); - s.m_assignment[l.index()] = l_undef; - s.m_assignment[(~l).index()] = l_undef; - } + if (in_coi) + unassign_literal(l); else s.m_trail[j++] = s.m_trail[i]; } @@ -171,52 +173,59 @@ namespace sat { s.propagate(false); } SASSERT(s.inconsistent()); - - auto add_dependency = [&](literal lit) { - bool_var v = lit.var(); - if (s.lvl(v) == 0) { - // inefficient for repeated insertions ? - auto j = s.m_justification[v]; - literal lit = literal(v, s.value(v) == l_false); - add_core(lit, j); - } - else if (s.lvl(v) == 2) - s.mark(v); - }; - - auto add_jdependency = [&](justification j) { - switch (j.get_kind()) { - case justification::BINARY: - add_dependency(j.get_literal()); - break; - case justification::TERNARY: - add_dependency(j.get_literal1()); - add_dependency(j.get_literal2()); - break; - case justification::CLAUSE: - for (auto lit : s.get_clause(j)) - if (s.value(lit) == l_false) - add_dependency(lit); - break; - default: - break; - } - }; + for (unsigned i = trail_size0; i < s.m_trail.size(); ++i) + m_propagated[s.m_trail[i].var()] = true; if (s.m_not_l != null_literal) add_dependency(s.m_not_l); - add_jdependency(s.m_conflict); + add_dependency(s.m_conflict); for (unsigned i = s.m_trail.size(); i-- > trail_size0; ) { bool_var v = s.m_trail[i].var(); + m_propagated[v] = false; if (!s.is_marked(v)) continue; s.reset_mark(v); - add_jdependency(s.m_justification[v]); + add_dependency(s.get_justification(v)); } s.pop(2); } + 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 + // inefficient for repeated insertions ? + auto j = s.get_justification(v); + literal lit = literal(v, s.value(v) == l_false); + add_core(lit, j); + } + } + + void proof_trim::add_dependency(justification j) { + switch (j.get_kind()) { + case justification::BINARY: + add_dependency(j.get_literal()); + break; + case justification::TERNARY: + add_dependency(j.get_literal1()); + add_dependency(j.get_literal2()); + break; + case justification::CLAUSE: + for (auto lit : s.get_clause(j)) + if (s.value(lit) == l_false) + add_dependency(lit); + break; + case justification::EXT_JUSTIFICATION: + UNREACHABLE(); + break; + default: + break; + } + } + + void proof_trim::add_core(literal l, justification j) { m_clause.reset(); switch (j.get_kind()) { @@ -256,7 +265,6 @@ namespace sat { s.mk_clause(cl, status::redundant()); } - clause* proof_trim::del(literal_vector const& cl) { clause* cp = nullptr; IF_VERBOSE(3, verbose_stream() << "del: " << cl << "\n"); @@ -283,19 +291,17 @@ namespace sat { IF_VERBOSE(3, verbose_stream() << "add: " << *cl << "\n"); auto& v = m_clauses.insert_if_not_there(lits, clause_vector()); v.push_back(cl); - } - - + } proof_trim::proof_trim(params_ref const& p, reslimit& lim): s(p, lim) {} - void proof_trim::assume(bool is_initial) { + void proof_trim::assume(unsigned id, bool is_initial) { std::sort(m_clause.begin(), m_clause.end()); IF_VERBOSE(3, verbose_stream() << "add: " << m_clause << "\n"); auto* cl = s.mk_clause(m_clause, status::redundant()); - m_trail.push_back({ m_clause, cl, true, is_initial }); + m_trail.push_back({ id, m_clause, cl, true, is_initial }); s.propagate(false); save(m_clause, cl); } @@ -303,11 +309,11 @@ namespace sat { void proof_trim::del() { std::sort(m_clause.begin(), m_clause.end()); clause* cp = del(m_clause); - m_trail.push_back({ m_clause, cp, false, true }); + m_trail.push_back({ 0, m_clause, cp, false, true }); } - void proof_trim::infer() { - assume(false); + void proof_trim::infer(unsigned id) { + assume(id, false); } diff --git a/src/sat/sat_proof_trim.h b/src/sat/sat_proof_trim.h index 4199b8386..bf0468bc9 100644 --- a/src/sat/sat_proof_trim.h +++ b/src/sat/sat_proof_trim.h @@ -33,7 +33,7 @@ namespace sat { literal_vector m_clause; uint_set m_in_clause; uint_set m_in_coi; - vector> m_trail; + vector> m_trail; struct hash { @@ -49,6 +49,7 @@ namespace sat { map m_clauses; hashtable m_core_literals; + bool_vector m_propagated; void del(literal_vector const& cl, clause* cp); @@ -57,6 +58,8 @@ 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(literal l, justification j); bool in_core(literal_vector const& cl, clause* cp) const; void revive(literal_vector const& cl, clause* cp); @@ -73,12 +76,12 @@ namespace sat { void add_literal(bool_var v, bool sign) { m_clause.push_back(literal(v, sign)); } unsigned num_vars() { return s.num_vars(); } - void assume(bool is_initial = true); + void assume(unsigned id, bool is_initial = true); void del(); - void infer(); + void infer(unsigned id); void updt_params(params_ref const& p) { s.updt_params(p); } - vector trim(); + unsigned_vector trim(); }; }