diff --git a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala index 2824b3f9794f6e7fda04642d7df10e3f1a90e870..8eb9d15653b1139caf640fb164da7488c7039cfd 100644 --- a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala +++ b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala @@ -28,11 +28,8 @@ object ChooseEntryPoint { private[this] val ids = new WeakHashMap[CompilationUnit, MutableMap[Problem, ChooseId]]() - private[this] var _next = 0 - private[this] def nextInt(): Int = { - _next += 1 - _next - } + private val intCounter = new UniqueCounter[Unit] + intCounter.nextGlobal // Start with 1 private def getUniqueId(unit: CompilationUnit, p: Problem): ChooseId = { if (!ids.containsKey(unit)) { @@ -42,7 +39,7 @@ object ChooseEntryPoint { if (ids.get(unit) contains p) { ids.get(unit)(p) } else { - val cid = new ChooseId(nextInt()) + val cid = new ChooseId(intCounter.nextGlobal) ids.get(unit) += p -> cid cid } diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala index 0433affa5cd69d958f9359adec8157f54a436b28..e4cfb8aafba33e82ef24806bd7b68de334c237b2 100644 --- a/src/main/scala/leon/repair/Repairman.scala +++ b/src/main/scala/leon/repair/Repairman.scala @@ -11,16 +11,19 @@ import purescala.Types._ import purescala.DefOps._ import purescala.Constructors._ import purescala.Extractors.unwrapTuple + import evaluators._ import solvers._ import utils._ import codegen._ import verification._ + import synthesis._ import synthesis.rules._ import synthesis.Witnesses._ +import synthesis.graph.{dotGenIds, DotGenerator} + import rules._ -import graph.DotGenerator import grammars._ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeoutMs: Option[Long], repairTimeoutMs: Option[Long]) { @@ -98,7 +101,7 @@ class Repairman(ctx0: LeonContext, initProgram: Program, fd: FunDef, verifTimeou if (synth.settings.generateDerivationTrees) { val dot = new DotGenerator(search.g) - dot.writeFile("derivation"+DotGenerator.nextId()+".dot") + dot.writeFile("derivation"+ dotGenIds.nextGlobal + ".dot") } if (solutions.isEmpty) { diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala index 067a79456b0c32a2927ef8ca2816f4fd69b4461f..73820eb3c079bf5c2f41a1394aedcadb8ce120d7 100644 --- a/src/main/scala/leon/synthesis/SynthesisPhase.scala +++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala @@ -80,7 +80,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] { try { if (options.generateDerivationTrees) { val dot = new DotGenerator(search.g) - dot.writeFile("derivation"+DotGenerator.nextId()+".dot") + dot.writeFile("derivation"+dotGenIds.nextGlobal+".dot") } val (sol, _) = solutions.head diff --git a/src/main/scala/leon/synthesis/graph/DotGenerator.scala b/src/main/scala/leon/synthesis/graph/DotGenerator.scala index e44496a2de7feb1a6936af8e49a62a86e140c21a..7da38716116f51d89e751a8aa12d709be776e17c 100644 --- a/src/main/scala/leon/synthesis/graph/DotGenerator.scala +++ b/src/main/scala/leon/synthesis/graph/DotGenerator.scala @@ -2,14 +2,17 @@ package leon.synthesis.graph +import leon.utils.UniqueCounter + import java.io.{File, FileWriter, BufferedWriter} class DotGenerator(g: Graph) { - private[this] var _nextID = 0 + private val idCounter = new UniqueCounter[Unit] + idCounter.nextGlobal // Start with 1 + def freshName(prefix: String) = { - _nextID += 1 - prefix+_nextID + prefix + idCounter.nextGlobal } def writeFile(f: File): Unit = { @@ -123,10 +126,4 @@ class DotGenerator(g: Graph) { } } -object DotGenerator { - private[this] var _nextID = 0 - def nextId() = { - _nextID += 1 - _nextID - } -} +object dotGenIds extends UniqueCounter[Unit] \ No newline at end of file