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

fixes to trim

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-07-03 19:26:12 +02:00
parent 30a2ced9aa
commit d9e7b8c21f
6 changed files with 123 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

28
src/cmd_context/extra_cmds/proof_cmds.cpp
View file

@ -63,6 +63,7 @@ class proof_trim {
vector<expr_ref_vector> m_clauses;
bool_vector m_is_infer;
symbol m_rup;
bool m_empty = false;
void mk_clause(expr_ref_vector const& clause) {
trim.init_clause();
@ -121,25 +122,32 @@ public:
*/
void infer(expr_ref_vector const& clause, app* hint) {
if (m_empty)
return;
if (hint && !is_rup(hint) && m_checker.check(hint)) {
auto clause1 = m_checker.clause(hint);
if (clause1.size() != clause.size()) {
mk_clause(clause1);
trim.assume(m_clauses.size());
clause1.push_back(hint);
trim.assume(m_clauses.size());
m_clauses.push_back(clause1);
m_is_infer.push_back(true);
mk_clause(clause);
trim.infer(m_clauses.size());
m_clauses.push_back(clause);
m_clauses.back().push_back(hint);
m_is_infer.push_back(true);
if (clause.empty())
m_is_infer.push_back(false);
if (clause.empty()) {
mk_clause(clause);
trim.infer(m_clauses.size());
m_clauses.push_back(clause);
m_clauses.back().push_back(hint);
m_is_infer.push_back(true);
m_empty = true;
do_trim(std::cout);
}
return;
}
}
mk_clause(clause);
if (is_rup(hint))
trim.infer(m_clauses.size());
@ -149,8 +157,10 @@ public:
if (hint)
m_clauses.back().push_back(hint);
m_is_infer.push_back(true);
if (clause.empty())
if (clause.empty()) {
m_empty = true;
do_trim(std::cout);
}
}
void updt_params(params_ref const& p) {

4
src/sat/sat_integrity_checker.cpp
View file

@ -28,7 +28,7 @@ namespace sat {
}
// for nary clauses
static bool contains_watched(watch_list const & wlist, clause const & c, clause_offset cls_off) {
bool integrity_checker::contains_watched(watch_list const & wlist, clause const & c, clause_offset cls_off) const {
for (watched const& w : wlist) {
if (w.is_clause()) {
if (w.get_clause_offset() == cls_off) {
@ -38,6 +38,8 @@ namespace sat {
}
}
}
TRACE("sat", tout << "clause " << c << " not found in watch-list\n");
TRACE("sat", s.display_watches(tout));
UNREACHABLE();
return false;
}

1
src/sat/sat_integrity_checker.h
View file

@ -25,6 +25,7 @@ Revision History:
namespace sat {
class integrity_checker {
solver const & s;
bool contains_watched(watch_list const & wlist, clause const & c, clause_offset cls_off) const;
public:
integrity_checker(solver const & s);

116
src/sat/sat_proof_trim.cpp
View file

@ -32,21 +32,33 @@ namespace sat {
unsigned_vector proof_trim::trim() {
unsigned_vector result;
m_core_literals.reset();
m_propagated.resize(num_vars(), false);
m_core_literals.insert(literal_vector());
m_propagated.resize(num_vars(), false);
for (unsigned i = m_trail.size(); i-- > 0; ) {
m_core_literals.insert(m_conflict);
conflict_analysis_core(m_conflict, m_conflict_clause);
IF_VERBOSE(10, s.display(verbose_stream() << "trim\n"));
auto const& [id, cl, clp, is_add, is_initial] = m_trail.back();
SASSERT(cl.empty());
result.push_back(id);
m_trail.pop_back();
for (unsigned i = m_trail.size(); i-- > 0; ) {
auto const& [id, cl, clp, is_add, is_initial] = m_trail[i];
if (!is_add) {
revive(cl, clp);
continue;
}
}
IF_VERBOSE(10, s.display(verbose_stream()));
prune_trail(cl, clp);
IF_VERBOSE(10, verbose_stream() << cl << " " << in_core(cl, clp) << ": "; for (auto const& c : m_core_literals) verbose_stream() << "{" << c << "} ");
IF_VERBOSE(10, s.display(verbose_stream() << "\n"));
del(cl, clp);
if (!in_core(cl, clp))
if (!in_core(cl, clp))
continue;
IF_VERBOSE(4, verbose_stream() << cl << " in-core " << in_core(cl, clp) << ": "; for (auto const& c : m_core_literals) verbose_stream() << "{" << c << "} "; verbose_stream() << "\n");
result.push_back(id);
if (is_initial)
continue;
@ -57,6 +69,7 @@ namespace sat {
}
void proof_trim::del(literal_vector const& cl, clause* cp) {
CTRACE("sat", cp, tout << "del " << *cp << "\n");
if (cp)
s.detach_clause(*cp);
else
@ -90,6 +103,8 @@ namespace sat {
void proof_trim::prune_trail(literal_vector const& cl, clause* cp) {
m_in_clause.reset();
m_in_coi.reset();
// verbose_stream() << "prune trail " << cl << "\n";
if (cl.empty())
return;
@ -120,13 +135,23 @@ namespace sat {
auto js = s.get_justification(l);
bool in_coi = false;
//verbose_stream() << l << " " << js << "\n";
if (js.is_clause())
for (literal lit : s.get_clause(j))
for (literal lit : s.get_clause(js))
in_coi |= m_in_coi.contains(lit.index());
else if (js.is_binary_clause())
in_coi = m_in_coi.contains(js.get_literal().index());
else
else if (js.is_none()) {
verbose_stream() << "none " << js << "\n";
}
else if (js.is_ext_justification()) {
verbose_stream() << js << "\n";
UNREACHABLE(); // approach does not work for external justifications
}
else {
verbose_stream() << js << "\n";
UNREACHABLE(); // approach does not work for external justifications
}
if (in_coi)
unassign_literal(l);
@ -134,6 +159,7 @@ namespace sat {
s.m_trail[j++] = s.m_trail[i];
}
s.m_trail.shrink(j);
// verbose_stream() << "trail after " << s.m_trail << "\n";
s.m_inconsistent = false;
s.m_qhead = s.m_trail.size();
s.propagate(false);
@ -188,11 +214,14 @@ namespace sat {
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_VERBOSE(3, s.display_justification(verbose_stream() << "conflict " << s.m_not_l << " ", s.m_conflict) << "\n");
IF_VERBOSE(3, s.display(verbose_stream()));
sat::literal l = sat::null_literal;
if (s.m_not_l != null_literal) {
add_core(~s.m_not_l, s.m_conflict);
add_dependency(s.m_not_l);
l = ~s.m_not_l;
}
add_core(l, s.m_conflict);
add_dependency(s.m_conflict);
for (unsigned i = s.m_trail.size(); i-- > trail_size0; ) {
@ -201,7 +230,7 @@ namespace sat {
if (!s.is_marked(v))
continue;
add_core(v);
s.reset_mark(v);
s.reset_mark(v);
add_dependency(s.get_justification(v));
}
if (!cl.empty())
@ -210,8 +239,10 @@ namespace sat {
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);
if (m_propagated[v]) { // literal was propagated after assuming ~C
if (!s.is_marked(v))
s.mark(v);
}
else if (s.lvl(v) == 0) // literal depends on level 0, it is not assumed by ~C
// inefficient for repeated insertions ?
add_core(v);
@ -253,17 +284,18 @@ namespace sat {
m_clause.push_back(j.get_literal());
break;
case justification::CLAUSE:
s.get_clause(j).mark_used();
IF_VERBOSE(3, verbose_stream() << "add core " << s.get_clause(j) << "\n");
return;
for (auto lit : s.get_clause(j))
m_clause.push_back(lit);
break;
default:
verbose_stream() << j << "\n";
UNREACHABLE();
break;
}
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) {
if (l != null_literal && s.lvl(l) == 0) {
m_clause.reset();
m_clause.push_back(l);
m_core_literals.insert(m_clause);
@ -271,10 +303,7 @@ namespace sat {
}
bool proof_trim::in_core(literal_vector const& cl, clause* cp) const {
if (cp)
return cp->was_used();
else
return m_core_literals.contains(cl);
return m_core_literals.contains(cl);
}
void proof_trim::revive(literal_vector const& cl, clause* cp) {
@ -286,7 +315,7 @@ namespace sat {
clause* proof_trim::del(literal_vector const& cl) {
clause* cp = nullptr;
IF_VERBOSE(3, verbose_stream() << "del: " << cl << "\n");
TRACE("sat", tout << "del: " << cl << "\n");
if (cl.size() == 2) {
s.detach_bin_clause(cl[0], cl[1], true);
return cp;
@ -297,7 +326,7 @@ namespace sat {
auto& v = e->get_data().m_value;
if (!v.empty()) {
cp = v.back();
IF_VERBOSE(3, verbose_stream() << "del: " << *cp << "\n");
TRACE("sat", tout << "del: " << *cp << "\n");
s.detach_clause(*cp);
v.pop_back();
}
@ -317,14 +346,57 @@ namespace sat {
s.set_trim();
}
proof_trim::~proof_trim() {
}
void proof_trim::assume(unsigned id, bool is_initial) {
std::sort(m_clause.begin(), m_clause.end());
if (unit_or_binary_occurs())
return;
if (!m_conflict.empty() && m_clause.empty())
m_trail.push_back({id , m_clause, nullptr, true, is_initial});
if (!m_conflict.empty())
return;
IF_VERBOSE(3, verbose_stream() << (is_initial?"assume ":"rup ") << m_clause << "\n");
auto* cl = s.mk_clause(m_clause, status::redundant());
auto is_unit2 = [&]() {
if (s.value(m_clause[0]) == l_false) {
std::swap(m_clause[0], m_clause[1]);
return true;
}
return s.value(m_clause[1]) == l_false;
};
auto is_unit = [&]() {
unsigned undef_idx = m_clause.size();
for (unsigned i = 0; i < m_clause.size(); ++i) {
sat::literal lit = (*cl)[i];
if (s.value(lit) != l_undef)
continue;
if (undef_idx < m_clause.size())
return false;
undef_idx = i;
}
if (undef_idx < m_clause.size()) {
std::swap((*cl)[undef_idx], (*cl)[0]);
return true;
}
return false;
};
m_trail.push_back({ id, m_clause, cl, true, is_initial });
if (m_clause.size() == 2 && is_unit2())
s.propagate_bin_clause(m_clause[0], m_clause[1]);
else if (m_clause.size() > 2 && is_unit())
s.propagate_clause(*cl, true, 0, s.cls_allocator().get_offset(cl));
s.propagate(false);
// verbose_stream() << m_clause << " - " << s.inconsistent() << "\n";
if (s.inconsistent() || all_of(m_clause, [&](sat::literal lit) { return s.value(lit) == l_false; }))
set_conflict(m_clause, cl);
save(m_clause, cl);
}

5
src/sat/sat_proof_trim.h
View file

@ -30,9 +30,10 @@ namespace sat {
class proof_trim {
solver s;
literal_vector m_clause;
literal_vector m_clause, m_conflict;
uint_set m_in_clause;
uint_set m_in_coi;
clause* m_conflict_clause = nullptr;
vector<std::tuple<unsigned, literal_vector, clause*, bool, bool>> m_trail;
@ -70,10 +71,12 @@ namespace sat {
uint_set m_units;
bool unit_or_binary_occurs();
void set_conflict(literal_vector const& c, clause* cp) { m_conflict.reset(); m_conflict.append(c); m_conflict_clause = cp;}
public:
proof_trim(params_ref const& p, reslimit& lim);
~proof_trim();
bool_var mk_var() { return s.mk_var(true, true); }
void init_clause() { m_clause.reset(); }

3
src/sat/sat_solver.cpp
View file

@ -90,7 +90,7 @@ namespace sat {
solver::~solver() {
m_ext = nullptr;
SASSERT(m_config.m_num_threads > 1 || check_invariant());
SASSERT(m_config.m_num_threads > 1 || m_trim || check_invariant());
CTRACE("sat", !m_clauses.empty(), tout << "Delete clauses\n";);
del_clauses(m_clauses);
CTRACE("sat", !m_learned.empty(), tout << "Delete learned\n";);
@ -878,6 +878,7 @@ namespace sat {
m_conflict = c;
m_not_l = not_l;
TRACE("sat", display(display_justification(tout << "conflict " << not_l << " ", c) << "\n"));
TRACE("sat", display_watches(tout));
}
void solver::assign_core(literal l, justification j) {