From 0346f87dddb24a969ef398a88a63a522158784c3 Mon Sep 17 00:00:00 2001
From: reuk <reuk@users.noreply.github.com>
Date: Fri, 6 Oct 2017 16:34:16 +0100
Subject: [PATCH] Add a join function for strings

---
 src/util/string_utils.h | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/src/util/string_utils.h b/src/util/string_utils.h
index 5779596cdcf..f818501d7ae 100644
--- a/src/util/string_utils.h
+++ b/src/util/string_utils.h
@@ -10,6 +10,7 @@ Author: Daniel Poetzl
 #ifndef CPROVER_UTIL_STRING_UTILS_H
 #define CPROVER_UTIL_STRING_UTILS_H
 
+#include <ostream>
 #include <string>
 #include <vector>
 
@@ -33,4 +34,31 @@ std::string trim_from_last_delimiter(
   const std::string &s,
   const char delim);
 
+/// Prints items to an stream, separated by a constant delimiter
+/// \tparam It An iterator type
+/// \tparam Delimiter A delimiter type which supports printing to ostreams
+/// \param os An ostream to write to
+/// \param b Iterator pointing to first item to print
+/// \param e Iterator pointing past last item to print
+/// \param delimiter Object to print between each item in the iterator range
+/// \return A reference to the ostream that was passed in
+template<typename Stream, typename It, typename Delimiter>
+Stream &join_strings(
+  Stream &os,
+  const It b,
+  const It e,
+  const Delimiter &delimiter)
+{
+  if(b==e)
+  {
+    return os;
+  }
+  os << *b;
+  for(auto it=std::next(b); it!=e; ++it)
+  {
+    os << delimiter << *it;
+  }
+  return os;
+}
+
 #endif