introduce the operator Apalache!Guess

src/tla/Apalache.tla

@@ -38,6 +38,18 @@ x := e == x = e
  *)
 Gen(size) == {}
 
+(**
+ * A non-deterministic version of CHOOSE x \in S: TRUE.  That is, whenever
+ * Guess(S) is called twice, it is free to return arbitrary elements of S, if S
+ * is non-empty. If S is empty, Guess(S) returns some value of the proper type.
+ *
+ * @type: Set(a) => a;
+ *)
+Guess(S) ==
+    \* Since this is not supported by TLC,
+    \* we fall back to the deterministic version for TLC.
+    CHOOSE x \in S: TRUE
+
 (**
  * Convert a set of pairs S to a function F. Note that if S contains at least
  * two pairs <<x, y>> and <<u, v>> such that x = u and y /= v,

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala

@@ -192,7 +192,9 @@ class SymbStateRewriterImpl(
         key(tla.forall(tla.name("x"), tla.name("S"), tla.name("p")))
           -> List(new QuantRule(this)),
         key(tla.choose(tla.name("x"), tla.name("S"), tla.name("p")))
-          -> List(new ChooseRule(this)),
+          -> List(new ChooseOrGuessRule(this)),
+        key(tla.guess(tla.name("S")))
+          -> List(new ChooseOrGuessRule(this)),
         // control flow
         key(tla.ite(tla.name("cond"), tla.name("then"), tla.name("else")))
           -> List(new IfThenElseRule(this)),

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/analyses/ExpansionMarker.scala

@@ -61,10 +61,15 @@ class ExpansionMarker @Inject() (tracker: TransformationTracker) extends TlaExTr
       OperEx(op, OperEx(TlaBoolOper.exists, name, transform(false)(set), transform(false)(pred))(tag))(tag)
 
     case ex @ OperEx(op @ TlaOper.chooseBounded, name, set, pred) =>
-      // CHOOSE is essentially a skolemizable existential with the constraint of uniqueness
+      // CHOOSE does not require the set to be expanded
       val tag = ex.typeTag
       OperEx(op, name, transform(false)(set), transform(false)(pred))(tag)
 
+    case ex @ OperEx(op @ ApalacheOper.guess, set) =>
+      // Guess does not require the set to be expanded
+      val tag = ex.typeTag
+      OperEx(op, transform(false)(set))(tag)
+
     case ex @ OperEx(op, name, set, pred) if op == TlaBoolOper.exists || op == TlaBoolOper.forall =>
       // non-skolemizable quantifiers require their sets to be expanded
       val tag = ex.typeTag

tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/ChooseOrGuessRule.scala

@@ -0,0 +1,87 @@
+package at.forsyte.apalache.tla.bmcmt.rules
+
+import at.forsyte.apalache.tla.bmcmt._
+import at.forsyte.apalache.tla.bmcmt.rules.aux.{CherryPick, OracleHelper}
+import at.forsyte.apalache.tla.lir.{OperEx, SetT1, TlaType1}
+import at.forsyte.apalache.tla.lir.TypedPredefs._
+import at.forsyte.apalache.tla.lir.convenience.tla
+import at.forsyte.apalache.tla.lir.oper.{ApalacheOper, TlaOper}
+
+/**
+ * <p>Rewriting rule for CHOOSE and Apalache!Guess. We implement a non-deterministic choice. It is not hard to add the
+ * requirement of determinism, but that will most likely affect efficiency.</p>
+ *
+ * <p>We will make CHOOSE deterministic in the issue #841 is solved.</p>
+ *
+ * @author
+ *   Igor Konnov
+ */
+class ChooseOrGuessRule(rewriter: SymbStateRewriter) extends RewritingRule {
+  private val pickRule = new CherryPick(rewriter)
+
+  override def isApplicable(state: SymbState): Boolean = {
+    state.ex match {
+      case OperEx(TlaOper.chooseBounded, _, _, _) =>
+        true
+
+      case OperEx(ApalacheOper.guess, _) =>
+        true
+
+      case _ =>
+        false
+    }
+  }
+
+  override def apply(state: SymbState): SymbState = {
+    state.ex match {
+      case OperEx(TlaOper.chooseBounded, varName, set, pred) =>
+        // This is a general encoding, handling both happy and unhappy scenarios,
+        // that is, when CHOOSE is defined on its arguments and not, respectively.
+        // Compute set comprehension and then pick an element from it.
+        val setT = set.typeTag.asTlaType1()
+        val filterEx = tla
+          .filter(varName, set, pred)
+          .typed(setT)
+        val nextState = rewriter.rewriteUntilDone(state.setRex(filterEx))
+        guess(setT, nextState)
+
+      case OperEx(ApalacheOper.guess, setEx) =>
+        val setT = setEx.typeTag.asTlaType1()
+        val nextState = rewriter.rewriteUntilDone(state.setRex(setEx))
+        guess(setT, nextState)
+
+      case _ =>
+        throw new RewriterException("%s is not applicable".format(getClass.getSimpleName), state.ex)
+    }
+  }
+
+  private def guess(setT: TlaType1, state: SymbState): SymbState = {
+    // pick an arbitrary witness
+    val setCell = state.asCell
+    if (state.arena.getHas(setCell).isEmpty) {
+      setT match {
+        case SetT1(elemT) =>
+          val (newArena, defaultValue) = rewriter.defaultValueCache.getOrCreate(state.arena, elemT)
+          state.setArena(newArena).setRex(defaultValue.toNameEx)
+
+        case _ =>
+          throw new IllegalStateException(s"Expected a set, found: $setT")
+      }
+    } else {
+      val elems = state.arena.getHas(setCell)
+      // add an oracle \in 0..N, where the indices from 0 to N - 1 correspond to the set elements,
+      // whereas the index N corresponds to the default choice when the set is empty
+      val (oracleState, oracle) = pickRule.oracleFactory.newDefaultOracle(state, elems.size + 1)
+
+      // pick a cell
+      val nextState = pickRule.pickByOracle(oracleState, oracle, elems, oracleState.arena.cellTrue().toNameEx)
+      val pickedCell = nextState.asCell
+      // require the oracle to produce only the values for the set elements (or no elements, when it is empty)
+      OracleHelper.assertOraclePicksSetMembers(rewriter, nextState, oracle, setCell, elems)
+
+      // If oracle = N, the picked cell is not constrained. In the past, we used a default value here,
+      // but it sometimes produced conflicts (e.g., a picked record domain had to coincide with a default domain)
+      nextState.setRex(pickedCell.toNameEx)
+    }
+  }
+}

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithArrays.scala

@@ -10,7 +10,7 @@ import org.scalatestplus.junit.JUnitRunner
 class TestRewriterWithArrays
     extends TestCherryPick with TestSymbStateDecoder with TestSymbStateRewriter with TestSymbStateRewriterAction
     with TestSymbStateRewriterApalacheGen with TestSymbStateRewriterAssignment with TestSymbStateRewriterBool
-    with TestSymbStateRewriterChoose with TestSymbStateRewriterControl with TestSymbStateRewriterExpand
+    with TestSymbStateRewriterChooseOrGuess with TestSymbStateRewriterControl with TestSymbStateRewriterExpand
     with TestSymbStateRewriterFiniteSets with TestSymbStateRewriterFoldSeq with TestSymbStateRewriterFoldSet
     with TestSymbStateRewriterFun with TestSymbStateRewriterFunSet with TestSymbStateRewriterInt
     with TestSymbStateRewriterPowerset with TestSymbStateRewriterRecFun with TestSymbStateRewriterRecord

tla-bmcmt/src/test/scala/at/forsyte/apalache/tla/bmcmt/TestRewriterWithOOPSLA19.scala

@@ -10,7 +10,7 @@ import org.scalatestplus.junit.JUnitRunner
 class TestRewriterWithOOPSLA19
     extends TestCherryPick with TestSymbStateDecoder with TestSymbStateRewriter with TestSymbStateRewriterAction
     with TestSymbStateRewriterApalacheGen with TestSymbStateRewriterAssignment with TestSymbStateRewriterBool
-    with TestSymbStateRewriterChoose with TestSymbStateRewriterControl with TestSymbStateRewriterExpand
+    with TestSymbStateRewriterChooseOrGuess with TestSymbStateRewriterControl with TestSymbStateRewriterExpand
     with TestSymbStateRewriterFiniteSets with TestSymbStateRewriterFoldSeq with TestSymbStateRewriterFoldSet
     with TestSymbStateRewriterFun with TestSymbStateRewriterFunSet with TestSymbStateRewriterInt
     with TestSymbStateRewriterPowerset with TestSymbStateRewriterRecFun with TestSymbStateRewriterRecord