Move method definition to cpp file

Author: romainbrenguier

src/solvers/refinement/string_builtin_function.cpp

@@ -137,6 +137,35 @@ std::vector<mp_integer> string_concatenation_builtin_functiont::eval(
   return result;
 }
 
+string_constraintst string_concatenation_builtin_functiont::constraints(
+  string_constraint_generatort &generator) const
+
+{
+  auto pair = [&]() -> std::pair<exprt, string_constraintst> {
+    if(args.size() == 0)
+      return add_axioms_for_concat(
+        generator.fresh_symbol, result, input1, input2);
+    if(args.size() == 2)
+    {
+      return add_axioms_for_concat_substr(
+        generator.fresh_symbol, result, input1, input2, args[0], args[1]);
+    }
+    UNREACHABLE;
+  }();
+  pair.second.existential.push_back(equal_exprt(pair.first, return_code));
+  return pair.second;
+}
+
+exprt string_concatenation_builtin_functiont::length_constraint() const
+{
+  if(args.size() == 0)
+    return length_constraint_for_concat(result, input1, input2);
+  if(args.size() == 2)
+    return length_constraint_for_concat_substr(
+      result, input1, input2, args[0], args[1]);
+  UNREACHABLE;
+}
+
 optionalt<exprt> string_concat_char_builtin_functiont::eval(
   const std::function<exprt(const exprt &)> &get_value) const
 {
@@ -158,6 +187,20 @@ optionalt<exprt> string_concat_char_builtin_functiont::eval(
   return make_string(input_opt.value(), type);
 }
 
+string_constraintst string_concat_char_builtin_functiont::constraints(
+  string_constraint_generatort &generator) const
+{
+  auto pair = add_axioms_for_concat_char(
+    generator.fresh_symbol, result, input, character);
+  pair.second.existential.push_back(equal_exprt(pair.first, return_code));
+  return pair.second;
+}
+
+exprt string_concat_char_builtin_functiont::length_constraint() const
+{
+  return length_constraint_for_concat_char(result, input);
+}
+
 optionalt<exprt> string_set_char_builtin_functiont::eval(
   const std::function<exprt(const exprt &)> &get_value) const
 {
@@ -174,6 +217,15 @@ optionalt<exprt> string_set_char_builtin_functiont::eval(
   return make_string(input_opt.value(), type);
 }
 
+string_constraintst string_set_char_builtin_functiont::constraints(
+  string_constraint_generatort &generator) const
+{
+  auto pair = add_axioms_for_set_char(
+    generator.fresh_symbol, result, input, position, character);
+  pair.second.existential.push_back(equal_exprt(pair.first, return_code));
+  return pair.second;
+}
+
 exprt string_set_char_builtin_functiont::length_constraint() const
 {
   const exprt out_of_bounds = or_exprt(
@@ -284,6 +336,30 @@ optionalt<exprt> string_insertion_builtin_functiont::eval(
   return make_string(result_value, type);
 }
 
+string_constraintst string_insertion_builtin_functiont::constraints(
+  string_constraint_generatort &generator) const
+{
+  if(args.size() == 1)
+  {
+    auto pair = add_axioms_for_insert(
+      generator.fresh_symbol, result, input1, input2, args[0]);
+    pair.second.existential.push_back(equal_exprt(pair.first, return_code));
+    return pair.second;
+  }
+  if(args.size() == 3)
+    UNIMPLEMENTED;
+  UNREACHABLE;
+}
+
+exprt string_insertion_builtin_functiont::length_constraint() const
+{
+  if(args.size() == 1)
+    return length_constraint_for_insert(result, input1, input2);
+  if(args.size() == 3)
+    UNIMPLEMENTED;
+  UNREACHABLE;
+}
+
 /// Constructor from arguments of a function application.
 /// The arguments in `fun_args` should be in order:
 /// an integer `result.length`, a character pointer `&result[0]`,
@@ -333,6 +409,20 @@ optionalt<exprt> string_of_int_builtin_functiont::eval(
     right_to_left_characters.rbegin(), right_to_left_characters.rend(), type);
 }
 
+string_constraintst string_of_int_builtin_functiont::constraints(
+  string_constraint_generatort &generator) const
+{
+  auto pair = add_axioms_for_string_of_int_with_radix(
+    generator.fresh_symbol,
+    result,
+    arg,
+    radix,
+    0,
+    generator.ns);
+  pair.second.existential.push_back(equal_exprt(pair.first, return_code));
+  return pair.second;
+}
+
 exprt string_of_int_builtin_functiont::length_constraint() const
 {
   const typet &type = result.length().type();
@@ -391,3 +481,12 @@ string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt(
       args.push_back(fun_args[i]);
   }
 }
+
+string_constraintst string_builtin_function_with_no_evalt::constraints(
+  string_constraint_generatort &generator) const
+{
+  auto pair = generator.add_axioms_for_function_application(
+    generator.fresh_symbol, function_application);
+  pair.second.existential.push_back(equal_exprt(pair.first, return_code));
+  return pair.second;
+}

src/solvers/refinement/string_builtin_function.h

@@ -7,9 +7,10 @@
 #include <vector>
 #include <util/optional.h>
 #include <util/string_expr.h>
-#include "string_constraint_generator.h"
 
 class array_poolt;
+class string_constraintst;
+class string_constraint_generatort;
 
 #define CHARACTER_FOR_UNKNOWN '?'
 
@@ -129,18 +130,9 @@ class string_concat_char_builtin_functiont
   }
 
   string_constraintst
-  constraints(string_constraint_generatort &generator) const override
-  {
-    auto pair = add_axioms_for_concat_char(
-      generator.fresh_symbol, result, input, character);
-    pair.second.existential.push_back(equal_exprt(pair.first, return_code));
-    return pair.second;
-  }
+  constraints(string_constraint_generatort &generator) const override;
 
-  exprt length_constraint() const override
-  {
-    return length_constraint_for_concat_char(result, input);
-  }
+  exprt length_constraint() const override;
 };
 
 /// Setting a character at a particular position of a string
@@ -175,13 +167,7 @@ class string_set_char_builtin_functiont
   }
 
   string_constraintst
