From e8fba87ec478c7056034f8e3b169fa4ee8865880 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 27 Sep 2024 17:53:31 +0200 Subject: [PATCH 1/3] produce true on distinct for less than 2 elements --- .../tla/bmcmt/smt/Z3SolverContext.scala | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala index a978d637bb..3e29161038 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala @@ -765,12 +765,17 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL (z3context.mkNot(eq.asInstanceOf[BoolExpr]).asInstanceOf[ExprSort], 1 + n) case OperEx(ApalacheInternalOper.distinct, args @ _*) => - val (es, ns) = (args.map(toExpr)).unzip - val distinct = z3context.mkDistinct(es: _*) - (distinct.asInstanceOf[ExprSort], - ns.foldLeft(1L) { - _ + _ - }) + if (args.length < 2) { + // Produce true for a singleton set or an empty set. Otherwise, we cannot replay the SMT log in CVC5. + (z3context.mkTrue().asInstanceOf[ExprSort], 1) + } else { + val (es, ns) = (args.map(toExpr)).unzip + val distinct = z3context.mkDistinct(es: _*) + (distinct.asInstanceOf[ExprSort], + ns.foldLeft(1L) { + _ + _ + }) + } case OperEx(TlaBoolOper.and, args @ _*) => val (es, ns) = (args.map(toExpr)).unzip From 5b7b5d67c82b065d18e6b4cf15bebbe3929060a7 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Fri, 27 Sep 2024 18:00:18 +0200 Subject: [PATCH 2/3] add release notes --- .unreleased/bug-fixes/distinct-on-singleton.md | 1 + 1 file changed, 1 insertion(+) create mode 100644 .unreleased/bug-fixes/distinct-on-singleton.md diff --git a/.unreleased/bug-fixes/distinct-on-singleton.md b/.unreleased/bug-fixes/distinct-on-singleton.md new file mode 100644 index 0000000000..ac08ba6fcd --- /dev/null +++ b/.unreleased/bug-fixes/distinct-on-singleton.md @@ -0,0 +1 @@ +Do not produce `(distinct ...)` for singletons (see #3005) From 7db8fa4178b96a9101417f2673abf6d1c6c068d6 Mon Sep 17 00:00:00 2001 From: Igor Konnov Date: Mon, 30 Sep 2024 16:26:49 +0200 Subject: [PATCH 3/3] Update .unreleased/bug-fixes/distinct-on-singleton.md Co-authored-by: Thomas Pani --- .unreleased/bug-fixes/distinct-on-singleton.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.unreleased/bug-fixes/distinct-on-singleton.md b/.unreleased/bug-fixes/distinct-on-singleton.md index ac08ba6fcd..e1aded6fdf 100644 --- a/.unreleased/bug-fixes/distinct-on-singleton.md +++ b/.unreleased/bug-fixes/distinct-on-singleton.md @@ -1 +1 @@ -Do not produce `(distinct ...)` for singletons (see #3005) +Do not produce `(distinct ...)` for singletons, see #3005