From 12fd4e1a87a33dc541a71747a9a3250fe3854aa9 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 31 Aug 2021 21:51:46 -0500 Subject: [PATCH] Fix issues with cyclic proofs due to double SYMM applications (#7083) Our way of constructing proofs from the equality engine in very rare cases may cause cyclic proofs due to constructing double applications of SYMM, which are not recognized as assumptions in CDProof. This is due to an interplay between LazyProofChain using an underlying CDProof as its default proof generator, where the proof chain would use the proofs from the CDProof to form a cyclic proof. This was encountered in 9 SMT-LIB benchmarks in QF_SLIA. This makes us safer in several places related to double SYMM steps. --- src/proof/lazy_proof.cpp | 9 +++- src/proof/proof.cpp | 23 +++++--- src/proof/proof_node_manager.cpp | 53 +++++++++++++++++-- src/proof/proof_node_manager.h | 13 ++++- test/regress/CMakeLists.txt | 1 + .../strings/proof-fail-083021-delta.smt2 | 12 +++++ 6 files changed, 99 insertions(+), 12 deletions(-) create mode 100644 test/regress/regress2/strings/proof-fail-083021-delta.smt2 diff --git a/src/proof/lazy_proof.cpp b/src/proof/lazy_proof.cpp index b16a8d758..eab452d49 100644 --- a/src/proof/lazy_proof.cpp +++ b/src/proof/lazy_proof.cpp @@ -100,7 +100,14 @@ std::shared_ptr LazyCDProof::getProofFor(Node fact) if (isSym) { - d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {}); + if (pgc->getRule() == PfRule::SYMM) + { + d_manager->updateNode(cur, pgc->getChildren()[0].get()); + } + else + { + d_manager->updateNode(cur, PfRule::SYMM, {pgc}, {}); + } } else { diff --git a/src/proof/proof.cpp b/src/proof/proof.cpp index 79f84135d..dc370a04d 100644 --- a/src/proof/proof.cpp +++ b/src/proof/proof.cpp @@ -97,8 +97,7 @@ std::shared_ptr CDProof::getProofSymm(Node fact) if (pf == nullptr) { Trace("cdproof") << "...fresh make symm" << std::endl; - std::shared_ptr psym = - d_manager->mkNode(PfRule::SYMM, pschild, args, fact); + std::shared_ptr psym = d_manager->mkSymm(pfs, fact); Assert(psym != nullptr); d_nodes.insert(fact, psym); return psym; @@ -411,13 +410,23 @@ bool CDProof::isAssumption(ProofNode* pn) { return true; } - else if (rule == PfRule::SYMM) + else if (rule != PfRule::SYMM) { - const std::vector>& pc = pn->getChildren(); - Assert(pc.size() == 1); - return pc[0]->getRule() == PfRule::ASSUME; + return false; } - return false; + pn = ProofNodeManager::cancelDoubleSymm(pn); + rule = pn->getRule(); + if (rule == PfRule::ASSUME) + { + return true; + } + else if (rule != PfRule::SYMM) + { + return false; + } + const std::vector>& pc = pn->getChildren(); + Assert(pc.size() == 1); + return pc[0]->getRule() == PfRule::ASSUME; } bool CDProof::isSame(TNode f, TNode g) diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp index cf19eebdf..7e41a9057 100644 --- a/src/proof/proof_node_manager.cpp +++ b/src/proof/proof_node_manager.cpp @@ -61,6 +61,18 @@ std::shared_ptr ProofNodeManager::mkAssume(Node fact) return mkNode(PfRule::ASSUME, {}, {fact}, fact); } +std::shared_ptr ProofNodeManager::mkSymm( + std::shared_ptr child, Node expected) +{ + if (child->getRule() == PfRule::SYMM) + { + Assert(expected.isNull() + || child->getChildren()[0]->getResult() == expected); + return child->getChildren()[0]; + } + return mkNode(PfRule::SYMM, {child}, {}, expected); +} + std::shared_ptr ProofNodeManager::mkTrans( const std::vector>& children, Node expected) { @@ -173,7 +185,14 @@ std::shared_ptr ProofNodeManager::mkScope( // use SYMM if possible if (aMatch == aeqSym) { - updateNode(pfs.get(), PfRule::SYMM, children, {}); + if (pfaa->getRule() == PfRule::SYMM) + { + updateNode(pfs.get(), pfaa->getChildren()[0].get()); + } + else + { + updateNode(pfs.get(), PfRule::SYMM, children, {}); + } } else { @@ -263,6 +282,11 @@ bool ProofNodeManager::updateNode(ProofNode* pn, ProofNode* pnr) { Assert(pn != nullptr); Assert(pnr != nullptr); + if (pn == pnr) + { + // same node, no update necessary + return true; + } if (pn->getResult() != pnr->getResult()) { return false; @@ -299,7 +323,7 @@ Node ProofNodeManager::checkInternal( ProofChecker* ProofNodeManager::getChecker() const { return d_checker; } std::shared_ptr ProofNodeManager::clone( - std::shared_ptr pn) + std::shared_ptr pn) const { const ProofNode* orig = pn.get(); std::unordered_map> visited; @@ -333,7 +357,13 @@ std::shared_ptr ProofNodeManager::clone( { it = visited.find(cp.get()); Assert(it != visited.end()); - Assert(it->second != nullptr); + // if we encounter nullptr here, then this child is currently being + // traversed at a higher level, hence this corresponds to a cyclic + // proof. + if (it->second == nullptr) + { + Unreachable() << "Cyclic proof encountered when cloning a proof node"; + } cchildren.push_back(it->second); } cloned = std::make_shared( @@ -347,6 +377,23 @@ std::shared_ptr ProofNodeManager::clone( return visited[orig]; } +ProofNode* ProofNodeManager::cancelDoubleSymm(ProofNode* pn) +{ + while (pn->getRule() == PfRule::SYMM) + { + std::shared_ptr pnc = pn->getChildren()[0]; + if (pnc->getRule() == PfRule::SYMM) + { + pn = pnc->getChildren()[0].get(); + } + else + { + break; + } + } + return pn; +} + bool ProofNodeManager::updateNodeInternal( ProofNode* pn, PfRule id, diff --git a/src/proof/proof_node_manager.h b/src/proof/proof_node_manager.h index 2fa7ed3e9..541686a30 100644 --- a/src/proof/proof_node_manager.h +++ b/src/proof/proof_node_manager.h @@ -84,6 +84,12 @@ class ProofNodeManager * @return The ASSUME proof of fact. */ std::shared_ptr mkAssume(Node fact); + /** + * Make symm, which accounts for whether the child is already a SYMM + * node, in which case we return its child. + */ + std::shared_ptr mkSymm(std::shared_ptr child, + Node expected = Node::null()); /** * Make transitivity proof, where children contains one or more proofs of * equalities that form an ordered chain. In other words, the vector children @@ -166,7 +172,12 @@ class ProofNodeManager * @param pn The proof node to clone * @return the cloned proof node. */ - std::shared_ptr clone(std::shared_ptr pn); + std::shared_ptr clone(std::shared_ptr pn) const; + /** + * Cancel double SYMM. Returns a proof node that is not a double application + * of SYMM, e.g. for (SYMM (SYMM (r P))), this returns (r P) where r != SYMM. + */ + static ProofNode* cancelDoubleSymm(ProofNode* pn); private: /** The (optional) proof checker */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0d8ec19dc..17585d363 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2539,6 +2539,7 @@ set(regress_2_tests regress2/strings/issue6639-replace-re-all.smt2 regress2/strings/issue918.smt2 regress2/strings/non_termination_regular_expression6.smt2 + regress2/strings/proof-fail-083021-delta.smt2 regress2/strings/range-perf.smt2 regress2/strings/repl-repl-i-no-push.smt2 regress2/strings/repl-repl.smt2 diff --git a/test/regress/regress2/strings/proof-fail-083021-delta.smt2 b/test/regress/regress2/strings/proof-fail-083021-delta.smt2 new file mode 100644 index 000000000..981102b7c --- /dev/null +++ b/test/regress/regress2/strings/proof-fail-083021-delta.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-const x Bool) +(declare-const x1 Int) +(declare-fun s () String) +(assert (ite (str.prefixof "-" (str.substr s 0 1)) (= 0 (str.to_int (str.substr (str.substr s 0 (+ 1 1)) 1 (- (str.len (str.substr s 0 (+ 1 1))) 1)))) true)) +(assert (not (<= (- (str.len s) 1 (+ 1 1) 1) 3))) +(assert (ite x true (> 1 (str.len (str.substr s (+ 1 1 1 1) (- (str.len s) (+ 1 1 1 1 1))))))) +(assert (ite (str.prefixof "-" (str.substr s (+ 1 1) 1)) (= 0 (str.to_int (str.substr (str.substr s (+ 1 1) (+ 1 1 1)) 1 (- (str.len (str.substr s 1 x1)) 1)))) true)) +(assert (str.in_re s (re.+ (re.range "0" "9")))) +(assert (not (<= (str.to_int (str.substr s 0 (+ 1 1))) 255))) +(check-sat) -- 2.30.2