Solvers are LeonComponents.

src/main/scala/leon/solvers/ParallelSolver.scala

@@ -22,8 +22,8 @@ class ParallelSolver(solvers : Solver*) extends Solver(solvers(0).context) with
   private val reporter = context.reporter
 
   val description = "Solver running subsolvers in parallel " + solvers.map(_.description).mkString("(", ", ", ")")
-  override val shortDescription = solvers.map(_.shortDescription).mkString("//")
-  override val superseeds : Seq[String] = solvers.map(_.shortDescription).toSeq
+  override val name = solvers.map(_.name).mkString("//")
+  override val superseeds : Seq[String] = solvers.map(_.name).toSeq
 
   case class Solve(expr: Expr)
   case object Init
@@ -39,10 +39,10 @@ class ParallelSolver(solvers : Solver*) extends Solver(solvers(0).context) with
         while(true) {
           receive {
             case Solve(expr) => {
-              reporter.info("Starting solver " + s.shortDescription)
+              reporter.info("Starting solver " + s.name)
               val res = s.solve(expr)
               that ! Result(res)
-              reporter.info("Ending solver " + s.shortDescription)
+              reporter.info("Ending solver " + s.name)
             }
           }
         }
@@ -54,15 +54,15 @@ class ParallelSolver(solvers : Solver*) extends Solver(solvers(0).context) with
       while(true) {
         receive {
           case Init => {
-            reporter.info("Init solver " + s.shortDescription)
+            reporter.info("Init solver " + s.name)
             s.init 
             coordinator ! Ready
           }
           case Solve(expr) => {
-            reporter.info("Starting solver " + s.shortDescription)
+            reporter.info("Starting solver " + s.name)
             val res = s.solve(expr)
             coordinator ! Result(res)
-            reporter.info("Ending solver " + s.shortDescription)
+            reporter.info("Ending solver " + s.name)
           }
         }
       }
@@ -140,7 +140,7 @@ class ParallelSolver(solvers : Solver*) extends Solver(solvers(0).context) with
 
   class SolverRunner(s: Solver, expr: Expr) extends Actor {
     def act() {
-      reporter.info("Starting solver " + s.shortDescription)
+      reporter.info("Starting solver " + s.name)
       s.solve(expr) match {
         case Some(b) => {
           lock.acquire      
@@ -162,7 +162,7 @@ class ParallelSolver(solvers : Solver*) extends Solver(solvers(0).context) with
       if(nbResponses >= nbSolvers)
         resultNotReady = false
       lock.release
-      reporter.info("Ending solver " + s.shortDescription)
+      reporter.info("Ending solver " + s.name)
     }
   }
   */

src/main/scala/leon/solvers/RandomSolver.scala

@@ -17,8 +17,8 @@ class RandomSolver(context: LeonContext, val nbTrial: Option[Int] = None) extend
 
   private val reporter = context.reporter
 
+  val name = "QC"
   val description = "Solver applying random testing (QuickCheck-like)"
-  override val shortDescription = "QC"
 
   private val random = new Random()
 

src/main/scala/leon/solvers/Solver.scala

@@ -6,11 +6,7 @@ import purescala.Definitions._
 import purescala.TreeOps._
 import purescala.Trees._
 
-abstract class Solver(val context : LeonContext) extends IncrementalSolverBuilder {
-  // This used to be in Extension
-  val description : String
-  val shortDescription : String
-
+abstract class Solver(val context : LeonContext) extends IncrementalSolverBuilder with LeonComponent {
   // This can be used by solvers to "see" the programs from which the
   // formulas come. (e.g. to set up some datastructures for the defined
   // ADTs, etc.) 

src/main/scala/leon/solvers/TrivialSolver.scala

@@ -7,8 +7,8 @@ import purescala.Trees._
 import purescala.TypeTrees._
 
 class TrivialSolver(context: LeonContext) extends Solver(context) with NaiveIncrementalSolver {
+  val name = "trivial"
   val description = "Solver for syntactically trivial formulas"
-  override val shortDescription = "trivial"
 
   def solve(expression: Expr) : Option[Boolean] = expression match {
     case BooleanLiteral(v) => Some(v)

src/main/scala/leon/solvers/z3/FairZ3Solver.scala

@@ -15,23 +15,22 @@ import purescala.TypeTrees._
 import scala.collection.mutable.{Map => MutableMap}
 import scala.collection.mutable.{Set => MutableSet}
 
-class FairZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ3Solver with Z3ModelReconstruction {
-  // have to comment this to use the solver for constraint solving...
-  // assert(Settings.useFairInstantiator)
-
-  private val UNKNOWNASSAT : Boolean = !Settings.noForallAxioms
+class FairZ3Solver(context : LeonContext)
+  extends Solver(context)
+     with AbstractZ3Solver
+     with Z3ModelReconstruction 
+     with LeonComponent {
 
+  val name = "Z3-f"
   val description = "Fair Z3 Solver"
-  override val shortDescription = "Z3-f"
 
   // this is fixed
   protected[leon] val z3cfg = new Z3Config(
     "MODEL" -> true,
     "MBQI" -> false,
-    // "SOFT_TIMEOUT" -> 100,
     "TYPE_CHECK" -> true,
     "WELL_SORTED_CHECK" -> true
-    )
+  )
   toggleWarningMessages(true)
 
   def isKnownDef(funDef: FunDef) : Boolean = functionMap.isDefinedAt(funDef)

src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala

@@ -20,8 +20,8 @@ import purescala.TypeTrees._
  *  Results should come back very quickly.
  */
 class UninterpretedZ3Solver(context : LeonContext) extends Solver(context) with AbstractZ3Solver with Z3ModelReconstruction {
+  val name = "Z3-u"
   val description = "Uninterpreted Z3 Solver"
-  override val shortDescription = "Z3-u"
 
   // this is fixed
   protected[leon] val z3cfg = new Z3Config(

src/main/scala/leon/verification/AnalysisPhase.scala

@@ -89,8 +89,8 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
         // try all solvers until one returns a meaningful answer
         var superseeded : Set[String] = Set.empty[String]
         solvers.find(se => {
-          reporter.info("Trying with solver: " + se.shortDescription)
-          if(superseeded(se.shortDescription) || superseeded(se.description)) {
+          reporter.info("Trying with solver: " + se.name)
+          if(superseeded(se.name) || superseeded(se.description)) {
             reporter.info("Solver was superseeded. Skipping.")
             false
           } else {

src/main/scala/leon/verification/VerificationCondition.scala

@@ -27,7 +27,7 @@ class VerificationCondition(val condition: Expr, val funDef: FunDef, val kind: V
   }
 
   def solverStr = solvedWith match {
-    case Some(s) => s.shortDescription
+    case Some(s) => s.name
     case None => ""
   }