From ac59c64e3181f72ad79fa4a759bac56e685a5067 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 22 Oct 2021 09:39:26 -0500 Subject: [PATCH] Do not use global proxy variable attribute for strings (#7460) Fixes #6180. --- src/theory/strings/term_registry.cpp | 27 +++++++------------ src/theory/strings/term_registry.h | 2 +- test/regress/CMakeLists.txt | 2 ++ .../strings/issue6180-2-proxy-vars.smt2 | 8 ++++++ .../strings/issue6180-proxy-vars.smt2 | 10 +++++++ 5 files changed, 31 insertions(+), 18 deletions(-) create mode 100644 test/regress/regress1/strings/issue6180-2-proxy-vars.smt2 create mode 100644 test/regress/regress1/strings/issue6180-proxy-vars.smt2 diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index c459649fb..688f232a1 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -34,12 +34,6 @@ namespace cvc5 { namespace theory { namespace strings { -struct StringsProxyVarAttributeId -{ -}; -typedef expr::Attribute - StringsProxyVarAttribute; - TermRegistry::TermRegistry(Env& env, SolverState& s, SequencesStatistics& statistics, @@ -58,12 +52,12 @@ TermRegistry::TermRegistry(Env& env, d_registeredTerms(userContext()), d_registeredTypes(userContext()), d_proxyVar(userContext()), + d_proxyVarToLength(userContext()), d_lengthLemmaTermsCache(userContext()), - d_epg(pnm ? new EagerProofGenerator( - pnm, - userContext(), - "strings::TermRegistry::EagerProofGenerator") - : nullptr) + d_epg( + pnm ? new EagerProofGenerator( + pnm, userContext(), "strings::TermRegistry::EagerProofGenerator") + : nullptr) { NodeManager* nm = NodeManager::currentNM(); d_zero = nm->mkConst(Rational(0)); @@ -387,8 +381,6 @@ TrustNode TermRegistry::getRegisterTermLemma(Node n) } } Node sk = d_skCache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym"); - StringsProxyVarAttribute spva; - sk.setAttribute(spva, true); Node eq = Rewriter::rewrite(sk.eqNode(n)); d_proxyVar[n] = sk; // If we are introducing a proxy for a constant or concat term, we do not @@ -403,12 +395,13 @@ TrustNode TermRegistry::getRegisterTermLemma(Node n) if (n.getKind() == STRING_CONCAT) { std::vector nodeVec; + NodeNodeMap::const_iterator itl; for (const Node& nc : n) { - if (nc.getAttribute(StringsProxyVarAttribute())) + itl = d_proxyVarToLength.find(nc); + if (itl != d_proxyVarToLength.end()) { - Assert(d_proxyVarToLength.find(nc) != d_proxyVarToLength.end()); - nodeVec.push_back(d_proxyVarToLength[nc]); + nodeVec.push_back(itl->second); } else { @@ -656,7 +649,7 @@ void TermRegistry::removeProxyEqs(Node n, std::vector& unproc) const for (size_t i = 0; i < 2; i++) { // determine whether this side has a proxy variable - if (ns[i].getAttribute(StringsProxyVarAttribute())) + if (d_proxyVar.find(ns[i]) != d_proxyVar.end()) { if (getProxyVariableFor(ns[1 - i]) == ns[i]) { diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h index a80e48744..1de5def9e 100644 --- a/src/theory/strings/term_registry.h +++ b/src/theory/strings/term_registry.h @@ -261,7 +261,7 @@ class TermRegistry : protected EnvObj * Map from proxy variables to their normalized length. In the above example, * we store "ABC" -> 3. */ - std::map d_proxyVarToLength; + NodeNodeMap d_proxyVarToLength; /** List of terms that we have register length for */ NodeSet d_lengthLemmaTermsCache; /** Proof generator, manages proofs for lemmas generated by this class */ diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index ca9ce349f..b80fd890b 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2217,6 +2217,8 @@ set(regress_1_tests regress1/strings/issue6101-2.smt2 regress1/strings/issue6132-non-unique-skolem.smt2 regress1/strings/issue6142-repl-inv-rew.smt2 + regress1/strings/issue6180-proxy-vars.smt2 + regress1/strings/issue6180-2-proxy-vars.smt2 regress1/strings/issue6184-unsat-core.smt2 regress1/strings/issue6191-replace-all.smt2 regress1/strings/issue6203-1-substr-ctn-strip.smt2 diff --git a/test/regress/regress1/strings/issue6180-2-proxy-vars.smt2 b/test/regress/regress1/strings/issue6180-2-proxy-vars.smt2 new file mode 100644 index 000000000..eb991433f --- /dev/null +++ b/test/regress/regress1/strings/issue6180-2-proxy-vars.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-fun a () String) +(assert (str.in_re (str.++ (str.update (str.++ "AB" a) 0 "A") a) (re.+ (str.to_re "A")))) +(assert (str.in_re a (re.++ (re.* (str.to_re "B")) (str.to_re "A")))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6180-proxy-vars.smt2 b/test/regress/regress1/strings/issue6180-proxy-vars.smt2 new file mode 100644 index 000000000..4503b3144 --- /dev/null +++ b/test/regress/regress1/strings/issue6180-proxy-vars.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: unsat +(set-logic ALL) +(set-info :status unsat) +(declare-fun x () String) +(declare-fun y () String) +(assert (= (= (str.suffixof "B" (str.replace (str.replace "A" (str.replace x "B" "A") "") "A" "")) +(str.suffixof "B" (str.replace x "B" "A"))) (str.suffixof "B" (str.replace x "B" "A")))) +(check-sat) +(exit) -- 2.30.2