Skip to content

Add 240+16 instances of the string matching problems. #10

New issue

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

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

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Apr 10, 2025

Conversation

Bazoka13
Copy link
Contributor

Instances include substring matching problems and string matching problems with wildcards.

The former determines whether the pattern string exists in the text string. Compared with randomly generated instances, the benchmark includes more complex instances(100+16 instances).

The latter determines whether two strings with wildcards match. It uses re.allchar and (re.* re.allchar) to represent wildcards, and compares the result of re.inter with re.none to determine whether they match. Modern SMT2 solvers are not able to solve this type of problem well(130 instances).

@hansjoergschurr
Copy link
Collaborator

Thank you for the submission.
The CI complains, because of the .DS_Store files. We will have to remove those.

@Bazoka13
Copy link
Contributor Author

I have removed the .DS_Store files, sorry about that.

@hansjoergschurr hansjoergschurr merged commit ef469b3 into SMT-LIB:main Apr 10, 2025
2 checks passed
@hansjoergschurr
Copy link
Collaborator

Thank you again for the submission. This looks like an interesting hard benchmark set. We will likely do some more tests (like running SMT solvers on the benchmarks), but they will be likely included in the upcoming release.

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

Successfully merging this pull request may close these issues.

2 participants