mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fixes to trim

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-10-07 09:58:04 +02:00
parent a792251a82
commit 5c9f69829b
3 changed files with 65 additions and 33 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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";
}
}

77
src/sat/sat_proof_trim.cpp
View file

@ -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());

4
src/sat/sat_proof_trim.h
View file

@ -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: