From cb0feb3cfd65f669016b1adbd67ef38939d2efdc Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 21 Jul 2015 02:21:58 +0200
Subject: [PATCH] API for telling which solver solved (for portfolio)
---
src/main/scala/leon/solvers/Solver.scala | 1 +
.../scala/leon/solvers/combinators/PortfolioSolver.scala | 8 +++++++-
src/main/scala/leon/verification/AnalysisPhase.scala | 4 ++--
3 files changed, 10 insertions(+), 3 deletions(-)
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index daf7b8499..69eef7449 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -21,6 +21,7 @@ trait Solver {
def check: Option[Boolean]
def getModel: Map[Identifier, Expr]
+ def getResultSolver: Option[Solver] = Some(this)
def free()
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index 5bb6d9471..1f990a0c5 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -23,6 +23,9 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
protected var modelMap = Map[Identifier, Expr]()
protected var solversInsts: Seq[S] = solvers.map(_.getNewSolver())
+ protected var resultSolver: Option[Solver] = None
+
+ override def getResultSolver = resultSolver
def assertCnstr(expression: Expr): Unit = {
solversInsts.foreach(_.assertCnstr(expression))
@@ -54,7 +57,10 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
val res = Await.result(result, 10.days) match {
case Some((s, r, m)) =>
modelMap = m
- context.reporter.debug("Solved with "+s.name)
+ resultSolver = s.getResultSolver
+ resultSolver.foreach { solv =>
+ context.reporter.debug("Solved with "+solv)
+ }
solversInsts.foreach(_.interrupt())
r
case None =>
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 3fbc3671e..e8b3b39f3 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -161,10 +161,10 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
VCResult(status, Some(s), Some(dt))
case Some(false) =>
- VCResult(VCStatus.Valid, Some(s), Some(dt))
+ VCResult(VCStatus.Valid, s.getResultSolver, Some(dt))
case Some(true) =>
- VCResult(VCStatus.Invalid(s.getModel), Some(s), Some(dt))
+ VCResult(VCStatus.Invalid(s.getModel), s.getResultSolver, Some(dt))
}
reporter.synchronized {
--
GitLab