Skip to content

Commit 44693e8

Browse files
Use eval of builtin function in get when available
When we can find a string in the string dependencies graph and the corresponding function can be evaluated we return that result instead of using get_array.
1 parent 56cb571 commit 44693e8

File tree

1 file changed

+6
-0
lines changed

1 file changed

+6
-0
lines changed

src/solvers/refinement/string_refinement.cpp

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2254,6 +2254,12 @@ exprt string_refinementt::get(const exprt &expr) const
22542254
{
22552255
array_string_exprt &arr = to_array_string_expr(ecopy);
22562256
arr.length() = generator.array_pool.get_length(arr);
2257+
2258+
if(
2259+
const auto from_dependencies =
2260+
dependencies.eval(arr, [&](const exprt &expr) { return get(expr); }))
2261+
return *from_dependencies;
2262+
22572263
const auto arr_model_opt =
22582264
get_array(super_get, ns, generator.max_string_length, debug(), arr);
22592265
// \todo Refactor with get array in model

0 commit comments

Comments
 (0)