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

Make records as they are work in the arrays encoding #1419

Merged
merged 16 commits into from
Mar 8, 2022
Merged

Make records as they are work in the arrays encoding #1419

Changes from 1 commit
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
5d3f30f
fix DomainRule with Records in the arrays encoding
rodrigo7491 Feb 23, 2022
3a7b380
fix record cherry pick in the arrays encoding
rodrigo7491 Feb 28, 2022
6869af9
remove EqRuleWithArrays
rodrigo7491 Feb 28, 2022
c46a828
Merge branch 'unstable' of https://github.com/informalsystems/apalach…
rodrigo7491 Feb 28, 2022
c0c71b8
fix merge conflict
rodrigo7491 Feb 28, 2022
dce272d
fix fun application bug in the arrays encoding
rodrigo7491 Mar 2, 2022
e181f4d
Merge branch 'unstable' of https://github.com/informalsystems/apalach…
rodrigo7491 Mar 2, 2022
42ff7a3
update release notes
rodrigo7491 Mar 2, 2022
e2db7ab
Update tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEqu…
rodrigo7491 Mar 2, 2022
5a2d262
Update tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEqu…
rodrigo7491 Mar 2, 2022
f6c0f06
Update tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/D…
rodrigo7491 Mar 2, 2022
09d4fc7
address review comments
rodrigo7491 Mar 2, 2022
58b0e6c
Merge branch 'enable-records-in-arrays-encoding' of https://github.co…
rodrigo7491 Mar 2, 2022
36059fb
fix quantifier use on funApp with arrays
rodrigo7491 Mar 7, 2022
195f8a0
Merge branch 'unstable' of https://github.com/informalsystems/apalach…
rodrigo7491 Mar 7, 2022
93a5942
Merge branch 'unstable' into enable-records-in-arrays-encoding
rodrigo7491 Mar 8, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Update tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/D… 
…omainRuleWithArrays.scala

Co-authored-by: Igor Konnov <igor@informal.systems>
  • Loading branch information
@rodrigo7491 @konnov
rodrigo7491 and konnov committed Mar 2, 2022
commit f6c0f0675d00b78e186ea0e9920de227699c815a
1 change: 0 additions & 1 deletion tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRuleWithArrays.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,6 @@ class DomainRuleWithArrays(rewriter: SymbStateRewriter, intRangeCache: IntRangeC
val funState = rewriter.rewriteUntilDone(state.setRex(funEx))
val funCell = funState.asCell

// no type information from the type finder is needed, as types are propagated in a straightforward manner
// TODO: consider records, tuples, and sequences in the arrays encoding
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

is this TODO obsolete?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not really. It is there as a reminder of what was not touched for when we decide to encode these features differently.

funCell.cellType match {
case RecordT(_) =>
Expand Down