From d4725971fd23359f53b2e8d7de896a50da124b94 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 30 Jun 2023 14:52:03 +0200 Subject: [PATCH 1/3] Merge --- src/main/scala/viper/silver/ast/utility/Simplifier.scala | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/main/scala/viper/silver/ast/utility/Simplifier.scala b/src/main/scala/viper/silver/ast/utility/Simplifier.scala index 25da7f858..83a803925 100644 --- a/src/main/scala/viper/silver/ast/utility/Simplifier.scala +++ b/src/main/scala/viper/silver/ast/utility/Simplifier.scala @@ -21,7 +21,7 @@ object Simplifier { * 0 are not treated. Note that an expression with non-terminating evaluation due to endless recursion * might be transformed to terminating expression. */ - def simplify[N <: Node](n: N): N = { + def simplify[N <: Node](n: N, p: Program): N = { /* Always simplify children first, then treat parent. */ StrategyBuilder.Slim[Node]({ // expression simplifications @@ -45,7 +45,9 @@ object Simplifier { FalseLit()(root.pos, root.info) case Implies(TrueLit(), consequent) => consequent - case root @ EqCmp(left, right) if left == right => TrueLit()(root.pos, root.info) + // ME: Disabled since it is not equivalent in case the expression is not well-defined. + // TODO: Consider checking if Expressions.proofObligations(left) is empty (requires adding the program as parameter). + // case root @ EqCmp(left, right) if left == right => TrueLit()(root.pos, root.info) case root @ EqCmp(BoolLit(left), BoolLit(right)) => BoolLit(left == right)(root.pos, root.info) case root @ EqCmp(FalseLit(), right) => Not(right)(root.pos, root.info) From 0e0616292bc93669e236e6ae481cb374a69d7cb7 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 30 Jun 2023 15:00:14 +0200 Subject: [PATCH 2/3] Removed accidentally committed added parameter --- src/main/scala/viper/silver/ast/utility/Simplifier.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/viper/silver/ast/utility/Simplifier.scala b/src/main/scala/viper/silver/ast/utility/Simplifier.scala index 83a803925..b6b5e36d7 100644 --- a/src/main/scala/viper/silver/ast/utility/Simplifier.scala +++ b/src/main/scala/viper/silver/ast/utility/Simplifier.scala @@ -21,7 +21,7 @@ object Simplifier { * 0 are not treated. Note that an expression with non-terminating evaluation due to endless recursion * might be transformed to terminating expression. */ - def simplify[N <: Node](n: N, p: Program): N = { + def simplify[N <: Node](n: N): N = { /* Always simplify children first, then treat parent. */ StrategyBuilder.Slim[Node]({ // expression simplifications From 11fc3792ead2a513d30fd7e2cd11d2835bee490a Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Fri, 30 Jun 2023 15:09:23 +0200 Subject: [PATCH 3/3] Added test --- src/test/scala/SimplifierTests.scala | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/test/scala/SimplifierTests.scala b/src/test/scala/SimplifierTests.scala index 3af44942e..50025e8f0 100644 --- a/src/test/scala/SimplifierTests.scala +++ b/src/test/scala/SimplifierTests.scala @@ -50,5 +50,11 @@ class SimplifierTests extends AnyFunSuite with Matchers { simplify(Mod(-3, -8)()) should be (5: IntLit) } + test("equality") { + val seqAcc = SeqIndex(EmptySeq(Int)(), 0: IntLit)() + // Do not simplify away definedness issues. + simplify(EqCmp(seqAcc, seqAcc)()) should be(EqCmp(seqAcc, seqAcc)()) + } + implicit def int2IntLit(i: Int): IntLit = IntLit(i)() }