From bd184f9813a91d8f60eb0521893a5154b9f92357 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 12 Aug 2020 15:51:15 -0500 Subject: [PATCH] (proof-new) Proof support in the strings term registry. (#4876) Adds basic support for proofs in the strings term registry. This code is not yet active until further parts of proof-new are merged. --- src/theory/strings/term_registry.cpp | 67 +++++++++++++++++++++------- src/theory/strings/term_registry.h | 8 ++-- 2 files changed, 54 insertions(+), 21 deletions(-) diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index ed20406df..f28db4c35 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -265,7 +265,7 @@ void TermRegistry::registerTerm(Node n, int effort) registerType(tn); Debug("strings-register") << "TheoryStrings::registerTerm() " << n << ", effort = " << effort << std::endl; - Node regTermLem; + TrustNode regTermLem; if (tn.isStringLike()) { // register length information: @@ -276,15 +276,29 @@ void TermRegistry::registerTerm(Node n, int effort) else if (n.getKind() != STRING_STRCTN) { // we don't send out eager reduction lemma for str.contains currently - regTermLem = eagerReduce(n, &d_skCache); + Node eagerRedLemma = eagerReduce(n, &d_skCache); + if (!eagerRedLemma.isNull()) + { + // if there was an eager reduction, we make the trust node for it + if (d_epg != nullptr) + { + regTermLem = d_epg->mkTrustNode( + eagerRedLemma, PfRule::STRING_EAGER_REDUCTION, {n}); + } + else + { + regTermLem = TrustNode::mkTrustLemma(eagerRedLemma, nullptr); + } + } } if (!regTermLem.isNull()) { Trace("strings-lemma") << "Strings::Lemma REG-TERM : " << regTermLem << std::endl; - Trace("strings-assert") << "(assert " << regTermLem << ")" << std::endl; + Trace("strings-assert") + << "(assert " << regTermLem.getNode() << ")" << std::endl; ++(d_statistics.d_lemmasRegisterTerm); - d_out.lemma(regTermLem); + d_out.trustedLemma(regTermLem); } } @@ -306,7 +320,7 @@ void TermRegistry::registerType(TypeNode tn) } } -Node TermRegistry::getRegisterTermLemma(Node n) +TrustNode TermRegistry::getRegisterTermLemma(Node n) { Assert(n.getType().isStringLike()); NodeManager* nm = NodeManager::currentNM(); @@ -322,7 +336,7 @@ Node TermRegistry::getRegisterTermLemma(Node n) if (lsum == lsumb) { registerTermAtomic(n, LENGTH_SPLIT); - return Node::null(); + return TrustNode::null(); } } Node sk = d_skCache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym"); @@ -368,7 +382,12 @@ Node TermRegistry::getRegisterTermLemma(Node n) Node ret = nm->mkNode(AND, eq, ceq); - return ret; + // it is a simple rewrite to justify this + if (d_epg != nullptr) + { + return d_epg->mkTrustNode(ret, PfRule::MACRO_SR_PRED_INTRO, {ret}); + } + return TrustNode::mkTrustLemma(ret, nullptr); } void TermRegistry::registerTermAtomic(Node n, LengthStatus s) @@ -385,14 +404,15 @@ void TermRegistry::registerTermAtomic(Node n, LengthStatus s) return; } std::map reqPhase; - Node lenLem = getRegisterTermAtomicLemma(n, s, reqPhase); + TrustNode lenLem = getRegisterTermAtomicLemma(n, s, reqPhase); if (!lenLem.isNull()) { Trace("strings-lemma") << "Strings::Lemma REGISTER-TERM-ATOMIC : " << lenLem << std::endl; - Trace("strings-assert") << "(assert " << lenLem << ")" << std::endl; + Trace("strings-assert") + << "(assert " << lenLem.getNode() << ")" << std::endl; ++(d_statistics.d_lemmasRegisterTermAtomic); - d_out.lemma(lenLem); + d_out.trustedLemma(lenLem); } for (const std::pair& rp : reqPhase) { @@ -415,16 +435,15 @@ const context::CDHashSet& TermRegistry::getInputVars() bool TermRegistry::hasStringCode() const { return d_hasStrCode; } -Node TermRegistry::getRegisterTermAtomicLemma(Node n, - LengthStatus s, - std::map& reqPhase) +TrustNode TermRegistry::getRegisterTermAtomicLemma( + Node n, LengthStatus s, std::map& reqPhase) { if (n.isConst()) { // No need to send length for constant terms. This case may be triggered // for cases where the skolem cache automatically replaces a skolem by // a constant. - return Node::null(); + return TrustNode::null(); } Assert(n.getType().isStringLike()); NodeManager* nm = NodeManager::currentNM(); @@ -438,7 +457,12 @@ Node TermRegistry::getRegisterTermAtomicLemma(Node n, Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one << std::endl; Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl; - return len_geq_one; + if (options::proofNewPedantic() > 0) + { + Unhandled() << "Unhandled lemma Strings::Lemma SK-GEQ-ONE : " + << len_geq_one << std::endl; + } + return TrustNode::mkTrustLemma(len_geq_one, nullptr); } if (s == LENGTH_ONE) @@ -447,7 +471,12 @@ Node TermRegistry::getRegisterTermAtomicLemma(Node n, Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one << std::endl; Trace("strings-assert") << "(assert " << len_one << ")" << std::endl; - return len_one; + if (options::proofNewPedantic() > 0) + { + Unhandled() << "Unhandled lemma Strings::Lemma SK-ONE : " << len_one + << std::endl; + } + return TrustNode::mkTrustLemma(len_one, nullptr); } Assert(s == LENGTH_SPLIT); @@ -478,7 +507,11 @@ Node TermRegistry::getRegisterTermAtomicLemma(Node n, Assert(!case_emptyr.getConst()); } - return lenLemma; + if (d_epg != nullptr) + { + return d_epg->mkTrustNode(lenLemma, PfRule::STRING_LENGTH_POS, {n}); + } + return TrustNode::mkTrustLemma(lenLemma, nullptr); } Node TermRegistry::getSymbolicDefinition(Node n, std::vector& exp) const diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index 9a66690b8..2048abec1 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -278,7 +278,7 @@ class TermRegistry * If n is an atomic term, the method registerTermAtomic is called for n * and s = LENGTH_SPLIT and no lemma is returned. */ - Node getRegisterTermLemma(Node n); + TrustNode getRegisterTermLemma(Node n); /** * Get the lemma required for registering the length information for * atomic term n given length status s. For details, see registerTermAtomic. @@ -287,9 +287,9 @@ class TermRegistry * argument reqPhase, which should be processed by a call to requiredPhase by * the caller of this method. */ - Node getRegisterTermAtomicLemma(Node n, - LengthStatus s, - std::map& reqPhase); + TrustNode getRegisterTermAtomicLemma(Node n, + LengthStatus s, + std::map& reqPhase); }; } // namespace strings -- 2.30.2