Skip to content
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.

Sign up for GitHub

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

Jump to bottom

String theory support #165

Draft
wants to merge 65 commits into
base: main
Choose a base branch
from
Draft

String theory support #165

wants to merge 65 commits into from

Conversation

raf-nr
Copy link

@raf-nr raf-nr commented Dec 3, 2024

No description provided.

raf-nr added 17 commits December 3, 2024 16:50
@raf-nr
Add string sort to core
183449f
@raf-nr
Add regex sort to core
25db759
@raf-nr
Add string and regex sorts to context
3b52e78
@raf-nr
Implement string literal's expr and decl
6815d4d
@raf-nr
Implement regex literal's expr and decl
e98b386
@raf-nr
Implement strings concatenation
c52235a
@raf-nr
Implement strings length expr and decl
2bdb945
@raf-nr
Implement expr and decl for translation string to a regex
779b5c2
@raf-nr
Implement regular expressions concatenation
4b8d5ad
@raf-nr
Implement regular expressions union
0099dc3
@raf-nr
Implement regular expressions intersection
ce1a550
@raf-nr
Implement regular expressions difference and Kleene closure
743b758
@raf-nr
Implement regular expressions Kleene cross
3a1c7c1
@raf-nr
Implement prefixOf and suffixOf strings' operations
5a139cd
@raf-nr
Implement operation to check whether a string belongs to a regex
fd259a5
@raf-nr
Implement operations for comparing strings
2a500d7
@raf-nr
Implement regular expression complement operation
d771e78
Saloed
Saloed reviewed Dec 4, 2024
View reviewed changes
ksmt-core/src/main/kotlin/io/ksmt/utils/DefaultValueSampler.kt Outdated
import io.ksmt.sort.KSort
import io.ksmt.sort.KSortVisitor
import io.ksmt.sort.KUninterpretedSort
import io.ksmt.sort.*
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please, avoid such changes

raf-nr added 30 commits December 9, 2024 23:37
@raf-nr
Add string theory to KTheory class
c8958dc
@raf-nr
Fix str name in KTheory class
c5b9f7e
@raf-nr
Implement string and regex sorts cvc5 internalizer
2e2286d
@raf-nr
Add string and regex expressions internalizer for cvc5
eac27d5
@raf-nr
Add cvc5 internalizer for substrings and indexOf expressions
3dc16f8
@raf-nr
Implement converter from cvc5 to ksmt
62b1a6a
@raf-nr
Implement string/regex methods for cvc5 uninterpreted sort collector
811d531
@raf-nr
Add exceptions that Yices does not support string theory
97bead4
@raf-nr
Fix typo in exceptions' messages
b3ecd8a
@raf-nr
Fix yices solver configuration after adding string theory
81ac05f
@raf-nr
Delete regex literal expression
ca8bff6
@raf-nr
Fix string theory name in KTheory class
b54264f
@raf-nr
Change the names of classes and methods, do the code formatting
6daeecc
@raf-nr
Update sort visitor implementation for theory requirement
ce19526
@raf-nr
Add string and regex sorts to z3 sort internalizer
c9e2e19
@raf-nr
Implement z3 internalizer some methods for strings
07bdf4b
@raf-nr
Add string literals printer with quotes
18d690d
@raf-nr
Implement toLower, toUpper and reverse string operations
3e7f8bd
@raf-nr
Add string and regex default values
a124b8b
@raf-nr
Fix bug with regex constants in cvc5
ceb95a2
@raf-nr
Add string and regex sorts serializer and deserializer
9c2e89b
@raf-nr
Add string and regex expressions serializer/deserializer
1e31092
@raf-nr
Partially implement z3 string internalizer/converter
17d40f5
@raf-nr
Fully implement z3 converter
8f0921e
@raf-nr
Implement regex power and loop operations
d16f8d9
@raf-nr
Fix regex power and loop expr deserializer
57db57a
@raf-nr
Add stubs in symfpu visitors
4f3c819
@raf-nr
Fix typo in z3 converter
0c22147
@raf-nr
Describe functions for further simplification of expressions
dbb8531
@raf-nr
Fix cvc5 sort converter
a865074
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Saloed Saloed Saloed left review comments

At least 1 approving review is required to merge this pull request.

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@raf-nr @Saloed