diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 4e91b91918b095e5bd83d7d71123e8d42e3c2e6e..2e1e6634f9c1a2e07ad594765c44bee97307c5b2 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -31,15 +31,6 @@ object Main {
//
// LeonFlagOptionDef("uniqid", "--uniqid", "When pretty-printing purescala trees, show identifiers IDs"),
// LeonFlagOptionDef("tolerant", "--tolerant", "Silently extracts non-pure function bodies as ''unknown''"),
- // LeonFlagOptionDef("bapa", "--bapa", "Use BAPA Z3 extension (incompatible with many other things)"),
- // LeonFlagOptionDef("impure", "--impure", "Generate testcases only for impure functions"),
- // LeonValueOptionDef("testcases", "--testcases=[1,2]", "Number of testcases to generate per function"),
- // LeonValueOptionDef("testbounds", "--testbounds=l:u", "Lower and upper bounds for integers in recursive datatypes"),
- // LeonValueOptionDef("timeout", "--timeout=N", "Sets a timeout of N seconds"),
- // LeonFlagOptionDef("BV", "--BV", "Use bit-vectors for integers"),
- // LeonFlagOptionDef("quickcheck", "--quickcheck", "Use QuickCheck-like random search"),
- // LeonFlagOptionDef("parallel", "--parallel", "Run all solvers in parallel"),
- // LeonValueOptionDef("tags", "--tags=t1:...", "Filter out debug information that are not of one of the given tags"),
)
lazy val allOptions = allComponents.flatMap(_.definedOptions) ++ topLevelOptions
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index c630cc32458b20fcc8e146aa3ef71209deb1f50b..9aa0c57ac2371bdaa01df63543a6947312c23a75 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -3,21 +3,9 @@ package leon
// typically these settings can be changed through some command-line switch.
// TODO this global object needs to die (or at least clean out of its var's)
object Settings {
- var showIDs: Boolean = false
lazy val reporter: Reporter = new DefaultReporter
- var useBAPA: Boolean = false
- var impureTestcases: Boolean = false
- var nbTestcases: Int = 1
- var testBounds: (Int, Int) = (0, 3)
- var solverTimeout : Option[Int] = None
- var useQuickCheck : Boolean = false
- var useParallel : Boolean = false
- var debugLevel: Int = 0
- var synthesis: Boolean = false
- var transformProgram: Boolean = true
- var stopAfterExtraction: Boolean = false
- var stopAfterTransformation: Boolean = false
- var stopAfterAnalysis: Boolean = true
+
+ var showIDs: Boolean = false
var silentlyTolerateNonPureBodies: Boolean = false
}
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index 670c41c83b9ec8cbe5ba48117d75594d3d325ad0..0eebd19c99d5e6749970eb501e6b492b70886ee5 100644
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -16,20 +16,7 @@ class LeonPlugin(val global: PluginRunner) extends Plugin {
/** The help message displaying the options for that plugin. */
override val optionsHelp: Option[String] = Some(
" --uniqid When pretty-printing purescala trees, show identifiers IDs" + "\n" +
- " --with-code Allows the compiler to keep running after the static analysis" + "\n" +
- " --parse Checks only whether the program is valid PureScala" + "\n" +
- " --axioms Generate simple forall axioms for recursive functions when possible" + "\n" +
- " --tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n" +
- " --bapa Use BAPA Z3 extension (incompatible with many other things)" + "\n" +
- " --impure Generate testcases only for impure functions" + "\n" +
- " --testcases=[1,2] Number of testcases to generate per function" + "\n" +
- " --testbounds=l:u Lower and upper bounds for integers in recursive datatypes" + "\n" +
- " --timeout=N Sets a timeout of N seconds" + "\n" +
- " --quickcheck Use QuickCheck-like random search" + "\n" +
- " --parallel Run all solvers in parallel" + "\n" +
- " --debug=[1-5] Debug level" + "\n" +
- " --imperative Preprocessing and transformation from imperative programs" + "\n" +
- " --synthesis Magic!"
+ " --tolerant Silently extracts non-pure function bodies as ''unknown''" + "\n"
)
/** Processes the command-line options. */
@@ -37,24 +24,9 @@ class LeonPlugin(val global: PluginRunner) extends Plugin {
override def processOptions(options: List[String], error: String => Unit) {
for(option <- options) {
option match {
- case "with-code" => leon.Settings.stopAfterAnalysis = false
case "uniqid" => leon.Settings.showIDs = true
- case "parse" => leon.Settings.stopAfterExtraction = true
case "tolerant" => leon.Settings.silentlyTolerateNonPureBodies = true
- case "bapa" => leon.Settings.useBAPA = true
- case "impure" => leon.Settings.impureTestcases = true
- case "quickcheck" => leon.Settings.useQuickCheck = true
- case "parallel" => leon.Settings.useParallel = true
- case "imperative" => leon.Settings.synthesis = false;
- leon.Settings.transformProgram = true;
- case "synthesis" => leon.Settings.synthesis = true;
- leon.Settings.transformProgram = false;
- leon.Settings.stopAfterTransformation = true;
- case s if s.startsWith("debug=") => leon.Settings.debugLevel = try { s.substring("debug=".length, s.length).toInt } catch { case _ => 0 }
- case s if s.startsWith("testbounds=") => leon.Settings.testBounds = try { val l = splitList(s.substring("testBounds=".length, s.length)).map(_.toInt); if (l.size != 2) (0, 3) else (l(0), l(1)) } catch { case _ => (0, 3) }
- case s if s.startsWith("timeout=") => leon.Settings.solverTimeout = try { Some(s.substring("timeout=".length, s.length).toInt) } catch { case _ => None }
- case s if s.startsWith("testcases=") => leon.Settings.nbTestcases = try { s.substring("testcases=".length, s.length).toInt } catch { case _ => 1 }
case _ => error("Invalid option: " + option + "\nValid options are:\n" + optionsHelp.get)
}
}