Skip to content

Commit c477d8e

Browse files
Compute dependency graph in string_refinement
This is only activated with the debug option. This can be useful to detect problem in the solver or in the dependency graph computation.
1 parent 699f042 commit c477d8e

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

src/solvers/refinement/string_refinement.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -679,6 +679,15 @@ decision_proceduret::resultt string_refinementt::dec_solve()
679679

680680
#ifdef DEBUG
681681
output_equations(debug(), equations, ns);
682+
683+
dependency_grapht dependencies;
684+
for(const equal_exprt &eq : equations)
685+
add_node(dependencies, eq, generator.array_pool);
686+
687+
debug() << "dec_solve: dependency graph:" << eom;
688+
dependencies.output_dot(debug(), [&](const exprt &e) { // NOLINT
689+
return from_expr(ns, "", e);
690+
});
682691
#endif
683692

684693
debug() << "dec_solve: Replace function applications" << eom;

0 commit comments

Comments
 (0)