Do not use global proxy variable attribute for strings (#7460)

Fixes #6180.

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index c459649fb2780b4a8bd9c5690f4db0dbdb874350..688f232a16096f551ae05e22ee27a9c5fedc023a 100644 (file)
--- 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<StringsProxyVarAttributeId, bool>
-    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<Node> 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<Node>& 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 a80e48744f415d0767e123295d2ac3b520db7174..1de5def9eba862e85d7431547ae9a21e92204dcc 100644 (file)
--- 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<Node, Node> 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 ca9ce349f0c4c99e99e2ab0955c4fd73be7ff3b5..b80fd890b27df4b4054cdb3de1a52bd3056a043c 100644 (file)
--- 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 (file)
index 0000000..eb99143
--- /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 (file)
index 0000000..4503b31
--- /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)