From 457b0fe003c8192e35df48cfb3528b9aefe2fd1b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 2 Nov 2020 13:46:05 -0600 Subject: 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. --- src/theory/strings/term_registry.cpp | 4 +--- src/theory/strings/term_registry.h | 4 ++-- 2 files changed, 3 insertions(+), 5 deletions(-) (limited to 'src') 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& exp) const Node TermRegistry::getProxyVariableFor(Node n) const { - NodeNodeMap::const_iterator it = d_proxyVar.find(n); + std::map::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 d_proxyVar; /** * Map from proxy variables to their normalized length. In the above example, * we store "ABC" -> 3. */ - NodeNodeMap d_proxyVarToLength; + std::map d_proxyVarToLength; /** List of terms that we have register length for */ NodeSet d_lengthLemmaTermsCache; /** Proof generator, manages proofs for lemmas generated by this class */ -- cgit v1.2.3