From 379ac744baccc879f57c06383bd8390b3da60249 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 5 Aug 2016 18:16:14 +0200
Subject: [PATCH] PortfolioSolvers
---
.../scala/inox/solvers/SolverResponses.scala | 2 +-
.../solvers/combinators/PortfolioSolver.scala | 66 +++++++++----------
.../combinators/PortfolioSolverFactory.scala | 29 ++++----
3 files changed, 47 insertions(+), 50 deletions(-)
diff --git a/src/main/scala/inox/solvers/SolverResponses.scala b/src/main/scala/inox/solvers/SolverResponses.scala
index 006d2624f..ac4f84418 100644
--- a/src/main/scala/inox/solvers/SolverResponses.scala
+++ b/src/main/scala/inox/solvers/SolverResponses.scala
@@ -72,7 +72,7 @@ object SolverResponses {
}
def cast[M, C](resp: SolverResponse[M,C]): Response[M,C] = ((this, resp) match {
- case (_, Unknown) => Unknown
+ case (_, Unknown) => Unknown
case (Simple | Cores, Sat) => Sat
case (Model | All , s @ SatWithModel(_)) => s
case (Simple | Model, Unsat) => Unsat
diff --git a/src/main/scala/inox/solvers/combinators/PortfolioSolver.scala b/src/main/scala/inox/solvers/combinators/PortfolioSolver.scala
index 1a942fd42..61c8b1605 100644
--- a/src/main/scala/inox/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/inox/solvers/combinators/PortfolioSolver.scala
@@ -1,24 +1,24 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon
+package inox
package solvers
package combinators
-import purescala.Expressions._
-import verification.VC
+import inox.solvers.SolverResponses._
-import utils.Interruptible
import scala.concurrent._
import scala.concurrent.duration._
+import scala.concurrent.ExecutionContext.Implicits.global
-import ExecutionContext.Implicits.global
+trait PortfolioSolver extends Solver { self =>
+ import program._
+ import trees._
-class PortfolioSolver[S <: Solver with Interruptible](val sctx: SolverContext, val solvers: Seq[S])
- extends Solver with NaiveAssumptionSolver {
+ final type SubSolver = Solver { val program: self.program.type }
+ val solvers: Seq[SubSolver]
val name = "Pfolio"
- protected var model = Model.empty
protected var resultSolver: Option[Solver] = None
override def getResultSolver = resultSolver
@@ -27,40 +27,29 @@ class PortfolioSolver[S <: Solver with Interruptible](val sctx: SolverContext, v
solvers.foreach(_.assertCnstr(expression))
}
- override def assertVC(vc: VC): Unit = {
- solvers.foreach(_.assertVC(vc))
- }
-
override def dbg(msg: => Any) = solvers foreach (_.dbg(msg))
- def check: Option[Boolean] = {
- model = Model.empty
+ private def genericCheck(config: Configuration)(f: SubSolver => config.Response[Model, Cores]): config.Response[Model, Cores] = {
reporter.debug("Running portfolio check")
// solving
- val fs = solvers.map { s =>
+ val fs: Seq[Future[(SubSolver, config.Response[Model, Cores])]] = solvers.map { s =>
Future {
try {
- val result = s.check
- val model: Model = if (result == Some(true)) {
- s.getModel
- } else {
- Model.empty
- }
- (s, result, model)
+ val result = f(s)
+ (s, result)
} catch {
case _: StackOverflowError =>
reporter.warning("Stack Overflow while running solver.check()!")
- (s, None, Model.empty)
+ (s, config.cast(Unknown))
}
}
}
- val result = Future.find(fs)(_._2.isDefined)
+ val result = Future.find(fs)(_._2 != Unknown)
val res = Await.result(result, Duration.Inf) match {
- case Some((s, r, m)) =>
- model = m
+ case Some((s, r)) =>
resultSolver = s.getResultSolver
resultSolver.foreach { solv =>
reporter.debug("Solved with "+solv)
@@ -70,13 +59,24 @@ class PortfolioSolver[S <: Solver with Interruptible](val sctx: SolverContext, v
case None =>
reporter.debug("No solver succeeded")
//fs.foreach(f => println(f.value))
- None
+ config.cast(Unknown)
}
- fs foreach { Await.ready(_, Duration.Inf) }
+ // TODO: Decide if we really want to wait for all the solvers.
+ // I understand we interrupt them, but what if one gets stuck
+ // fs foreach { Await.ready(_, Duration.Inf) }
res
}
+
+ def check(config: Configuration): config.Response[Model, Cores] = {
+ genericCheck(config)(subSolver => subSolver.check(config))
+ }
+
+ def checkAssumptions(config: Configuration)(assumptions: Set[Trees]): config.Response[Model, Cores] = {
+ genericCheck(config)(subSolver => subSolver.checkAssumptions(config)(assumptions))
+ }
+
def push(): Unit = {
solvers.foreach(_.push())
}
@@ -86,12 +86,7 @@ class PortfolioSolver[S <: Solver with Interruptible](val sctx: SolverContext, v
}
def free() = {
- solvers.foreach(_.free)
- model = Model.empty
- }
-
- def getModel: Model = {
- model
+ solvers.foreach(_.free())
}
def interrupt(): Unit = {
@@ -103,7 +98,6 @@ class PortfolioSolver[S <: Solver with Interruptible](val sctx: SolverContext, v
}
def reset() = {
- solvers.foreach(_.reset)
- model = Model.empty
+ solvers.foreach(_.reset())
}
}
diff --git a/src/main/scala/inox/solvers/combinators/PortfolioSolverFactory.scala b/src/main/scala/inox/solvers/combinators/PortfolioSolverFactory.scala
index 2c5f8df14..411240eca 100644
--- a/src/main/scala/inox/solvers/combinators/PortfolioSolverFactory.scala
+++ b/src/main/scala/inox/solvers/combinators/PortfolioSolverFactory.scala
@@ -1,26 +1,29 @@
/* Copyright 2009-2016 EPFL, Lausanne */
-package leon
+package inox
package solvers
package combinators
import scala.reflect.runtime.universe._
-class PortfolioSolverFactory[S <: Solver](ctx: SolverContext, sfs: Seq[SolverFactory[S]])
- extends SolverFactory[PortfolioSolver[S] with TimeoutSolver] {
+trait PortfolioSolverFactory extends SolverFactory { self =>
- def getNewSolver(): PortfolioSolver[S] with TimeoutSolver = {
- new PortfolioSolver[S](ctx, sfs.map(_.getNewSolver())) with TimeoutSolver
- }
+ final type PT = program.type
+ override type S = PortfolioSolver { val program: PT }
+ final type SF = SolverFactory { val program: PT }
+
+ val sfs: Seq[SF]
- override def reclaim(s: Solver) = s match {
- case ps: PortfolioSolver[_] =>
- sfs.zip(ps.solvers).foreach { case (sf, s) =>
- sf.reclaim(s)
- }
+ def getNewSolver(): S = {
+ new PortfolioSolver {
+ val program: PT = self.program
+ val solvers = sfs map (_.getNewSolver())
+ val options: SolverOptions = solvers.head.options
+ }
+ }
- case _ =>
- ctx.context.reporter.error("Failed to reclaim a non-portfolio solver.")
+ override def reclaim(s: S) = sfs.zip(s.solvers).foreach { case (sf, s) =>
+ sf.reclaim(s)
}
val name = sfs.map(_.name).mkString("Pfolio(", ",", ")")
--
GitLab