diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 7fbb19e6cb47065cd7c4909460bc694421049dbb..2e27856cb36b68d4e716559527e384c31d13fcc5 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -143,13 +143,13 @@ object Main {
case LeonValueOption("debug", ListValue(sections)) =>
val debugSections = sections.flatMap { s =>
if (s == "all") {
- ReportingSections.all
+ DebugSections.all
} else {
- ReportingSections.all.find(_.name == s) match {
+ DebugSections.all.find(_.name == s) match {
case Some(rs) =>
Some(rs)
case None =>
- initReporter.error("Section "+s+" not found, available: "+ReportingSections.all.map(_.name).mkString(", "))
+ initReporter.error("Section "+s+" not found, available: "+DebugSections.all.map(_.name).mkString(", "))
None
}
}
@@ -163,7 +163,7 @@ object Main {
// Create a new reporter taking settings into account
val reporter = new DefaultReporter(settings)
- reporter.whenDebug(ReportingOptions) { debug =>
+ reporter.whenDebug(DebugSectionOptions) { debug =>
debug("Options considered by Leon:")
for (lo <- leonOptions) lo match {
@@ -235,7 +235,7 @@ object Main {
ctx.timers.get("Leon Run") += timer
- ctx.reporter.whenDebug(ReportingTimers) { debug =>
+ ctx.reporter.whenDebug(DebugSectionTimers) { debug =>
debug("-"*80)
debug("Times:")
debug("-"*80)
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index 98d72ed9fcccc4f7d7bdb948c0c1e210830bf429..0f693f1ae22e7911b1a1366b1c558d29b3bc47de 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -37,19 +37,19 @@ abstract class Reporter(settings: Settings) {
private val debugMask = settings.debugSections.foldLeft(0){ _ | _.mask }
- def ifDebug(body: (Any => Unit) => Any)(implicit section: ReportingSection) = {
+ def ifDebug(body: (Any => Unit) => Any)(implicit section: DebugSection) = {
if ((debugMask & section.mask) == section.mask) {
body(debugFunction)
}
}
- def whenDebug(section: ReportingSection)(body: (Any => Unit) => Any) {
+ def whenDebug(section: DebugSection)(body: (Any => Unit) => Any) {
if ((debugMask & section.mask) == section.mask) {
body(debugFunction)
}
}
- def debug(msg: => Any)(implicit section: ReportingSection) = {
+ def debug(msg: => Any)(implicit section: DebugSection) = {
ifDebug{ debug =>
debug(msg)
}(section)
@@ -89,21 +89,21 @@ class DefaultReporter(settings: Settings) extends Reporter(settings) {
}
}
-@implicitNotFound("No implicit debug section found in scope. You need define an implicit ReportingSection to use debug/ifDebug")
-sealed abstract class ReportingSection(val name: String, val mask: Int)
-
-case object ReportingSolver extends ReportingSection("solver", 1 << 0)
-case object ReportingSynthesis extends ReportingSection("synthesis", 1 << 1)
-case object ReportingTimers extends ReportingSection("timers", 1 << 2)
-case object ReportingOptions extends ReportingSection("options", 1 << 3)
-case object ReportingVerification extends ReportingSection("verification", 1 << 4)
-
-object ReportingSections {
- val all = Set[ReportingSection](
- ReportingSolver,
- ReportingSynthesis,
- ReportingTimers,
- ReportingOptions,
- ReportingVerification
+@implicitNotFound("No implicit debug section found in scope. You need define an implicit DebugSection to use debug/ifDebug")
+sealed abstract class DebugSection(val name: String, val mask: Int)
+
+case object DebugSectionSolver extends DebugSection("solver", 1 << 0)
+case object DebugSectionSynthesis extends DebugSection("synthesis", 1 << 1)
+case object DebugSectionTimers extends DebugSection("timers", 1 << 2)
+case object DebugSectionOptions extends DebugSection("options", 1 << 3)
+case object DebugSectionVerification extends DebugSection("verification", 1 << 4)
+
+object DebugSections {
+ val all = Set[DebugSection](
+ DebugSectionSolver,
+ DebugSectionSynthesis,
+ DebugSectionTimers,
+ DebugSectionOptions,
+ DebugSectionVerification
)
}
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index a121d69ca7d1b2913ec7ab3b5a7452354336f408..d280e634421eba6daa56192d8af98629969dd5b6 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -3,13 +3,13 @@
package leon
case class Settings(
- val strictCompilation: Boolean = true, // Terminates Leon in case an error occured during extraction
- val debugSections: Set[ReportingSection] = Set(), // Enables debug message for the following sections
- val termination: Boolean = false,
- val synthesis: Boolean = false,
- val xlang: Boolean = false,
- val verify: Boolean = true,
- val classPath: List[String] = Settings.defaultClassPath()
+ val strictCompilation: Boolean = true, // Terminates Leon in case an error occured during extraction
+ val debugSections: Set[DebugSection] = Set(), // Enables debug message for the following sections
+ val termination: Boolean = false,
+ val synthesis: Boolean = false,
+ val xlang: Boolean = false,
+ val verify: Boolean = true,
+ val classPath: List[String] = Settings.defaultClassPath()
)
object Settings {
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index a4fd36aa6825b1966c482b446df3c06587fb6173..cb257d2369d532836e9b77a25da23432af453ef3 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -17,5 +17,5 @@ trait Solver extends Interruptible {
def getModel: Map[Identifier, Expr]
def getUnsatCore: Set[Expr]
- implicit val debugSection = ReportingSolver
+ implicit val debugSection = DebugSectionSolver
}
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 97e99d7d0051f6acde4a51463aadf88148df3ee1..aa343136abe8927b2077c7b220c164ee4fd5a8f8 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -39,5 +39,5 @@ trait SolverFactory[S <: Solver] extends Interruptible with LeonComponent {
}
}
- implicit val debugSection = ReportingSolver
+ implicit val debugSection = DebugSectionSolver
}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index dc3c2aaff391ef3c299b153989e600020c46caae..619d8926b59abf47bd2ca51a9ee0e91641a59b96 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -85,6 +85,8 @@ abstract class Rule(val name: String) {
def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replace(Map(Variable(what._1) -> what._2), in)
def substAll(what: Map[Identifier, Expr], in: Expr): Expr = replace(what.map(w => Variable(w._1) -> w._2), in)
+ implicit val debugSection = DebugSectionSynthesis
+
val forward: List[Solution] => Option[Solution] = {
case List(s) =>
Some(Solution(s.pre, s.defs, s.term))
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 0ee2b35523c585cb809d66e1f965a5637eee8690..c1c53fc00f9558c64b2aa46d01c9fd455a7fd0e4 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -272,11 +272,6 @@ case object CEGIS extends Rule("CEGIS") {
val simplerRes = simplifyLets(res)
- //println("COMPILATION RESULT: ")
- //println(ScalaPrinter(simplerRes))
- //println("BSS: "+bssOrdered)
- //println("FREE: "+variablesOf(simplerRes))
-
def compileWithArray(): Option[(Seq[Expr], Seq[Expr]) => EvaluationResult] = {
val ba = FreshIdentifier("bssArray").setType(ArrayType(BooleanType))
val bav = Variable(ba)
@@ -285,12 +280,7 @@ case object CEGIS extends Rule("CEGIS") {
}).toMap
val forArray = replace(substMap, simplerRes)
- // println("FORARRAY RESULT: ")
- // println(ScalaPrinter(forArray))
- // println("FREE: "+variablesOf(simplerRes))
-
// We trust arrays to be fast...
- // val simple = evaluator.compile(simplerRes, bssOrdered ++ p.as)
val eval = evaluator.compile(forArray, ba +: p.as)
eval.map{e => { case (bss, ins) =>
@@ -549,11 +539,13 @@ case object CEGIS extends Rule("CEGIS") {
bssAssumptions = closedBs
- //println("UNROLLING: ")
- //for (c <- clauses) {
- // println(" - " + c)
- //}
- //println("CLOSED Bs "+closedBs)
+ sctx.reporter.ifDebug { debug =>
+ debug("UNROLLING: ")
+ for (c <- clauses) {
+ debug(" - " + c)
+ }
+ debug("CLOSED Bs "+closedBs)
+ }
val clause = And(clauses)
@@ -570,8 +562,7 @@ case object CEGIS extends Rule("CEGIS") {
val allPrograms = prunedPrograms.size
- //println("Programs: "+prunedPrograms.size)
- //println("#Tests: "+exampleInputs.size)
+ sctx.reporter.debug("#Programs: "+prunedPrograms.size)
// We further filter the set of working programs to remove those that fail on known examples
if (useCEPruning && hasInputExamples() && ndProgram.canTest()) {
@@ -593,6 +584,8 @@ case object CEGIS extends Rule("CEGIS") {
val nPassing = prunedPrograms.size
+ sctx.reporter.debug("#Programs passing tests: "+nPassing)
+
if (nPassing == 0) {
needMoreUnrolling = true;
} else if (nPassing <= testUpTo) {
@@ -601,7 +594,6 @@ case object CEGIS extends Rule("CEGIS") {
} else if (((nPassing < allPrograms*filterThreshold) || didFilterAlready) && useBssFiltering) {
// We filter the Bss so that the formula we give to z3 is much smalled
val bssToKeep = prunedPrograms.foldLeft(Set[Identifier]())(_ ++ _)
- //println("To Keep: "+bssToKeep.size+"/"+ndProgram.bss.size)
// Cannot unroll normally after having filtered, so we need to
// repeat the filtering procedure at next unrolling.
@@ -618,12 +610,6 @@ case object CEGIS extends Rule("CEGIS") {
solver1.assertCnstr(clause)
solver2.assertCnstr(clause)
-
- //println("Filtered clauses:")
- //for (c <- clauses) {
- // println(" - " + c)
- //}
-
}
val bss = ndProgram.bss
@@ -639,14 +625,6 @@ case object CEGIS extends Rule("CEGIS") {
case BooleanLiteral(false) => Not(Variable(b))
})
- //println("CEGIS OUT!")
- //println("Found solution: "+bssAssumptions)
-
- //bssAssumptions.collect { case Variable(b) => ndProgram.mappings(b) }.foreach {
- // case (c, ex) =>
- // println(". "+c+" = "+ex)
- //}
-
val validateWithZ3 = if (useCETests && hasInputExamples() && ndProgram.canTest()) {
val p = bssAssumptions.collect { case Variable(b) => b }
@@ -666,10 +644,8 @@ case object CEGIS extends Rule("CEGIS") {
}
if (validateWithZ3) {
- //println("Looking for CE...")
solver2.checkAssumptions(bssAssumptions) match {
case Some(true) =>
- //println("#"*80)
val invalidModel = solver2.getModel
val fixedAss = And(ass.collect {
@@ -680,12 +656,9 @@ case object CEGIS extends Rule("CEGIS") {
baseExampleInputs = newCE +: baseExampleInputs
- //println("Found counter example: "+fixedAss)
-
// Retest whether the newly found C-E invalidates all programs
if (useCEPruning && ndProgram.canTest) {
if (prunedPrograms.forall(p => !ndProgram.testForProgram(p)(newCE))) {
- // println("I found a killer example!")
needMoreUnrolling = true
}
}
@@ -744,8 +717,6 @@ case object CEGIS extends Rule("CEGIS") {
case Some(false) =>
- //println("%%%% UNSAT")
-
if (useUninterpretedProbe) {
solver1.check match {
case Some(false) =>
@@ -772,7 +743,6 @@ case object CEGIS extends Rule("CEGIS") {
} catch {
case e: Throwable =>
sctx.reporter.warning("CEGIS crashed: "+e.getMessage)
- e.printStackTrace
RuleApplicationImpossible
}
} finally {
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 1f2ef2143ea84f111ee7c41226f775b3efa84c7a..bdbcc6c304c22513c707d2f457a5eaf3559d3996 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -18,7 +18,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val name = "Analysis"
val description = "Leon Verification"
- implicit val debugSection = ReportingVerification
+ implicit val debugSection = DebugSectionVerification
override val definedOptions : Set[LeonOptionDef] = Set(
LeonValueOptionDef("functions", "--functions=f1:f2", "Limit verification to f1,f2,..."),