One rule for ADT ≠ decomposition.

Note that many ADT problems seem to diverge now. Also, preconditions are
missing? Or maybe just not displayed.

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

@@ -9,7 +9,8 @@ import rules._
 object Rules {
   def all = Set[Synthesizer => Rule](
     new Unification.DecompTrivialClash(_),
-    new Unification.OccursCheck(_),
+    new Unification.OccursCheck(_), // probably useless
+    new Disunification.Decomp(_),
     new ADTDual(_),
     new OnePoint(_),
     new Ground(_),

src/main/scala/leon/synthesis/rules/Disunification.scala

+package leon
+package synthesis
+package rules
+
+import purescala.Trees._
+import purescala.TypeTrees._
+import purescala.TreeOps._
+import purescala.Extractors._
+
+object Disunification {
+  class Decomp(synth: Synthesizer) extends Rule("Disunif. Decomp.", synth, 200) {
+    def attemptToApplyOn(p: Problem): RuleResult = {
+      val TopLevelAnds(exprs) = p.phi
+
+      val (toRemove, toAdd) = exprs.collect {
+        case neq @ Not(Equals(cc1 @ CaseClass(cd1, args1), cc2 @ CaseClass(cd2, args2))) =>
+          if (cc1 == cc2) {
+            (neq, List(BooleanLiteral(false)))
+          } else if (cd1 == cd2) {
+            (neq, (args1 zip args2).map(p => Not(Equals(p._1, p._2))))
+          } else {
+            (neq, List(BooleanLiteral(true)))
+          }
+      }.unzip
+
+      if (!toRemove.isEmpty) {
+        val sub = p.copy(phi = Or((exprs.toSet -- toRemove ++ toAdd.flatten).toSeq))
+
+        RuleFastStep(List(sub), forward)
+      } else {
+        RuleInapplicable
+      }
+    }
+  }
+}
+

src/main/scala/leon/synthesis/rules/Unification.scala

@@ -34,6 +34,8 @@ object Unification {
     }
   }
 
+  // This rule is probably useless; it never happens except in crafted
+  // examples, and will be found by OptimisticGround anyway.
   class OccursCheck(synth: Synthesizer) extends Rule("Unif OccursCheck", synth, 200) {
     def attemptToApplyOn(p: Problem): RuleResult = {
       val TopLevelAnds(exprs) = p.phi