diff --git a/src/main/scala/leon/LeonComponent.scala b/src/main/scala/leon/LeonComponent.scala new file mode 100644 index 0000000000000000000000000000000000000000..95f947b94370f3f60587ecd37157e0183b7d6832 --- /dev/null +++ b/src/main/scala/leon/LeonComponent.scala @@ -0,0 +1,11 @@ +package leon + +/** A common trait for everything that is important enough to be named, + * and that processes command line options. And important category are + * `LeonPhase`s. */ +trait LeonComponent { + val name : String + val description : String + + val definedOptions : Set[LeonOptionDef] = Set() +} diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala index c9c7b25eb2c0bf5ab25709d1a2125872498832ab..466abaf1df1c2d221ab6e1009eecd4c82c3f5df2 100644 --- a/src/main/scala/leon/synthesis/SynthesisPhase.scala +++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala @@ -13,7 +13,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] { val name = "Synthesis" val description = "Synthesis" - override def definedOptions = Set( + override val definedOptions : Set[LeonOptionDef] = Set( LeonFlagOptionDef( "inplace", "--inplace", "Debug level"), LeonFlagOptionDef( "parallel", "--parallel", "Parallel synthesis search"), LeonFlagOptionDef( "derivtrees", "--derivtrees", "Generate derivation trees"), diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala index ce3dc0198e5afbc7d78f29cf691e19bd8178faff..e8bb9791cbe68049296d8cddcbf42039df567988 100644 --- a/src/main/scala/leon/verification/AnalysisPhase.scala +++ b/src/main/scala/leon/verification/AnalysisPhase.scala @@ -16,7 +16,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] { val name = "Analysis" val description = "Leon Verification" - override def definedOptions = Set( + override val definedOptions : Set[LeonOptionDef] = Set( LeonValueOptionDef("functions", "--functions=f1:f2", "Limit verification to f1,f2,...") )