From d3a54bc91c0c240a40a2f94fb5be70c2bb92e96e Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 18 Mar 2016 18:17:34 +0100
Subject: [PATCH] Fix timers
---
src/main/scala/leon/synthesis/Synthesizer.scala | 4 ++++
src/main/scala/leon/synthesis/rules/CEGISLike.scala | 6 +++---
2 files changed, 7 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 3a2a1df7f..c8a900bea 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -137,6 +137,9 @@ class Synthesizer(val context : LeonContext,
import verification.VerificationPhase._
import verification.VerificationContext
+ val timer = context.timers.synthesis.validation
+ timer.start()
+
reporter.info("Solution requires validation")
val (npr, fds) = solutionToProgram(sol)
@@ -160,6 +163,7 @@ class Synthesizer(val context : LeonContext,
(new PartialSolution(search.strat, false).getSolutionFor(search.g.root), Some(false))
}
} finally {
+ timer.stop()
solverf.shutdown()
}
}
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index d4f5e7240..cdd7d4333 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -45,7 +45,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
// Track non-deterministic programs up to 100'000 programs, or give up
val nProgramsLimit = 100000
- val timers = hctx.timers.synthesis.cegis
+ val timers = hctx.timers.synthesis.applications.CEGIS
// CEGIS Flags to activate or deactivate features
val useOptTimeout = hctx.settings.cegisUseOptTimeout
@@ -144,7 +144,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
// Update the c-tree after an increase in termsize
def updateCTree(): Unit = {
- hctx.timers.synthesis.cegis.updateCTree.start()
+ timers.updateCTree.start()
def freshB() = {
val id = FreshIdentifier("B", BooleanType, true)
bs += id
@@ -198,7 +198,7 @@ abstract class CEGISLike(name: String) extends Rule(name) {
excludedPrograms = Set()
prunedPrograms = allPrograms().toSet
- hctx.timers.synthesis.cegis.updateCTree.stop()
+ timers.updateCTree.stop()
}
// Returns a count of all possible programs
--
GitLab