-
-
Notifications
You must be signed in to change notification settings - Fork 40
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.
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
Make records as they are work in the arrays encoding #1419
Conversation
…into enable-records-in-arrays-encoding � Conflicts: � tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRule.scala
Codecov Report
@@ 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
Continue to review full report at Codecov.
|
…into enable-records-in-arrays-encoding
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., 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. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good. I have added a few comments.
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala
Outdated
Show resolved
Hide resolved
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala
Outdated
Show resolved
Hide resolved
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 { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is a very old piece of code. Let's replace it with an assertion that both left.cellType
and right.cellType
are FinSetT(_)
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
See #1430.
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/LazyEquality.scala
Show resolved
Hide resolved
tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/DomainRuleWithArrays.scala
Outdated
Show resolved
Hide resolved
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)) | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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>
…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
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? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good! Perhaps, we can simplify things when we add SMT-native support for records, tuples, etc.
@@ -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 |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
is this TODO obsolete?
There was a problem hiding this comment.
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.
make fmt-fix
(or had formatting run automatically on all files edited)Documentation added for any new functionalityThis PR fixes three errors that were blocking the use of records in the arrays encoding, they are detailed below. Closes #1288.
DomainRuleWithArrays
was computingfunEx
twice due to call tosuper
. This was solved by moving the remaining cases ofapply
fromDomainRule
toDomainRuleWithArrays
.LazyEquality
. This was solved by callingcacheEqConstraints
with the sets'/functions' elements. For this fixEqRuleWithArrays
was deleted and its logic moved toLazyEquality
, making that class less lazy than before :-).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 astoreNotInSet
operation being in the rhs of an implication. This was solved by changing the operation tonot(selectInSet)
, which ensures absence from the set without updating the array, given that sets are initially empty.