diff --git a/src/main/scala/leon/solvers/EnumerationSolver.scala b/src/main/scala/leon/solvers/EnumerationSolver.scala
index 35f1ed907decceb84d138914c253eb467040cb2e..39203125c95d2fff859a5046d21180d7b2b37398 100644
--- a/src/main/scala/leon/solvers/EnumerationSolver.scala
+++ b/src/main/scala/leon/solvers/EnumerationSolver.scala
@@ -14,7 +14,7 @@ import purescala.TypeTrees._
import datagen._
-class EnumerationSolver(val context: LeonContext, val program: Program) extends Solver with Interruptible {
+class EnumerationSolver(val context: LeonContext, val program: Program) extends Solver with Interruptible with IncrementalSolver with NaiveAssumptionSolver {
def name = "Enum"
val maxTried = 10000;
@@ -23,14 +23,25 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends
private var interrupted = false;
- var freeVars = List[Identifier]()
- var constraints = List[Expr]()
+ var freeVars = List[List[Identifier]](Nil)
+ var constraints = List[List[Expr]](Nil)
def assertCnstr(expression: Expr): Unit = {
- constraints = constraints :+ expression
+ constraints = (constraints.head :+ expression) :: constraints.tail
- val newFreeVars = (variablesOf(expression) -- freeVars).toList
- freeVars = freeVars ::: newFreeVars
+ val newFreeVars = (variablesOf(expression) -- freeVars.flatten).toList
+
+ freeVars = (freeVars.head ::: newFreeVars) :: freeVars.tail
+ }
+
+ def push() = {
+ freeVars = Nil :: freeVars
+ constraints = Nil :: constraints
+ }
+
+ def pop(lvl: Int) = {
+ freeVars = freeVars.drop(lvl)
+ constraints = constraints.drop(lvl)
}
private var modelMap = Map[Identifier, Expr]()
@@ -42,12 +53,14 @@ class EnumerationSolver(val context: LeonContext, val program: Program) extends
None
} else {
modelMap = Map()
+ val allFreeVars = freeVars.reverse.flatten
+ val allConstraints = constraints.reverse.flatten
- val it = datagen.get.generateFor(freeVars, And(constraints), 1, maxTried)
+ val it = datagen.get.generateFor(allFreeVars, And(allConstraints), 1, maxTried)
if (it.hasNext) {
val model = it.next
- modelMap = (freeVars zip model).toMap
+ modelMap = (allFreeVars zip model).toMap
Some(true)
} else {
None
diff --git a/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala b/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8f20bb51a30376eb158ebddc41ae170ba43d4e8b
--- /dev/null
+++ b/src/main/scala/leon/solvers/NaiveAssumptionSolver.scala
@@ -0,0 +1,31 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon
+package solvers
+
+import utils._
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Trees._
+import purescala.Extractors._
+import purescala.TreeOps._
+import purescala.TypeTrees._
+
+trait NaiveAssumptionSolver extends AssumptionSolver {
+ self: IncrementalSolver =>
+
+ var lastBs = Set[Expr]()
+ def checkAssumptions(bs: Set[Expr]): Option[Boolean] = {
+ push()
+ lastBs = bs;
+ assertCnstr(And(bs.toSeq))
+ val res = check
+ pop()
+
+ res
+ }
+
+ def getUnsatCore(): Set[Expr] = {
+ lastBs
+ }
+}
diff --git a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
index 4aa880a7006adc972662083dc3387b7ac56e313c..7ddf0abcde8408ab09e61b326fe2e91acf3c4dba 100644
--- a/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/PortfolioSolver.scala
@@ -18,31 +18,32 @@ import scala.collection.mutable.{Map=>MutableMap}
import ExecutionContext.Implicits.global
-class PortfolioSolver(val context: LeonContext, solvers: Seq[SolverFactory[Solver with Interruptible]])
- extends Solver with Interruptible {
+class PortfolioSolver(val context: LeonContext, solvers: Seq[SolverFactory[AssumptionSolver with IncrementalSolver with Interruptible]])
+ extends Solver with IncrementalSolver with Interruptible with NaiveAssumptionSolver {
val name = "Pfolio"
var constraints = List[Expr]()
+ private var modelMap = Map[Identifier, Expr]()
+ private var solversInsts = solvers.map(_.getNewSolver)
+
def assertCnstr(expression: Expr): Unit = {
- constraints ::= expression
+ solversInsts.foreach(_.assertCnstr(expression))
}
- private var modelMap = Map[Identifier, Expr]()
- private var solversInsts = Seq[Solver with Interruptible]()
+ def push(): Unit = {
+ solversInsts.foreach(_.push())
+ }
+
+ def pop(lvl: Int): Unit = {
+ solversInsts.foreach(_.pop(lvl))
+ }
def check: Option[Boolean] = {
modelMap = Map()
- // create fresh solvers
- solversInsts = solvers.map(_.getNewSolver)
-
- // assert
- solversInsts.foreach { s =>
- s.assertCnstr(And(constraints.reverse))
- }
-
+ context.reporter.debug("Running portfolio check")
// solving
val fs = solversInsts.map { s =>
Future {
@@ -65,19 +66,20 @@ class PortfolioSolver(val context: LeonContext, solvers: Seq[SolverFactory[Solve
// Block until all solvers finished
Await.result(Future.fold(fs)(0){ (i, r) => i+1 }, 10.days);
- solversInsts.foreach(_.free)
-
res
}
- def getModel: Map[Identifier, Expr] = {
- modelMap
- }
-
def free() = {
+ solversInsts.foreach(_.free)
+ solversInsts = Nil
+ modelMap = Map()
constraints = Nil
}
+ def getModel: Map[Identifier, Expr] = {
+ modelMap
+ }
+
def interrupt(): Unit = {
solversInsts.foreach(_.interrupt())
}
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index d5d01b73b038d22b682485439988dbed135b52cf..b699c8bc8a3d7bfe09f5193d28d0c77c8449cc53 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -4,6 +4,7 @@ package leon
package synthesis
import solvers._
+import solvers.combinators.PortfolioSolver
import solvers.z3._
import purescala.Trees._
@@ -20,15 +21,29 @@ case class SynthesisContext(
reporter: Reporter
) {
+ val allSolvers: Map[String, SolverFactory[SynthesisContext.SynthesisSolver]] = Map(
+ "fairz3" -> SolverFactory(() => new FairZ3Solver(context, program) with TimeoutAssumptionSolver),
+ "enum" -> SolverFactory(() => new EnumerationSolver(context, program) with TimeoutAssumptionSolver)
+ )
+
+ val solversToUse = allSolvers.filterKeys(options.selectedSolvers)
+
+ val solverFactory: SolverFactory[SynthesisContext.SynthesisSolver] = if (solversToUse.isEmpty) {
+ reporter.fatalError("No solver selected. Aborting")
+ } else if (solversToUse.size == 1) {
+ solversToUse.values.head
+ } else {
+ SolverFactory( () => new PortfolioSolver(context, solversToUse.values.toSeq) with TimeoutAssumptionSolver)
+ }
+
def newSolver: SynthesisContext.SynthesisSolver = {
- new FairZ3Solver(context, program) with TimeoutAssumptionSolver
+ solverFactory.getNewSolver()
}
def newFastSolver: SynthesisContext.SynthesisSolver = {
new UninterpretedZ3Solver(context, program) with TimeoutAssumptionSolver
}
- val solverFactory = SolverFactory(() => newSolver)
val fastSolverFactory = SolverFactory(() => newFastSolver)
}
diff --git a/src/main/scala/leon/synthesis/SynthesisOptions.scala b/src/main/scala/leon/synthesis/SynthesisOptions.scala
index 6287edbdddd7ef0545ab9cc29c86756d509a4b2b..90f0e3c84a39604b970f1af8e1dfaceea8dadb8b 100644
--- a/src/main/scala/leon/synthesis/SynthesisOptions.scala
+++ b/src/main/scala/leon/synthesis/SynthesisOptions.scala
@@ -14,6 +14,7 @@ case class SynthesisOptions(
rules: Seq[Rule] = Rules.all ++ Heuristics.all,
manualSearch: Boolean = false,
searchBound: Option[Int] = None,
+ selectedSolvers: Set[String] = Set("fairz3"),
// Cegis related options
cegisUseUninterpretedProbe: Boolean = false,
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 47fee50c9ff5c34d3e085e84505ffcb9813221b6..d8756d3c8e10993c5a77eb878fa8815befe5706c 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -24,6 +24,7 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
LeonValueOptionDef("timeout", "--timeout=T", "Timeout after T seconds when searching for synthesis solutions .."),
LeonValueOptionDef("costmodel", "--costmodel=cm", "Use a specific cost model for this search"),
LeonValueOptionDef("functions", "--functions=f1:f2", "Limit synthesis of choose found within f1,f2,.."),
+ LeonValueOptionDef("solvers", "--solvers=s1,s2", "Use solvers s1 and s2 (fairz3,enum)", default = Some("fairz3")),
// CEGIS options
LeonFlagOptionDef( "cegis:gencalls", "--cegis:gencalls", "Include function calls in CEGIS generators", true),
LeonFlagOptionDef( "cegis:unintprobe", "--cegis:unintprobe", "Check for UNSAT without bloecks and with uninterpreted functions", false),
@@ -36,6 +37,8 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
def processOptions(ctx: LeonContext): SynthesisOptions = {
var options = SynthesisOptions()
+ val allSolvers = Set("fairz3", "enum")
+
for(opt <- ctx.options) opt match {
case LeonFlagOption("manual", v) =>
options = options.copy(manualSearch = v)
@@ -62,6 +65,13 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
ctx.reporter.fatalError(errorMsg)
}
+ case LeonValueOption("solvers", ListValue(ss)) =>
+ val unknownSolvers = ss.toSet -- allSolvers
+ if (unknownSolvers.nonEmpty) {
+ ctx.reporter.error("Unknown solver(s): "+unknownSolvers.mkString(", ")+" (Available: "+allSolvers.mkString(", ")+")")
+ }
+ options = options.copy(selectedSolvers = Set() ++ ss)
+
case v @ LeonValueOption("timeout", _) =>
v.asInt(ctx).foreach { t =>
options = options.copy(timeoutMs = Some(t.toLong))
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index 9bfcd0383dba38e115fd4fca3706752ffc3a3757..96a1e125016ae8cc2cca320eb00cbc028bafdbf6 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -13,23 +13,26 @@ import purescala.Extractors._
case object Ground extends Rule("Ground") {
def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
if (p.as.isEmpty) {
-
- val solver = SimpleSolverAPI(new TimeoutSolverFactory(sctx.solverFactory, 5000L))
-
- val tpe = TupleType(p.xs.map(_.getType))
-
- val result = solver.solveSAT(p.phi) match {
- case (Some(true), model) =>
- val sol = Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe))
- Some(RuleInstantiation.immediateSuccess(p, this, sol))
- case (Some(false), model) =>
- val sol = Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))
- Some(RuleInstantiation.immediateSuccess(p, this, sol))
- case _ =>
- None
- }
-
- result
+ List(new RuleInstantiation(p, this, SolutionBuilder.none, "Ground") {
+ def apply(sctx: SynthesisContext): RuleApplicationResult = {
+ val solver = SimpleSolverAPI(new TimeoutSolverFactory(sctx.solverFactory, 10000L))
+
+ val tpe = TupleType(p.xs.map(_.getType))
+
+ val result = solver.solveSAT(p.phi) match {
+ case (Some(true), model) =>
+ val sol = Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(model))).setType(tpe))
+ RuleSuccess(sol)
+ case (Some(false), model) =>
+ val sol = Solution(BooleanLiteral(false), Set(), Error(p.phi+" is UNSAT!").setType(tpe))
+ RuleSuccess(sol)
+ case _ =>
+ RuleApplicationImpossible
+ }
+
+ result
+ }
+ })
} else {
None
}