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

bypass built-in proof objects for clause trail

Browse source 
the build-in proof constructors are not flexible when it comes to allowing alternation of justified lemmas and lemmas without justifications.
This commit is contained in:
Nikolaj Bjorner 2022-11-06 11:59:56 -08:00
parent 8ff1e44a95
commit 53b6059276
1 changed files with 8 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/smt/smt_clause_proof.cpp
View file

@ -147,18 +147,22 @@ namespace smt {
for (auto& info : m_trail) { for (auto& info : m_trail) {
expr_ref fact = mk_or(info.m_clause); expr_ref fact = mk_or(info.m_clause);
proof* pr = info.m_proof; proof* pr = info.m_proof;
expr* args[2] = { pr, fact };
unsigned num_args = 2, offset = 0;
if (!pr)
offset = 1;
switch (info.m_status) { switch (info.m_status) {
case status::assumption: case status::assumption:
ps.push_back(m.mk_assumption_add(pr, fact)); ps.push_back(m.mk_app(symbol("assumption"), num_args - offset, args + offset, m.mk_proof_sort()));
break; break;
case status::lemma: case status::lemma:
ps.push_back(m.mk_lemma_add(pr, fact)); ps.push_back(m.mk_app(symbol("lemma"), num_args - offset, args + offset, m.mk_proof_sort()));
break; break;
case status::th_assumption: case status::th_assumption:
ps.push_back(m.mk_th_assumption_add(pr, fact)); ps.push_back(m.mk_app(symbol("th-assumption"), num_args - offset, args + offset, m.mk_proof_sort()));
break; break;
case status::th_lemma: case status::th_lemma:
ps.push_back(m.mk_th_lemma_add(pr, fact)); ps.push_back(m.mk_app(symbol("th-lemma"), num_args - offset, args + offset, m.mk_proof_sort()));
break; break;
case status::deleted: case status::deleted:
ps.push_back(m.mk_redundant_del(fact)); ps.push_back(m.mk_redundant_del(fact));