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

Sort disjuncts generated by ZipOracle #2149

Merged
merged 4 commits into from
Sep 9, 2022
Merged

Sort disjuncts generated by ZipOracle #2149

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
6612422
Sort disjuncts generated by ZipOracle
thpani Sep 6, 2022
d3496bf
Add changelog
thpani Sep 6, 2022
7bd2343
Merge branch 'main' into th/sort-zip-oracle
thpani Sep 9, 2022
396fb41
Merge branch 'main' into th/sort-zip-oracle
apalache-bot Sep 9, 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
1 change: 1 addition & 0 deletions .unreleased/bug-fixes/sort-zip-oracle.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Sort SMT disjuncts generated by `ZipOracle`, see #2149
5 changes: 4 additions & 1 deletion tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,10 @@ class CherryPick(rewriter: SymbStateRewriter) {
// This optimization gives us a 20% speed up on a small set of benchmarks.
val groups = elems.indices.groupBy(elems(_))
if (groups.size < elems.size) {
val zipOracle = new ZipOracle(oracle, groups.values.toList.map(is => Set(is: _*)))
val zipOracle = new ZipOracle(oracle,
// Sort indices, it determines the order of SMT disjuncts generated by the oracle;
// See https://github.com/informalsystems/apalache/issues/2120
groups.values.toSeq.map(_.sorted))
return pickByOracle(state, zipOracle, groups.keys.toSeq, elseAssert)
}

Expand Down
6 changes: 4 additions & 2 deletions tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/ZipOracle.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,11 @@ import at.forsyte.apalache.tla.lir.{BoolT1, TlaEx}
* @param backOracle
* the background oracle whose values are grouped together
* @param groups
* a list of groups over the indices of the background oracle
* A list of groups over the indices of the background oracle. Indices within each group must be sorted, as the
* sorting determines the order of generated SMT constraints; see
* https://github.com/informalsystems/apalache/issues/2120.
*/
class ZipOracle(backOracle: Oracle, groups: List[Set[Int]]) extends Oracle {
class ZipOracle(backOracle: Oracle, groups: Seq[Seq[Int]]) extends Oracle {
override def size: Int = groups.size

override def whenEqualTo(state: SymbState, index: Int): TlaEx = {
Expand Down