Add an linear_functiont::add for linear function

This will be useful for instance to compute the inverse of a function.

Author: romainbrenguier

src/solvers/strings/string_constraint_instantiation.cpp

@@ -91,6 +91,14 @@ linear_functiont::linear_functiont(const exprt &f)
   }
 }
 
+void linear_functiont::add(const linear_functiont &other)
+{
+  PRECONDITION(type == other.type);
+  constant_coefficient += other.constant_coefficient;
+  for(auto pair : other.coefficients)
+    coefficients[pair.first] += pair.second;
+}
+
 exprt linear_functiont::to_expr(bool negated) const
 {
   exprt sum = nil_exprt{};

src/solvers/strings/string_constraint_instantiation.h

@@ -48,6 +48,9 @@ struct linear_functiont
   /// its cannonical representation
   explicit linear_functiont(const exprt &f);
 
+  /// Make this function the sum of the current function with \p other
+  void add(const linear_functiont &other);
+
   /// \param negated: optional Boolean asking to negate the function
   /// \return an expression corresponding to the linear function
   exprt to_expr(bool negated = false) const;