EnumerationSolver/Portfolio extends Incremental+Assumption

This allows us to use them in synthesis. Expose --solvers=..
option for synthesis.

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

src/main/scala/leon/solvers/NaiveAssumptionSolver.scala

+/* 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
+  }
+}

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())
   }

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)
 
 }

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,

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))

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
     }