Better names for SolverFactory and fixed bug in quantifiers

src/main/scala/leon/invariant/templateSolvers/CegisSolver.scala

@@ -155,7 +155,7 @@ class CegisCore(ctx: InferenceContext,
             }
             val t3 = System.currentTimeMillis()
             val elapsedTime = (t3 - startTime)
-            val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => new ExtendedUFSolver(context, program) with TimeoutSolver),
+            val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory("extededUF", () => new ExtendedUFSolver(context, program) with TimeoutSolver),
               timeoutMillis - elapsedTime))
             val (res1, newModel) = if (solveAsInt) {
               val intctr = And(newctr, initRealCtr)
@@ -214,7 +214,7 @@ class CegisCore(ctx: InferenceContext,
   val debugMinimization = false
 
   def minimizeReals(inputCtr: Expr, objective: Expr): (Option[Boolean], Model) = {
-    val sol = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
+    val sol = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory("extendedUF", () => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
     val (res, model1) = sol.solveSAT(inputCtr)
     res match {
       case Some(true) => {
@@ -253,7 +253,7 @@ class CegisCore(ctx: InferenceContext,
 
               }
               val boundCtr = LessEquals(objective, currval)
-              val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
+              val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory("extendedUF", () => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
               val (res, newModel) = sol.solveSAT(And(inputCtr, boundCtr))
               res match {
                 case Some(true) => {
@@ -296,7 +296,7 @@ class CegisCore(ctx: InferenceContext,
   }
 
   def minimizeIntegers(inputCtr: Expr, objective: Expr): (Option[Boolean], Model) = {
-    val sol = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
+    val sol = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory("extendedUF", () => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
     val (res, model1) = sol.solveSAT(inputCtr)
     res match {
       case Some(true) => {
@@ -328,7 +328,7 @@ class CegisCore(ctx: InferenceContext,
               } else 2 * upperBound
             }
             val boundCtr = LessEquals(objective, InfiniteIntegerLiteral(currval))
-            val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
+            val solver2 = SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory("extededUF", () => new ExtendedUFSolver(context, program) with TimeoutSolver), timeoutMillis))
             val (res, newModel) = sol.solveSAT(And(inputCtr, boundCtr))
             res match {
               case Some(true) => {
@@ -367,4 +367,4 @@ class CegisCore(ctx: InferenceContext,
     }
   }
 
-}
+}

src/main/scala/leon/invariant/templateSolvers/FarkasLemmaSolver.scala

@@ -273,8 +273,9 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
       //new ExtendedUFSolver(leonctx, program, useBitvectors = true, bitvecSize = bvsize) with TimeoutSolver
     } else {
       //new AbortableSolver(() => new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver, ctx)
-      SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() =>
-        new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver), timeout * 1000))
+      SimpleSolverAPI(new TimeoutSolverFactory(
+        SolverFactory.getFromName(leonctx, program)("smt-z3-u"),
+        timeout * 1000))
     }
     if (verbose) reporter.info("solving...")
     val (res, model) =
@@ -324,4 +325,4 @@ class FarkasLemmaSolver(ctx: InferenceContext, program: Program) {
         (res, model)
     }
   }
-}
+}

src/main/scala/leon/invariant/templateSolvers/UniversalQuantificationSolver.scala

@@ -63,8 +63,9 @@ class UniversalQuantificationSolver(ctx: InferenceContext, program: Program,
     if (usePortfolio) {
       if (useIncrementalSolvingForVCs)
         throw new IllegalArgumentException("Cannot perform incremental solving with portfolio solvers!")
-      SolverFactory(() => new PortfolioSolver(leonctx, Seq(new SMTLIBCVC4Solver(leonctx, program),
-        new SMTLIBZ3Solver(leonctx, program))) with TimeoutSolver)
+      new PortfolioSolverFactory(leonctx, Seq(
+        SolverFactory.getFromName(leonctx, program)("smt-cvc4-u"),
+        SolverFactory.getFromName(leonctx, program)("smt-z3-u")))
     } else
       SolverFactory.uninterpreted(leonctx, program)
 
@@ -360,7 +361,7 @@ class UniversalQuantificationSolver(ctx: InferenceContext, program: Program,
             solver.pop()
           solRes
         } else
-          SimpleSolverAPI(SolverFactory(() => solver)).solveSAT(instExpr)
+          SimpleSolverAPI(SolverFactory(solver.name, () => solver)).solveSAT(instExpr)
       } { vccTime =>
         if (verbose) reporter.info("checked VC inst... in " + vccTime / 1000.0 + "s")
         updateCounterTime(vccTime, "VC-check-time", "disjuncts")
@@ -370,7 +371,7 @@ class UniversalQuantificationSolver(ctx: InferenceContext, program: Program,
       /*ctrTracker.getVC(fd).checkUnflattening(tempVarMap,
         SimpleSolverAPI(SolverFactory(() => solverFactory.getNewSolver())),
         defaultEval)*/
-      verifyModel(funData.simpleParts, packedModel, SimpleSolverAPI(SolverFactory(() => solverFactory.getNewSolver())))
+      verifyModel(funData.simpleParts, packedModel, SimpleSolverAPI(solverFactory))
       //val unflatPath = ctrTracker.getVC(fd).pickSatFromUnflatFormula(funData.simpleParts, packedModel, defaultEval)
     }
     //for statistics
@@ -379,7 +380,7 @@ class UniversalQuantificationSolver(ctx: InferenceContext, program: Program,
         unflatten(simplifyArithmetic(instantiateTemplate(ctrTracker.getVC(fd).eliminateBlockers, tempVarMap)))
       Stats.updateCounterStats(atomNum(compressedVC), "Compressed-VC-size", "disjuncts")
       time {
-        SimpleSolverAPI(SolverFactory(() => solverFactory.getNewSolver())).solveSAT(compressedVC)
+        SimpleSolverAPI(solverFactory).solveSAT(compressedVC)
       } { compTime =>
         Stats.updateCumTime(compTime, "TotalCompressVCCTime")
         reporter.info("checked compressed VC... in " + compTime / 1000.0 + "s")

src/main/scala/leon/invariant/util/Minimizer.scala

@@ -54,8 +54,9 @@ class Minimizer(ctx: InferenceContext, program: Program) {
    */
   def minimizeBounds(nestMap: Map[Variable, Int])(inputCtr: Expr, initModel: Model): Model = {
     val orderedTempVars = nestMap.toSeq.sortWith((a, b) => a._2 >= b._2).map(_._1)
-    lazy val solver = new SimpleSolverAPI(new TimeoutSolverFactory(SolverFactory(() =>
-      new SMTLIBZ3Solver(leonctx, program) with TimeoutSolver), ctx.vcTimeout * 1000))
+    lazy val solver = new SimpleSolverAPI(new TimeoutSolverFactory(
+      SolverFactory.getFromName(leonctx,program)("smt-z3-u"),
+      ctx.vcTimeout * 1000))
 
     reporter.info("minimizing...")
     var currentModel = initModel
@@ -189,4 +190,4 @@ class Minimizer(ctx: InferenceContext, program: Program) {
     functionNesting(template)
     nestMap
   }
-}
+}

src/main/scala/leon/invariant/util/SolverUtil.scala

@@ -72,7 +72,7 @@ object SolverUtil {
     if (idmap.keys.nonEmpty) {
       val newpathcond = replace(idmap, expr)
       //check if this is solvable
-      val solver = SimpleSolverAPI(SolverFactory(() => new ExtendedUFSolver(ctx, prog)))
+      val solver = SimpleSolverAPI(SolverFactory("extendedUF", () => new ExtendedUFSolver(ctx, prog)))
       solver.solveSAT(newpathcond)._1 match {
         case Some(true) => {
           println("Path satisfiable for a?,c? -->6,2 ")
@@ -143,4 +143,4 @@ object SolverUtil {
     }
   }
 
-}
+}

src/main/scala/leon/solvers/SolverFactory.scala

@@ -13,7 +13,7 @@ import purescala.Definitions._
 import scala.reflect.runtime.universe._
 import _root_.smtlib.interpreters._
 
-abstract class SolverFactory[+S <: Solver : TypeTag] {
+abstract class SolverFactory[+S <: Solver] {
   def getNewSolver(): S
 
   def shutdown(): Unit = {}
@@ -22,12 +22,13 @@ abstract class SolverFactory[+S <: Solver : TypeTag] {
     s.free()
   }
 
-  val name = typeOf[S].toString.split("\\.").last.replaceAll("Solver", "")+"*"
+  val name: String
 }
 
 object SolverFactory {
-  def apply[S <: Solver : TypeTag](builder: () => S): SolverFactory[S] = {
+  def apply[S <: Solver : TypeTag](nme: String, builder: () => S): SolverFactory[S] = {
     new SolverFactory[S] {
+      val name = nme
       def getNewSolver() = builder()
     }
   }
@@ -80,36 +81,19 @@ object SolverFactory {
   }
 
   def getFromName(ctx: LeonContext, program: Program)(name: String): SolverFactory[TimeoutSolver] = name match {
-    case "fairz3" =>
-      SolverFactory(() => new FairZ3Solver(ctx, program) with TimeoutSolver)
-
-    case "unrollz3" =>
-      SolverFactory(() => new Z3UnrollingSolver(ctx, program, new UninterpretedZ3Solver(ctx, program)) with TimeoutSolver)
-
-    case "enum"   =>
-      SolverFactory(() => new EnumerationSolver(ctx, program) with TimeoutSolver)
-
-    case "ground" =>
-      SolverFactory(() => new GroundSolver(ctx, program) with TimeoutSolver)
-
-    case "smt-z3" =>
-      SolverFactory(() => new Z3UnrollingSolver(ctx, program, new SMTLIBZ3Solver(ctx, program)) with TimeoutSolver)
-
-    case "smt-z3-q" =>
-      SolverFactory(() => new SMTLIBZ3QuantifiedSolver(ctx, program) with TimeoutSolver)
-
-    case "smt-cvc4" =>
-      SolverFactory(() => new CVC4UnrollingSolver(ctx, program, new SMTLIBCVC4Solver(ctx, program)) with TimeoutSolver)
-
-    case "smt-cvc4-proof" =>
-      SolverFactory(() => new SMTLIBCVC4ProofSolver(ctx, program) with TimeoutSolver)
-
-    case "smt-cvc4-cex" =>
-      SolverFactory(() => new SMTLIBCVC4CounterExampleSolver(ctx, program) with TimeoutSolver)
-
-    case "isabelle" =>
-      new isabelle.IsabelleSolverFactory(ctx, program)
-
+    case "enum"           => SolverFactory(name, () => new EnumerationSolver(ctx, program) with TimeoutSolver)
+    case "ground"         => SolverFactory(name, () => new GroundSolver(ctx, program) with TimeoutSolver)
+    case "fairz3"         => SolverFactory(name, () => new FairZ3Solver(ctx, program) with TimeoutSolver)
+    case "unrollz3"       => SolverFactory(name, () => new Z3UnrollingSolver(ctx, program, new UninterpretedZ3Solver(ctx, program)) with TimeoutSolver)
+    case "smt-z3"         => SolverFactory(name, () => new Z3UnrollingSolver(ctx, program, new SMTLIBZ3Solver(ctx, program)) with TimeoutSolver)
+    case "smt-z3-q"       => SolverFactory(name, () => new SMTLIBZ3QuantifiedSolver(ctx, program) with TimeoutSolver)
+    case "smt-cvc4"       => SolverFactory(name, () => new CVC4UnrollingSolver(ctx, program, new SMTLIBCVC4Solver(ctx, program)) with TimeoutSolver)
+    case "smt-cvc4-proof" => SolverFactory(name, () => new SMTLIBCVC4ProofSolver(ctx, program) with TimeoutSolver)
+    case "smt-cvc4-cex"   => SolverFactory(name, () => new SMTLIBCVC4CounterExampleSolver(ctx, program) with TimeoutSolver)
+    case "smt-z3-u"       => SolverFactory(name, () => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
+    case "smt-cvc4-u"     => SolverFactory(name, () => new SMTLIBCVC4Solver(ctx, program) with TimeoutSolver)
+    case "nativez3-u"     => SolverFactory(name, () => new UninterpretedZ3Solver(ctx, program) with TimeoutSolver)
+    case "isabelle"       => new isabelle.IsabelleSolverFactory(ctx, program)
     case _ =>
       ctx.reporter.error(s"Unknown solver $name")
       showSolvers(ctx)
@@ -137,29 +121,30 @@ object SolverFactory {
   // Fast solver used by simplifications, to discharge simple tautologies
   def uninterpreted(ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
     val names = ctx.findOptionOrDefault(GlobalOptions.optSelectedSolvers)
-
+    val fromName = getFromName(ctx, program) _
+
     if ((names contains "fairz3") && !hasNativeZ3) {
       if (hasZ3) {
         if (!reported) {
           ctx.reporter.warning("The Z3 native interface is not available, falling back to smt-z3.")
           reported = true
         }
-        SolverFactory(() => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
+        fromName("smt-z3-u")
       } else if (hasCVC4) {
         if (!reported) {
           ctx.reporter.warning("The Z3 native interface is not available, falling back to smt-cvc4.")
           reported = true
         }
-        SolverFactory(() => new SMTLIBCVC4Solver(ctx, program) with TimeoutSolver)
+        fromName("smt-cvc4-u")
       } else {
         ctx.reporter.fatalError("No SMT solver available: native Z3 api could not load and 'cvc4' or 'z3' binaries were not found in PATH.")
       }
     } else if(names contains "smt-cvc4") {
-      SolverFactory(() => new SMTLIBCVC4Solver(ctx, program) with TimeoutSolver)
+      fromName("smt-cvc4-u")
     } else if(names contains "smt-z3") {
-      SolverFactory(() => new SMTLIBZ3Solver(ctx, program) with TimeoutSolver)
+      fromName("smt-z3-u")
     } else if ((names contains "fairz3") && hasNativeZ3) {
-      SolverFactory(() => new UninterpretedZ3Solver(ctx, program) with TimeoutSolver)
+      fromName("nativez3-u")
     } else {
       ctx.reporter.fatalError("No SMT solver available: native Z3 api could not load and 'cvc4' or 'z3' binaries were not found in PATH.")
     }

src/main/scala/leon/solvers/combinators/PortfolioSolverFactory.scala

@@ -6,7 +6,7 @@ package combinators
 
 import scala.reflect.runtime.universe._
 
-class PortfolioSolverFactory[S <: Solver](ctx: LeonContext, sfs: Seq[SolverFactory[S]])(implicit tag: TypeTag[S]) extends SolverFactory[PortfolioSolver[S] with TimeoutSolver] {
+class PortfolioSolverFactory[S <: Solver](ctx: LeonContext, sfs: Seq[SolverFactory[S]]) extends SolverFactory[PortfolioSolver[S] with TimeoutSolver] {
 
   def getNewSolver(): PortfolioSolver[S] with TimeoutSolver = {
     new PortfolioSolver[S](ctx, sfs.map(_.getNewSolver())) with TimeoutSolver
@@ -21,5 +21,7 @@ class PortfolioSolverFactory[S <: Solver](ctx: LeonContext, sfs: Seq[SolverFacto
     case _ =>
       ctx.reporter.error("Failed to reclaim a non-portfolio solver.")
   }
+
+  val name = sfs.map(_.name).mkString("Pfolio(", ",", ")")
 }
 

src/main/scala/leon/solvers/combinators/SolverPool.scala

@@ -17,7 +17,9 @@ import scala.reflect.runtime.universe._
  * growing/shrinking pool size...
  */
 
-class SolverPoolFactory[+S <: Solver](ctx: LeonContext, sf: SolverFactory[S])(implicit tag: TypeTag[S]) extends SolverFactory[S] {
+class SolverPoolFactory[+S <: Solver](ctx: LeonContext, sf: SolverFactory[S]) extends SolverFactory[S] {
+
+  val name = "Pool(" + sf.name + ")"
 
   var poolSize    = 0
   val poolMaxSize = 5

src/main/scala/leon/solvers/isabelle/IsabelleSolverFactory.scala

@@ -12,6 +12,8 @@ import leon.solvers._
 
 final class IsabelleSolverFactory(context: LeonContext, program: Program) extends SolverFactory[TimeoutSolver] {
 
+  val name = "isabelle"
+
   private val env = IsabelleEnvironment(context, program)
 
   override def shutdown() =

src/main/scala/leon/solvers/unrolling/QuantificationManager.scala

@@ -446,7 +446,7 @@ class QuantificationManager[T](encoder: TemplateEncoder[T]) extends LambdaManage
         (qarg, arg) <- (qargs zip args)
         _ = strictnessCnstr(qarg, arg)
       } qarg match {
-        case Left(quant) if subst.isDefinedAt(quant) =>
+        case Left(quant) if !quantified(quant) || subst.isDefinedAt(quant) =>
           eqConstraints += (quant -> arg.encoded)
         case Left(quant) if quantified(quant) =>
           subst += quant -> arg

src/test/scala/leon/integration/purescala/SimplifyPathsSuite.scala

@@ -25,7 +25,7 @@ class SimplifyPathsSuite extends LeonTestSuite {
   val l2 = InfiniteIntegerLiteral(2)
 
   def simplifyPaths(ctx: LeonContext, expr: Expr): Expr = {
-    val uninterpretedZ3 = SolverFactory(() => new UninterpretedZ3Solver(ctx, Program.empty))
+    val uninterpretedZ3 = SolverFactory.getFromName(ctx, Program.empty)("nativez3-u")
     try {
       ExprOps.simplifyPaths(uninterpretedZ3)(expr)
     } finally {

src/test/scala/leon/integration/solvers/TimeoutSolverSuite.scala

@@ -45,7 +45,7 @@ class TimeoutSolverSuite extends LeonTestSuite {
   }
 
   private def getTOSolver(ctx: LeonContext): SolverFactory[Solver] = {
-    SolverFactory(() => (new IdioticSolver(ctx, Program.empty) with TimeoutSolver).setTimeout(200L))
+    SolverFactory("idiotic", () => (new IdioticSolver(ctx, Program.empty) with TimeoutSolver).setTimeout(200L))
   }
 
   private def check(sf: SolverFactory[Solver], e: Expr): Option[Boolean] = {

src/test/scala/leon/unit/solvers/SolverPoolSuite.scala

@@ -28,7 +28,7 @@ class SolverPoolSuite extends LeonTestSuite {
   }
 
   def sfactory(implicit ctx: LeonContext): SolverFactory[Solver] = {
-    SolverFactory(() => new DummySolver(ctx, Program.empty))
+    SolverFactory("dummy", () => new DummySolver(ctx, Program.empty))
   }
 
   val poolSize = 5;