diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 6279ec7f5aa..aeabd7e28ea 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -166,6 +166,7 @@ SRC = $(BOOLEFORCE_SRC) \ refinement/string_builtin_function.cpp \ refinement/string_refinement.cpp \ refinement/string_refinement_util.cpp \ + refinement/string_constraint.cpp \ refinement/string_constraint_generator_code_points.cpp \ refinement/string_constraint_generator_comparison.cpp \ refinement/string_constraint_generator_concat.cpp \ diff --git a/src/solvers/refinement/string_constraint.cpp b/src/solvers/refinement/string_constraint.cpp new file mode 100644 index 00000000000..4312dd4b745 --- /dev/null +++ b/src/solvers/refinement/string_constraint.cpp @@ -0,0 +1,21 @@ +/*******************************************************************\ + + Module: String solver + + Author: Diffblue Ltd. + +\*******************************************************************/ + +#include "string_constraint.h" + +string_constraintt::string_constraintt( + symbol_exprt _univ_var, + exprt lower_bound, + exprt upper_bound, + exprt body) + : univ_var(_univ_var), + lower_bound(lower_bound), + upper_bound(upper_bound), + body(body) +{ +} diff --git a/src/solvers/refinement/string_constraint.h b/src/solvers/refinement/string_constraint.h index 3284faa6305..ee643998dfc 100644 --- a/src/solvers/refinement/string_constraint.h +++ b/src/solvers/refinement/string_constraint.h @@ -71,13 +71,7 @@ class string_constraintt final symbol_exprt _univ_var, exprt lower_bound, exprt upper_bound, - exprt body) - : univ_var(_univ_var), - lower_bound(lower_bound), - upper_bound(upper_bound), - body(body) - { - } + exprt body); // Default bound inferior is 0 string_constraintt(symbol_exprt univ_var, exprt upper_bound, exprt body)