Skip to content

Theory of rational relations (custom transducers) - #405

Merged
jurajsic merged 61 commits into
develfrom
rational_relations
Jul 25, 2026
Merged

Theory of rational relations (custom transducers)#405
jurajsic merged 61 commits into
develfrom
rational_relations

Conversation

@jurajsic

Copy link
Copy Markdown
Member

No description provided.

@jurajsic
jurajsic requested a review from Copilot July 21, 2026 23:12

Copilot AI left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

Copilot was unable to review this pull request because the user who requested the review has reached their quota limit.

@jurajsic jurajsic changed the title [WIP] Theory of rational relations (custom transducers) Theory of rational relations (custom transducers) Jul 22, 2026
@jurajsic
jurajsic marked this pull request as ready for review July 22, 2026 11:23
@jurajsic
jurajsic requested a review from vhavlena July 22, 2026 11:23
@jurajsic
jurajsic requested a review from Adda0 July 23, 2026 10:02

@vhavlena vhavlena left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Great work! Just a couple of minor comments.

Comment thread src/smt/theory_str_noodler/theory_str_noodler_final_check.cpp Outdated
Comment thread src/smt/theory_str_noodler/theory_str_noodler.cpp Outdated
Comment thread src/ast/seq_decl_plugin.cpp Outdated
Comment thread src/ast/rewriter/seq_rewriter.cpp
Comment thread src/ast/rewriter/seq_rewriter.cpp Outdated
@vhavlena

Copy link
Copy Markdown
Collaborator

Also, can you add e2e tests containing rat.compose (+ other uncovered constructions?). We also discussed that it would be nice to have a projection operator.

@jurajsic

Copy link
Copy Markdown
Member Author

Also, can you add e2e tests containing rat.compose (+ other uncovered constructions?). We also discussed that it would be nice to have a projection operator.

I added the tests.I would not add the projection operator for now, it would be a new regex operator and I am not sure what everything I need to change for it to work properly. We will anyway support only explicit rational relations, and I think for that projection is not that needed.

Comment thread ADDITIONAL_FUNCTIONS.md Outdated
@jurajsic
jurajsic merged commit bf5cc34 into devel Jul 25, 2026
4 checks passed
@jurajsic
jurajsic deleted the rational_relations branch July 25, 2026 09:09
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.

3 participants