From 2eed573c17c93417f6a84c97d5c115a46f498bca Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Fri, 15 Sep 2017 18:47:02 +0100
Subject: [PATCH] Static add_axioms for strings

---
 src/solvers/refinement/string_refinement.cpp | 30 ++++++++++++++++----
 src/solvers/refinement/string_refinement.h   |  1 -
 2 files changed, 24 insertions(+), 7 deletions(-)

diff --git a/src/solvers/refinement/string_refinement.cpp b/src/solvers/refinement/string_refinement.cpp
index bd36f7b944b..307ecd4a1cc 100644
--- a/src/solvers/refinement/string_refinement.cpp
+++ b/src/solvers/refinement/string_refinement.cpp
@@ -266,8 +266,11 @@ static void depends_in_symbol_map(const exprt &expr, std::vector<exprt> &accu)
 /// \param rhs: an expression to map it to, which should be either a symbol
 ///             a string_exprt, an array_exprt, an array_of_exprt or an
 ///             if_exprt with branches of the previous kind
-void string_refinementt::add_symbol_to_symbol_map(
-  const exprt &lhs, const exprt &rhs)
+void add_symbol_to_symbol_map(
+  replace_mapt& symbol_resolve,
+  std::map<exprt, std::list<exprt>> &reverse_symbol_resolve,
+  const exprt &lhs,
+  const exprt &rhs)
 {
   PRECONDITION(lhs.id()==ID_symbol);
   PRECONDITION(rhs.id()==ID_symbol ||
@@ -373,18 +376,29 @@ bool string_refinementt::add_axioms_for_string_assigns(
     set_char_array_equality(lhs, rhs);
     if(rhs.id() == ID_symbol || rhs.id() == ID_array)
     {
-      add_symbol_to_symbol_map(lhs, rhs);
+      add_symbol_to_symbol_map(
+        symbol_resolve,
+        reverse_symbol_resolve,
+        lhs,
+        rhs);
       return false;
     }
     else if(rhs.id()==ID_nondet_symbol)
     {
       add_symbol_to_symbol_map(
-        lhs, generator.fresh_symbol("nondet_array", lhs.type()));
+        symbol_resolve,
+        reverse_symbol_resolve,
+        lhs,
+        generator.fresh_symbol("nondet_array", lhs.type()));
       return false;
     }
     else if(rhs.id()==ID_if)
     {
-      add_symbol_to_symbol_map(lhs, rhs);
+      add_symbol_to_symbol_map(
+        symbol_resolve,
+        reverse_symbol_resolve,
+        lhs,
+        rhs);
       return true;
     }
     else
@@ -396,7 +410,11 @@ bool string_refinementt::add_axioms_for_string_assigns(
   if(is_refined_string_type(rhs.type()))
   {
     exprt refined_rhs=generator.add_axioms_for_refined_string(rhs);
-    add_symbol_to_symbol_map(lhs, refined_rhs);
+    add_symbol_to_symbol_map(
+      symbol_resolve,
+      reverse_symbol_resolve,
+      lhs,
+      refined_rhs);
     return false;
   }
   // Other cases are to be handled by supert::set_to.
diff --git a/src/solvers/refinement/string_refinement.h b/src/solvers/refinement/string_refinement.h
index 1f45b9dece5..f889ebb2c7b 100644
--- a/src/solvers/refinement/string_refinement.h
+++ b/src/solvers/refinement/string_refinement.h
@@ -101,7 +101,6 @@ class string_refinementt final: public bv_refinementt
                  bool simplify=true,
                  bool add_to_index_set=true);
 
-  void add_symbol_to_symbol_map(const exprt &lhs, const exprt &rhs);
   bool add_axioms_for_string_assigns(const exprt &lhs, const exprt &rhs);
   void set_to(const exprt &expr, bool value) override;