From 0c9662c76bce118996f839c5889b6bb0d1965044 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 4 Aug 2021 17:11:08 -0500 Subject: [PATCH] Fix policy for merging subproofs (#6981) This makes it so that we replace subproof A with subproof B if A and B prove the same thing, and B contains no assumptions. This is independent of the scope that A and B are in. The previous policy replaced subproof A with subproof B if A and B prove the same thing and were in the same scope. This is not safe if A occurs in multiple scopes, where free assumptions can escape. The new policy is more effective and safer than the previous one. --- src/proof/proof_node_updater.cpp | 76 +++++++++++++------ src/proof/proof_node_updater.h | 14 ++-- test/regress/CMakeLists.txt | 1 + .../regress1/strings/open-pf-merge.smt2 | 8 ++ 4 files changed, 69 insertions(+), 30 deletions(-) create mode 100644 test/regress/regress1/strings/open-pf-merge.smt2 diff --git a/src/proof/proof_node_updater.cpp b/src/proof/proof_node_updater.cpp index 2bdb54a45..561d4a761 100644 --- a/src/proof/proof_node_updater.cpp +++ b/src/proof/proof_node_updater.cpp @@ -69,15 +69,25 @@ void ProofNodeUpdater::process(std::shared_ptr pf) } } } - std::vector> traversing; - processInternal(pf, d_freeAssumps, traversing); + processInternal(pf, d_freeAssumps); } -void ProofNodeUpdater::processInternal( - std::shared_ptr pf, - const std::vector& fa, - std::vector>& traversing) +void ProofNodeUpdater::processInternal(std::shared_ptr pf, + std::vector& fa) { + // Note that processInternal uses a single scope; fa is updated based on + // the current free assumptions of the proof nodes on the stack. + + // The list of proof nodes we are currently traversing beneath. This is used + // for checking for cycles in the overall proof. + std::vector> traversing; + // Map from formulas to (closed) proof nodes that prove that fact + std::map> resCache; + // Map from formulas to non-closed proof nodes that prove that fact. These + // are replaced by proofs in the above map when applicable. + std::map>> resCacheNcWaiting; + // Map from proof nodes to whether they contain assumptions + std::unordered_map cfaMap; Trace("pf-process") << "ProofNodeUpdater::process" << std::endl; std::unordered_map, bool> visited; std::unordered_map, bool>::iterator it; @@ -85,10 +95,6 @@ void ProofNodeUpdater::processInternal( std::shared_ptr cur; visit.push_back(pf); std::map>::iterator itc; - // A cache from formulas to proof nodes that are in the current scope. - // Notice that we make a fresh recursive call to process if the current - // rule is SCOPE below. - std::map> resCache; Node res; do { @@ -106,6 +112,9 @@ void ProofNodeUpdater::processInternal( // already have a proof, merge it into this one visited[cur] = true; d_pnm->updateNode(cur.get(), itc->second.get()); + // does not contain free assumptions since the range of resCache does + // not contain free assumptions + cfaMap[cur.get()] = false; continue; } } @@ -121,7 +130,7 @@ void ProofNodeUpdater::processInternal( // no further changes should be made to cur according to the callback Trace("pf-process-debug") << "...marked to not continue update." << std::endl; - runFinalize(cur, fa, resCache); + runFinalize(cur, fa, resCache, resCacheNcWaiting, cfaMap); continue; } traversing.push_back(cur); @@ -131,16 +140,10 @@ void ProofNodeUpdater::processInternal( // 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 (cur->getRule() == PfRule::SCOPE) { - std::vector nfa; - nfa.insert(nfa.end(), fa.begin(), fa.end()); const std::vector& 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; + fa.insert(fa.end(), args.begin(), args.end()); } const std::vector>& ccp = cur->getChildren(); // now, process children @@ -163,7 +166,13 @@ void ProofNodeUpdater::processInternal( traversing.pop_back(); visited[cur] = true; // finalize the node - runFinalize(cur, fa, resCache); + if (cur->getRule() == PfRule::SCOPE) + { + const std::vector& args = cur->getArguments(); + Assert(fa.size() >= args.size()); + fa.resize(fa.size() - args.size()); + } + runFinalize(cur, fa, resCache, resCacheNcWaiting, cfaMap); } } while (!visit.empty()); Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl; @@ -227,13 +236,34 @@ bool ProofNodeUpdater::runUpdate(std::shared_ptr cur, void ProofNodeUpdater::runFinalize( std::shared_ptr cur, const std::vector& fa, - std::map>& resCache) + std::map>& resCache, + std::map>>& resCacheNcWaiting, + std::unordered_map& cfaMap) { if (d_mergeSubproofs) { Node res = cur->getResult(); - // cache result if we are merging subproofs - resCache[res] = cur; + // cache the result if we don't contain an assumption + if (!expr::containsAssumption(cur.get(), cfaMap)) + { + // cache result if we are merging subproofs + resCache[res] = cur; + // go back and merge into the non-closed proofs of the same fact + std::map>>::iterator itnw = + resCacheNcWaiting.find(res); + if (itnw != resCacheNcWaiting.end()) + { + for (std::shared_ptr& ncp : itnw->second) + { + d_pnm->updateNode(ncp.get(), cur.get()); + } + resCacheNcWaiting.erase(res); + } + } + else + { + resCacheNcWaiting[res].push_back(cur); + } } if (d_debugFreeAssumps) { diff --git a/src/proof/proof_node_updater.h b/src/proof/proof_node_updater.h index 6b8841e67..603583715 100644 --- a/src/proof/proof_node_updater.h +++ b/src/proof/proof_node_updater.h @@ -122,12 +122,8 @@ class ProofNodeUpdater * @param fa The assumptions of the scope that fa is a subproof of with * respect to the original proof. For example, if (SCOPE P :args (A B)), we * may call this method on P with fa = { A, B }. - * @param traversing The list of proof nodes we are currently traversing - * beneath. This is used for checking for cycles in the overall proof. */ - void processInternal(std::shared_ptr pf, - const std::vector& fa, - std::vector>& traversing); + void processInternal(std::shared_ptr pf, std::vector& fa); /** * Update proof node cur based on the callback. This modifies curr using * ProofNodeManager::updateNode based on the proof node constructed to @@ -141,11 +137,15 @@ class ProofNodeUpdater /** * Finalize the node cur. This is called at the moment that it is established * that cur will appear in the final proof. We do any final debug checking - * and add it to the results cache resCache if we are merging subproofs. + * and add it to resCache/resCacheNcWaiting if we are merging subproofs, where + * these map result formulas to proof nodes with/without assumptions. */ void runFinalize(std::shared_ptr cur, const std::vector& fa, - std::map>& resCache); + std::map>& resCache, + std::map>>& + resCacheNcWaiting, + std::unordered_map& cfaMap); /** Are we debugging free assumptions? */ bool d_debugFreeAssumps; /** The initial free assumptions */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 87512e35b..2f807d939 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2193,6 +2193,7 @@ set(regress_1_tests regress1/strings/norn-simp-rew-sat.smt2 regress1/strings/nt6-dd.smt2 regress1/strings/nterm-re-inter-sigma.smt2 + regress1/strings/open-pf-merge.smt2 regress1/strings/pierre150331.smt2 regress1/strings/policy_variable.smt2 regress1/strings/pre_ctn_no_skolem_share.smt2 diff --git a/test/regress/regress1/strings/open-pf-merge.smt2 b/test/regress/regress1/strings/open-pf-merge.smt2 new file mode 100644 index 000000000..645ea4797 --- /dev/null +++ b/test/regress/regress1/strings/open-pf-merge.smt2 @@ -0,0 +1,8 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-const x String) +(declare-const y String) +(assert (not (str.prefixof "ab" x))) +(assert (and (str.prefixof y (str.substr x 1 (str.len x))) (str.prefixof "bb" y))) +(assert (str.prefixof "a" x)) +(check-sat) -- 2.30.2