Simplify is_mine_symb#1130
Merged
Merged
Conversation
Halbaroth
force-pushed
the
simplify-is_mine_symb
branch
from
1a86a93 to
2ca94c2
Compare
Collaborator
|
@Halbaroth Please rebase |
Collaborator
Author
|
ah we have the same request :) |
Halbaroth
force-pushed
the
simplify-is_mine_symb
branch
from
2ca94c2 to
e843595
Compare
Collaborator
Author
|
Done |
The argument `ty` of `is_mine_symbol` was only used by `Enum` and `Adt` theories because they shared the `Construct` symbol. As we merged these theories, we can remove this argument now.
bclement-ocp
approved these changes
Jun 12, 2024
Halbaroth
added a commit
to Halbaroth/alt-ergo
that referenced
this pull request
Jun 15, 2024
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
Halbaroth
added a commit
to Halbaroth/alt-ergo
that referenced
this pull request
Jun 15, 2024
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
Halbaroth
added a commit
that referenced
this pull request
Jun 18, 2024
* Simple ADTs with a single constructor are records This PR fixes a bug in `D_cnf` that have been exposed by #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
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.
The argument
tyofis_mine_symbolwas only used byEnumandAdttheories because they shared theConstructsymbol.As we merged these theories, we can remove this argument now.
This PR is rebased on #1094