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

QP single-recvr merge Issue #882

Merged
merged 2 commits into from
Dec 4, 2024
Merged

QP single-recvr merge Issue #882

Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
03ae2b4
merge qp-single-recvr chunks only if entire condition is equal
mlimbeck Dec 4, 2024
8f047fa
Merge branch 'master' into qp-singler-recvr-merge-fix
marcoeilers Dec 4, 2024
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
20 changes: 13 additions & 7 deletions src/main/scala/rules/QuantifiedChunkSupport.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1968,11 +1968,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
case qfc: QuantifiedFieldChunk if qfc.invs.isDefined =>
Left(qfc.invs.get.invertibles, qfc.quantifiedVars, qfc.condition)
case qfc: QuantifiedFieldChunk if qfc.singletonArguments.isDefined =>
Right(qfc.singletonArguments.get)
Right(qfc.singletonArguments.get, qfc.condition)
case qpc: QuantifiedPredicateChunk if qpc.invs.isDefined =>
Left(qpc.invs.get.invertibles, qpc.quantifiedVars, qpc.condition)
case qpc: QuantifiedPredicateChunk if qpc.singletonArguments.isDefined =>
Right(qpc.singletonArguments.get)
Right(qpc.singletonArguments.get, qpc.condition)
case _ => return None
}
val relevantChunks: Iterable[QuantifiedBasicChunk] = chunks.flatMap {
Expand All @@ -1982,19 +1982,25 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {

val (receiverTerms, quantVars, cond) = lr match {
case Left(tuple) => tuple
case Right(singletonArguments) =>
case Right((singletonArguments, cond)) =>
return relevantChunks.find { ch =>
val chunkInfo = ch match {
case qfc: QuantifiedFieldChunk if qfc.singletonArguments.isDefined =>
Some(qfc.singletonArguments.get)
Some(qfc.singletonArguments.get, qfc.condition)
case qpc: QuantifiedPredicateChunk if qpc.singletonArguments.isDefined =>
Some(qpc.singletonArguments.get)
Some(qpc.singletonArguments.get, qpc.condition)
case _ => None
}
chunkInfo match {
case Some(cSingletonArguments) =>
case Some((cSingletonArguments, cCond)) =>

val equalityTerm = And(singletonArguments.zip(cSingletonArguments).map { case (a, b) => a === b })
val result = v.decider.check(equalityTerm, Verifier.config.checkTimeout())
// The conditions of two chunks with the same receivers can differ if they originate from separate branches
marcoeilers marked this conversation as resolved.
Show resolved Hide resolved
// that were joined. In such cases, additional conjuncts might have been added to the conditions.
// Hence, we need to compare the conditions for equality in addition to verifying that the receivers match.
val equalityCond = And(cond.replace(chunk.quantifiedVars, singletonArguments),
cCond.replace(ch.quantifiedVars, cSingletonArguments))
val result = v.decider.check(And(equalityCond, equalityTerm), Verifier.config.checkTimeout())
if (result) {
// Learn the equality
val debugExp = Option.when(withExp)(DebugExp.createInstance("Chunks alias", true))
Expand Down
Loading