[SMT] Add function application operation, function and uninterpreted sort types #6847
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
uenoku
reviewed
Mar 18, 2024
math-fehr
approved these changes
Mar 18, 2024
There was a problem hiding this comment.
Nice! I would just rename declare to declare-fun, to follow SMT-LIB.
Note also that having two separate functions might make some matching/lowerings more annoying, as we will need to check what is the result type of the declare-fun. But I'm not sure what is best, so I'm fine with keeping them merged.
Note that we need to be clear on one part of the semantics. Functions with no arguments do not exist in SMT-LIB. Or at least, they cannot be called, as they are equivalent to their non-function value type.
maerhart
force-pushed
the
maerhart-smt-quantifiers
branch
from
672949c
to
2f48229
Compare
maerhart
force-pushed
the
maerhart-smt-functions
branch
from
2c3f817
to
94b3bab
Compare
maerhart
force-pushed
the
maerhart-smt-functions
branch
from
94b3bab
to
8719bb4
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Recursive functions are not (yet) supported and would require their own operations.