From 73f7e301c3f60924a8d7e1518e714711eeb5f059 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 12 Mar 2018 17:09:55 -0400
Subject: [PATCH] preliminary refactoring to use obj_map

---
 src/smt/theory_str.cpp | 19 ++++++++++---------
 src/smt/theory_str.h   | 21 ++++++++++-----------
 2 files changed, 20 insertions(+), 20 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 3335370eb..90eb01fa8 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -4582,8 +4582,9 @@ namespace smt {
 
         std::pair<expr*, expr*> key = std::make_pair(concat, unroll);
         expr_ref toAssert(mgr);
+        expr * _toAssert;
 
-        if (concat_eq_unroll_ast_map.find(key) == concat_eq_unroll_ast_map.end()) {
+        if (!concat_eq_unroll_ast_map.find(concat, unroll, _toAssert)) {
             expr_ref arg1(to_app(concat)->get_arg(0), mgr);
             expr_ref arg2(to_app(concat)->get_arg(1), mgr);
             expr_ref r1(to_app(unroll)->get_arg(0), mgr);
@@ -4634,9 +4635,9 @@ namespace smt {
 
             toAssert = mgr.mk_and(opAnd1, opAnd2);
             m_trail.push_back(toAssert);
-            concat_eq_unroll_ast_map[key] = toAssert;
+            concat_eq_unroll_ast_map.insert(concat, unroll, toAssert);
         } else {
-            toAssert = concat_eq_unroll_ast_map[key];
+            toAssert = _toAssert;
         }
 
         assert_axiom(toAssert);
@@ -4920,7 +4921,7 @@ namespace smt {
 
         expr_ref_vector litems(m);
 
-        if (contain_pair_idx_map.find(varNode) != contain_pair_idx_map.end()) {
+        if (contain_pair_idx_map.contains(varNode)) {
             std::set<std::pair<expr*, expr*> >::iterator itor1 = contain_pair_idx_map[varNode].begin();
             for (; itor1 != contain_pair_idx_map[varNode].end(); ++itor1) {
                 expr * strAst = itor1->first;
@@ -5057,7 +5058,7 @@ namespace smt {
         ast_manager & m = get_manager();
         expr_ref_vector litems(m);
 
-        if (contain_pair_idx_map.find(varNode) != contain_pair_idx_map.end()) {
+        if (contain_pair_idx_map.contains(varNode)) {
             std::set<std::pair<expr*, expr*> >::iterator itor1 = contain_pair_idx_map[varNode].begin();
             for (; itor1 != contain_pair_idx_map[varNode].end(); ++itor1) {
                 expr * strAst = itor1->first;
@@ -5125,7 +5126,7 @@ namespace smt {
     }
 
     bool theory_str::in_contain_idx_map(expr * n) {
-        return contain_pair_idx_map.find(n) != contain_pair_idx_map.end();
+        return contain_pair_idx_map.contains(n);
     }
 
     void theory_str::check_contain_by_eq_nodes(expr * n1, expr * n2) {
@@ -6456,7 +6457,7 @@ namespace smt {
         } else {
             expr_ref_vector::iterator itor = eqNodeSet.begin();
             for (; itor != eqNodeSet.end(); itor++) {
-                if (regex_in_var_reg_str_map.find(*itor) != regex_in_var_reg_str_map.end()) {
+                if (regex_in_var_reg_str_map.contains(*itor)) {
                     std::set<zstring>::iterator strItor = regex_in_var_reg_str_map[*itor].begin();
                     for (; strItor != regex_in_var_reg_str_map[*itor].end(); strItor++) {
                         zstring regStr = *strItor;
@@ -6469,7 +6470,7 @@ namespace smt {
                             expr * regexTerm = a_regexIn->get_arg(1);
 
                             // TODO figure out regex NFA stuff
-                            if (regex_nfa_cache.find(regexTerm) == regex_nfa_cache.end()) {
+                            if (!regex_nfa_cache.contains(regexTerm)) {
                                 TRACE("str", tout << "regex_nfa_cache: cache miss" << std::endl;);
                                 regex_nfa_cache[regexTerm] = nfa(u, regexTerm);
                             } else {
@@ -9596,7 +9597,7 @@ namespace smt {
             if (low.is_neg()) {
                 toAssert = m_autil.mk_ge(cntInUnr, mk_int(0));
             } else {
-                if (unroll_var_map.find(unrFunc) == unroll_var_map.end()) {
+                if (!unroll_var_map.contains(unrFunc)) {
 
                     expr_ref newVar1(mk_regex_rep_var(), mgr);
                     expr_ref newVar2(mk_regex_rep_var(), mgr);
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 9288bac7c..5a249f5dc 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -312,30 +312,29 @@ protected:
     obj_hashtable<expr> input_var_in_len;
 
     obj_map<expr, unsigned int> fvar_len_count_map;
-    std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
+    obj_map<expr, ptr_vector<expr> > fvar_lenTester_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;
+    obj_map<expr, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
+    obj_map<expr, expr*> valueTester_fvar_map;
 
-    std::map<expr*, int_vector> val_range_map;
+    obj_map<expr, int_vector> val_range_map;
 
     // This can't be an expr_ref_vector because the constructor is wrong,
     // we would need to modify the allocator so we pass in ast_manager
-    std::map<expr*, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
-    std::map<expr*, expr*> unroll_var_map;
-    std::map<std::pair<expr*, expr*>, expr*> concat_eq_unroll_ast_map;
+    obj_map<expr, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
+    obj_map<expr, expr*> unroll_var_map;
+    obj_pair_map<expr, expr, expr*> concat_eq_unroll_ast_map;
 
     expr_ref_vector contains_map;
 
     theory_str_contain_pair_bool_map_t contain_pair_bool_map;
-    //obj_map<expr, obj_pair_set<expr, expr> > contain_pair_idx_map;
-    std::map<expr*, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
+    obj_map<expr, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
 
     std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map;
-    std::map<expr*, std::set<zstring> > regex_in_var_reg_str_map;
+    obj_map<expr, std::set<zstring> > regex_in_var_reg_str_map;
 
-    std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
+    obj_map<expr, nfa> regex_nfa_cache; // Regex term --> NFA
 
     svector<char> char_set;
     std::map<char, int>  charSetLookupTable;