-  constraints(string_constraint_generatort &generator) const override
-  {
-    auto pair = add_axioms_for_set_char(
-      generator.fresh_symbol, result, input, position, character);
-    pair.second.existential.push_back(equal_exprt(pair.first, return_code));
-    return pair.second;
-  }
+  constraints(string_constraint_generatort &generator) const override;
 
   // \todo: length_constraint is not the best possible name because we also
   // \todo: add constraint about the return code
@@ -298,28 +284,9 @@ class string_insertion_builtin_functiont : public string_builtin_functiont
   }
 
   string_constraintst
-  constraints(string_constraint_generatort &generator) const override
-  {
-    if(args.size() == 1)
-    {
-      auto pair = add_axioms_for_insert(
-        generator.fresh_symbol, result, input1, input2, args[0]);
-      pair.second.existential.push_back(equal_exprt(pair.first, return_code));
-      return pair.second;
-    }
-    if(args.size() == 3)
-      UNIMPLEMENTED;
-    UNREACHABLE;
-  };
+  constraints(string_constraint_generatort &generator) const override;
 
-  exprt length_constraint() const override
-  {
-    if(args.size() == 1)
-      return length_constraint_for_insert(result, input1, input2);
-    if(args.size() == 3)
-      UNIMPLEMENTED;
-    UNREACHABLE;
-  };
+  exprt length_constraint() const override;
 
   bool maybe_testing_function() const override
   {
@@ -359,32 +326,9 @@ class string_concatenation_builtin_functiont final
   }
 
   string_constraintst
-  constraints(string_constraint_generatort &generator) const override
-  {
-    auto pair = [&]() -> std::pair<exprt, string_constraintst> {
-      if(args.size() == 0)
-        return add_axioms_for_concat(
-          generator.fresh_symbol, result, input1, input2);
-      if(args.size() == 2)
-      {
-        return add_axioms_for_concat_substr(
-          generator.fresh_symbol, result, input1, input2, args[0], args[1]);
-      }
-      UNREACHABLE;
-    }();
-    pair.second.existential.push_back(equal_exprt(pair.first, return_code));
-    return pair.second;
-  };
+  constraints(string_constraint_generatort &generator) const override;
 
-  exprt length_constraint() const override
-  {
-    if(args.size() == 0)
-      return length_constraint_for_concat(result, input1, input2);
-    if(args.size() == 2)
-      return length_constraint_for_concat_substr(
-        result, input1, input2, args[0], args[1]);
-    UNREACHABLE;
-  }
+  exprt length_constraint() const override;
 };
 
 /// String creation from other types
@@ -436,18 +380,7 @@ class string_of_int_builtin_functiont : public string_creation_builtin_functiont
   }
 
   string_constraintst
-  constraints(string_constraint_generatort &generator) const override
-  {
-    auto pair = add_axioms_for_string_of_int_with_radix(
-      generator.fresh_symbol,
-      result,
-      arg,
-      radix,
-      0,
-      generator.ns);
-    pair.second.existential.push_back(equal_exprt(pair.first, return_code));
-    return pair.second;
-  }
+  constraints(string_constraint_generatort &generator) const override;
 
   exprt length_constraint() const override;
 
@@ -505,13 +438,7 @@ class string_builtin_function_with_no_evalt : public string_builtin_functiont
   }
 
   string_constraintst
-  constraints(string_constraint_generatort &generator) const override
-  {
-    auto pair = generator.add_axioms_for_function_application(
-      generator.fresh_symbol, function_application);
-    pair.second.existential.push_back(equal_exprt(pair.first, return_code));
-    return pair.second;
-  };
+  constraints(string_constraint_generatort &generator) const override;
 
   exprt length_constraint() const override
   {