Skip to content

Commit 08812b3

Browse files
Make node point to builtin func they result from
This make finding the function the string results from easier.
1 parent b9718a9 commit 08812b3

File tree

2 files changed

+11
-10
lines changed

2 files changed

+11
-10
lines changed

src/solvers/refinement/string_refinement_util.cpp

+9-10
Original file line numberDiff line numberDiff line change
@@ -478,17 +478,11 @@ optionalt<exprt> string_dependencest::eval(
478478
return eval_string_cache[it->second];
479479

480480
const auto node = string_nodes[it->second];
481-
482-
if(node.dependencies.size() == 1)
481+
if(const auto &f = node.result_from)
483482
{
484-
const auto &f = get_builtin_function(node.dependencies[0]);
485-
const auto result = f.string_result();
486-
if(result && *result == s)
487-
{
488-
const auto value_opt = f.eval(get_value);
489-
eval_string_cache[it->second] = value_opt;
490-
return value_opt;
491-
}
483+
const auto value_opt = get_builtin_function(*f).eval(get_value);
484+
eval_string_cache[it->second] = value_opt;
485+
return value_opt;
492486
}
493487
return {};
494488
}
@@ -525,7 +519,12 @@ bool add_node(
525519
if(
526520
const auto &string_result =
527521
dependencies.get_builtin_function(builtin_function_node).string_result())
522+
{
528523
dependencies.add_dependency(*string_result, builtin_function_node);
524+
auto &node = dependencies.get_node(*string_result);
525+
node.result_from = builtin_function_node;
526+
527+
}
529528
else
530529
add_dependency_to_string_subexprs(
531530
dependencies, *fun_app, builtin_function_node, array_pool);

src/solvers/refinement/string_refinement_util.h

+2
Original file line numberDiff line numberDiff line change
@@ -309,6 +309,8 @@ class string_dependencest
309309
std::size_t index;
310310
// builtin functions on which it depends
311311
std::vector<builtin_function_nodet> dependencies;
312+
// builtin function of which it is the result
313+
optionalt<builtin_function_nodet> result_from;
312314
// In case it depends on a builtin_function we don't support yet
313315
bool depends_on_unknown_builtin_function = false;
314316

0 commit comments

Comments
 (0)