Remove chain IR operator #1354
Remove chain IR operator #1354
Conversation
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCupRule.scala
Show resolved
Hide resolved
| val cons = consChain(cells) | ||
| solverContext.assertGroundExpr(tla.apalacheAssignChain(set.toNameEx, cons)) | ||
| } | ||
| solverContext.assertGroundExpr(tla.and(cells.map(c => tla.apalacheStoreInSet(c.toNameEx, set.toNameEx)): _*)) |
There was a problem hiding this comment.
shall we introduce a loop over cells that pushes assertions over individual cells? By doing so, we will avoid the same bottleneck with recursion.
There was a problem hiding this comment.
Good call, will change it to
for (cell <- cells) solverContext.assertGroundExpr(tla.apalacheStoreInSet(cell.toNameEx, set.toNameEx))
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetCupRule.scala
Show resolved
Hide resolved
| } | ||
|
|
||
| val pointingSets = (sets.zip(elemsOfSets) filter (isPointedBySet _).tupled) map (_._1) |
There was a problem hiding this comment.
pointingSets is always non-empty, right? Maybe add an assertion.
| val cons = consChain(elemsCells) | ||
| rewriter.solverContext.assertGroundExpr(tla.apalacheAssignChain(newSetCell.toNameEx, cons)) | ||
| def addOneElemCons(elemCell: ArenaCell): Unit = { | ||
| def isPointedBySet(set: ArenaCell, setElems: Set[ArenaCell]): Boolean = setElems.contains(elemCell) |
There was a problem hiding this comment.
setElems.contains(elemCell) is linear in setElems, and addOneElemCons is called for every element. Shall we worry about that?
There was a problem hiding this comment.
It is not nice, but at least it does not affect solving time. It is not obvious to me how we can improve this.
There was a problem hiding this comment.
A quick fix is just to introduce a set like val setElemsAsSet = setElems.toSet (outside this loop!). It should decrease the cost of contains.
There was a problem hiding this comment.
Not sure what this will do. setElems is already a Set[ArenaCell].
I imagine you meant to have val setElemsAsSet = elemsOfSets.toSet outside addOneElemCons, and use setElemsAsSet instead of elemsOfSets in the definition of pointingSets. Doesn't the call to isPointedBySet typecast to Set[ArenaCell] regardless?
There was a problem hiding this comment.
Oh, setElems is already a set. I got confused. Ignore the above comments then!
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
Outdated
Show resolved
Hide resolved
…olverContext.scala Co-authored-by: Igor Konnov <igor@informal.systems>
Codecov Report
@@ Coverage Diff @@
## unstable #1354 +/- ##
============================================
- Coverage 75.24% 75.12% -0.13%
============================================
Files 334 333 -1
Lines 10855 10768 -87
Branches 538 544 +6
============================================
- Hits 8168 8089 -79
+ Misses 2687 2679 -8
Continue to review full report at Codecov.
|
…apalache into ro/remove-chain
…into ro/remove-chain � Conflicts: � tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SetUnionRule.scala � tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala � tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
|
I am totally ok with merging it |
…into ro/remove-chain
Tests added for any new codemake fmt-fix(or had formatting run automatically on all files edited)Documentation added for any new functionalityEntry added to UNRELEASED.md for any new functionalityThis PR removes the chain IR operator. All uses of SMT select and store over many cells are now done iteratively, as done prior to #1171. The most complex change was done in
SetFilterRule, due to the interaction with SMT maps. Closes #1339.