Plop

src/main/scala/leon/purescala/TypeTrees.scala

@@ -87,6 +87,10 @@ object TypeTrees {
     case _ => None
   }
 
+  def isSubtypeOf(t1: TypeTree, t2: TypeTree): Boolean = {
+    leastUpperBound(t1, t2) == Some(t2)
+  }
+
   // returns the number of distinct values that inhabit a type
   sealed abstract class TypeSize extends Serializable
   case class FiniteSize(size: Int) extends TypeSize

src/main/scala/leon/synthesis/Heuristics.scala

@@ -248,16 +248,23 @@ class CEGISOnSteroids(synth: Synthesizer) extends Rule("cegis w. gen.", synth, 5
         g
     }
 
+    def inputAlternatives(t: TypeTree): List[(Expr, Set[Identifier])] = {
+      p.as.filter(a => isSubtypeOf(a.getType, t)).map(id => (Variable(id) : Expr, Set[Identifier]()))
+    }
+
     case class TentativeFormula(f: Expr, recTerms: Map[Identifier, Set[Identifier]]) {
       def unroll: TentativeFormula = {
         var newF = this.f
         var newRecTerms = Map[Identifier, Set[Identifier]]()
         for ((_, recIds) <- recTerms; recId <- recIds) {
           val gen  = getGenerator(recId.getType)
-          val alts = gen.altBuilder().map(alt => FreshIdentifier("b", true) -> alt)
+          val alts = gen.altBuilder() ::: inputAlternatives(recId.getType)
+
+          println("For "+recId.getType+": "+alts)
+          val altsWithBranches = alts.map(alt => FreshIdentifier("b", true).setType(BooleanType) -> alt)
 
-          val pre = Or(alts.map{ case (id, _) => Variable(id) }) // b1 OR b2
-          val cases = for((bid, (ex, rec)) <- alts.toList) yield { // b1 => E(gen1, gen2)     [b1 -> {gen1, gen2}]
+          val pre = Or(altsWithBranches.map{ case (id, _) => Variable(id) }) // b1 OR b2
+          val cases = for((bid, (ex, rec)) <- altsWithBranches.toList) yield { // b1 => E(gen1, gen2)     [b1 -> {gen1, gen2}]
             if (!rec.isEmpty) {
               newRecTerms += bid -> rec
             }
@@ -276,34 +283,37 @@ class CEGISOnSteroids(synth: Synthesizer) extends Rule("cegis w. gen.", synth, 5
     var result: Option[RuleResult]   = None
 
     var ass = p.as.toSet
+    var xss = p.xs.toSet
 
-    var lastF     = TentativeFormula(p.phi, Map() ++ p.xs.map(x => x -> Set(x)))
+    var lastF     = TentativeFormula(And(p.c, p.phi), Map() ++ p.xs.map(x => x -> Set(x)))
     var currentF  = lastF.unroll
     var unrolings = 0
+    val maxUnrolings = 2
     do {
       println("Was: "+lastF.closedFormula)
       println("Now Trying : "+currentF.closedFormula)
 
       val tpe = TupleType(p.xs.map(_.getType))
 
-      var i = 0;
-      var maxTries = 10;
-
       var predicates: Seq[Expr]        = Seq()
+      var continue = true
 
-      while (result.isEmpty && i < maxTries) {
+      while (result.isEmpty && continue) {
         val phi = And(currentF.closedFormula +: predicates)
         synth.solver.solveSAT(phi) match {
           case (Some(true), satModel) =>
-            val notAss = satModel.keySet.filterNot(ass)
-            val satXsModel = satModel.filterKeys(notAss)
+            var bss = satModel.keySet.filterNot(xss ++ ass)
+            println("Found candidate!: "+satModel)
 
-            val newPhi = valuateWithModelIn(phi, notAss, satModel)
+            val newPhi = valuateWithModelIn(phi, bss++xss, satModel)
+            println("new Phi: "+newPhi)
 
             synth.solver.solveSAT(Not(newPhi)) match {
               case (Some(true), invalidModel) =>
                 // Found as such as the xs break, refine predicates
-                predicates = valuateWithModelIn(phi, ass, invalidModel) +: predicates
+                println("Found counter EX: "+invalidModel)
+                predicates = valuateWithModelIn(currentF.closedFormula, ass, invalidModel) +: predicates
+                println(valuateWithModelIn(currentF.closedFormula, ass, invalidModel))
 
               case (Some(false), _) =>
                 result = Some(RuleSuccess(Solution(BooleanLiteral(true), Tuple(p.xs.map(valuateWithModel(satModel))).setType(tpe))))
@@ -312,16 +322,16 @@ class CEGISOnSteroids(synth: Synthesizer) extends Rule("cegis w. gen.", synth, 5
             }
 
           case (Some(false), _) =>
+            continue = false
           case _ =>
+            continue = false
         }
-
-        i += 1 
       }
 
       lastF = currentF
-      currentF = lastF.unroll
+      currentF = currentF.unroll
       unrolings += 1
-    } while(unrolings < 5 && lastF != currentF && result.isEmpty)
+    } while(unrolings < maxUnrolings && lastF != currentF && result.isEmpty)
 
     result.getOrElse(RuleInapplicable)
   }