VeriFIT / mata

A fast and simple automata library
MIT License
14 stars 11 forks source link

Implement NFT operations for solving string constraints `replace(_re)()` and `replace(_re)_all()` #391

Closed Adda0 closed 4 months ago

Adda0 commented 4 months ago

This PR implements the first part of implementation of reluctant replace operations for string solving. This PR includes implementation of functions to create reluctant NFAs and NFTs which perform the reluctant match of a regex, and reluctant replacement operations (for replace_re_all() and replace_re() operations), respectively. Furthermore, the PR implements creation of begin marker DFT which precedes the reluctant replace NFT in reluctant replace modelling.

This PR implements creation of NFTs for reluctant replace of:

Further implementation except for optimization of the current methods may include generation of NFTs for finite regular language replacement. However, I believe that in our implementation (using data structure Delta), the NFT's state space would explode

codecov[bot] commented 4 months ago

Codecov Report

Attention: Patch coverage is 92.60204% with 29 lines in your changes are missing coverage. Please review.

Project coverage is 74.66%. Comparing base (f0ac876) to head (73ad4f6). Report is 1 commits behind head on states_with_levels.

Files Patch % Lines
src/nft/operations.cc 75.71% 13 Missing and 4 partials :warning:
src/nft/strings.cc 95.58% 6 Missing and 6 partials :warning:
Additional details and impacted files ```diff @@ Coverage Diff @@ ## states_with_levels #391 +/- ## ====================================================== + Coverage 73.43% 74.66% +1.23% ====================================================== Files 43 43 Lines 5180 5487 +307 Branches 1173 1215 +42 ====================================================== + Hits 3804 4097 +293 - Misses 939 947 +8 - Partials 437 443 +6 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

Adda0 commented 4 months ago

I will merge the PR immediately due to time constraint reasons. The reviewers can submit their review later and the issues raised in the reviews will be resolved in future PRs.