Refactor how command line options are handled by Leon
- Command line option definitions are now represented by a type parametric class. - Components can declare legal option definitions. - Options are parsed according to those definitions in Main, and stored in LeonContext. - Components can then retrieve back the options from LeonContext. This is not perfect, as it requires some type casts. - leon.Settings only contained redundant information and has been removed. - Unused options from SynthesisSettings have been removed.
Showing
- src/main/scala/leon/LeonComponent.scala 1 addition, 1 deletionsrc/main/scala/leon/LeonComponent.scala
- src/main/scala/leon/LeonContext.scala 13 additions, 3 deletionssrc/main/scala/leon/LeonContext.scala
- src/main/scala/leon/LeonOption.scala 85 additions, 54 deletionssrc/main/scala/leon/LeonOption.scala
- src/main/scala/leon/Main.scala 86 additions, 179 deletionssrc/main/scala/leon/Main.scala
- src/main/scala/leon/Pipeline.scala 1 addition, 1 deletionsrc/main/scala/leon/Pipeline.scala
- src/main/scala/leon/Reporter.scala 4 additions, 4 deletionssrc/main/scala/leon/Reporter.scala
- src/main/scala/leon/Settings.scala 0 additions, 17 deletionssrc/main/scala/leon/Settings.scala
- src/main/scala/leon/SharedOptions.scala 57 additions, 0 deletionssrc/main/scala/leon/SharedOptions.scala
- src/main/scala/leon/frontends/scalac/CodeExtraction.scala 3 additions, 3 deletionssrc/main/scala/leon/frontends/scalac/CodeExtraction.scala
- src/main/scala/leon/frontends/scalac/ExtractionPhase.scala 6 additions, 2 deletionssrc/main/scala/leon/frontends/scalac/ExtractionPhase.scala
- src/main/scala/leon/purescala/PrinterOptions.scala 2 additions, 2 deletionssrc/main/scala/leon/purescala/PrinterOptions.scala
- src/main/scala/leon/repair/RepairPhase.scala 2 additions, 15 deletionssrc/main/scala/leon/repair/RepairPhase.scala
- src/main/scala/leon/repair/Repairman.scala 1 addition, 1 deletionsrc/main/scala/leon/repair/Repairman.scala
- src/main/scala/leon/solvers/SolverFactory.scala 10 additions, 5 deletionssrc/main/scala/leon/solvers/SolverFactory.scala
- src/main/scala/leon/solvers/combinators/UnrollingSolver.scala 4 additions, 13 deletions...main/scala/leon/solvers/combinators/UnrollingSolver.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala 12 additions, 7 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
- src/main/scala/leon/solvers/z3/FairZ3Component.scala 10 additions, 7 deletionssrc/main/scala/leon/solvers/z3/FairZ3Component.scala
- src/main/scala/leon/solvers/z3/FairZ3Solver.scala 8 additions, 20 deletionssrc/main/scala/leon/solvers/z3/FairZ3Solver.scala
- src/main/scala/leon/synthesis/Rules.scala 0 additions, 1 deletionsrc/main/scala/leon/synthesis/Rules.scala
- src/main/scala/leon/synthesis/SynthesisContext.scala 0 additions, 1 deletionsrc/main/scala/leon/synthesis/SynthesisContext.scala
Loading
Please register or sign in to comment