Add a linear_functiont::format for debugging

This can be useful for debugging or testing the class.

Author: romainbrenguier

src/solvers/strings/string_constraint_instantiation.cpp

@@ -156,6 +156,15 @@ exprt linear_functiont::solve(
   return f.to_expr(positive);
 }
 
+std::string linear_functiont::format()
+{
+  std::ostringstream stream;
+  stream << constant_coefficient;
+  for(const auto &pair : coefficients)
+    stream << " + " << pair.second << " * " << ::format(pair.first);
+  return stream.str();
+}
+
 /// Instantiates a string constraint by substituting the quantifiers.
 /// For a string constraint of the form `forall q. P(x)`,
 /// substitute `q` the universally quantified variable of `axiom`, by

src/solvers/strings/string_constraint_instantiation.h

@@ -58,6 +58,9 @@ class linear_functiont
   /// returns the expression `v - x`.
   static exprt solve(linear_functiont f, const exprt &var, const exprt &val);
 
+  /// Format the linear function as a string, can be used for debugging
+  std::string format();
+
 private:
   mp_integer constant_coefficient;
   std::unordered_map<exprt, mp_integer, irep_hash> coefficients;