diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 98b3d0507369d4829d34cbebddf834cd367c50f1..1c33acc3bfbf90671df4446a07decb5d0040f744 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -11,8 +11,6 @@ import purescala.Types._
import purescala.Constructors._
import purescala.Extractors._
-import solvers.TimeoutSolver
-
import xlang.Expressions._
import solvers.SolverFactory
import synthesis.ConvertHoles.convertHoles
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index a4deddb594cf6b7e105366a61bbd171677f35a9d..a9297cb2fbaa750f005f9f21c26299e745e859b3 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -62,7 +62,7 @@ object Common {
case Some(ow) => ow.id :: ow.id.ownerChain
}
- def fullName: String = ownerChain.map(_.name).mkString(".")
+ def fullName: String = (ownerChain.map(_.name) :+ name).mkString(".")
}
diff --git a/src/main/scala/leon/repair/Repairman.scala b/src/main/scala/leon/repair/Repairman.scala
index 929505394862bab21ec3fa57c97d2b638d856c35..0163d4ceeec92ff50acaec0c6e3f8930b5b2c349 100644
--- a/src/main/scala/leon/repair/Repairman.scala
+++ b/src/main/scala/leon/repair/Repairman.scala
@@ -370,7 +370,7 @@ class Repairman(ctx: LeonContext, initProgram: Program, fd: FunDef, verifTimeout
private def getVerificationCounterExamples(fd: FunDef, prog: Program): VerificationResult = {
val timeoutMs = verifTimeoutMs.getOrElse(3000L)
- val solver = new TimeoutSolverFactory(SolverFactory.getFromSettings(ctx, prog), timeoutMs)
+ val solver = SolverFactory.getFromSettings(ctx, prog).withTimeout(timeoutMs)
val vctx = VerificationContext(ctx, prog, solver, reporter)
val vcs = AnalysisPhase.generateVCs(vctx, Some(List(fd.id.name)))
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 19e2f20ea74552c5be641898e07bd26e7f672662..b326199b2bd85029dfa27f2b4e19c42582962fcc 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -30,11 +30,16 @@ object SolverFactory {
"enum" -> "Enumeration-based counter-example-finder"
)
- def getFromSettings[S](ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
+ def getFromSettings(ctx: LeonContext, program: Program): SolverFactory[TimeoutSolver] = {
+ getFromName(ctx, program)(ctx.settings.selectedSolvers.toSeq : _*)
+ }
+
+ def getFromName(ctx: LeonContext, program: Program)(names: String*): SolverFactory[TimeoutSolver] = {
import combinators._
import z3._
import smtlib._
+
def getSolver(name: String): SolverFactory[TimeoutSolver] = name match {
case "fairz3" =>
SolverFactory(() => new FairZ3Solver(ctx, program) with TimeoutSolver)
@@ -64,7 +69,9 @@ object SolverFactory {
ctx.reporter.fatalError("Unknown solver "+name)
}
- val selectedSolvers = ctx.settings.selectedSolvers.map(getSolver)
+ val solvers = names.toSeq.toSet
+
+ val selectedSolvers = solvers.map(getSolver)
if (selectedSolvers.isEmpty) {
ctx.reporter.fatalError("No solver selected. Aborting")
diff --git a/src/main/scala/leon/solvers/TimeoutSolverFactory.scala b/src/main/scala/leon/solvers/TimeoutSolverFactory.scala
index c3509eb8ccf8afbd4facf5adb5d9a763eb663bcf..4ec2968b41892604c3b864524ec9000b069ba5eb 100644
--- a/src/main/scala/leon/solvers/TimeoutSolverFactory.scala
+++ b/src/main/scala/leon/solvers/TimeoutSolverFactory.scala
@@ -5,9 +5,9 @@ package solvers
import scala.reflect.runtime.universe._
-
class TimeoutSolverFactory[+S <: TimeoutSolver : TypeTag](sf: SolverFactory[S], to: Long) extends SolverFactory[S] {
override def getNewSolver() = sf.getNewSolver().setTimeout(to)
override val name = "SFact("+typeOf[S].toString+") with t.o"
}
+
diff --git a/src/main/scala/leon/solvers/package.scala b/src/main/scala/leon/solvers/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e7bb86a63a3fb102a2a90051f8ffce6db1b189c1
--- /dev/null
+++ b/src/main/scala/leon/solvers/package.scala
@@ -0,0 +1,16 @@
+package leon
+
+import scala.reflect.runtime.universe._
+import scala.concurrent.duration._
+
+package object solvers {
+ implicit class TimeoutableSolverFactory[+S <: TimeoutSolver : TypeTag](sf: SolverFactory[S]) {
+ def withTimeout(to: Long) = {
+ new TimeoutSolverFactory[S](sf, to)
+ }
+
+ def withTimeout(du: Duration) = {
+ new TimeoutSolverFactory[S](sf, du.toMillis)
+ }
+ }
+}
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 446871711f2de853df6d49654aed7bb3ca7931cd..acce32ff10747b3217b831fc1a04f65614da7545 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -12,6 +12,8 @@ import purescala.ScalaPrinter
import solvers._
import solvers.z3._
+import scala.concurrent.duration._
+
import synthesis.graph._
class Synthesizer(val context : LeonContext,
@@ -56,7 +58,7 @@ class Synthesizer(val context : LeonContext,
case sol if sol.isTrusted =>
(sol, true)
case sol =>
- validateSolution(s, sol, 5000L)
+ validateSolution(s, sol, 5.seconds)
}
(s, if (result.isEmpty) {
@@ -66,7 +68,7 @@ class Synthesizer(val context : LeonContext,
})
}
- def validateSolution(search: Search, sol: Solution, timeoutMs: Long): (Solution, Boolean) = {
+ def validateSolution(search: Search, sol: Solution, timeout: Duration): (Solution, Boolean) = {
import verification.AnalysisPhase._
import verification.VerificationContext
@@ -74,7 +76,7 @@ class Synthesizer(val context : LeonContext,
val (npr, fds) = solutionToProgram(sol)
- val solverf = SolverFactory(() => (new FairZ3Solver(context, npr) with TimeoutSolver).setTimeout(timeoutMs))
+ val solverf = SolverFactory.getFromName(context, npr)("fairz3").withTimeout(timeout)
val vctx = VerificationContext(context, npr, solverf, context.reporter)
val vcs = generateVCs(vctx, Some(fds.map(_.id.name).toSeq))
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 3bfcaef5ee742248a53b9700e6588bece0185cb1..6215814ed33e49e2e573c8cc1d26f49e48c6ebed 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -15,7 +15,7 @@ import solvers._
case object ADTSplit extends Rule("ADT Split.") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
- val solver = SimpleSolverAPI(new TimeoutSolverFactory(hctx.sctx.solverFactory, 200L))
+ val solver = SimpleSolverAPI(hctx.sctx.solverFactory.withTimeout(200L))
val candidates = p.as.collect {
case IsTyped(id, act @ AbstractClassType(cd, tpes)) =>
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index d0e16ce546d5187b0f5b88532afd26b1061b77ee..49663409fab1fb22dc102e35cfcfd3fb0ab5cdb4 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -8,13 +8,14 @@ import solvers._
import purescala.Expressions._
import purescala.ExprOps._
import purescala.Constructors._
+import scala.concurrent.duration._
case object Ground extends Rule("Ground") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
if (p.as.isEmpty) {
List(new RuleInstantiation(this.name) {
def apply(hctx: SearchContext): RuleApplication = {
- val solver = SimpleSolverAPI(new TimeoutSolverFactory(hctx.sctx.solverFactory, 10000L))
+ val solver = SimpleSolverAPI(hctx.sctx.solverFactory.withTimeout(10.seconds))
val result = solver.solveSAT(p.phi) match {
case (Some(true), model) =>
diff --git a/src/main/scala/leon/synthesis/rules/InlineHoles.scala b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
index 3a904e52a577a438df073d8920e129fb78781f39..2ad8a822b566cdff4a33e2efe1550b721b6f2961 100644
--- a/src/main/scala/leon/synthesis/rules/InlineHoles.scala
+++ b/src/main/scala/leon/synthesis/rules/InlineHoles.scala
@@ -5,6 +5,7 @@ package synthesis
package rules
import scala.annotation.tailrec
+import scala.concurrent.duration._
import solvers._
@@ -108,8 +109,8 @@ case object InlineHoles extends Rule("Inline-Holes") {
// Creates two alternative branches:
// 1) a version with holes unreachable, on which this rule won't re-apply
- val sfact = new TimeoutSolverFactory(sctx.solverFactory, 500L)
- val solver = SimpleSolverAPI(new TimeoutSolverFactory(sctx.solverFactory, 2000L))
+ val sfact = sctx.solverFactory.withTimeout(500.millis)
+ val solver = SimpleSolverAPI(sctx.solverFactory.withTimeout(2.seconds))
val(holesAvoidable, _) = solver.solveSAT(and(p.pc, pc))
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 2094169ac418f82c5e0d1562f8f864bdedb9bbc3..865f3b484ccad97f77410974d6937d7b2e60ec14 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -8,6 +8,8 @@ import purescala.Definitions._
import purescala.Expressions._
import purescala.ExprOps._
+import scala.concurrent.duration._
+
import solvers._
object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
@@ -39,16 +41,16 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
}
// Solvers selection and validation
- val entrySolverFactory = SolverFactory.getFromSettings(ctx, program)
+ var baseSolverF = SolverFactory.getFromSettings(ctx, program)
- val mainSolverFactory = timeout match {
+ val solverF = timeout match {
case Some(sec) =>
- new TimeoutSolverFactory(entrySolverFactory, sec*1000L)
+ baseSolverF.withTimeout(sec.seconds)
case None =>
- entrySolverFactory
+ baseSolverF
}
- val vctx = VerificationContext(ctx, program, mainSolverFactory, reporter)
+ val vctx = VerificationContext(ctx, program, solverF, reporter)
reporter.debug("Generating Verification Conditions...")
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 781c38c75766176e2fddf210ac12fd19cbd8ff98..46e255d9caa2c8d5edf84442ef725eb9f70faca9 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -75,6 +75,10 @@ case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option
}
}
+object VCResult {
+ def unknown = VCResult(VCStatus.Unknown, None, None)
+}
+
sealed abstract class VCStatus(val name: String) {
override def toString = name
}
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index f20b1280d2a00b961957a3cf4ad00e0140c968a6..0667ed67271b076df8ee7de496c9a1a038281798 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -12,7 +12,7 @@ case class VerificationReport(val results: Map[VC, Option[VCResult]]) {
import scala.math.Ordering.Implicits._
val vrs: Seq[(VC, VCResult)] = results.toSeq.sortBy { case (vc, _) => (vc.fd.id.name, vc.kind.toString) }.map {
- case (vc, or) => (vc, or.getOrElse(VCResult(Unknown, None, None)))
+ case (vc, or) => (vc, or.getOrElse(VCResult.unknown))
}
lazy val totalConditions : Int = vrs.size