add string constant cache to theory_str and associated param

src/smt/params/smt_params_helper.pyg

@@ -68,5 +68,6 @@ def_module_params(module_name='smt',
                           ('str.aggressive_unroll_testing', BOOL, True, 'prioritize testing concrete regex unroll counts over generating more options'),
                           ('str.fast_length_tester_cache', BOOL, False, 'cache length tester constants instead of regenerating them'),
                           ('str.fast_value_tester_cache', BOOL, True, 'cache value tester constants instead of regenerating them'),
+                          ('str.string_constant_cache', BOOL, True, 'cache all generated string constants generated from anywhere in theory_str'),
                           ('theory_case_split', BOOL, False, 'Allow the context to use heuristics involving theory case splits, which are a set of literals of which exactly one can be assigned True. If this option is false, the context will generate extra axioms to enforce this instead.')
                           ))

src/smt/params/theory_str_params.cpp

@@ -26,4 +26,5 @@ void theory_str_params::updt_params(params_ref const & _p) {
     m_AggressiveUnrollTesting = p.str_aggressive_unroll_testing();
     m_UseFastLengthTesterCache = p.str_fast_length_tester_cache();
     m_UseFastValueTesterCache = p.str_fast_value_tester_cache();
+    m_StringConstantCache = p.str_string_constant_cache();
 }

src/smt/params/theory_str_params.h

@@ -62,13 +62,20 @@ struct theory_str_params {
      */
     bool m_UseFastValueTesterCache;
 
+    /*
+     * If StringConstantCache is set to true,
+     * all string constants in theory_str generated from anywhere will be cached and saved.
+     */
+    bool m_StringConstantCache;
+
     theory_str_params(params_ref const & p = params_ref()):
         m_AssertStrongerArrangements(true),
         m_AggressiveLengthTesting(false),
         m_AggressiveValueTesting(false),
         m_AggressiveUnrollTesting(true),
         m_UseFastLengthTesterCache(false),
-        m_UseFastValueTesterCache(true)
+        m_UseFastValueTesterCache(true),
+        m_StringConstantCache(true)
     {
         updt_params(p);
     }

src/smt/theory_str.cpp

@@ -70,25 +70,29 @@ theory_str::~theory_str() {
 }
 
 expr * theory_str::mk_string(std::string str) {
-    ++totalCacheAccessCount;
+    if (m_params.m_StringConstantCache) {
-    expr * val;
+        ++totalCacheAccessCount;
-    if (stringConstantCache.find(str, val)) {
+        expr * val;
-        // cache hit
+        if (stringConstantCache.find(str, val)) {
-        ++cacheHitCount;
+            // cache hit
-        TRACE("t_str_cache", tout << "cache hit: \"" << str << "\" ("
+            ++cacheHitCount;
-                << cacheHitCount << " hits, " << cacheMissCount << " misses out of "
+            TRACE("t_str_cache", tout << "cache hit: \"" << str << "\" ("
-                << totalCacheAccessCount << " accesses)" << std::endl;);
+                    << cacheHitCount << " hits, " << cacheMissCount << " misses out of "
-        return val;
+                    << totalCacheAccessCount << " accesses)" << std::endl;);
+            return val;
+        } else {
+            // cache miss
+            ++cacheMissCount;
+            TRACE("t_str_cache", tout << "cache miss: \"" << str << "\" ("
+                            << cacheHitCount << " hits, " << cacheMissCount << " misses out of "
+                            << totalCacheAccessCount << " accesses)" << std::endl;);
+            val = m_strutil.mk_string(str);
+            m_trail.push_back(val);
+            stringConstantCache.insert(str, val);
+            return val;
+        }
     } else {
-        // cache miss
+        return m_strutil.mk_string(str);
-        ++cacheMissCount;
-        TRACE("t_str_cache", tout << "cache miss: \"" << str << "\" ("
-                        << cacheHitCount << " hits, " << cacheMissCount << " misses out of "
-                        << totalCacheAccessCount << " accesses)" << std::endl;);
-        val = m_strutil.mk_string(str);
-        m_trail.push_back(val);
-        stringConstantCache.insert(str, val);
-        return val;
     }
 }