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

rodrigo7491 · 2022-02-28T15:45:11Z

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~~
Entry added to UNRELEASED.md for any new functionality

This PR fixes three errors that were blocking the use of records in the arrays encoding, they are detailed below. Closes #1288.

DomainRuleWithArrays was computing funEx twice due to call to super. This was solved by moving the remaining cases of apply from DomainRule to DomainRuleWithArrays.
As pointed out by @konnov, when equating sets or functions we need to generate equalities for their elements using LazyEquality. This was solved by calling cacheEqConstraints with the sets'/functions' elements. For this fix EqRuleWithArrays was deleted and its logic moved to LazyEquality, making that class less lazy than before :-).
Picking a record via CherryPick.pickRecord was generating unsatisfiable formulas in some cases. The problem was that when constructing the domain of the picked record we could lose the chain of SSA updates, due to a storeNotInSet operation being in the rhs of an implication. This was solved by changing the operation to not(selectInSet), which ensures absence from the set without updating the array, given that sets are initially empty.

…into enable-records-in-arrays-encoding � Conflicts: � tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRule.scala

codecov-commenter · 2022-03-02T07:26:45Z

Codecov Report

Merging #1419 (93a5942) into unstable (bbdf123) will increase coverage by 0.05%.
The diff coverage is 87.83%.

@@             Coverage Diff              @@
##           unstable    #1419      +/-   ##
============================================
+ Coverage     74.52%   74.58%   +0.05%     
============================================
  Files           360      359       -1     
  Lines         11433    11442       +9     
  Branches        535      532       -3     
============================================
+ Hits           8521     8534      +13     
+ Misses         2912     2908       -4

Impacted Files	Coverage Δ
.../forsyte/apalache/tla/bmcmt/rules/DomainRule.scala	`94.00% <ø> (ø)`
...palache/tla/bmcmt/rules/DomainRuleWithArrays.scala	`75.00% <60.00%> (ø)`
...a/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala	`73.52% <86.20%> (+0.61%)`	⬆️
...palache/tla/bmcmt/rules/FunAppRuleWithArrays.scala	`94.82% <91.66%> (-5.18%)`	⬇️
...he/tla/bmcmt/SymbStateRewriterImplWithArrays.scala	`100.00% <100.00%> (ø)`
...apalache/tla/bmcmt/rules/SetInRuleWithArrays.scala	`92.06% <100.00%> (ø)`
...syte/apalache/tla/bmcmt/rules/aux/CherryPick.scala	`93.75% <100.00%> (+0.34%)`	⬆️
...he/io/annotations/parser/CommentPreprocessor.scala	`93.97% <0.00%> (+1.20%)`	⬆️
.../forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala	`80.00% <0.00%> (+7.00%)`	⬆️

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update bbdf123...93a5942. Read the comment docs.

…into enable-records-in-arrays-encoding

rodrigo7491 · 2022-03-02T08:49:23Z

The integration tests caught a bug that surfaced due to the changes made for point 2 (see PR description). When handling function application we were comparing cells directly, which is problematic in the presence of quantifiers, e.g., \A x \in S . f(x). The fix I made involved using part of the logic in FunAppRule.applyFun, using an oracle to avoid the direct cell comparison. In contrast to FunAppRule however, the constraints generated are for the domain and not the range. See the latest commit for these changes.

The integration tests are now passing, but the fix introduced a major efficiency loss. In #1169, the integration tests check for the arrays encoding took 4min, now it takes 1h. This should be addressed before merging the PR.

rodrigo7491 · 2022-03-02T08:50:36Z

@konnov, this PR will hopefully help with #1381. If not, work on #1418 should do the trick.

konnov

Looks good. I have added a few comments.

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala

konnov · 2022-03-02T09:06:10Z

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala

