Skip to content

Conversation

grahnen
Copy link
Contributor

@grahnen grahnen commented Mar 27, 2025

FuncDecl for partial/linear/piecewise linear/tree orders.

Z3 specializes these, this is better than adding assertions manually :)

Please help me double check that this does what it's supposed to; and that it does it in a good way.

I am not well versed with the internals of z3 or with this library.

API Reference, section "Special relations"

@toolCHAINZ
Copy link
Member

@grahnen thanks for the PR! Would you be willing to write some unit tests for these new APIs? This will also be useful as an example for how they should be used.

@toolCHAINZ toolCHAINZ added the enhancement New feature or request label Jul 15, 2025
@toolCHAINZ
Copy link
Member

I went ahead and added a doc test for partial_order and some doc comments to each API pointing to the others in this family, as well as pointing to the z3 special relations page as a reference.

Thanks for contributing this!

@toolCHAINZ toolCHAINZ changed the title Add Order instantiation to FuncDecl feat: Special Binary Relation FuncDecls Sep 11, 2025
@toolCHAINZ toolCHAINZ merged commit f8ae967 into prove-rs:master Sep 11, 2025
10 checks passed
@toolCHAINZ toolCHAINZ mentioned this pull request Sep 11, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants