Remove abstractLhs and rhsSnapshot from MagicWandSnapshot.

src/main/scala/decider/TermToSMTLib2Converter.scala

@@ -316,7 +316,7 @@ class TermToSMTLib2Converter
       val docBindings = ssep((bindings.toSeq map (p => parens(render(p._1) <+> render(p._2)))).to(collection.immutable.Seq), space)
       parens(text("let") <+> parens(docBindings) <+> render(body))
 
-    case MagicWandSnapshot(_, _, wandMap) => render(wandMap)
+    case MagicWandSnapshot(mwsf) => render(mwsf)
     case MWSFLookup(mwsf, snap) => renderApp("MWSF_apply", Seq(mwsf, snap), sorts.Snap)
 
     case _: MagicWandChunkTerm

src/main/scala/rules/HavocSupporter.scala

@@ -185,12 +185,10 @@ object havocSupporter extends SymbolicExecutionRules {
       case ch: MagicWandChunk =>
         val havockedSnap = freshSnap(sorts.Snap, v)
         val abstractLhs = freshSnap(sorts.Snap, v)
-        val freshWandMap = v.decider.fresh("mwsf", sorts.MagicWandSnapFunction)
         val cond = replacementCond(lhs, ch.args, condInfo)
 
         // Define a new `MagicWandSnapshot` that checks the havoc condition when being applied
-        val magicWandSnapshot = MagicWandSnapshot(abstractLhs, Ite(cond, havockedSnap, MWSFLookup(ch.snap.wandMap, abstractLhs)), freshWandMap)
-        v.decider.assumeDefinition(magicWandSnapshot.definition)
+        val magicWandSnapshot = magicWandSupporter.createMagicWandSnapshot(abstractLhs, Ite(cond, havockedSnap, MWSFLookup(ch.snap.mwsf, abstractLhs)), v)
         ch.withSnap(magicWandSnapshot)
 
       case ch =>

src/main/scala/rules/MagicWandSupporter.scala

@@ -80,7 +80,7 @@ object magicWandSupporter extends SymbolicExecutionRules {
 //  }
 
   /**
-   * Evaluate the wand's arguments and create a `MagicWandChunk` out of it.
+   * Evaluate the wand's arguments and create a [[viper.silicon.state.MagicWandChunk]] out of it.
    */
   def createChunk(s: State,
                   wand: ast.MagicWand,
@@ -94,6 +94,30 @@ object magicWandSupporter extends SymbolicExecutionRules {
     )
   }
 
+  /**
+   * Create a new [[viper.silicon.state.terms.MagicWandSnapshot]]
+   * and add the corresponding [[viper.silicon.state.terms.sorts.MagicWandSnapFunction]] definition to the state.
+   *
+   * It defines that when we apply the MagicWandSnapFunction to a snapshot `snap`
+   * we will get back `rhsSnapshot` that includes the values from that snapshot `snap`.
+   *
+   * @param abstractLhs The term that represent the snapshot of the consumed left-hand side of the magic wand.
+   *                    It is used as a bound variable in a forall quantifier.
+   * @param rhsSnapshot The term that integrates the left-hand side in the snapshot that is produced after applying the magic wand.
+   * @param v           Verifier instance
+   * @return Fresh instance of [[viper.silicon.state.terms.MagicWandSnapshot]]
+   */
+  def createMagicWandSnapshot(abstractLhs: Var, rhsSnapshot: Term, v: Verifier): MagicWandSnapshot = {
+    val mwsf = v.decider.fresh("mwsf", sorts.MagicWandSnapFunction)
+    val magicWandSnapshot = MagicWandSnapshot(mwsf)
+    v.decider.assumeDefinition(Forall(
+      abstractLhs,
+      MWSFLookup(mwsf, abstractLhs) === rhsSnapshot,
+      Trigger(MWSFLookup(mwsf, abstractLhs))
+    ))
+    magicWandSnapshot
+  }
+
   /**
    * Evaluate all expressions inside the given magic wand instance in the current state.
    *
@@ -259,9 +283,8 @@ object magicWandSupporter extends SymbolicExecutionRules {
                                        : VerificationResult = {
       val preMark = v3.decider.setPathConditionMark()
 
-      v3.decider.prover.comment(s"Create WandMap for wand $wand")
-      val wandSnapshot = MagicWandSnapshot(freshSnapRoot, snapRhs, v3.decider.fresh("mwsf", sorts.MagicWandSnapFunction))
-      v3.decider.assumeDefinition(wandSnapshot.definition)
+      v3.decider.prover.comment(s"Create MagicWandSnapFunction for wand $wand")
+      val wandSnapshot = this.createMagicWandSnapshot(freshSnapRoot, snapRhs, v3)
 
       // If the wand is used as a quantified resource anywhere in the program
       if (s4.qpMagicWands.contains(MagicWandIdentifier(wand, s.program))) {
@@ -282,20 +305,20 @@ object magicWandSupporter extends SymbolicExecutionRules {
       } else {
         this.createChunk(s4, wand, wandSnapshot, pve, v3)((s5, ch, v4) => {
           val conservedPcs = s5.conservedPcs.head :+ v4.decider.pcs.after(preMark).definitionsOnly
-          // Partition path conditions into a set which include the abstractLhs and those which do not
-          val (pcsWithAbstractLhs, pcsWithoutAbstractLhs) = conservedPcs.flatMap(_.conditionalized).partition(pcs => pcs.contains(wandSnapshot.abstractLhs))
-          // For all path conditions which include the abstractLhs, add those as part of the definition of the wandMap in the same forall quantifier
+          // Partition path conditions into a set which include the freshSnapRoot and those which do not
+          val (pcsWithFreshSnapRoot, pcsWithoutFreshSnapRoot) = conservedPcs.flatMap(_.conditionalized).partition(pcs => pcs.contains(freshSnapRoot))
+          // For all path conditions which include the freshSnapRoot, add those as part of the definition of the MWSF in the same forall quantifier
           val pcsQuantified = Forall(
-            wandSnapshot.abstractLhs,
-            And(pcsWithAbstractLhs.map {
-              // Remove redundant forall quantifiers with the same quantified variable
-              case Quantification(Forall, wandSnapshot.abstractLhs :: Nil, body: Term, _, _, _, _) => body
+            freshSnapRoot,
+            And(pcsWithFreshSnapRoot.map {
+              // Remove forall quantifiers with the same quantified variable
+              case Quantification(Forall, v :: Nil, body: Term, _, _, _, _) if v == freshSnapRoot => body
               case p => p
             }),
-            Trigger(MWSFLookup(wandSnapshot.wandMap, wandSnapshot.abstractLhs)),
+            Trigger(MWSFLookup(wandSnapshot.mwsf, freshSnapRoot)),
           )
 
-          appendToResults(s5, ch, v4.decider.pcs.after(preMark), pcsQuantified +: pcsWithoutAbstractLhs, v4)
+          appendToResults(s5, ch, v4.decider.pcs.after(preMark), pcsQuantified +: pcsWithoutFreshSnapRoot, v4)
           Success()
         })
       }
@@ -418,8 +441,8 @@ object magicWandSupporter extends SymbolicExecutionRules {
 
         // If the snapWand is a (wrapped) MagicWandSnapshot then lookup the snapshot of the right-hand side by applying snapLhs.
         val magicWandSnapshotLookup = snapWand match {
-          case snapshot: MagicWandSnapshot => snapshot.applyToWandMap(snapLhs)
-          case SortWrapper(snapshot: MagicWandSnapshot, _) => snapshot.applyToWandMap(snapLhs)
+          case snapshot: MagicWandSnapshot => snapshot.applyToMWSF(snapLhs)
+          case SortWrapper(snapshot: MagicWandSnapshot, _) => snapshot.applyToMWSF(snapLhs)
           // Fallback solution for quantified magic wands
           case predicateLookup: PredicateLookup =>
             v2.decider.assume(snapLhs === First(snapWand))

src/main/scala/rules/Producer.scala

@@ -399,16 +399,14 @@ object producer extends ProductionRules {
       case wand: ast.MagicWand =>
         val snapRhs = sf(sorts.MagicWandSnapFunction, v)
 
-        // Create Map that takes a snapshot, which represent the values of the consumed LHS of the wand,
+        // Create MWSF that takes a snapshot, which represent the values of the consumed LHS of the wand,
         // and relates it to the snapshot of the RHS. We use this to preserve values of the LHS in the RHS snapshot.
-        v.decider.prover.comment(s"Produce new magic wand snapshot map for wand $wand")
+        v.decider.prover.comment(s"Produce MagicWandSnapFunction for wand $wand")
         val abstractLhs = v.decider.fresh(sorts.Snap)
-        val wandMap = v.decider.fresh("$mwsf", sorts.MagicWandSnapFunction)
-        val magicWandSnapshot = MagicWandSnapshot(abstractLhs, MWSFLookup(snapRhs, abstractLhs), wandMap)
 
-        // We assume that the wandMap that we get from `snapRhs`, which potentially is nested in a binary tree,
-        // is the same as our newly created wandMap.
-        v.decider.assumeDefinition(magicWandSnapshot.definition)
+        // We assume that the MWSF that we get from `snapRhs` is the same as our newly created MWSF.
+        // `snapRhs` is an expression that potentially returns a nested element of a binary tree.
+        val magicWandSnapshot = magicWandSupporter.createMagicWandSnapshot(abstractLhs, MWSFLookup(snapRhs, abstractLhs), v)
 
         magicWandSupporter.createChunk(s, wand, magicWandSnapshot, pve, v)((s1, chWand, v1) =>
           chunkSupporter.produce(s1, s1.h, chWand, v1)((s2, h2, v2) =>

src/main/scala/state/Terms.scala

@@ -2301,36 +2301,20 @@ object PredicateTrigger extends PreciseCondFlyweightFactory[(String, Term, Seq[T
 /* Magic wands */
 
 /**
- * Represents a snapshot of a magic wand, which is a map from Snap to Snap.
+ * Represents a snapshot of a magic wand, which is a function from `Snap` to `Snap`.
  *
- * @param abstractLhs The term that represent the snapshot of the consumed left-hand side of the magic wand.
- *                    It is used as a bound variable in a forall quantifier.
- * @param rhsSnapshot The term that integrates the left-hand side in the snapshot that is produced after applying the magic wand.
- * @param wandMap The map that represents the snapshot of the magic wand. It is a variable of sort Map(Snap, Snap).
- *                In the symbolic execution this represents a function that when we apply a magic wand
- *                it consumes the left-hand side and uses the resulting snapshot to look up which right-hand side should be produced.
+ * @param mwsf The function that represents the snapshot of the magic wand. It is a variable of sort [[sorts.MagicWandSnapFunction]].
+ *             In the symbolic execution when we apply a magic wand, it consumes the left-hand side
+ *             and uses this function and the resulting snapshot to look up which right-hand side to produce.
  */
-class MagicWandSnapshot(val abstractLhs: Var, val rhsSnapshot: Term, val wandMap: Term) extends Term with ConditionalFlyweight[(Var, Term, Term), MagicWandSnapshot] {
-  utils.assertSort(abstractLhs, "abstract lhs", sorts.Snap)
-  utils.assertSort(rhsSnapshot, "rhs snapshot", sorts.Snap)
-  utils.assertSort(wandMap, "wand map", sorts.MagicWandSnapFunction)
+class MagicWandSnapshot(val mwsf: Term) extends Term with ConditionalFlyweight[Term, MagicWandSnapshot] {
+  utils.assertSort(mwsf, "magic wand snap function", sorts.MagicWandSnapFunction)
 
   override val sort: Sort = sorts.MagicWandSnapFunction
 
-  override lazy val toString = s"wandSnap($wandMap)"
+  override lazy val toString = s"wandSnap($mwsf)"
 
-  override val equalityDefiningMembers: (Var, Term, Term) = (abstractLhs, rhsSnapshot, wandMap)
-
-  /**
-   * Creates a term that can be used to define a `wandMap`.
-   *
-   * @return Expression which says that the map applied to an arbitrary lhs equals to the snapshot of the rhs.
-   */
-  def definition: Term = Forall(
-    abstractLhs,
-    MWSFLookup(wandMap, abstractLhs) === rhsSnapshot,
-    Trigger(MWSFLookup(wandMap, abstractLhs))
-  )
+  override val equalityDefiningMembers: Term = mwsf
 
   /**
    * Apply the given snapshot of the left-hand side to the magic wand map to get the snapshot of the right-hand side
@@ -2339,15 +2323,22 @@ class MagicWandSnapshot(val abstractLhs: Var, val rhsSnapshot: Term, val wandMap
    * @param snapLhs The snapshot of the left-hand side that should be applied to the magic wand map.
    * @return The snapshot of the right-hand side that preserves the values of the left-hand side.
    */
-  def applyToWandMap(snapLhs: Term): Term = MWSFLookup(wandMap, snapLhs)
+  def applyToMWSF(snapLhs: Term): Term = MWSFLookup(mwsf, snapLhs)
 }
 
-object MagicWandSnapshot extends PreciseCondFlyweightFactory[(Var, Term, Term), MagicWandSnapshot]  {
+object MagicWandSnapshot extends PreciseCondFlyweightFactory[Term, MagicWandSnapshot]  {
   /** Create an instance of [[viper.silicon.state.terms.MagicWandSnapshot]]. */
-  override def actualCreate(args: (Var, Term, Term)): MagicWandSnapshot =
-    new MagicWandSnapshot(args._1, args._2, args._3)
+  override def actualCreate(arg: Term): MagicWandSnapshot =
+    new MagicWandSnapshot(arg)
 }
 
+/**
+ * Term that applies a [[sorts.MagicWandSnapFunction]] to a snapshot.
+ * It returns a snapshot for the RHS of a magic wand that includes that values of the given snapshot.
+ *
+ * @param mwsf Term of sort [[sorts.MagicWandSnapFunction]]. Function from `Snap` to `Snap`.
+ * @param snap Term of sort [[sorts.Snap]] to which the MWSF is applied to. It represents the values of the wand's LHS.
+ */
 class MWSFLookup(val mwsf: Term, val snap: Term) extends Term with ConditionalFlyweightBinaryOp[MWSFLookup] {
   val sort: Sort = sorts.Snap
   override def p0: Term = mwsf
@@ -2363,7 +2354,9 @@ object MWSFLookup extends PreciseCondFlyweightFactory[(Term, Term), MWSFLookup]
     createIfNonExistent(pair)
   }
 
-  override def actualCreate(args: (Term, Term)): MWSFLookup = new MWSFLookup(args._1, args._2)
+  /** Create an instance of [[viper.silicon.state.terms.MWSFLookup]]. */
+  override def actualCreate(args: (Term, Term)): MWSFLookup =
+    new MWSFLookup(args._1, args._2)
 }
 
 class MagicWandChunkTerm(val chunk: MagicWandChunk) extends Term with ConditionalFlyweight[MagicWandChunk, MagicWandChunkTerm] {

src/main/scala/state/Utils.scala

@@ -196,7 +196,7 @@ package object utils {
       case MapUpdate(t0, t1, t2) => MapUpdate(go(t0), go(t1), go(t2))
       case MapDomain(t) => MapDomain(go(t))
       case MapRange(t) => MapRange(go(t))
-      case MagicWandSnapshot(t0, t1, t2) => MagicWandSnapshot(go(t0), go(t1), go(t2))
+      case MagicWandSnapshot(t) => MagicWandSnapshot(go(t))
       case MWSFLookup(t0, t1) => MWSFLookup(go(t0), go(t1))
       case Combine(t0, t1) => Combine(go(t0), go(t1))
       case First(t) => First(go(t))

src/main/scala/supporters/BuiltinDomainsContributor.scala

@@ -16,7 +16,6 @@ import viper.silicon.interfaces.PreambleContributor
 import viper.silicon.interfaces.decider.ProverLike
 import viper.silicon.state.DefaultSymbolConverter
 import viper.silicon.state.terms._
-import viper.silver.ast.DomainType
 
 abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, DomainFun, Term] {
   type BuiltinDomainType <: ast.GenericType
@@ -82,7 +81,7 @@ abstract class BuiltinDomainsContributor extends PreambleContributor[Sort, Domai
   /**
    * For each necessary domain type, instantiate the corresponding domain
    */
-  private def instantiateWithDomain(sourceProgram: ast.Program, sourceDomain: ast.Domain, sourceDomainTypeInstances: InsertionOrderedSet[DomainType]): Set[(ast.DomainType, ast.Domain)] = {
+  private def instantiateWithDomain(sourceProgram: ast.Program, sourceDomain: ast.Domain, sourceDomainTypeInstances: InsertionOrderedSet[ast.DomainType]): Set[(ast.DomainType, ast.Domain)] = {
     sourceDomainTypeInstances map (domainType => {
       /* TODO: Copied from DomainInstances.getInstanceMembers.
        *       Cannot directly use that because it filters according to which domain instances