From cd29e3e24ff9267611c790e5b3bcc7ca5a156a04 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 1 Sep 2015 17:35:56 +0200
Subject: [PATCH] Use UniqueCounter consistently
---
.../leon/codegen/runtime/ChooseEntryPoint.scala | 9 +++------
src/main/scala/leon/repair/Repairman.scala | 7 +++++--
.../scala/leon/synthesis/SynthesisPhase.scala | 2 +-
.../leon/synthesis/graph/DotGenerator.scala | 17 +++++++----------
4 files changed, 16 insertions(+), 19 deletions(-)
diff --git a/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala b/src/main/scala/leon/codegen/runtime/ChooseEntryPoint.scala
index 2824b3f97..8eb9d1565 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 0433affa5..e4cfb8aaf 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 067a79456..73820eb3c 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 e44496a2d..7da387161 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
--
GitLab