From d395bae9434e6c7a650a5ec1f1d3882119cc35b1 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 23 Jun 2015 16:51:58 +0200
Subject: [PATCH] Simlify check/getModel in ProofSolver
In case of PortfolioSolver, the Exception should be handled correctly
through Future magic
---
.../solvers/combinators/PortfolioSolver.scala | 4 +---
.../solvers/smtlib/SMTLIBCVC4ProofSolver.scala | 18 ++----------------
.../leon/verification/AnalysisPhase.scala | 2 --
3 files changed, 3 insertions(+), 21 deletions(-)
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index 6cc38396d..5bb6d9471 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -61,9 +61,7 @@ class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext,
None
}
- // Block until all solvers finished
- Await.result(Future.fold(fs)(0){ (i, r) => i+1 }, 10.days)
-
+ fs map { Await.ready(_, 10.days) }
res
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index e02c0dfc9..3684d61bf 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -37,22 +37,8 @@ class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTL
// This solver does not support model extraction
override def getModel: Map[Identifier, Expr] = {
- reporter.warning(s"Solver $name does not support model extraction.")
- Map()
- }
-
- // FIXME: mk: This is kind of hiding the problem under the carpet.
- // We could just return an empty counterexample, but this breaks PortfolioSolver
- override def check: Option[Boolean] = {
- super.check match {
- case Some(true) =>
- reporter.warning(s"Solver $name found a counterexample, " +
- "but masking it as unknown because counterexamples are not supported."
- )
- None
- case other =>
- other
- }
+ // We don't send the error through reporter because it may be caught by PortfolioSolver
+ throw LeonFatalError(Some(s"Solver $name does not support model extraction."))
}
protected val allowQuantifiedAssersions: Boolean = true
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 2975fef19..92ae2308d 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -9,8 +9,6 @@ import purescala.ExprOps._
import scala.concurrent.duration._
import solvers._
-import solvers.combinators.PortfolioSolver
-import solvers.smtlib.SMTLIBCVC4QuantifiedSolver
object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
val name = "Analysis"
--
GitLab