From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 2 Nov 2020 19:46:05 +0000 (-0600)
Subject: Update strings proxy variable map to be context independent (#5377)
X-Git-Tag: cvc5-1.0.0~2640
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=457b0fe003c8192e35df48cfb3528b9aefe2fd1b;p=cvc5.git

Update strings proxy variable map to be context independent (#5377)

This makes strings proxy variables map to be context-independent. They should be context independent since we are using attributes to mark proxy variables, which are context-independent. This led to the crash reported on #5374 since proxy variables would persist across multiple user contexts, but would be missing in the user-context dependent map.

This fixes #5374.
---

diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp
index 2b5daa476..76230bcff 100644
--- a/src/theory/strings/term_registry.cpp
+++ b/src/theory/strings/term_registry.cpp
@@ -49,8 +49,6 @@ TermRegistry::TermRegistry(SolverState& s,
       d_preregisteredTerms(s.getUserContext()),
       d_registeredTerms(s.getUserContext()),
       d_registeredTypes(s.getUserContext()),
-      d_proxyVar(s.getUserContext()),
-      d_proxyVarToLength(s.getUserContext()),
       d_lengthLemmaTermsCache(s.getUserContext()),
       d_epg(pnm ? new EagerProofGenerator(
                       pnm,
@@ -567,7 +565,7 @@ Node TermRegistry::getSymbolicDefinition(Node n, std::vector<Node>& exp) const
 
 Node TermRegistry::getProxyVariableFor(Node n) const
 {
-  NodeNodeMap::const_iterator it = d_proxyVar.find(n);
+  std::map<Node, Node>::const_iterator it = d_proxyVar.find(n);
   if (it != d_proxyVar.end())
   {
     return (*it).second;
diff --git a/src/theory/strings/term_registry.h b/src/theory/strings/term_registry.h
index 06993aa97..a713cc60f 100644
--- a/src/theory/strings/term_registry.h
+++ b/src/theory/strings/term_registry.h
@@ -249,12 +249,12 @@ class TermRegistry
    * which rewrites to 3 = 3.
    * In the above example, we store "ABC" -> v_{"ABC"} in this map.
    */
-  NodeNodeMap d_proxyVar;
+  std::map<Node, Node> d_proxyVar;
   /**
    * Map from proxy variables to their normalized length. In the above example,
    * we store "ABC" -> 3.
    */
-  NodeNodeMap d_proxyVarToLength;
+  std::map<Node, Node> 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 cd99823f1..98fde9847 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1844,6 +1844,7 @@ set(regress_1_tests
   regress1/strings/issue4735.smt2
   regress1/strings/issue4735_2.smt2
   regress1/strings/issue4759-comp-delta.smt2
+  regress1/strings/issue5374-proxy-i.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2
diff --git a/test/regress/regress1/strings/issue5374-proxy-i.smt2 b/test/regress/regress1/strings/issue5374-proxy-i.smt2
new file mode 100644
index 000000000..89b2d007b
--- /dev/null
+++ b/test/regress/regress1/strings/issue5374-proxy-i.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: -i
+; EXPECT: sat
+(set-logic QF_UFSLIA)
+(set-option :strings-lazy-pp false)
+(declare-fun str0 () String)
+(declare-fun str4 () String)
+(declare-fun str15 () String)
+(push 1)
+(assert (str.in_re (str.replace str0 "gpQrbuIlpcirZXw" "") (str.to_re "")))
+(push 1)
+(check-sat)
+(pop 1)
+(pop 1)
+(assert (distinct str15 str4 (str.replace str0 "gpQrbuIlpcirZXw" "") ""))
+(push 1)