diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 0b999061a..23679f6ef 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -185,7 +185,7 @@ object evaluator extends EvaluationRules { * term returned by eval, mark as constrainable on client-side (e.g. in consumer). */ val s1 = - s.copy(functionRecorder = s.functionRecorder.recordArp(tVar, tConstraints)) + s.copy(functionRecorder = s.functionRecorder.recordConstrainedVar(tVar, tConstraints)) .setConstrainable(Seq(tVar), true) Q(s1, tVar, v) diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index 8e983f573..0e6778bd5 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -365,7 +365,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { ) v.decider.assume(constraint) - newFr = newFr.recordArp(permTaken, constraint) + newFr = newFr.recordConstrainedVar(permTaken, constraint) ch.withPerm(PermMinus(ch.perm, permTaken)) }) diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala index 452d0c7b3..49e22100c 100644 --- a/src/main/scala/rules/StateConsolidator.scala +++ b/src/main/scala/rules/StateConsolidator.scala @@ -216,7 +216,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol * to use t1 or t2 and constrain it. */ val t3 = v.decider.fresh(t1.sort) - (fr.recordFreshSnapshot(t3), t3, And(Implies(b1, t3 === t1), Implies(b2, t3 === t2))) + (fr.recordConstrainedVar(t3, And(Implies(b1, t3 === t1), Implies(b2, t3 === t2))), t3, And(Implies(b1, t3 === t1), Implies(b2, t3 === t2))) } } diff --git a/src/main/scala/supporters/functions/FunctionData.scala b/src/main/scala/supporters/functions/FunctionData.scala index 41f884e0a..1bf87874a 100644 --- a/src/main/scala/supporters/functions/FunctionData.scala +++ b/src/main/scala/supporters/functions/FunctionData.scala @@ -93,7 +93,7 @@ class FunctionData(val programFunction: ast.Function, private[functions] var fappToSnap: Map[ast.FuncApp, Term] = Map.empty private[this] var freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet.empty private[this] var freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet.empty - private[this] var freshArps: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty + private[this] var freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty private[this] var freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet.empty private[this] var freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet.empty private[this] var freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet.empty @@ -101,7 +101,7 @@ class FunctionData(val programFunction: ast.Function, private[this] var freshSymbolsAcrossAllPhases: InsertionOrderedSet[Decl] = InsertionOrderedSet.empty private[functions] def getFreshFieldInvs: InsertionOrderedSet[InverseFunctions] = freshFieldInvs - private[functions] def getFreshArps: InsertionOrderedSet[Var] = freshArps.map(_._1) + private[functions] def getFreshConstrainedVars: InsertionOrderedSet[Var] = freshConstrainedVars.map(_._1) private[functions] def getFreshSymbolsAcrossAllPhases: InsertionOrderedSet[Decl] = freshSymbolsAcrossAllPhases private[functions] def advancePhase(recorders: Seq[FunctionRecorder]): Unit = { @@ -117,14 +117,14 @@ class FunctionData(val programFunction: ast.Function, fappToSnap = mergedFunctionRecorder.fappToSnap freshFvfsAndDomains = mergedFunctionRecorder.freshFvfsAndDomains freshFieldInvs = mergedFunctionRecorder.freshFieldInvs - freshArps = mergedFunctionRecorder.freshArps + freshConstrainedVars = mergedFunctionRecorder.freshConstrainedVars freshConstraints = mergedFunctionRecorder.freshConstraints freshSnapshots = mergedFunctionRecorder.freshSnapshots freshPathSymbols = mergedFunctionRecorder.freshPathSymbols freshMacros = mergedFunctionRecorder.freshMacros freshSymbolsAcrossAllPhases ++= freshPathSymbols map FunctionDecl - freshSymbolsAcrossAllPhases ++= freshArps.map(pair => FunctionDecl(pair._1)) + freshSymbolsAcrossAllPhases ++= freshConstrainedVars.map(pair => FunctionDecl(pair._1)) freshSymbolsAcrossAllPhases ++= freshSnapshots map FunctionDecl freshSymbolsAcrossAllPhases ++= freshFieldInvs.flatMap(i => (i.inverses ++ i.images) map FunctionDecl) freshSymbolsAcrossAllPhases ++= freshMacros @@ -145,7 +145,7 @@ class FunctionData(val programFunction: ast.Function, val nested = ( freshFieldInvs.flatMap(_.definitionalAxioms) ++ freshFvfsAndDomains.flatMap (fvfDef => fvfDef.domainDefinitions ++ fvfDef.valueDefinitions) - ++ freshArps.map(_._2) + ++ freshConstrainedVars.map(_._2) ++ freshConstraints) // Filter out nested definitions that contain free variables. diff --git a/src/main/scala/supporters/functions/FunctionRecorder.scala b/src/main/scala/supporters/functions/FunctionRecorder.scala index 48c0ee2d8..756cb3545 100644 --- a/src/main/scala/supporters/functions/FunctionRecorder.scala +++ b/src/main/scala/supporters/functions/FunctionRecorder.scala @@ -25,7 +25,7 @@ trait FunctionRecorder extends Mergeable[FunctionRecorder] { def fappToSnap: Map[ast.FuncApp, Term] def freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] def freshFieldInvs: InsertionOrderedSet[InverseFunctions] - def freshArps: InsertionOrderedSet[(Var, Term)] + def freshConstrainedVars: InsertionOrderedSet[(Var, Term)] def freshConstraints: InsertionOrderedSet[Term] def freshSnapshots: InsertionOrderedSet[Function] def freshPathSymbols: InsertionOrderedSet[Function] @@ -34,7 +34,7 @@ trait FunctionRecorder extends Mergeable[FunctionRecorder] { def recordSnapshot(fapp: ast.FuncApp, guards: Stack[Term], snap: Term): FunctionRecorder def recordFvfAndDomain(fvfDef: SnapshotMapDefinition): FunctionRecorder def recordFieldInv(inv: InverseFunctions): FunctionRecorder - def recordArp(arp: Var, constraint: Term): FunctionRecorder + def recordConstrainedVar(v: Var, constraint: Term): FunctionRecorder def recordConstraint(constraint: Term): FunctionRecorder def recordFreshSnapshot(snap: Function): FunctionRecorder def recordPathSymbol(symbol: Function): FunctionRecorder @@ -48,7 +48,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData, private[functions] val fappToSnaps: Map[ast.FuncApp, InsertionOrderedSet[(Stack[Term], Term)]] = Map(), freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet(), freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet(), - freshArps: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet(), + freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet(), freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet(), freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet(), freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet(), @@ -189,8 +189,8 @@ case class ActualFunctionRecorder(private val _data: FunctionData, if (depth <= 2) copy(freshFieldInvs = freshFieldInvs + inv) else this - def recordArp(arp: Var, constraint: Term): ActualFunctionRecorder = - if (depth <= 2) copy(freshArps = freshArps + ((arp, constraint))) + def recordConstrainedVar(arp: Var, constraint: Term): ActualFunctionRecorder = + if (depth <= 2) copy(freshConstrainedVars = freshConstrainedVars + ((arp, constraint))) else this def recordConstraint(constraint: Term): ActualFunctionRecorder = @@ -237,7 +237,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData, val fvfs = freshFvfsAndDomains ++ other.freshFvfsAndDomains val fieldInvs = freshFieldInvs ++ other.freshFieldInvs - val arps = freshArps ++ other.freshArps + val arps = freshConstrainedVars ++ other.freshConstrainedVars val constraints = freshConstraints ++ other.freshConstraints val snaps = freshSnapshots ++ other.freshSnapshots val symbols = freshPathSymbols ++ other.freshPathSymbols @@ -247,7 +247,7 @@ case class ActualFunctionRecorder(private val _data: FunctionData, fappToSnaps = fts, freshFvfsAndDomains = fvfs, freshFieldInvs = fieldInvs, - freshArps = arps, + freshConstrainedVars = arps, freshConstraints = constraints, freshSnapshots = snaps, freshPathSymbols = symbols, @@ -277,7 +277,7 @@ case object NoopFunctionRecorder extends FunctionRecorder { val locToSnap: Map[ast.LocationAccess, Term] = Map.empty val freshFvfsAndDomains: InsertionOrderedSet[SnapshotMapDefinition] = InsertionOrderedSet.empty val freshFieldInvs: InsertionOrderedSet[InverseFunctions] = InsertionOrderedSet.empty - val freshArps: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty + val freshConstrainedVars: InsertionOrderedSet[(Var, Term)] = InsertionOrderedSet.empty val freshConstraints: InsertionOrderedSet[Term] = InsertionOrderedSet.empty val freshSnapshots: InsertionOrderedSet[Function] = InsertionOrderedSet.empty val freshPathSymbols: InsertionOrderedSet[Function] = InsertionOrderedSet.empty @@ -294,7 +294,7 @@ case object NoopFunctionRecorder extends FunctionRecorder { def recordFvfAndDomain(fvfDef: SnapshotMapDefinition): NoopFunctionRecorder.type = this def recordFieldInv(inv: InverseFunctions): NoopFunctionRecorder.type = this def recordSnapshot(fapp: ast.FuncApp, guards: Stack[Term], snap: Term): NoopFunctionRecorder.type = this - def recordArp(arp: Var, constraint: Term): NoopFunctionRecorder.type = this + def recordConstrainedVar(arp: Var, constraint: Term): NoopFunctionRecorder.type = this def recordConstraint(constraint: Term): NoopFunctionRecorder.type = this def recordFreshSnapshot(snap: Function): NoopFunctionRecorder.type = this def recordPathSymbol(symbol: Function): NoopFunctionRecorder.type = this