Skip to content

Commit 54a4d7d

Browse files
Add class for builtin function with no eval
This is for builtin functions supported by string_constraint_generatort but not string_builtin_functiont.
1 parent 8e0f974 commit 54a4d7d

File tree

1 file changed

+31
-0
lines changed

1 file changed

+31
-0
lines changed

src/solvers/refinement/string_builtin_function.h

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -197,4 +197,35 @@ class string_test_builtin_functiont : public string_builtin_functiont
197197
}
198198
};
199199

200+
/// Functions that are not yet supported in this class but are supported by
201+
/// string_constraint_generatort.
202+
/// \note Ultimately this should be disappear, once all builtin function have
203+
/// a corresponding string_builtin_functiont class.
204+
class string_builtin_function_with_no_evalt : public string_builtin_functiont
205+
{
206+
public:
207+
function_application_exprt function_application;
208+
optionalt<array_string_exprt> string_res;
209+
std::vector<array_string_exprt> string_args;
210+
std::vector<exprt> args;
211+
std::string name() const override
212+
{
213+
return id2string(function_application.id());
214+
}
215+
std::vector<array_string_exprt> string_arguments() const override
216+
{
217+
return std::vector<array_string_exprt>(string_args);
218+
}
219+
optionalt<array_string_exprt> string_result() const override
220+
{
221+
return string_res;
222+
}
223+
224+
optionalt<exprt>
225+
eval(const std::function<exprt(const exprt &)> &get_value) const override
226+
{
227+
return {};
228+
}
229+
};
230+
200231
#endif // CPROVER_SOLVERS_REFINEMENT_STRING_BUILTIN_FUNCTION_H

0 commit comments

Comments
 (0)