From e5e1ff4b81f60e97bca59874c542ecfe1618599b Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 19:12:53 +0100
Subject: [PATCH] static index_set functions

---
 src/solvers/refinement/string_refinement.cpp | 39 ++++++++++++++++----
 src/solvers/refinement/string_refinement.h   |  3 --
 2 files changed, 31 insertions(+), 11 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index 307ecd4a1cc..a6d1f5637e5 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -71,6 +71,18 @@ static std::pair<bool, std::vector<exprt>> check_axioms(
   ui_message_handlert::uit ui,
   const replace_mapt& symbol_resolve);
 
+static void initial_index_set(
+  std::map<exprt, std::set<exprt>> &index_set,
+  std::map<exprt, std::set<exprt>> &current_index_set,
+  const namespacet &ns,
+  const string_constraintt &axiom);
+
+static void initial_index_set(
+  std::map<exprt, std::set<exprt>> &index_set,
+  std::map<exprt, std::set<exprt>> &current_index_set,
+  const namespacet &ns,
+  const std::vector<string_constraintt>  &string_axioms);
+
 exprt simplify_sum(const exprt &f);
 
 /// Convert exprt to a specific type. Throw bad_cast if conversion
@@ -669,7 +681,7 @@ decision_proceduret::resultt string_refinementt::dec_solve()
     }
   }
 
-  initial_index_set(universal_axioms);
+  initial_index_set(index_set, current_index_set, ns, universal_axioms);
   update_index_set(cur);
   cur.clear();
   for (const auto& lemma :
@@ -1602,11 +1614,14 @@ static bool find_qvar(const exprt index, const symbol_exprt &qvar)
 /// add to the index set all the indices that appear in the formulas and the
 /// upper bound minus one
 /// \par parameters: a list of string constraints
-void string_refinementt::initial_index_set(
+static void initial_index_set(
+  std::map<exprt, std::set<exprt>> &index_set,
+  std::map<exprt, std::set<exprt>> &current_index_set,
+  const namespacet &ns,
   const std::vector<string_constraintt>  &string_axioms)
 {
   for(const auto &axiom : string_axioms)
-    initial_index_set(axiom);
+    initial_index_set(index_set, current_index_set, ns, axiom);
 }
 
 /// add to the index set all the indices that appear in the formulas
@@ -1644,7 +1659,11 @@ static std::vector<exprt> sub_arrays(const exprt &array_expr)
 /// add to the index set all the indices that appear in the formula and the
 /// upper bound minus one
 /// \par parameters: a string constraint
-void string_refinementt::add_to_index_set(const exprt &s, exprt i)
+static void add_to_index_set(
+  std::map<exprt, std::set<exprt>> &index_set,
+  std::map<exprt, std::set<exprt>> &current_index_set,
+  const namespacet &ns,
+  const exprt &s, exprt i)
 {
   simplify(i, ns);
   if(i.id()!=ID_constant || expr_cast<size_t>(i))
@@ -1655,7 +1674,11 @@ void string_refinementt::add_to_index_set(const exprt &s, exprt i)
   }
 }
 
-void string_refinementt::initial_index_set(const string_constraintt &axiom)
+static void initial_index_set(
+  std::map<exprt, std::set<exprt>> &index_set,
+  std::map<exprt, std::set<exprt>> &current_index_set,
+  const namespacet &ns,
+  const string_constraintt &axiom)
 {
   symbol_exprt qvar=axiom.univ_var();
   std::list<exprt> to_process;
@@ -1675,7 +1698,7 @@ void string_refinementt::initial_index_set(const string_constraintt &axiom)
       // if cur is of the form s[i] and no quantified variable appears in i
       if(!has_quant_var)
       {
-        add_to_index_set(s, i);
+        add_to_index_set(index_set, current_index_set, ns, s, i);
       }
       else
       {
@@ -1685,7 +1708,7 @@ void string_refinementt::initial_index_set(const string_constraintt &axiom)
           axiom.upper_bound(),
           from_integer(1, axiom.upper_bound().type()));
         replace_expr(qvar, kminus1, e);
-        add_to_index_set(s, e);
+        add_to_index_set(index_set, current_index_set, ns, s, e);
       }
     }
     else
@@ -1713,7 +1736,7 @@ void string_refinementt::update_index_set(const exprt &formula)
         s.type().id()==ID_array,
         string_refinement_invariantt("index expressions must index on arrays"));
       exprt simplified=simplify_sum(i);
-      add_to_index_set(s, simplified);
+      add_to_index_set(index_set, current_index_set, ns, s, simplified);
     }
     else
     {
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 7acad3c67c3..84a7bc4a8d0 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -105,9 +105,6 @@ class string_refinementt final: public bv_refinementt
   void set_char_array_equality(const exprt &lhs, const exprt &rhs);
   void update_index_set(const exprt &formula);
   void update_index_set(const std::vector<exprt> &cur);
-  void initial_index_set(const string_constraintt &axiom);
-  void initial_index_set(const std::vector<string_constraintt> &string_axioms);
-  void add_to_index_set(const exprt &s, exprt i);
 
   std::vector<exprt> instantiate_not_contains(
     const string_not_contains_constraintt &axiom);