From f004478565fe29eaf28cf48d328841e803e57a29 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 6 Nov 2022 12:00:25 -0800 Subject: [PATCH] produce tseitin justification for clause proofs when a clause is a "gate". --- src/smt/smt_internalizer.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 2483b2ca4..63848418f 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1593,6 +1593,18 @@ namespace smt { TRACE("gate_clause", tout << mk_ll_pp(pr, m);); mk_clause(num_lits, lits, mk_justification(justification_proof_wrapper(*this, pr))); } + else if (m_clause_proof.on_clause_active()) { + ptr_buffer 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 { mk_clause(num_lits, lits, nullptr); }