mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

produce tseitin justification for clause proofs when a clause is a "gate".

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-06 12:00:25 -08:00
parent 53b6059276
commit f004478565
1 changed files with 12 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/smt/smt_internalizer.cpp
View file

@ -1593,6 +1593,18 @@ namespace smt {
TRACE("gate_clause", tout << mk_ll_pp(pr, m);); TRACE("gate_clause", tout << mk_ll_pp(pr, m););
mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr))); mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr)));
} }
else if (m_clause_proof.on_clause_active()) {
ptr_buffer<expr> new_lits;
for (unsigned i = 0; i < num_lits; i++) {
literal l = lits[i];
bool_var v = l.var();
expr * atom = m_bool_var2expr[v];
new_lits.push_back(l.sign() ? m.mk_not(atom) : atom);
}
// expr* fact = m.mk_or(new_lits);
proof* pr = m.mk_app(symbol("tseitin"), new_lits.size(), new_lits.data(), m.mk_proof_sort());
mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr)));
}
else { else {
mk_clause(num_lits, lits, nullptr); mk_clause(num_lits, lits, nullptr);
} }