From eed0766ddfeecda7ddb5883d3866028e701b6790 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 5 Feb 2016 19:32:26 +0100
Subject: [PATCH] Don't print help message when wrong option
---
src/main/scala/leon/LeonOption.scala | 6 ++++--
src/main/scala/leon/Main.scala | 6 ++++--
src/main/scala/leon/synthesis/rules/CEGIS.scala | 4 ++--
src/main/scala/leon/synthesis/rules/CEGISLike.scala | 1 -
4 files changed, 10 insertions(+), 7 deletions(-)
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index a0a9c9d92..f079399f9 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -25,8 +25,10 @@ abstract class LeonOptionDef[+A] {
try { parser(s) }
catch {
case _ : IllegalArgumentException =>
- reporter.error(s"Invalid option usage: $usageDesc")
- Main.displayHelp(reporter, error = true)
+ reporter.fatalError(
+ s"Invalid option usage: --$name\n" +
+ "Try 'leon --help' for more information."
+ )
}
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index f238d4a85..db49d0425 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -116,8 +116,10 @@ object Main {
}
// Find respective LeonOptionDef, or report an unknown option
val df = allOptions.find(_. name == name).getOrElse{
- initReporter.error(s"Unknown option: $name")
- displayHelp(initReporter, error = true)
+ initReporter.fatalError(
+ s"Unknown option: $name\n" +
+ "Try 'leon --help' for more information."
+ )
}
df.parse(value)(initReporter)
}
diff --git a/src/main/scala/leon/synthesis/rules/CEGIS.scala b/src/main/scala/leon/synthesis/rules/CEGIS.scala
index e8455147a..865d55647 100644
--- a/src/main/scala/leon/synthesis/rules/CEGIS.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGIS.scala
@@ -14,7 +14,7 @@ case object CEGIS extends CEGISLike[TypeTree]("CEGIS") {
grammar = Grammars.typeDepthBound(Grammars.default(sctx, p), 2), // This limits type depth
rootLabel = {(tpe: TypeTree) => tpe },
optimizations = false,
- maxUnfoldings = 7
+ maxUnfoldings = 5
)
}
}
@@ -26,7 +26,7 @@ case object CEGIS2 extends CEGISLike[TaggedNonTerm[TypeTree]]("CEGIS2") {
grammar = TaggedGrammar(base),
rootLabel = TaggedNonTerm(_, Tags.Top, 0, None),
optimizations = true,
- maxUnfoldings = 7
+ maxUnfoldings = 5
)
}
}
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 06a89f323..3f12c9207 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -450,7 +450,6 @@ abstract class CEGISLike[T <: Typed](name: String) extends Rule(name) {
evaluator.eval(eq, p.as.zip(ins).toMap)
}
timers.testForProgram.stop()
- val l = timers.testForProgram.last
cTreeFd.fullBody = origImpl
--
GitLab