`ModelValueCache` rework #2675

Kukovec · 2023-07-27T15:21:46Z

Tests added for any new code
Ran make fmt-fix (or had formatting run automatically on all files edited)
Documentation added for any new functionality
Entries added to ./unreleased/ for any new functionality

Note that ModelValueCache is being renamed to UninterpretedLiteralCache, since we're not using the terminology "model value" anymore.

shonfeder

Looking good!

I have some questions, mostly for my own edification.

In the future, for there PRs, could you also provide a link to the class you are porting over? I think that is useful context for us reviewers. In this case it is https://github.com/informalsystems/apalache/tree/4e0094ee5d03a068188a85dcdc8ead021b17033e/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/ModelValueCache.scala

shonfeder · 2023-07-27T17:34:49Z

.../scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/UninterpretedLiteralCacheTest.scala

+    assert(newArena3 != newArena2 && cell3 != cell2)
+  }
+
+  test("Constraints are only added when addConstraintsForElem is explicitly called, and only once per value") {


addConstraintsForElem is not used in this test. Should this be

Suggested change

test("Constraints are only added when addConstraintsForElem is explicitly called, and only once per value") {

test("Constraints are only added when addAllConstraints is explicitly called, and only once per value") {

Incidentally, it doesn't look like addConstaintsForElem is being tested?

Good catch, slipped my mind. I am a little torn though, given how impractical calling distinct on single elements is, I should probably try and find a way to discourage/disable invoking the "-ForElem" method.

Funnily enough, adding these tests helped find a logic bug: In ModelValueCache, the line [1]: https://github.com/informalsystems/apalache/blob/4e0094ee5d03a068188a85dcdc8ead021b17033e/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/ModelValueCache.scala#L30
In create returns a collection of all other cells of the same type as the newest cell. However, in AbstractCache https://github.com/informalsystems/apalache/blob/4e0094ee5d03a068188a85dcdc8ead021b17033e/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/caches/AbstractCache.scala#L52-L60
performs create before addToCache. If one would have used line [1] as is in addConstaintsForElem, this would create UNSAT constraints, because that method gets called after both create and addToCache, effectively creating distinct(x, ..., x, ...) constraints, since the latest cell is now part of the others collection too.
Note that the addAllConstraints behavior is unaffected by this, so the "normal" use case wouldn't have been affected, but I'm sure we'd be dealing with the single-elem constraints bug down the line.

...ala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala

Co-authored-by: Shon Feder <[email protected]>

codecov-commenter · 2023-07-28T11:52:00Z

Codecov Report

Merging #2675 (7e5f642) into main (b374361) will increase coverage by 0.02%.
The diff coverage is 100.00%.

@@            Coverage Diff             @@
##             main    #2675      +/-   ##
==========================================
+ Coverage   78.47%   78.50%   +0.02%     
==========================================
  Files         458      459       +1     
  Lines       15859    15873      +14     
  Branches     2606     2578      -28     
==========================================
+ Hits        12446    12461      +15     
+ Misses       3413     3412       -1

Files Changed	Coverage Δ
...edRules/aux/caches/UninterpretedLiteralCache.scala	`100.00% <100.00%> (ø)`

... and 4 files with indirect coverage changes

📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more

Kukovec · 2023-07-28T12:35:59Z

I'm just going to leave a note here on the difference between batching distincts and adding them incrementally, since GH has nicer formatting than in-code comments.

If we consider a naive implementation of distinct(a1,..., an) as a1 != a2 /\ a1 != a3 /\ ... /\ a{n-1} != an, a distinct with n elements is equivalent to dn = n(n-1)/2 disequalities. Suppose we end up with a collection of N cache values (of a given type). If we called addConstaintsForElem after each addition, we'd end up with d1 + d2 + ... + dN disequalities, i.e.

\sum_{i=1}^N n(n-1)/2 = N(N^2 -1)/6

In contrast, addAllConstraints produces dN = N(N-1)/2 disequalities, which is O(N^2), instead of O(N^3). A pretty good reason to avoid addConstaintsForElem, in favor of addAllConstraints, if possible.

shonfeder · 2023-07-28T14:39:04Z

...ala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala

+  override def addConstraintsForElem(ctx: SolverContext): (((String, String), ArenaCell)) => Unit = {
+    case ((tp, _), v) =>
+      val cellType = if (tp == StrT1.toString) StrT1 else ConstT1(tp)
+      val others = values().withFilter { c => c.cellType == CellTFrom(cellType) && c != v }.map(_.toBuilder).toSeq
+      // The fresh cell should differ from the previously created cells.
+      // We use the SMT constraint (distinct ...).


Why don't we need a check that the entry is actually in the cache?

We could add it, but there's technically nothing wrong is asserting that a value outside the cache is distinct from all values in the cache. Theoretically, once this is wired to some manager class, this method will either:

get called once, immediately after an element is added, so membership is established by construction, or

never get called in favor of addAll, so the issue is irrelevant

it's just that, at this point in time, I cannot 100% predict what the integration of this class into the rules engine will look like, since it won't exactly be 1-to-1 with ModelValueCache. If you want a QOL exception trigger, I'd be happy to put that in though.

shonfeder · 2023-07-28T14:39:07Z

...ala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala

+   * The UninterpretedLiteralCache maintains that a cell cache for a value `idx` of type `tp` is distinct from all other
+   * values of type `tp` (defined so far).
+   *
+   * Whenever possible, try to use [[addAllConstraints]] instead of this method, for performance reasons instead.


Could we just implement this method as a deferred call to addAllConstraints? Is there some reason this one would need to be used instead of addAll?

Not sure exactly what you mean by "deferred", and the overhead of figuring out when to actually resolve it seems to not be worth it to me.
It'd be easier to answer whether or not we need this, when I actually start wiring this up, so that these assertion methods are called by something. At that point, if we see that this one is redundant, we can delete it then.

shonfeder

Just a couple followup questions to be sure I understand the rationale for the choices. Also please do add your comment here on the rationale to the comments in the code. Tat is where will be most useful!! :)

Kukovec · 2023-08-10T10:45:40Z

@thpani since Shon is on vacation, could you please finish the review in his stead?

thpani

LGTM, just 2 small questions

...ala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/caches/UninterpretedLiteralCache.scala

thpani · 2023-08-10T11:36:01Z

.../scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/aux/UninterpretedLiteralCacheTest.scala

+    ))
+  }
+
+  test("Constraints are only added when addAllConstraintsForElem is explicitly called, and only once per value") {


Should this have a different description? It uses addConstraintsForElem

Ah, I'll fix the name

…iedRules/aux/caches/UninterpretedLiteralCache.scala Co-authored-by: Thomas Pani <[email protected]>

Add cache + tests

4e0094e

Kukovec requested review from thpani and shonfeder July 27, 2023 15:21

Kukovec requested a review from rodrigo7491 as a code owner July 27, 2023 15:21

shonfeder reviewed Jul 27, 2023

View reviewed changes

Apply suggestions from code review

c4b8743

Co-authored-by: Shon Feder <[email protected]>

PR comments

477d71c

Kukovec requested a review from shonfeder July 28, 2023 12:18

shonfeder reviewed Jul 28, 2023

View reviewed changes

Kukovec added 2 commits August 9, 2023 15:11

Merge branch 'main' into jk/2664

e6adab0

Pr comments

a79becc

Kukovec requested review from thpani and removed request for thpani August 10, 2023 10:44

test fix

c1a0d6d

thpani approved these changes Aug 10, 2023

View reviewed changes

Kukovec and others added 2 commits August 10, 2023 13:37

Update tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratif…

a9935a9

…iedRules/aux/caches/UninterpretedLiteralCache.scala Co-authored-by: Thomas Pani <[email protected]>

pr comments

7e5f642

Kukovec enabled auto-merge (squash) August 10, 2023 11:38

Kukovec merged commit d9a9e90 into main Aug 10, 2023
10 checks passed

Kukovec deleted the jk/2664 branch August 10, 2023 12:37

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

`ModelValueCache` rework #2675

`ModelValueCache` rework #2675

Kukovec commented Jul 27, 2023

shonfeder left a comment

shonfeder Jul 27, 2023

shonfeder Jul 27, 2023

Kukovec Jul 28, 2023

Kukovec Jul 28, 2023

shonfeder Jul 28, 2023

codecov-commenter commented Jul 28, 2023 •

edited

Loading

Kukovec commented Jul 28, 2023

shonfeder Jul 28, 2023

Kukovec Aug 10, 2023

shonfeder Jul 28, 2023

Kukovec Aug 10, 2023

shonfeder left a comment

Kukovec commented Aug 10, 2023

thpani left a comment

thpani Aug 10, 2023

Kukovec Aug 10, 2023

	test("Constraints are only added when addConstraintsForElem is explicitly called, and only once per value") {
	test("Constraints are only added when addAllConstraints is explicitly called, and only once per value") {

ModelValueCache rework #2675

ModelValueCache rework #2675

Conversation

Kukovec commented Jul 27, 2023

shonfeder left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

codecov-commenter commented Jul 28, 2023 • edited Loading

Codecov Report

Kukovec commented Jul 28, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

shonfeder left a comment

Choose a reason for hiding this comment

Kukovec commented Aug 10, 2023

thpani left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

`ModelValueCache` rework #2675

`ModelValueCache` rework #2675

codecov-commenter commented Jul 28, 2023 •

edited

Loading