split_string with return value now also has 'strip' and 'remove_empty'

Author: Daniel Kroening

src/util/string_utils.cpp

@@ -116,10 +116,14 @@ void split_string(
   right=result[1];
 }
 
-std::vector<std::string> split_string(const std::string &s, char delim)
+std::vector<std::string> split_string(
+  const std::string &s,
+  char delim,
+  bool strip,
+  bool remove_empty)
 {
   std::vector<std::string> result;
-  split_string(s, delim, result);
+  split_string(s, delim, result, strip, remove_empty);
   return result;
 }
 

src/util/string_utils.h

@@ -30,7 +30,11 @@ void split_string(
   std::string &right,
   bool strip=false);
 
-std::vector<std::string> split_string(const std::string &s, char delim);
+std::vector<std::string> split_string(
+  const std::string &s,
+  char delim,
+  bool strip = false,
+  bool remove_empty = false);
 
 std::string trim_from_last_delimiter(
   const std::string &s,