From 823a25dabc885e7be5e41e55df611e5362fc7853 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Anders=20M=C3=B8ller?= Date: Sun, 31 Oct 2021 23:09:21 +0100 Subject: [PATCH] Cumulative updates --- build.sbt | 2 +- src/tip/Tip.scala | 14 +- src/tip/analysis/AndersenAnalysis.scala | 2 +- src/tip/analysis/ControlFlowAnalysis.scala | 4 +- .../CopyConstantPropagationAnalysis.scala | 2 +- src/tip/analysis/Dependencies.scala | 2 +- src/tip/analysis/SteensgaardAnalysis.scala | 2 +- src/tip/analysis/TypeAnalysis.scala | 2 +- src/tip/ast/AstOps.scala | 11 +- src/tip/ast/TipSublanguages.scala | 2 +- src/tip/solvers/CubicSolver.scala | 206 ------------------ src/tip/solvers/IDESolver.scala | 7 +- src/tip/solvers/SimpleCubicSolver.scala | 141 ++++++++++++ src/tip/solvers/SpecialCubicSolver.scala | 151 +++++++++++++ 14 files changed, 323 insertions(+), 225 deletions(-) delete mode 100644 src/tip/solvers/CubicSolver.scala create mode 100644 src/tip/solvers/SimpleCubicSolver.scala create mode 100644 src/tip/solvers/SpecialCubicSolver.scala diff --git a/build.sbt b/build.sbt index 559b209..adfd47e 100644 --- a/build.sbt +++ b/build.sbt @@ -9,4 +9,4 @@ scalacOptions ++= Seq("-unchecked", "-deprecation", "-feature") libraryDependencies += "org.parboiled" %% "parboiled" % "2.1.8" libraryDependencies += "com.regblanc" % "scala-smtlib_2.12" % "0.2.1" -scalaSource in Compile := baseDirectory.value / "src" +Compile / scalaSource := baseDirectory.value / "src" diff --git a/src/tip/Tip.scala b/src/tip/Tip.scala index 97d9259..9a5529e 100644 --- a/src/tip/Tip.scala +++ b/src/tip/Tip.scala @@ -179,11 +179,15 @@ object Tip extends App { log.error(s"Failure parsing the program: $file", e) sys.exit(1) case Success(parsedNode: AProgram) => - // run normalizer - log.verb("Normalizing") - val programNode = options.normalizer.normalizeProgram(parsedNode) - if (options.normalizer != NoNormalizer) - Output.output(file, OtherOutput(OutputKindE.normalized), programNode.toString, options.out) + val programNode = + if (options.normalizer == NoNormalizer) parsedNode + else { + // run normalizer + log.verb("Normalizing") + val p = options.normalizer.normalizeProgram(parsedNode) + Output.output(file, OtherOutput(OutputKindE.normalized), p.toString, options.out) + p + } // run declaration analysis // (for information about the use of 'implicit', see [[tip.analysis.TypeAnalysis]]) diff --git a/src/tip/analysis/AndersenAnalysis.scala b/src/tip/analysis/AndersenAnalysis.scala index 944e433..cc05d25 100644 --- a/src/tip/analysis/AndersenAnalysis.scala +++ b/src/tip/analysis/AndersenAnalysis.scala @@ -18,7 +18,7 @@ class AndersenAnalysis(program: AProgram)(implicit declData: DeclarationData) ex override def toString = id.toString } - val solver = new CubicSolver[Cell, Cell] + val solver = new SimpleCubicSolver[Cell, Cell] import AstOps._ val cells: Set[Cell] = (program.appearingIds.map(Var): Set[Cell]) union program.appearingAllocs.map(Alloc) diff --git a/src/tip/analysis/ControlFlowAnalysis.scala b/src/tip/analysis/ControlFlowAnalysis.scala index d0b1da5..dcc202c 100644 --- a/src/tip/analysis/ControlFlowAnalysis.scala +++ b/src/tip/analysis/ControlFlowAnalysis.scala @@ -1,7 +1,7 @@ package tip.analysis import tip.ast.{AAssignStmt, AIdentifier, AProgram, AstNode, DepthFirstAstVisitor, _} -import tip.solvers.CubicSolver +import tip.solvers.SimpleCubicSolver import tip.util.Log import tip.ast.AstNodeData.{AstNodeWithDeclaration, DeclarationData} @@ -24,7 +24,7 @@ class ControlFlowAnalysis(program: AProgram)(implicit declData: DeclarationData) } } - private val solver = new CubicSolver[AstVariable, Decl] + private val solver = new SimpleCubicSolver[AstVariable, Decl] val allFunctions: Set[AFunDeclaration] = program.funs.toSet diff --git a/src/tip/analysis/CopyConstantPropagationAnalysis.scala b/src/tip/analysis/CopyConstantPropagationAnalysis.scala index 9c06520..1b3ad90 100644 --- a/src/tip/analysis/CopyConstantPropagationAnalysis.scala +++ b/src/tip/analysis/CopyConstantPropagationAnalysis.scala @@ -63,7 +63,7 @@ trait CopyConstantPropagationAnalysisFunctions extends IDEAnalysis[ADeclaration, case AAssignStmt(id: AIdentifier, right, _) => val edges = assign(d, id.declaration, right) d match { - case Left(a) if id != a => + case Left(a) if id.declaration != a => edges :+ ((d, IdEdge())) // not at the variable being written to, so add identity edge case _ => edges diff --git a/src/tip/analysis/Dependencies.scala b/src/tip/analysis/Dependencies.scala index bb68f70..886aa76 100644 --- a/src/tip/analysis/Dependencies.scala +++ b/src/tip/analysis/Dependencies.scala @@ -89,7 +89,7 @@ trait ContextSensitiveForwardDependencies[C <: CallContext] extends Dependencies */ override def outdep(n: (C, CfgNode)): Set[(C, CfgNode)] = (n._2 match { - case call: CfgCallNode => Set() + case _: CfgCallNode => Set() case _ => n._2.succ.toSet }).map { d => (n._1, d) diff --git a/src/tip/analysis/SteensgaardAnalysis.scala b/src/tip/analysis/SteensgaardAnalysis.scala index d030902..7afbecf 100644 --- a/src/tip/analysis/SteensgaardAnalysis.scala +++ b/src/tip/analysis/SteensgaardAnalysis.scala @@ -112,7 +112,7 @@ sealed trait StTerm */ case class AllocVariable(alloc: AAlloc) extends StTerm with Var[StTerm] { - override def toString: String = s"\u27E6alloc{${alloc.loc}}]]" + override def toString: String = s"\u27E6alloc{${alloc.loc}}\u27E7" } /** diff --git a/src/tip/analysis/TypeAnalysis.scala b/src/tip/analysis/TypeAnalysis.scala index f7f0fe6..7239810 100644 --- a/src/tip/analysis/TypeAnalysis.scala +++ b/src/tip/analysis/TypeAnalysis.scala @@ -2,7 +2,7 @@ package tip.analysis import tip.ast._ import tip.solvers._ -import tip.types.{AbsentFieldType, _} +import tip.types._ import tip.ast.AstNodeData._ import tip.util.{Log, TipProgramException} import AstOps._ diff --git a/src/tip/ast/AstOps.scala b/src/tip/ast/AstOps.scala index fc79f78..b9208fd 100644 --- a/src/tip/ast/AstOps.scala +++ b/src/tip/ast/AstOps.scala @@ -131,7 +131,7 @@ object AstOps { * Checks whether the subtree of the node contains an 'input' expression. */ def containsInput: Boolean = { - var res = false; + var res = false new DepthFirstAstVisitor[Unit] { override def visit(node: AstNode, arg: Unit): Unit = node match { @@ -156,6 +156,15 @@ object AstOps { case rec: ARecord => fields ++= rec.fields.map { _.field } visitChildren(rec, ()) + case as: AAssignStmt => + as.left match { + case dfw: ADirectFieldWrite => + fields += dfw.field + case ifw: AIndirectFieldWrite => + fields += ifw.field + case _ => + } + visitChildren(as, ()) case _ => visitChildren(node, ()) } } diff --git a/src/tip/ast/TipSublanguages.scala b/src/tip/ast/TipSublanguages.scala index dd255b5..f267383 100644 --- a/src/tip/ast/TipSublanguages.scala +++ b/src/tip/ast/TipSublanguages.scala @@ -39,7 +39,7 @@ class NoFunctionPointers(implicit declData: DeclarationData) extends TipSublangu LanguageRestrictionViolation(s"Indirect call not allowed, $targetFun is not a function", ast.loc) } args.foreach(visit(_, x)) - case ACallFuncExpr(targetFun, args, _) => + case ACallFuncExpr(targetFun, _, _) => LanguageRestrictionViolation(s"Indirect call not allowed, $targetFun is not a function", ast.loc) case id: AIdentifier => id.declaration match { diff --git a/src/tip/solvers/CubicSolver.scala b/src/tip/solvers/CubicSolver.scala deleted file mode 100644 index 86e3f4b..0000000 --- a/src/tip/solvers/CubicSolver.scala +++ /dev/null @@ -1,206 +0,0 @@ -package tip.solvers - -import tip.util.Log - -import scala.collection.mutable -import scala.language.implicitConversions - -/** - * The cubic solver. - * - * @param cycleElimination: whether to use cycle elimination or not - * @tparam V type of variables - * @tparam T type of tokens - */ -class CubicSolver[V, T](cycleElimination: Boolean = true) { - - val log = Log.logger[this.type]() - - var lastTknId: Int = -1 - - def nextTokenId: Int = { - lastTknId += 1; lastTknId - } - - class Node( - val succ: mutable.Set[V] = mutable.Set(), // note: the edges between nodes go via the variables - val tokenSol: mutable.BitSet = new mutable.BitSet(), // the current solution bitvector - val conditionals: mutable.Map[Int, mutable.Set[(V, V)]] = mutable.Map(), // the pending conditional constraints - val vars: mutable.Set[V] = mutable.Set() // the variables belonging to this node - ) { - def this(x: V) { - this() - vars += x - } - - override def toString = this.hashCode.toString - } - - /** - * The map from variables to nodes. - */ - val varToNode: mutable.Map[V, Node] = mutable.Map() - - /** - * Provides an index for each token that we have seen. - */ - val tokenToInt: mutable.Map[T, Int] = mutable.Map() - - /** - * Returns the index associated with the given token. - * Allocates a fresh index if the token hasn't been seen before. - */ - implicit private def getTokenInt(tkn: T): Int = - tokenToInt.getOrElseUpdate(tkn, nextTokenId) - - /** - * Retrieves the node associated with the given variable. - * Allocates a fresh node if the variable hasn't been seen before. - */ - private def getOrPutNode(x: V): Node = - varToNode.getOrElseUpdate(x, new Node(x)) - - /** - * Attempts to detect a path from `from` to `to` in the graph. - * @return the list of variables in the path if such path is found, an empty list otherwise. - */ - private def detectPath(from: Node, to: Node): List[Node] = { - val visited: mutable.Set[Node] = mutable.Set() - - def detectPathRec(current: Node): List[Node] = - if (current == to) { - // Detected a path from from to to - List(current) - } else { - visited += current - // Search for the first cycle we can find, and save it - // If no cycle is found, return the empty list - var toReturn: List[Node] = List() - current.succ - .map(varToNode(_)) - .toSet - .filter(!visited.contains(_)) - .exists { n: Node => - val cycleVisited = detectPathRec(n) - if (cycleVisited.nonEmpty) { - // Cycle found - toReturn = current :: cycleVisited - true - } else false // keep searching - } - toReturn - } - val res = detectPathRec(from) - res - } - - /** - * Collapses the given cycle (if nonempty). - */ - private def collapseCycle(cycle: List[Node]) = - if (cycle.nonEmpty) { - log.verb(s"Collapsing cycle $cycle") - val first = cycle.head - cycle.tail.foreach { oldNode => - // Merge oldNode into first - first.succ ++= oldNode.succ - first.conditionals.keys.foreach { k => - first.conditionals(k) ++= oldNode.conditionals(k) - } - first.tokenSol |= oldNode.tokenSol - // Redirect all the variables that were pointing to this node to the new one - oldNode.vars.foreach { v => - varToNode(v) = first - first.vars += v - } - } - } - - /** - * Adds the set of tokens `s` to the variable `x` and propagates along the graph. - */ - private def addAndPropagateBits(s: mutable.BitSet, x: V): Unit = { - val node = getOrPutNode(x) - val old = node.tokenSol.clone() - val newTokens = old | s - if (newTokens != old) { - // Set the new bits - node.tokenSol |= s - val diff = newTokens &~ old - - // Add edges from pending lists, then clear the lists - diff.foreach { t => - node.conditionals.getOrElse(t, Set()).foreach { - case (v1, v2) => - addSubsetConstraint(v1, v2) - } - } - diff.foreach { t => - node.conditionals.remove(t) - } - - // Propagate to successors - node.succ.foreach { s => - addAndPropagateBits(newTokens, s) - } - } - } - - /** - * Adds a constraint of type t ∈ x. - */ - def addConstantConstraint(t: T, x: V): Unit = { - log.verb(s"Adding constraint $t \u2208 \u27E6$x\u27E7") - val bs = new mutable.BitSet() - bs.add(t) - addAndPropagateBits(bs, x) - } - - /** - * Adds a constraint of type x ⊆ y. - */ - def addSubsetConstraint(x: V, y: V): Unit = { - log.verb(s"Adding constraint \u27E6$x\u27E7 \u2286 \u27E6$y\u27E7") - val nx = getOrPutNode(x) - val ny = getOrPutNode(y) - - if (nx != ny) { - // Add the edge - log.verb(s"Adding edge $x -> $y") - nx.succ += y - - // Propagate the bits - addAndPropagateBits(nx.tokenSol, y) - - // Collapse newly introduced cycle, if any - if (cycleElimination) - collapseCycle(detectPath(ny, nx)) - } - } - - /** - * Adds a constraint of type t ∈ x ⇒ y ⊆ z. - */ - def addConditionalConstraint(t: T, x: V, y: V, z: V): Unit = { - log.verb(s"Adding constraint $t \u2208 \u27E6$x\u27E7 => \u27E6$y\u27E7 \u2286 \u27E6$z\u27E7") - val xn = getOrPutNode(x) - if (xn.tokenSol.contains(t)) { - // Already enabled - addSubsetConstraint(y, z) - } else if (y != z) { - // Not yet enabled, add to pending list - log.verb(s"Condition $t \u2208 \u27E6$x\u27E7 not yet enabled, adding (\u27E6$y\u27E7,\u27E6$z\u27E7) to pending") - xn.conditionals - .getOrElseUpdate(t, mutable.Set[(V, V)]()) - .add((y, z)) - } - } - - /** - * Returns the current solution as a map from variables to token sets. - */ - def getSolution: Map[V, Set[T]] = { - val intToToken = tokenToInt.map(p => p._2 -> p._1).toMap[Int, T] - varToNode.keys.map(v => v -> getOrPutNode(v).tokenSol.map(intToToken).toSet).toMap - } -} diff --git a/src/tip/solvers/IDESolver.scala b/src/tip/solvers/IDESolver.scala index 584a9df..8f423cd 100644 --- a/src/tip/solvers/IDESolver.scala +++ b/src/tip/solvers/IDESolver.scala @@ -183,14 +183,13 @@ abstract class IDEPhase1Analysis[D, L <: Lattice](val cfg: InterproceduralProgra */ def summaries(): mutable.Map[AFunDeclaration, mutable.Map[DL, mutable.Map[DL, Edge]]] = { import edgelattice.Edge - import mutable.Map - val res = Map[AFunDeclaration, Map[DL, Map[DL, Edge]]]() + val res = mutable.Map[AFunDeclaration, mutable.Map[DL, mutable.Map[DL, Edge]]]() x.foreach { case ((n, d1, d2), e) => n match { case funexit: CfgFunExitNode => - val m1 = res.getOrElseUpdate(funexit.data, Map[DL, Map[DL, Edge]]().withDefaultValue(Map[DL, Edge]())) - val m2 = m1.getOrElseUpdate(d1, Map[DL, Edge]()) + val m1 = res.getOrElseUpdate(funexit.data, mutable.Map[DL, mutable.Map[DL, Edge]]().withDefaultValue(mutable.Map[DL, Edge]())) + val m2 = m1.getOrElseUpdate(d1, mutable.Map[DL, Edge]()) m2 += d2 -> e case _ => // ignore other node kinds } diff --git a/src/tip/solvers/SimpleCubicSolver.scala b/src/tip/solvers/SimpleCubicSolver.scala new file mode 100644 index 0000000..087c8d2 --- /dev/null +++ b/src/tip/solvers/SimpleCubicSolver.scala @@ -0,0 +1,141 @@ +package tip.solvers + +import tip.util.Log + +import scala.collection.mutable +import scala.language.implicitConversions + +/** + * Simple cubic solver. + * + * @tparam V type of variables + * @tparam T type of tokens + */ +class SimpleCubicSolver[V, T] { + + private val log = Log.logger[this.type]() + + private var lastTknId: Int = -1 + + private def nextTokenId: Int = { + lastTknId += 1; lastTknId + } + + private class Node( + val succ: mutable.Set[V] = mutable.Set(), // note: the edges between nodes go via the variables + val tokenSol: mutable.BitSet = new mutable.BitSet(), // the current solution bitvector + val conditionals: mutable.Map[Int, mutable.Set[(V, V)]] = mutable.Map() // the pending conditional constraints + ) + + /** + * The map from variables to nodes. + */ + private val varToNode: mutable.Map[V, Node] = mutable.Map() + + /** + * Provides an index for each token that we have seen. + */ + private val tokenToInt: mutable.Map[T, Int] = mutable.Map() + + /** + * Worklist of (token, variable) pairs. + */ + private val worklist: mutable.Queue[(Int, V)] = mutable.Queue() + + /** + * Returns the index associated with the given token. + * Allocates a fresh index if the token hasn't been seen before. + */ + implicit private def getTokenInt(tkn: T): Int = + tokenToInt.getOrElseUpdate(tkn, nextTokenId) + + /** + * Retrieves the node associated with the given variable. + * Allocates a fresh node if the variable hasn't been seen before. + */ + private def getOrMakeNode(x: V): Node = + varToNode.getOrElseUpdate(x, new Node) + + /** + * Adds a token to the solution for a variable. + */ + private def addToken(t: Int, x: V): Unit = + if (getOrMakeNode(x).tokenSol.add(t)) + worklist += ((t, x)) + + /** + * Adds an inclusion edge. + */ + private def addEdge(x: V, y: V): Unit = + if (x != y) { + val nx = getOrMakeNode(x) + if (nx.succ.add(y)) { + getOrMakeNode(y) + log.verb(s"Adding edge \u27E6$x\u27E7 -> \u27E6$y\u27E7") + for (t <- nx.tokenSol) + addToken(t, y) + } + } + + /** + * Processes items in the worklist. + */ + private def propagate(): Unit = + while (worklist.nonEmpty) { + // Pick element from worklist + val (t, x) = worklist.dequeue() + // Process pending constraints + val nx = getOrMakeNode(x) + nx.conditionals.remove(t).foreach { s => + for ((y, z) <- s) + addEdge(y, z) + } + // Propagate token to successors + for (v <- nx.succ) + addToken(t, v) + } + + /** + * Adds a constraint of type t∈⟦x⟧. + */ + def addConstantConstraint(t: T, x: V): Unit = { + log.verb(s"Adding constraint $t \u2208 \u27E6$x\u27E7") + addToken(t, x) + propagate() + } + + /** + * Adds a constraint of type ⟦x⟧⊆⟦y⟧. + */ + def addSubsetConstraint(x: V, y: V): Unit = { + log.verb(s"Adding constraint \u27E6$x\u27E7 \u2286 \u27E6$y\u27E7") + addEdge(x, y) + propagate() + } + + /** + * Adds a constraint of type t∈⟦x⟧⇒⟦y⟧⊆⟦z⟧. + */ + def addConditionalConstraint(t: T, x: V, y: V, z: V): Unit = { + log.verb(s"Adding constraint $t \u2208 \u27E6$x\u27E7 \u21D2 \u27E6$y\u27E7 \u2286 \u27E6$z\u27E7") + val xn = getOrMakeNode(x) + if (xn.tokenSol.contains(t)) { + // Already enabled + addSubsetConstraint(y, z) + } else if (y != z) { + // Not yet enabled, add to pending list + log.verb(s"Condition $t \u2208 \u27E6$x\u27E7 not yet enabled, adding (\u27E6$y\u27E7,\u27E6$z\u27E7) to pending") + xn.conditionals + .getOrElseUpdate(t, mutable.Set[(V, V)]()) + .add((y, z)) + } + } + + /** + * Returns the current solution as a map from variables to token sets. + */ + def getSolution: Map[V, Set[T]] = { + val intToToken = tokenToInt.map(p => p._2 -> p._1).toMap[Int, T] + varToNode.keys.map(v => v -> getOrMakeNode(v).tokenSol.map(intToToken).toSet).toMap + } +} diff --git a/src/tip/solvers/SpecialCubicSolver.scala b/src/tip/solvers/SpecialCubicSolver.scala new file mode 100644 index 0000000..4c59d46 --- /dev/null +++ b/src/tip/solvers/SpecialCubicSolver.scala @@ -0,0 +1,151 @@ +package tip.solvers + +import tip.util.Log + +import scala.collection.mutable +import scala.language.implicitConversions + +/** + * Special cubic solver. + * + * @tparam V type of variables (tokens are a subset of variables) + */ +class SpecialCubicSolver[V] { + + private val log = Log.logger[this.type]() + + private var lastTknId: Int = -1 + + private def nextTokenId: Int = { + lastTknId += 1; lastTknId + } + + private class Node( + val succ: mutable.Set[V] = mutable.Set(), // note: the edges between nodes go via the variables + val tokenSol: mutable.BitSet = new mutable.BitSet(), // the current solution bitvector + val fromTriggers: mutable.Set[V] = mutable.Set(), // universally quantified constraints from the current node + val toTriggers: mutable.Set[V] = mutable.Set() // universally quantified constraints to the current node + ) + + /** + * The map from variables to nodes. + */ + private val varToNode: mutable.Map[V, Node] = mutable.Map() + + /** + * Provides an index for each token that we have seen. + */ + private val tokenToInt: mutable.Map[V, Int] = mutable.Map() + + /** + * Maps each token index to the corresponding token. + */ + private val intToToken: mutable.ArrayBuffer[V] = mutable.ArrayBuffer() + + /** + * Worklist of (token, variable) pairs. + */ + private val worklist: mutable.Queue[(Int, V)] = mutable.Queue() + + /** + * Returns the index associated with the given token. + * Allocates a fresh index if the token hasn't been seen before. + */ + implicit private def getTokenInt(tkn: V): Int = + tokenToInt.getOrElseUpdate(tkn, { intToToken += tkn; nextTokenId }) + + /** + * Retrieves the node associated with the given variable. + * Allocates a fresh node if the variable hasn't been seen before. + */ + private def getOrMakeNode(x: V): Node = + varToNode.getOrElseUpdate(x, new Node) + + /** + * Adds a token to the solution for a variable. + */ + private def addToken(t: Int, x: V): Unit = + if (getOrMakeNode(x).tokenSol.add(t)) + worklist += ((t, x)) + + /** + * Adds an inclusion edge. + */ + private def addEdge(x: V, y: V): Unit = + if (x != y) { + val nx = getOrMakeNode(x) + if (nx.succ.add(y)) { + getOrMakeNode(y) + log.verb(s"Adding edge \u27E6$x\u27E7 -> \u27E6$y\u27E7") + for (t <- nx.tokenSol) + addToken(t, y) + } + } + + /** + * Processes items in the worklist. + */ + private def propagate(): Unit = + while (worklist.nonEmpty) { + // Pick element from worklist + val (t, x) = worklist.dequeue() + val tkn = intToToken(t) + val nx = varToNode(x) + // Process quantified constraints + for (y <- nx.fromTriggers) + addEdge(tkn, y) + for (y <- nx.toTriggers) + addEdge(y, tkn) + // Propagate token to successors + for (v <- nx.succ) + addToken(t, v) + } + + /** + * Adds a constraint of type t∈⟦x⟧. + */ + def addConstantConstraint(t: V, x: V): Unit = { + log.verb(s"Adding constraint $t \u2208 \u27E6$x\u27E7") + addToken(t, x) + propagate() + } + + /** + * Adds a constraint of type ⟦x⟧⊆⟦y⟧. + */ + def addSubsetConstraint(x: V, y: V): Unit = { + log.verb(s"Adding constraint \u27E6$x\u27E7 \u2286 \u27E6$y\u27E7") + addEdge(x, y) + propagate() + } + + /** + * Adds a constraint of type ∀t∈⟦x⟧: ⟦t⟧⊆⟦y⟧. + */ + def addUniversallyQuantifiedFromConstraint(x: V, y: V): Unit = { + log.verb(s"Adding constraint \u2200t \u2208 \u27E6$x\u27E7: \u27E6t\u27E7 \u2286 \u27E6$y\u27E7") + val xn = getOrMakeNode(x) + xn.fromTriggers += y + for (t <- xn.tokenSol) + addEdge(intToToken(t), y) + propagate() + } + + /** + * Adds a constraint of type ∀t∈⟦x⟧: ⟦y⟧⊆⟦t⟧. + */ + def addUniversallyQuantifiedToConstraint(x: V, y: V): Unit = { + log.verb(s"Adding constraint \u2200t \u2208 \u27E6$x\u27E7: \u27E6$y\u27E7 \u2286 \u27E6t\u27E7") + val xn = getOrMakeNode(x) + xn.toTriggers += y + for (t <- xn.tokenSol) + addEdge(y, intToToken(t)) + propagate() + } + + /** + * Returns the current solution as a map from variables to token sets. + */ + def getSolution: Map[V, Set[V]] = + varToNode.keys.map(v => v -> getOrMakeNode(v).tokenSol.map(intToToken).toSet).toMap +}