Simple ADTs with a single constructor are records#1146
Merged
Conversation
This PR fixes a bug in `D_cnf` that have been exposed by OCamlPro#1130. Before merging `Enum` into `ADT` the situation was as follows: - simple ADT with several constructors and with at least one payload was sent to the `Adt` theory - simple ADT with several constructors but no payload was sent to `Enum` theory - simple ADT with a single constructor was sent to the `Record` theory. The last corner case includes a corner corner case: An ADT with a single constructor without payload (so basically the unit type with an extra step...) The `D_cnf` included a bug. It produced single constructors without payload of type ADT instead of type record but the check done in `is_mine_symb` prevented from sending it to `Adt`. As I removed this check, we got an assert on the following input: ```smt2 (set-logic ALL) (declare-datatype t ((Record))) (define-fun a () t Record) (check-sat) ``` After this patch, the situation is as follows: - simple ADT with several constructors is sent to the `Adt` theory - simple ADT with only one constructor is sent to the `Record` theory - mutually recursive ADT whose all the types are record is sent to the `Record` theory
hra687261
approved these changes
Jun 17, 2024
hra687261
reviewed
Jun 17, 2024
Comment on lines
+978
to
+981
| | Tunit -> | ||
| E.void | ||
| | ty -> | ||
| Fmt.failwith "unexpected type %a@." Ty.print ty |
Contributor
There was a problem hiding this comment.
Is there a test that shows that Tunit is used? And that we crash if we don't match it here?
Collaborator
Author
There was a problem hiding this comment.
There are 2000 regressions on ae-format without this case, so yes, we have tests :)
Actually the builtin unit type of Dolmen is an ADT but a distinct builtin type Tunit in Alt-Ergo. It's a corner corner corner case...
I tested this PR on ae-format and now there is no regression anymore ;)
Collaborator
Author
There was a problem hiding this comment.
I will add a unit test to catch unit (sic) case
Collaborator
Author
There was a problem hiding this comment.
Finally, I removed the Ty.Tunit type of AE in #1148, so this corner case disappears.
Halbaroth
added a commit
to Halbaroth/alt-ergo
that referenced
this pull request
Jul 24, 2024
* Simple ADTs with a single constructor are records This PR fixes a bug in `D_cnf` that have been exposed by OCamlPro#1130. Before merging `Enum` into `ADT` the situation was as follows: - simple ADT with several constructors and with at least one payload was sent to the `Adt` theory - simple ADT with several constructors but no payload was sent to `Enum` theory - simple ADT with a single constructor was sent to the `Record` theory. The last corner case includes a corner corner case: An ADT with a single constructor without payload (so basically the unit type with an extra step...) The `D_cnf` included a bug. It produced single constructors without payload of type ADT instead of type record but the check done in `is_mine_symb` prevented from sending it to `Adt`. As I removed this check, we got an assert on the following input: ```smt2 (set-logic ALL) (declare-datatype t ((Record))) (define-fun a () t Record) (check-sat) ``` After this patch, the situation is as follows: - simple ADT with several constructors is sent to the `Adt` theory - simple ADT with only one constructor is sent to the `Record` theory - mutually recursive ADT whose all the types are record is sent to the `Record` theory
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
This PR fixes a bug in
D_cnfthat have been exposed by #1130. Before mergingEnumintoADTthe situation was as follows:AdttheoryEnumtheoryRecordtheory.The last corner case includes a corner corner case: an ADT with a single constructor without payload (so basically the unit type with an extra step...)
The
D_cnfincluded a bug. It produced single constructors without payload of type ADT instead of type record but the check done inis_mine_symbprevented from sending it toAdt. As I removed this check, we got an assert on the following input:After this patch, the situation is as follows:
AdttheoryRecordtheoryRecordtheory