Merge pull request #2697 from informalsystems/th/fix-2690

Construct fresh model values
apalache-mc · Aug 16, 2023 · 4601ff8 · 4601ff8
2 parents b989958 + 5089837
commit 4601ff8
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 20 deletions.
diff --git a/.unreleased/bug-fixes/2697-fresh-model-values.md b/.unreleased/bug-fixes/2697-fresh-model-values.md
@@ -0,0 +1 @@
+Fix a bug with decoding unconstrained model values of uninterpreted types.
diff --git a/docs/src/HOWTOs/uninterpretedTypes.md b/docs/src/HOWTOs/uninterpretedTypes.md
@@ -39,6 +39,8 @@ where:
 Example: `"1_OF_UT"` is a value belonging to the uninterpreted type `UT`, as is `"2_OF_UT"`. These two values are distinct by definition. On the contrary,
 `"1_OF_ut"` does _not_ meet the criteria for a value belonging to an uninterpreted type ( lowercase `ut` is not a valid identifier for an uninterpreted type), so it is treated as a string value.
 
+**Note**: Values matching the pattern `"FRESH[0-9]+_OF_TYPENAME"` are reserved for internal use, to allow Apalache to construct fresh values.
+
 ## Uninterpreted types, `Str`, and comparisons
 Importantly, while both strings and values belonging to uninterpreted types are introduced using the `"..."` notation, they are treated as having distinct, incomparable types.
 Examples:

diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateDecoder.scala
@@ -9,7 +9,7 @@ import at.forsyte.apalache.tla.lir._
 import at.forsyte.apalache.tla.lir.oper.TlaSetOper
 import at.forsyte.apalache.tla.lir.values._
 import at.forsyte.apalache.tla.typecomp.TBuilderInstruction
-import at.forsyte.apalache.tla.types.{tla, ModelValueHandler}
+import at.forsyte.apalache.tla.types.tla
 import com.typesafe.scalalogging.LazyLogging
 
 import scala.collection.immutable.SortedMap
@@ -35,27 +35,28 @@ class SymbStateDecoder(solverContext: SolverContext, rewriter: SymbStateRewriter
     case CellTFrom(IntT1) =>
       cell.toBuilder.map(solverContext.evalGroundExpr)
 
-    case tt @ (CellTFrom(ConstT1(_)) | CellTFrom(StrT1)) =>
+    case ct @ CellTFrom(StrT1 | ConstT1(_)) =>
       // First, attempt to check the cache
       val found = rewriter.modelValueCache.findKey(cell)
-      if (found.isDefined) {
-        val pa @ (_, index) = found.get
-        if (tt == CellTFrom(StrT1)) tla.str(index)
-        else tla.constParsed(ModelValueHandler.construct(pa))
-      } else {
-        // if not in the cache, it might be the case that another cell, which has asserted equivalence
-        // with the original cell can be found
-        val values = rewriter.modelValueCache.values().filter(_.cellType == tt).toSeq
-        findCellInSet(values, cell.toBuilder) match {
-          // found among the cached keys
-          case Some(c) =>
-            decodeCellToTlaEx(arena, c)
-
-          case None =>
-            // not found, just use the name
-            // a value that was assigned by the solver, and not created by us
-            tla.str(cell.toString)
-        }
+      found match {
+        case Some((_, index)) =>
+          if (ct == CellTFrom(StrT1)) tla.str(index)
+          else tla.const(index, ct.tt.asInstanceOf[ConstT1])
+        case None =>
+          // if not in the cache, it might be the case that another cell, which has asserted equivalence
+          // with the original cell can be found
+          val values = rewriter.modelValueCache.values().filter(_.cellType == cell.cellType).toSeq
+          findCellInSet(values, cell.toBuilder) match {
+            case Some(c) =>
+              // found among the cached keys
+              decodeCellToTlaEx(arena, c)
+
+            case None =>
+              // not found, just use the name
+              // a value that was assigned by the solver, and not created by us
+              if (ct == CellTFrom(StrT1)) tla.str(s"FRESH${cell.id}")
+              else tla.const(s"FRESH${cell.id}", ct.tt.asInstanceOf[ConstT1])
+          }
       }
 
     case UnknownT() =>