Merge branch 'master' of laragit.epfl.ch:projects/leon-2.0

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

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

@@ -22,6 +22,7 @@ object Rules {
     new UnusedInput(_),
     new UnconstrainedOutput(_),
     new OptimisticGround(_),
+    new EqualitySplit(_),
     new CEGIS(_),
     new Assert(_),
     new IntegerEquation(_)
@@ -284,7 +285,7 @@ class ADTDual(synth: Synthesizer) extends Rule("ADTDual", synth, 200) {
   }
 }
 
-class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 50) {
+class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
   def applyOn(task: Task): RuleResult = {
     val p = task.problem
 
@@ -460,7 +461,7 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 50) {
   }
 }
 
-class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 90) {
+class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", synth, 150) {
   def applyOn(task: Task): RuleResult = {
     val p = task.problem
 
@@ -516,6 +517,25 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
   }
 }
 
+class EqualitySplit(synth: Synthesizer) extends Rule("Eq. Split.", synth, 10) {
+  def applyOn(task: Task): RuleResult = {
+    val p = task.problem
+
+    val asgroups = p.as.groupBy(_.getType).filter(_._2.size == 2).mapValues(_.toList)
+
+    val extraConds = for (List(a1, a2) <- asgroups.values) yield {
+      Or(Equals(Variable(a1), Variable(a2)), Not(Equals(Variable(a1), Variable(a2))))
+    }
+
+    if (!extraConds.isEmpty) {
+      val sub = p.copy(phi = And(And(extraConds.toSeq), p.phi))
+      RuleStep(List(sub), forward)
+    } else {
+      RuleInapplicable
+    }
+  }
+}
+
 class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth, 300) {
   def applyOn(task: Task): RuleResult = {