+        if (left.cellType == FinSetT(UnknownT()) && state.arena.getHas(left).isEmpty) {
+          // The statically empty set is a very special case, as its element type is unknown.
+          // Hence, we cannot use SMT equality, as it does not work with different sorts.
+          mkEmptySetEq(state, left, right)
+        } else if (right.cellType == FinSetT(UnknownT()) && state.arena.getHas(right).isEmpty) {
+          mkEmptySetEq(state, right, left) // same here
+        } else {


This is a very old piece of code. Let's replace it with an assertion that both left.cellType and right.cellType are FinSetT(_).

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRuleWithArrays.scala

konnov · 2022-03-02T09:33:00Z

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/FunAppRuleWithArrays.scala

+      val (oracleState, oracle) = picker.oracleFactory.newDefaultOracle(nextState, nElems + 1)
+      nextState = picker.pickByOracle(oracleState, oracle, relationElems, oracleState.arena.cellTrue().toNameEx)
+      val pickedElem = nextState.asCell
+
+      assert(nextState.arena.getHas(pickedElem).size == 2)
+      val pickedArg = nextState.arena.getHas(pickedElem)(0)
+      val pickedRes = nextState.arena.getHas(pickedElem)(1)
+
+      // Cache the equality between the picked argument and the supplied argument, O(1) constraints
+      nextState = rewriter.lazyEq.cacheEqConstraints(nextState, Seq((pickedArg, argCell)))
+      // If oracle < N, then pickedArg = argCell
+      val pickedElemInDom = tla.not(oracle.whenEqualTo(nextState, nElems))
+      val argEq = tla.eql(pickedArg.toNameEx, argCell.toNameEx)
+      val argEqWhenNonEmpty = tla.impl(pickedElemInDom, argEq)
+      rewriter.solverContext.assertGroundExpr(argEqWhenNonEmpty)
+
+      // We require oracle = N iff there is no element equal to argCell, O(N) constraints
+      for ((elem, no) <- relationElems.zipWithIndex) {
+        val elemArg = nextState.arena.getHas(elem).head
+        nextState = rewriter.lazyEq.cacheEqConstraints(nextState, Seq((elemArg, argCell)))
+        val inDom = tla.apalacheSelectInSet(elemArg.toNameEx, domainCell.toNameEx)
+        val neqArg = tla.not(rewriter.lazyEq.safeEq(elemArg, argCell))
+        val found = tla.not(oracle.whenEqualTo(nextState, nElems))
+        // ~inDom \/ neqArg \/ found, or equivalently, (inDom /\ elemArg = argCell) => found
+        rewriter.solverContext.assertGroundExpr(tla.or(tla.not(inDom), neqArg, found))
+        // oracle = i => inDom. The equality pickedArg = argCell is enforced by argEqWhenNonEmpty
+        rewriter.solverContext.assertGroundExpr(tla.or(tla.not(oracle.whenEqualTo(nextState, no)), inDom))
+      }


Do you have to do all of this to propagate lazy equality? If so, maybe we should limit this code to non-scalar types, that is, do not apply it Int, Bool, Str, and an uninterpreted type.

…ality.scala Co-authored-by: Igor Konnov <igor@informal.systems>

…omainRuleWithArrays.scala Co-authored-by: Igor Konnov <igor@informal.systems>

…m/informalsystems/apalache into enable-records-in-arrays-encoding

…into enable-records-in-arrays-encoding � Conflicts: � UNRELEASED.md

rodrigo7491 · 2022-03-07T09:33:54Z

The slowdown seen before was due to having to use an oracle to ascertain the argument of the function application. I made a fix in which, if the argument can be found in Scala by comparing cells, we generate a single SMT constraint querying the array that encodes the function. If we can't, e.g., in the presence of quantifiers, we use an oracle and need to have O(N) SMT constraints, with N being the cardinality of the domain of the function.

This change made the integration tests for the arrays encoding go back to their previous runtime, observed in #1169. Shall we merge the PR @konnov?

konnov

Looks good! Perhaps, we can simplify things when we add SMT-native support for records, tuples, etc.

konnov · 2022-03-08T14:57:00Z

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRuleWithArrays.scala

@@ -21,14 +21,25 @@ class DomainRuleWithArrays(rewriter: SymbStateRewriter, intRangeCache: IntRangeC
        val funState = rewriter.rewriteUntilDone(state.setRex(funEx))
        val funCell = funState.asCell

+        // TODO: consider records, tuples, and sequences in the arrays encoding


is this TODO obsolete?

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

rodrigo7491 added 6 commits February 23, 2022 10:31

fix DomainRule with Records in the arrays encoding

5d3f30f

fix record cherry pick in the arrays encoding

3a7b380

remove EqRuleWithArrays

6869af9

Merge branch 'unstable' of https://github.com/informalsystems/apalache …

c46a828

…into enable-records-in-arrays-encoding � Conflicts: � tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRule.scala

fix merge conflict

c0c71b8

fix fun application bug in the arrays encoding

dce272d

rodrigo7491 added 2 commits March 2, 2022 08:26

Merge branch 'unstable' of https://github.com/informalsystems/apalache …

e181f4d

…into enable-records-in-arrays-encoding

update release notes

42ff7a3

konnov approved these changes Mar 2, 2022

View reviewed changes

rodrigo7491 and others added 5 commits March 2, 2022 12:08

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

e2db7ab

…ality.scala Co-authored-by: Igor Konnov <igor@informal.systems>

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

5a2d262

…ality.scala Co-authored-by: Igor Konnov <igor@informal.systems>

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

f6c0f06

…omainRuleWithArrays.scala Co-authored-by: Igor Konnov <igor@informal.systems>

address review comments

09d4fc7

Merge branch 'enable-records-in-arrays-encoding' of https://github.co…

58b0e6c

…m/informalsystems/apalache into enable-records-in-arrays-encoding

rodrigo7491 mentioned this pull request Mar 2, 2022

Empty functions lead to incorrect SAT formulas #1430

Open

rodrigo7491 added 2 commits March 7, 2022 09:58

fix quantifier use on funApp with arrays

36059fb

Merge branch 'unstable' of https://github.com/informalsystems/apalache …

195f8a0

…into enable-records-in-arrays-encoding � Conflicts: � UNRELEASED.md

konnov approved these changes Mar 8, 2022

View reviewed changes

Merge branch 'unstable' into enable-records-in-arrays-encoding

93a5942

rodrigo7491 merged commit 6a3dd9f into unstable Mar 8, 2022

rodrigo7491 deleted the enable-records-in-arrays-encoding branch March 8, 2022 15:47

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

rodrigo7491 commented Feb 28, 2022 •

edited

Loading

codecov-commenter commented Mar 2, 2022 •

edited

Loading

rodrigo7491 commented Mar 2, 2022 •

edited

Loading

rodrigo7491 commented Mar 2, 2022

konnov left a comment

konnov Mar 2, 2022

rodrigo7491 Mar 2, 2022

konnov Mar 2, 2022

rodrigo7491 commented Mar 7, 2022

konnov left a comment

konnov Mar 8, 2022

rodrigo7491 Mar 8, 2022

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

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

Conversation

rodrigo7491 commented Feb 28, 2022 • edited Loading

codecov-commenter commented Mar 2, 2022 • edited Loading

Codecov Report

rodrigo7491 commented Mar 2, 2022 • edited Loading

rodrigo7491 commented Mar 2, 2022

konnov left a comment

Choose a reason for hiding this comment

konnov Mar 2, 2022

Choose a reason for hiding this comment

rodrigo7491 Mar 2, 2022

Choose a reason for hiding this comment

konnov Mar 2, 2022

Choose a reason for hiding this comment

rodrigo7491 commented Mar 7, 2022

konnov left a comment

Choose a reason for hiding this comment

konnov Mar 8, 2022

Choose a reason for hiding this comment

rodrigo7491 Mar 8, 2022

Choose a reason for hiding this comment

rodrigo7491 commented Feb 28, 2022 •

edited

Loading

codecov-commenter commented Mar 2, 2022 •

edited

Loading

rodrigo7491 commented Mar 2, 2022 •

edited

Loading