From 9f21f5f9199b9d87e842a5aaf1daee4d4e5818e2 Mon Sep 17 00:00:00 2001 From: Philippe Suter <philippe.suter@gmail.com> Date: Wed, 11 Sep 2013 21:39:42 +0200 Subject: [PATCH] Minor renamings. --- src/main/scala/leon/LeonContext.scala | 2 +- src/main/scala/leon/Main.scala | 2 +- .../scala/leon/datagen/DataGenerator.scala | 2 ++ src/main/scala/leon/plugin/ScalaCompiler.scala | 2 ++ .../scala/leon/solvers/SimpleSolverAPI.scala | 2 ++ .../scala/leon/solvers/SolverFactory.scala | 2 ++ .../TimeoutSolverFactory.scala} | 5 +++-- .../leon/solvers/z3/AbstractZ3Solver.scala | 2 +- .../leon/solvers/z3/FairZ3Component.scala | 2 ++ .../scala/leon/synthesis/SimpleSearch.scala | 2 +- .../scala/leon/synthesis/Synthesizer.scala | 1 + .../scala/leon/synthesis/TaskRunRule.scala | 2 ++ .../scala/leon/synthesis/TaskTryRules.scala | 2 ++ .../search/AndOrGraphParallelSearch.scala | 10 +++++----- .../leon/synthesis/utils/Benchmarks.scala | 2 +- .../scala/leon/utils/InterruptManager.scala | 2 ++ src/main/scala/leon/utils/Interruptible.scala | 2 ++ .../utils/{Stopwatch.scala => Timer.scala} | 18 +++++++++--------- .../leon/test/solvers/TimeoutSolverTests.scala | 1 + 19 files changed, 42 insertions(+), 21 deletions(-) rename src/main/scala/leon/solvers/{TimeoutSolver.scala => combinators/TimeoutSolverFactory.scala} (94%) rename src/main/scala/leon/utils/{Stopwatch.scala => Timer.scala} (76%) diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala index 761f882d2..91ad25d72 100644 --- a/src/main/scala/leon/LeonContext.scala +++ b/src/main/scala/leon/LeonContext.scala @@ -16,5 +16,5 @@ case class LeonContext( settings: Settings = Settings(), options: Seq[LeonOption] = Seq(), files: Seq[File] = Seq(), - timers: StopwatchCollections = new StopwatchCollections + timers: TimerCollections = new TimerCollections ) diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala index 343ed2da4..7fbb19e6c 100644 --- a/src/main/scala/leon/Main.scala +++ b/src/main/scala/leon/Main.scala @@ -211,7 +211,7 @@ object Main { def main(args : Array[String]) { try { // Process options - val timer = new Stopwatch().start + val timer = new Timer().start val ctx = processOptions(args.toList) diff --git a/src/main/scala/leon/datagen/DataGenerator.scala b/src/main/scala/leon/datagen/DataGenerator.scala index add01c033..c15f07a2b 100644 --- a/src/main/scala/leon/datagen/DataGenerator.scala +++ b/src/main/scala/leon/datagen/DataGenerator.scala @@ -1,3 +1,5 @@ +/* Copyright 2009-2013 EPFL, Lausanne */ + package leon package datagen diff --git a/src/main/scala/leon/plugin/ScalaCompiler.scala b/src/main/scala/leon/plugin/ScalaCompiler.scala index f6052d60a..489404d02 100644 --- a/src/main/scala/leon/plugin/ScalaCompiler.scala +++ b/src/main/scala/leon/plugin/ScalaCompiler.scala @@ -1,3 +1,5 @@ +/* Copyright 2009-2013 EPFL, Lausanne */ + package leon package plugin diff --git a/src/main/scala/leon/solvers/SimpleSolverAPI.scala b/src/main/scala/leon/solvers/SimpleSolverAPI.scala index 4812f1171..fd4c65252 100644 --- a/src/main/scala/leon/solvers/SimpleSolverAPI.scala +++ b/src/main/scala/leon/solvers/SimpleSolverAPI.scala @@ -1,3 +1,5 @@ +/* Copyright 2009-2013 EPFL, Lausanne */ + package leon package solvers diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala index 237722428..97e99d7d0 100644 --- a/src/main/scala/leon/solvers/SolverFactory.scala +++ b/src/main/scala/leon/solvers/SolverFactory.scala @@ -3,6 +3,8 @@ package leon package solvers +import solvers.combinators._ + import utils._ import purescala.Common._ import purescala.Definitions._ diff --git a/src/main/scala/leon/solvers/TimeoutSolver.scala b/src/main/scala/leon/solvers/combinators/TimeoutSolverFactory.scala similarity index 94% rename from src/main/scala/leon/solvers/TimeoutSolver.scala rename to src/main/scala/leon/solvers/combinators/TimeoutSolverFactory.scala index fe8c590c0..ce9e50712 100644 --- a/src/main/scala/leon/solvers/TimeoutSolver.scala +++ b/src/main/scala/leon/solvers/combinators/TimeoutSolverFactory.scala @@ -2,6 +2,7 @@ package leon package solvers +package combinators import purescala.Common._ import purescala.Definitions._ @@ -17,7 +18,7 @@ class TimeoutSolverFactory[S <: Solver](val sf: SolverFactory[S], val timeoutMs: val context = sf.context val program = sf.program - private class Timer(onTimeout: => Unit) extends Thread { + private class Countdown(onTimeout: => Unit) extends Thread { private var keepRunning = true private val asMillis : Long = timeoutMs @@ -46,7 +47,7 @@ class TimeoutSolverFactory[S <: Solver](val sf: SolverFactory[S], val timeoutMs: } def withTimeout[T](solver: S)(body: => T): T = { - val timer = new Timer(timeout(solver)) + val timer = new Countdown(timeout(solver)) timer.start val res = body timer.finishedRunning diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala index 7eb358708..6e8dbd5f7 100644 --- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala +++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala @@ -124,7 +124,7 @@ trait AbstractZ3Solver extends SolverFactory[Solver] { var isInitialized = false protected[leon] def initZ3() { if (!isInitialized) { - val initTime = new Stopwatch().start + val initTime = new Timer().start counter = 0 z3 = new Z3Context(z3cfg) diff --git a/src/main/scala/leon/solvers/z3/FairZ3Component.scala b/src/main/scala/leon/solvers/z3/FairZ3Component.scala index 14e3e4d55..116ce98cf 100644 --- a/src/main/scala/leon/solvers/z3/FairZ3Component.scala +++ b/src/main/scala/leon/solvers/z3/FairZ3Component.scala @@ -1,3 +1,5 @@ +/* Copyright 2009-2013 EPFL, Lausanne */ + package leon package solvers.z3 diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala index 39d7f0c77..cb2dd57c1 100644 --- a/src/main/scala/leon/synthesis/SimpleSearch.scala +++ b/src/main/scala/leon/synthesis/SimpleSearch.scala @@ -160,7 +160,7 @@ class SimpleSearch(synth: Synthesizer, def searchStep() { - val t = new Stopwatch().start + val t = new Timer().start val nl = nextLeaf() synth.context.timers.get("Synthesis NextLeaf") += t diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala index 40c3e4951..b138fcc8a 100644 --- a/src/main/scala/leon/synthesis/Synthesizer.scala +++ b/src/main/scala/leon/synthesis/Synthesizer.scala @@ -10,6 +10,7 @@ import purescala.Trees._ import purescala.ScalaPrinter import solvers._ +import solvers.combinators._ import solvers.z3._ import java.io.File diff --git a/src/main/scala/leon/synthesis/TaskRunRule.scala b/src/main/scala/leon/synthesis/TaskRunRule.scala index 642820672..a7f90e74f 100644 --- a/src/main/scala/leon/synthesis/TaskRunRule.scala +++ b/src/main/scala/leon/synthesis/TaskRunRule.scala @@ -1,3 +1,5 @@ +/* Copyright 2009-2013 EPFL, Lausanne */ + package leon package synthesis diff --git a/src/main/scala/leon/synthesis/TaskTryRules.scala b/src/main/scala/leon/synthesis/TaskTryRules.scala index 4ede43ce0..fd26092cf 100644 --- a/src/main/scala/leon/synthesis/TaskTryRules.scala +++ b/src/main/scala/leon/synthesis/TaskTryRules.scala @@ -1,3 +1,5 @@ +/* Copyright 2009-2013 EPFL, Lausanne */ + package leon package synthesis diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala index 8aba2ad6f..63ecfbafa 100644 --- a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala +++ b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala @@ -22,8 +22,8 @@ abstract class AndOrGraphParallelSearch[WC, var system: ActorSystem = _ - val sendWorkTimers = new StopwatchCollection("Synthesis-par SendWork") - val expandTimers = new StopwatchCollection("Synthesis-par Expand") + val sendWorkTimers = new TimerCollection("Synthesis-par SendWork") + val expandTimers = new TimerCollection("Synthesis-par Expand") def search(): Option[(S, Boolean)] = { system = ActorSystem("ParallelSearch") @@ -96,7 +96,7 @@ abstract class AndOrGraphParallelSearch[WC, assert(idleWorkers.size > 0) - val t = new Stopwatch().start + val t = new Timer().start getNextLeaves(idleWorkers, workingWorkers) match { case Nil => @@ -136,7 +136,7 @@ abstract class AndOrGraphParallelSearch[WC, case WorkerAndTaskDone(w, res) => workers.get(w) match { case Some(Some(l: g.AndLeaf)) => - val t = new Stopwatch().start + val t = new Timer().start onExpansion(l, res) expandTimers += t workers += w -> None @@ -147,7 +147,7 @@ abstract class AndOrGraphParallelSearch[WC, case WorkerOrTaskDone(w, res) => workers.get(w) match { case Some(Some(l: g.OrLeaf)) => - val t = new Stopwatch().start + val t = new Timer().start onExpansion(l, res) expandTimers += t workers += w -> None diff --git a/src/main/scala/leon/synthesis/utils/Benchmarks.scala b/src/main/scala/leon/synthesis/utils/Benchmarks.scala index 228e8720c..55756ad45 100644 --- a/src/main/scala/leon/synthesis/utils/Benchmarks.scala +++ b/src/main/scala/leon/synthesis/utils/Benchmarks.scala @@ -142,7 +142,7 @@ object Benchmarks extends App { // "║ └────────────┘" + (" " * 71) + "║" //println(infoHeader2) - //for ((name, sw) <- StopwatchCollections.getAll.toSeq.sortBy(_._1)) { + //for ((name, sw) <- TimerCollections.getAll.toSeq.sortBy(_._1)) { // println("║ %-70s %10s ms ║".format(name, sw.getMillis)) //} //println(infoFooter) diff --git a/src/main/scala/leon/utils/InterruptManager.scala b/src/main/scala/leon/utils/InterruptManager.scala index d69786ca1..d9a149aae 100644 --- a/src/main/scala/leon/utils/InterruptManager.scala +++ b/src/main/scala/leon/utils/InterruptManager.scala @@ -1,3 +1,5 @@ +/* Copyright 2009-2013 EPFL, Lausanne */ + package leon package utils diff --git a/src/main/scala/leon/utils/Interruptible.scala b/src/main/scala/leon/utils/Interruptible.scala index b9667d6bd..b81e64ed8 100644 --- a/src/main/scala/leon/utils/Interruptible.scala +++ b/src/main/scala/leon/utils/Interruptible.scala @@ -1,3 +1,5 @@ +/* Copyright 2009-2013 EPFL, Lausanne */ + package leon package utils diff --git a/src/main/scala/leon/utils/Stopwatch.scala b/src/main/scala/leon/utils/Timer.scala similarity index 76% rename from src/main/scala/leon/utils/Stopwatch.scala rename to src/main/scala/leon/utils/Timer.scala index 9622a4bd8..853ae298d 100644 --- a/src/main/scala/leon/utils/Stopwatch.scala +++ b/src/main/scala/leon/utils/Timer.scala @@ -3,13 +3,13 @@ package leon package utils -class StopwatchCollection(val name: String) { +class TimerCollection(val name: String) { var min: Long = 0L var tot: Long = 0L var max: Long = 0L var n: Int = 0 - def +=(sw: Stopwatch) = synchronized { + def +=(sw: Timer) = synchronized { val ms = sw.getMillis if(n == 0 || ms < min) { min = ms @@ -34,8 +34,8 @@ class StopwatchCollection(val name: String) { def getMillis = tot } -/** Implements a stopwatch for profiling purposes */ -class Stopwatch(name: String = "Stopwatch") { +/** Implements a timer for profiling purposes */ +class Timer(name: String = "Timer") { var beginning: Long = 0L var end: Long = 0L var acc: Long = 0L @@ -73,16 +73,16 @@ class Stopwatch(name: String = "Stopwatch") { override def toString = "%20s: %5d%sms".format(name, getMillis, if (isRunning) "..." else "") } -class StopwatchCollections { - private var all = Map[String, StopwatchCollection]() +class TimerCollections { + private var all = Map[String, TimerCollection]() - def get(name: String): StopwatchCollection = all.getOrElse(name, { - val sw = new StopwatchCollection(name) + def get(name: String): TimerCollection = all.getOrElse(name, { + val sw = new TimerCollection(name) all += name -> sw sw }) - def add(swc: StopwatchCollection) { + def add(swc: TimerCollection) { all += swc.name -> swc } diff --git a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala index 988a514e9..9745d3a12 100644 --- a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala +++ b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala @@ -5,6 +5,7 @@ package solvers import leon._ import leon.solvers._ +import leon.solvers.combinators._ import leon.purescala.Common._ import leon.purescala.Definitions._ import leon.purescala.Trees._ -- GitLab