From d5536f7cd6d0cc2cea295503397e45ee8d748e0a Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 3 Jun 2015 17:00:03 +0200
Subject: [PATCH] Choose GroupedTactic even if subsolver of Portfolio needs it
---
.../solvers/combinators/PortfolioSolver.scala | 2 +-
.../leon/verification/AnalysisPhase.scala | 18 +++++++++++++-----
2 files changed, 14 insertions(+), 6 deletions(-)
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index 3c9938571..6cc38396d 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -14,7 +14,7 @@ import scala.concurrent.duration._
import ExecutionContext.Implicits.global
-class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext, solvers: Seq[SolverFactory[S]])
+class PortfolioSolver[S <: Solver with Interruptible](val context: LeonContext, val solvers: Seq[SolverFactory[S]])
extends Solver with Interruptible {
val name = "Pfolio"
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index dbaa76433..01bfc5ec2 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -9,6 +9,7 @@ import purescala.ExprOps._
import scala.concurrent.duration._
import solvers._
+import solvers.combinators.PortfolioSolver
import solvers.smtlib.SMTLIBCVC4QuantifiedSolver
object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
@@ -33,10 +34,17 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
baseSolverF
}
- val isSMTQuantified = {
- val solver = baseSolverF.getNewSolver
- val res = solver.isInstanceOf[SMTLIBCVC4QuantifiedSolver]
- solver.free
+ def isSMTQuantified[S <: Solver](sf: SolverFactory[S]): Boolean = {
+ val solver: S = sf.getNewSolver()
+ val res = solver match {
+ case _ : SMTLIBCVC4QuantifiedSolver =>
+ true
+ case ps: PortfolioSolver[_] =>
+ ps.solvers exists isSMTQuantified
+ case _ =>
+ false
+ }
+ solver.free()
res
}
@@ -45,7 +53,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
reporter.debug("Generating Verification Conditions...")
try {
- val vcs = generateVCs(vctx, filterFuns, forceGrouped = isSMTQuantified)
+ val vcs = generateVCs(vctx, filterFuns, forceGrouped = isSMTQuantified(baseSolverF))
reporter.debug("Checking Verification Conditions...")
--
GitLab