ADTDual

src/main/scala/leon/purescala/Definitions.scala

@@ -246,6 +246,8 @@ object Definitions {
       fields.map(f => f.id).toSet
     }
 
+    def fieldsIds = fields.map(_.id)
+
     def selectorID2Index(id: Identifier) : Int = {
       var i : Int = 0
       var found = false

src/main/scala/leon/synthesis/Rules.scala

@@ -9,6 +9,7 @@ object Rules {
   def all(synth: Synthesizer) = List(
     new Unification.DecompTrivialClash(synth),
     new Unification.OccursCheck(synth),
+    new ADTDual(synth),
     new OnePoint(synth),
     new Ground(synth),
     new CaseSplit(synth),
@@ -243,3 +244,38 @@ object Unification {
     }
   }
 }
+
+
+class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth) {
+  def isApplicable(task: Task): List[DecomposedTask] = {
+    val p = task.problem
+
+    val xs = p.xs.toSet
+    val as = p.as.toSet
+
+    val TopLevelAnds(exprs) = p.phi
+
+
+    val (toRemove, toAdd, toPre) = exprs.collect {
+      case eq @ Equals(cc @ CaseClass(cd, args), e) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) -- xs).isEmpty =>
+        (eq, (cd.fieldsIds zip args).map{ case (id, ex) => Equals(ex, CaseClassSelector(cd, e, id)) }, CaseClassInstanceOf(cd, e) )
+      case eq @ Equals(e, cc @ CaseClass(cd, args)) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) -- xs).isEmpty =>
+        (eq, (cd.fieldsIds zip args).map{ case (id, ex) => Equals(ex, CaseClassSelector(cd, e, id)) }, CaseClassInstanceOf(cd, e) )
+    }.unzip3
+
+    if (!toRemove.isEmpty) {
+      val sub = p.copy(phi = And((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
+
+      val onSuccess: List[Solution] => Solution = { 
+        case List(s) => 
+          Solution(And(s.pre +: toPre), s.term)
+        case _ =>
+          Solution.none
+      }
+
+      List(task.decompose(this, List(sub), onSuccess, 80))
+    } else {
+      Nil
+    }
+  }
+}

src/main/scala/leon/synthesis/Synthesizer.scala

@@ -64,11 +64,11 @@ class Synthesizer(val r: Reporter, val solvers: List[Solver]) {
   }
 
   def onTaskSucceeded(task: Task, solution: Solution) {
+    info(" => Solved "+task.problem+" ⊢  "+solution)
     if (task.parent eq null) {
       info(" SUCCESS!")
       this.solution = Some(solution)
     } else {
-      info(" => Solved "+task.problem+" ⊢  "+solution)
       task.parent.subSucceeded(task.problem, solution)
     }
   }

testcases/synthesis/Unification.scala

@@ -12,6 +12,8 @@ object UnificationSynthesis {
 
   def u5(a1: Int): List = choose { (xs: List) => Cons(a1, Nil()) == xs }
 
+  def u6(a1: List): Int = choose { (xs: Int) => Cons(xs, Nil()) == a1 }
+
   sealed abstract class List
   case class Nil() extends List
   case class Cons(head : Int, tail : List) extends List