Skip to content

Sort definitions of SMV models to reduce recursion depth in typecheck #234

New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Open
wants to merge 4 commits into
base: main
Choose a base branch
from

Conversation

mgudemann
Copy link
Contributor

This fixes #17 (superseeding #26 as EBMC code has changed)

@kroening
Copy link
Member

kroening commented Dec 3, 2023

How about using a std::stack?

@mgudemann
Copy link
Contributor Author

For the topological sort? Sure, but this is implemented in cbmc/src/util/graph.h so it would require a change to CBMC.

@kroening
Copy link
Member

kroening commented Dec 3, 2023

For the topological sort? Sure, but this is implemented in cbmc/src/util/graph.h so it would require a change to CBMC.

No, to replace the recursion. Then you don't need the topological sort anymore.

@mgudemann mgudemann force-pushed the feature/topsort_SMV_defines branch 3 times, most recently from 6a09655 to 41a1395 Compare March 28, 2025 07:45
@mgudemann mgudemann force-pushed the feature/topsort_SMV_defines branch from 41a1395 to 79a9715 Compare March 28, 2025 07:48
@mgudemann
Copy link
Contributor Author

I thought about changing this to using a stack, but this requires more work in typecheck_expr_rec and the functionality is already implemented using topsort. If this PR is not included, maybe the topsort should also be removed from CBMC because at the time I added it for this specific reason. It probably only affects SMV files converted from AIG.

@kroening
Copy link
Member

#1040

# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

segfault on typecheck
2 participants