From d67f732c7cf4a62f3b0d7a992d5096b69e7f6bf6 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 15 Feb 2017 13:39:55 -0500
Subject: [PATCH] theory_str data structure refactoring

---
 src/smt/theory_str.cpp | 6 +++---
 src/smt/theory_str.h   | 7 +++----
 2 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 9fcf1f084..da6f94afe 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -6606,7 +6606,7 @@ void theory_str::finite_model_test(expr * testvar, expr * str) {
                 }
             } else {
                 bool map_effectively_empty = false;
-                if (fvar_len_count_map.find(v) == fvar_len_count_map.end()) {
+                if (!fvar_len_count_map.contains(v)) {
                     map_effectively_empty = true;
                 }
 
@@ -6701,7 +6701,7 @@ void theory_str::finite_model_test(expr * testvar, expr * str) {
 
 void theory_str::more_len_tests(expr * lenTester, std::string lenTesterValue) {
     ast_manager & m = get_manager();
-    if (lenTester_fvar_map.find(lenTester) != lenTester_fvar_map.end()) {
+    if (lenTester_fvar_map.contains(lenTester)) {
         expr * fVar = lenTester_fvar_map[lenTester];
         expr * toAssert = gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue);
         TRACE("t_str_detail", tout << "asserting more length tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;);
@@ -9952,7 +9952,7 @@ expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTe
 	    return binary_search_length_test(freeVar, lenTesterInCbEq, lenTesterValue);
 	} else {
         bool map_effectively_empty = false;
-        if (fvar_len_count_map.find(freeVar) == fvar_len_count_map.end()) {
+        if (!fvar_len_count_map.contains(freeVar)) {
             TRACE("t_str_detail", tout << "fvar_len_count_map is empty" << std::endl;);
             map_effectively_empty = true;
         }
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 47a8e8d0b..f81b4ada7 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -195,7 +195,6 @@ namespace smt {
 
         bool finalCheckProgressIndicator;
 
-        // TODO make sure that all generated expressions are saved into the trail
         expr_ref_vector m_trail; // trail for generated terms
 
         str_value_factory * m_factory;
@@ -236,11 +235,11 @@ namespace smt {
         obj_hashtable<expr> internal_valTest_vars;
         obj_hashtable<expr> internal_unrollTest_vars;
 
-        std::set<expr*> input_var_in_len;
+        obj_hashtable<expr> input_var_in_len;
 
-        std::map<expr*, unsigned int> fvar_len_count_map;
+        obj_map<expr, unsigned int> fvar_len_count_map;
         std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
-        std::map<expr*, expr*> lenTester_fvar_map;
+        obj_map<expr, expr*> lenTester_fvar_map;
 
         std::map<expr*, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
         std::map<expr*, expr*> valueTester_fvar_map;