Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Assertion failed in Expr on next #1099

Closed
Halbaroth opened this issue Apr 29, 2024 · 0 comments · Fixed by #1102
Closed

Assertion failed in Expr on next #1099

Halbaroth opened this issue Apr 29, 2024 · 0 comments · Fixed by #1102
Assignees
@Halbaroth
Labels
bug
Milestone
2.6.0

Comments

@Halbaroth
Copy link
Collaborator

The next branch raises an assertion on 23 tests of our internal benchmark set. We should fix this issue before releasing the next
version of Alt-Ergo:

alt-ergo: option '--frontend': this option is deprecated and will be ignored in the next version
Fatal error: exception File "src/lib/structures/expr.ml", line 1707, characters 4-10: Assertion failed
Raised at Stdlib__Hashtbl.MakeSeeded.find in file "hashtbl.ml", line 389, characters 17-32
Called from AltErgoLib__Satml_types.Flat_Formula.make in file "src/lib/structures/satml_types.ml", line 626, characters 10-29
Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52
Called from Alt_ergo_common__Solving_loop.main.d_fe in file "src/bin/common/solving_loop.ml", line 1047, characters 6-1023
@Halbaroth Halbaroth added the bug label Apr 29, 2024
@Halbaroth Halbaroth added this to the 2.6.0 milestone Apr 29, 2024
@Halbaroth Halbaroth self-assigned this Apr 29, 2024
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this issue Apr 30, 2024
@Halbaroth
Fix the issue 1099
b289987 
The `D_cnf` module didn't use the flag `toplevel` as it was done in `Cnf`.
This flag is important because the `Expr` AST doesn't store quantified
type variables with binders it does for the term variable. Instead, we
use a `prenex polymorphism` approach, which means the quantified type
variables are at the top level only.

I believe this PR fixes the issue OCamlPro#1099.
@Halbaroth Halbaroth mentioned this issue Apr 30, 2024
Merged
@Halbaroth Halbaroth linked a pull request Apr 30, 2024 that will close this issue
Fix issue 1099 #1102
Merged
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this issue Apr 30, 2024
@Halbaroth
Fix issue 1099
a55dcc8 
The `D_cnf` module didn't use the flag `toplevel` as it was done in `Cnf`.
This flag is important because the `Expr` AST doesn't store quantified
type variables with binders as it does for the term variable. Instead, we
use a `prenex polymorphism` approach, which means the quantified type
variables are at the top level only.

I believe this PR fixes the issue OCamlPro#1099.
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this issue Apr 30, 2024
@Halbaroth
Fix issue 1099
1be1c40 
The `D_cnf` module didn't use the flag `toplevel` as it was done in `Cnf`.
This flag is important because the `Expr` AST doesn't store quantified
type variables with binders as it does for the term variable. Instead, we
use a `prenex polymorphism` approach, which means the quantified type
variables are at the top level only.

I believe this PR fixes the issue OCamlPro#1099.
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this issue May 3, 2024
@Halbaroth
Documentation of quantified type in Expr
3d9c596 
While fixing the issue OCamlPro#1099, I wrote a bit of documentation for `Expr`.
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this issue May 3, 2024
@Halbaroth
Documentation of quantified type in Expr
51c6209 
While fixing the issue OCamlPro#1099, I wrote a bit of documentation for `Expr`.
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this issue May 3, 2024
@Halbaroth
Documentation of quantified type in Expr
156135b 
While fixing the issue OCamlPro#1099, I wrote a bit of documentation for `Expr`.
@Halbaroth Halbaroth mentioned this issue May 3, 2024
Merged
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this issue May 10, 2024
@Halbaroth
Documentation of quantified type in Expr
f7463a5 
While fixing the issue OCamlPro#1099, I wrote a bit of documentation for `Expr`.
Halbaroth added a commit that referenced this issue May 10, 2024
@Halbaroth
Documentation of quantified type in Expr (#1106)
8661027 
* Documentation of quantified type in `Expr`

While fixing the issue #1099, I wrote a bit of documentation for `Expr`.

* Review changes

* Clarify CNF form of implications
Halbaroth added a commit to Halbaroth/alt-ergo that referenced this issue Jun 11, 2024
@Halbaroth
Fix issue 1099
af77783 
The `D_cnf` module didn't use the flag `toplevel` as it was done in `Cnf`.
This flag is important because the `Expr` AST doesn't store quantified
type variables with binders as it does for the term variable. Instead, we
use a `prenex polymorphism` approach, which means the quantified type
variables are at the top level only.

I believe this PR fixes the issue OCamlPro#1099.
@Halbaroth Halbaroth mentioned this issue Jun 12, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@Halbaroth Halbaroth

Labels
bug
Projects
None yet
Milestone
2.6.0
Development

Successfully merging a pull request may close this issue.

Fix issue 1099 Halbaroth/alt-ergo
1 participant
@Halbaroth