ADTDual and Unification become normalizing rules

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

@@ -6,7 +6,7 @@ import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
 
-case object ADTDual extends Rule("ADTDual") {
+case object ADTDual extends NormalizingRule("ADTDual") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val xs = p.xs.toSet
     val as = p.as.toSet
@@ -15,9 +15,10 @@ case object ADTDual extends Rule("ADTDual") {
 
 
     val (toRemove, toAdd) = exprs.collect {
-      case eq @ Equals(cc @ CaseClass(cd, args), e) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) -- xs).isEmpty =>
+      case eq @ Equals(cc @ CaseClass(cd, args), e) if (variablesOf(e) -- as).isEmpty && !(variablesOf(cc) & xs).isEmpty =>
         (eq, CaseClassInstanceOf(cd, e) +: (cd.fieldsIds zip args).map{ case (id, ex) => Equals(ex, CaseClassSelector(cd, e, id)) } )
-      case eq @ Equals(e, cc @ CaseClass(cd, args)) if (variablesOf(e) -- as).isEmpty && (variablesOf(cc) -- xs).isEmpty =>
+
+      case eq @ Equals(e, cc @ CaseClass(cd, args)) if (variablesOf(e) -- as).isEmpty && !(variablesOf(cc) & xs).isEmpty =>
         (eq, CaseClassInstanceOf(cd, e) +: (cd.fieldsIds zip args).map{ case (id, ex) => Equals(ex, CaseClassSelector(cd, e, id)) } )
     }.unzip
 

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

@@ -8,7 +8,7 @@ import purescala.TreeOps._
 import purescala.Extractors._
 
 object Unification {
-  case object DecompTrivialClash extends Rule("Unif Dec./Clash/Triv.") {
+  case object DecompTrivialClash extends NormalizingRule("Unif Dec./Clash/Triv.") {
     def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
       val TopLevelAnds(exprs) = p.phi
 
@@ -36,7 +36,7 @@ object Unification {
 
   // This rule is probably useless; it never happens except in crafted
   // examples, and will be found by OptimisticGround anyway.
-  case object OccursCheck extends Rule("Unif OccursCheck") {
+  case object OccursCheck extends NormalizingRule("Unif OccursCheck") {
     def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
       val TopLevelAnds(exprs) = p.phi