From 324beff9bd9a30b154b2969cd4d1ee2c096df6a7 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 21 Apr 2015 15:27:02 +0200
Subject: [PATCH] Fix fullname, improve solver timeouts
---
.../leon/evaluators/RecursiveEvaluator.scala | 2 --
src/main/scala/leon/purescala/Common.scala | 2 +-
src/main/scala/leon/repair/Repairman.scala | 2 +-
src/main/scala/leon/solvers/SolverFactory.scala | 11 +++++++++--
.../leon/solvers/TimeoutSolverFactory.scala | 2 +-
src/main/scala/leon/solvers/package.scala | 16 ++++++++++++++++
src/main/scala/leon/synthesis/Synthesizer.scala | 8 +++++---
.../scala/leon/synthesis/rules/ADTSplit.scala | 2 +-
src/main/scala/leon/synthesis/rules/Ground.scala | 3 ++-
.../scala/leon/synthesis/rules/InlineHoles.scala | 5 +++--
.../scala/leon/verification/AnalysisPhase.scala | 12 +++++++-----
.../verification/VerificationCondition.scala | 4 ++++
.../leon/verification/VerificationReport.scala | 2 +-
13 files changed, 51 insertions(+), 20 deletions(-)
create mode 100644 src/main/scala/leon/solvers/package.scala
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 98b3d0507..1c33acc3b 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 a4deddb59..a9297cb2f 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 929505394..0163d4cee 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 19e2f20ea..b326199b2 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 c3509eb8c..4ec2968b4 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 000000000..e7bb86a63
--- /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 446871711..acce32ff1 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 3bfcaef5e..6215814ed 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 d0e16ce54..49663409f 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 3a904e52a..2ad8a822b 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 2094169ac..865f3b484 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 781c38c75..46e255d9c 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 f20b1280d..0667ed672 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
--
GitLab