From 94762d276d7a6cac121e72fae0d39be046701ac9 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Sun, 18 Dec 2016 18:47:38 -0500
Subject: [PATCH] add string constant cache to theory_str and associated param

---
 src/smt/params/smt_params_helper.pyg |  1 +
 src/smt/params/theory_str_params.cpp |  1 +
 src/smt/params/theory_str_params.h   |  9 ++++++-
 src/smt/theory_str.cpp               | 40 +++++++++++++++-------------
 4 files changed, 32 insertions(+), 19 deletions(-)

diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 3f2c6a54a..3bcb867b4 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/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.')
                           ))
diff --git a/src/smt/params/theory_str_params.cpp b/src/smt/params/theory_str_params.cpp
index f952c6c87..dae7765cc 100644
--- a/src/smt/params/theory_str_params.cpp
+++ b/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();
 }
diff --git a/src/smt/params/theory_str_params.h b/src/smt/params/theory_str_params.h
index f4e7ecf33..dc4e1aa89 100644
--- a/src/smt/params/theory_str_params.h
+++ b/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);
     }
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 19e677acb..3a3d36c36 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -70,25 +70,29 @@ theory_str::~theory_str() {
 }
 
 expr * theory_str::mk_string(std::string str) {
-    ++totalCacheAccessCount;
-    expr * val;
-    if (stringConstantCache.find(str, val)) {
-        // cache hit
-        ++cacheHitCount;
-        TRACE("t_str_cache", tout << "cache hit: \"" << str << "\" ("
-                << cacheHitCount << " hits, " << cacheMissCount << " misses out of "
-                << totalCacheAccessCount << " accesses)" << std::endl;);
-        return val;
+    if (m_params.m_StringConstantCache) {
+        ++totalCacheAccessCount;
+        expr * val;
+        if (stringConstantCache.find(str, val)) {
+            // cache hit
+            ++cacheHitCount;
+            TRACE("t_str_cache", tout << "cache hit: \"" << str << "\" ("
+                    << cacheHitCount << " hits, " << cacheMissCount << " misses out of "
+                    << 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
-        ++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;
+        return m_strutil.mk_string(str);
     }
 }