mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 20:31:21 +00:00
Code Activity

Fix in proof_util:elim_aux_assertions

Browse source 
Replace assertions/hypotheses of aux variables with PR_TRUE.
Rebuild unit resolution as needed.
This makes the transformation stable against new proof rules.
This commit is contained in:
Arie Gurfinkel 2018-07-02 21:37:30 -04:00
parent 5d1149adb2
commit 8502f1fe36
1 changed files with 17 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/ast/proofs/proof_utils.h
View file

@ -164,10 +164,12 @@ public:
// skip (asserted m_aux) // skip (asserted m_aux)
else if (m.is_asserted(arg, a) && a == m_aux.get()) { else if (m.is_asserted(arg, a) && a == m_aux.get()) {
dirty = true; dirty = true;
args.push_back(m.mk_true_proof());
} }
// skip (hypothesis m_aux) // skip (hypothesis m_aux)
else if (m.is_hypothesis(arg, a) && a == m_aux.get()) { else if (m.is_hypothesis(arg, a) && a == m_aux.get()) {
dirty = true; dirty = true;
args.push_back(m.mk_true_proof());
} else if (is_app(arg) && cache.find(to_app(arg), r)) { } else if (is_app(arg) && cache.find(to_app(arg), r)) {
dirty |= (arg != r); dirty |= (arg != r);
args.push_back(r); args.push_back(r);
@ -188,13 +190,18 @@ public:
app_ref newp(m); app_ref newp(m);
if (!dirty) { newp = p; } if (!dirty) { newp = p; }
else if (m.is_unit_resolution(p)) { else if (m.is_unit_resolution(p)) {
if (args.size() == 2) ptr_buffer<proof> parents;
// unit resolution with m_aux that got collapsed to nothing for (unsigned i = 0, sz = args.size() - 1; i < sz; ++i) {
{ newp = to_app(args.get(0)); } app *arg = to_app(args.get(i));
if (!m.is_true(m.get_fact(arg)))
parents.push_back(arg);
}
// unit resolution that collapsed to nothing
if (parents.size() == 1) {
newp = parents.get(0);
}
else { else {
ptr_vector<proof> parents; // rebuild unit resolution
for (unsigned i = 0, sz = args.size() - 1; i < sz; ++i)
{ parents.push_back(to_app(args.get(i))); }
SASSERT(parents.size() == args.size() - 1); SASSERT(parents.size() == args.size() - 1);
newp = m.mk_unit_resolution(parents.size(), parents.c_ptr()); newp = m.mk_unit_resolution(parents.size(), parents.c_ptr());
// XXX the old and new facts should be // XXX the old and new facts should be
@ -203,9 +210,11 @@ public:
SASSERT(m.get_fact(newp) == args.back()); SASSERT(m.get_fact(newp) == args.back());
pinned.push_back(newp); pinned.push_back(newp);
} }
} else if (matches_fact(args, a)) { }
else if (matches_fact(args, a)) {
newp = to_app(a); newp = to_app(a);
} else { }
else {
expr_ref papp(m); expr_ref papp(m);
mk_app(p->get_decl(), args, papp); mk_app(p->get_decl(), args, papp);
newp = to_app(papp.get()); newp = to_app(papp.get());