From 227a971007e9cdb9472254cf628567d673a1e7f7 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt Date: Fri, 8 Apr 2022 14:07:41 +0200 Subject: [PATCH 1/2] Fix bug in cardinality optimization --- .../scala/at/forsyte/apalache/tla/pp/ExprOptimizer.scala | 7 +++++-- .../at/forsyte/apalache/tla/pp/TestExprOptimizer.scala | 8 ++++++-- 2 files changed, 11 insertions(+), 4 deletions(-) diff --git a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ExprOptimizer.scala b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ExprOptimizer.scala index b761370549..6bee553cd5 100644 --- a/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ExprOptimizer.scala +++ b/tla-pp/src/main/scala/at/forsyte/apalache/tla/pp/ExprOptimizer.scala @@ -83,9 +83,12 @@ class ExprOptimizer(nameGen: UniqueNameGenerator, tracker: TransformationTracker private def transformCard: PartialFunction[TlaEx, TlaEx] = { case OperEx(TlaFiniteSetOper.cardinality, OperEx(TlaArithOper.dotdot, left, right)) => // A pattern that emerged in issue #748 - // Cardinality(a..b) is equivalent to (b - a) + 1. + // Cardinality(a..b) is equivalent to IF a =< b THEN (b - a) + 1 ELSE 0. + val condition = OperEx(TlaArithOper.le, left, right)(boolTag) val bMinusA = OperEx(TlaArithOper.minus, right, left)(intTag) - OperEx(TlaArithOper.plus, bMinusA, ValEx(TlaInt(1))(intTag))(intTag) + val bMinusAPlusOne = OperEx(TlaArithOper.plus, bMinusA, ValEx(TlaInt(1))(intTag))(intTag) + val zero = ValEx(TlaInt(0))(intTag) + OperEx(TlaControlOper.ifThenElse, condition, bMinusAPlusOne, zero)(intTag) case OperEx(TlaFiniteSetOper.cardinality, OperEx(TlaSetOper.powerset, set)) => // A pattern that emerged in issue #1360 diff --git a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala index dffea9912c..79860f73e4 100644 --- a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala +++ b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala @@ -156,11 +156,15 @@ class TestExprOptimizer extends AnyFunSuite with BeforeAndAfterEach { optimizer.apply(input) } - test("""Cardinality(a..b) becomes (b - a) + 1""") { + test("""Cardinality(a..b) becomes IF a =< b THEN (b - a) + 1 ELSE 0""") { val input = card(dotdot(name("a").as(intT), name("b").as(intT)).as(intSetT)).as(intT) val output = optimizer.apply(input) val expected = - plus(minus(name("b").as(intT), name("a").as(intT)).as(intT), int(1).as(intT)).as(intT) + ite( + le(name("a").as(intT), name("b").as(intT)).as(boolT), + plus(minus(name("b").as(intT), name("a").as(intT)).as(intT), int(1).as(intT)).as(intT), + int(0).as(intT), + ).as(intT) assert(expected == output) } From d7f3a29f9ad5e4f5d614908241222597a1ce9923 Mon Sep 17 00:00:00 2001 From: Philip Offtermatt <57488781+p-offtermatt@users.noreply.github.com> Date: Fri, 8 Apr 2022 15:17:25 +0200 Subject: [PATCH 2/2] Avoid adding types to integer literals Co-authored-by: Igor Konnov --- .../scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala index 79860f73e4..73e093b4ca 100644 --- a/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala +++ b/tla-pp/src/test/scala/at/forsyte/apalache/tla/pp/TestExprOptimizer.scala @@ -162,8 +162,8 @@ class TestExprOptimizer extends AnyFunSuite with BeforeAndAfterEach { val expected = ite( le(name("a").as(intT), name("b").as(intT)).as(boolT), - plus(minus(name("b").as(intT), name("a").as(intT)).as(intT), int(1).as(intT)).as(intT), - int(0).as(intT), + plus(minus(name("b").as(intT), name("a").as(intT)).as(intT), int(1)).as(intT), + int(0), ).as(intT) assert(expected == output) }