diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-04-07 18:17:33 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-07 21:17:33 +0000 |
commit | 8d62f892ddc6ca1b38b3efb2134f12d5678d21ad (patch) | |
tree | 955f14b7b9f4769ae7363395b5051eb1ad0f04e8 /src/expr | |
parent | c35aad2ce7ffe910200906d7758a41c0cf70dfe5 (diff) |
[proof-new] Fixing SMT post-processor's handling of assumptions (#6277)
Previously the SMT post-processor would update any assumption as long as it
had a proof for it. This can be a problem when one as assumption introduced in a
scope that should not be expanded. This commit fixes the issue by adding the
option of configuring a proof node updater to track scopes and the assumptions
they introduce, which can be used to determine the prood nodes which should be
updated. It also changes the SMT post-processor to only update assumptions that
have not been introduced in some scope.
This commit fixes an issue found by @Lachnitt during the integration of CVC4 and Isabelle.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/proof_node_updater.cpp | 41 | ||||
-rw-r--r-- | src/expr/proof_node_updater.h | 2 |
2 files changed, 19 insertions, 24 deletions
diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp index 933e5b999..cbd457cd7 100644 --- a/src/expr/proof_node_updater.cpp +++ b/src/expr/proof_node_updater.cpp @@ -125,28 +125,21 @@ void ProofNodeUpdater::processInternal( } traversing.push_back(cur); visit.push_back(cur); - if (d_mergeSubproofs) + // If we are not the top-level proof, we were a scope, or became a scope + // after updating, we do a separate recursive call to this method. This + // allows us to properly track the assumptions in scope, which is + // important for example to merge or to determine updates based on free + // assumptions. + if (cur->getRule() == PfRule::SCOPE && cur != pf) { - // If we are not the top-level proof, we were a scope, or became a - // scope after updating, we need to make a separate recursive call to - // this method. This is not necessary if we are not merging subproofs. - if (cur->getRule() == PfRule::SCOPE && cur != pf) - { - std::vector<Node> nfa; - // if we are debugging free assumptions, update the set - if (d_debugFreeAssumps) - { - nfa.insert(nfa.end(), fa.begin(), fa.end()); - const std::vector<Node>& args = cur->getArguments(); - nfa.insert(nfa.end(), args.begin(), args.end()); - Trace("pfnu-debug2") - << "Process new scope with " << args << std::endl; - } - // Process in new call separately, since we should not cache - // the results of proofs that have a different scope. - processInternal(cur, nfa, traversing); - continue; - } + std::vector<Node> nfa; + nfa.insert(nfa.end(), fa.begin(), fa.end()); + const std::vector<Node>& args = cur->getArguments(); + nfa.insert(nfa.end(), args.begin(), args.end()); + Trace("pfnu-debug2") << "Process new scope with " << args << std::endl; + // Process in new call separately + processInternal(cur, nfa, traversing); + continue; } const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren(); // now, process children @@ -180,7 +173,7 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur, bool& continueUpdate) { // should it be updated? - if (!d_cb.shouldUpdate(cur, continueUpdate)) + if (!d_cb.shouldUpdate(cur, fa, continueUpdate)) { return false; } @@ -196,9 +189,9 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr<ProofNode> cur, // store in the proof cpf.addProof(cp); } - Trace("pf-process-debug") - << "Updating (" << cur->getRule() << ")..." << std::endl; Node res = cur->getResult(); + Trace("pf-process-debug") + << "Updating (" << cur->getRule() << "): " << res << std::endl; // only if the callback updated the node if (d_cb.update(res, id, ccn, cur->getArguments(), &cpf, continueUpdate)) { diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h index 8e30f14d2..268fcda5e 100644 --- a/src/expr/proof_node_updater.h +++ b/src/expr/proof_node_updater.h @@ -41,10 +41,12 @@ class ProofNodeUpdaterCallback /** Should proof pn be updated? * * @param pn the proof node that maybe should be updated + * @param fa the assumptions in scope * @param continueUpdate whether we should continue recursively updating pn * @return whether we should run the update method on pn */ virtual bool shouldUpdate(std::shared_ptr<ProofNode> pn, + const std::vector<Node>& fa, bool& continueUpdate) = 0; /** * Update the proof rule application, store steps in cdp. Return true if |