add lexicographic comparison of argument lists

src/main/scala/leon/termination/ComplexTerminationChecker.scala

@@ -12,20 +12,34 @@ class ComplexTerminationChecker(context: LeonContext, program: Program) extends
 
   val name = "Complex Termination Checker"
   val description = "A modular termination checker with a few basic modules™"
-  
-  val modules = new StructuralSize
-               with RelationComparator
-               with ChainComparator
-               with Strengthener
-               with RelationBuilder
-               with ChainBuilder 
+
+  val modules =
+        new StructuralSize
+       with ArgsSizeSumRelationComparator
+       with ChainComparator
+       with Strengthener
+       with RelationBuilder
+       with ChainBuilder 
+  {
+    val checker = ComplexTerminationChecker.this
+  }
+
+  val modulesLexicographic =
+        new StructuralSize
+       with LexicographicRelationComparator
+       with ChainComparator
+       with Strengthener
+       with RelationBuilder
+       with ChainBuilder 
   {
     val checker = ComplexTerminationChecker.this
   }
 
   def processors = List(
     new RecursionProcessor(this, modules),
+    // RelationProcessor is the only Processor which benefits from trying a different RelationComparator
     new RelationProcessor(this, modules),
+    new RelationProcessor(this, modulesLexicographic),
     new ChainProcessor(this, modules),
     new SelfCallsProcessor(this),
     new LoopProcessor(this, modules)

src/main/scala/leon/termination/RelationComparator.scala

@@ -7,6 +7,19 @@ import purescala.Expressions._
 import leon.purescala.Constructors._
 
 trait RelationComparator { self : StructuralSize =>
+  
+  val comparisonMethod: String
+
+  def sizeDecreasing(args1: Seq[Expr], args2: Seq[Expr]): Expr
+
+  def softDecreasing(args1: Seq[Expr], args2: Seq[Expr]): Expr
+
+}
+
+
+trait ArgsSizeSumRelationComparator extends RelationComparator { self : StructuralSize =>
+
+  val comparisonMethod = "comparing sum of argument sizes"
 
   def sizeDecreasing(args1: Seq[Expr], args2: Seq[Expr]): Expr = {
     GreaterThan(self.size(tupleWrap(args1)), self.size(tupleWrap(args2)))
@@ -18,4 +31,31 @@ trait RelationComparator { self : StructuralSize =>
 
 }
 
+
+trait LexicographicRelationComparator extends RelationComparator { self : StructuralSize =>
+
+  val comparisonMethod = "comparing argument lists lexicographically"
+  
+  def lexicographicDecreasing(s1: Seq[Expr], s2: Seq[Expr], strict: Boolean): Expr = {
+    val sameSizeExprs = for ((arg1, arg2) <- (s1 zip s2)) yield Equals(self.size(arg1), self.size(arg2))
+    
+    val greaterBecauseGreaterAtFirstDifferentPos =
+      orJoin(for (firstDifferent <- 0 until scala.math.min(s1.length, s2.length)) yield and(
+          andJoin(sameSizeExprs.take(firstDifferent)),
+          GreaterThan(self.size(s1(firstDifferent)), self.size(s2(firstDifferent)))
+      ))
+      
+    if (s1.length > s2.length || (s1.length == s2.length && !strict)) {
+      or(andJoin(sameSizeExprs), greaterBecauseGreaterAtFirstDifferentPos)
+    } else {
+      greaterBecauseGreaterAtFirstDifferentPos
+    }
+  }
+
+  def sizeDecreasing(s1: Seq[Expr], s2: Seq[Expr]) = lexicographicDecreasing(s1, s2, strict = true)
+
+  def softDecreasing(s1: Seq[Expr], s2: Seq[Expr]) = lexicographicDecreasing(s1, s2, strict = false)
+
+}
+
 // vim: set ts=4 sw=4 et:

src/main/scala/leon/termination/RelationProcessor.scala

@@ -16,7 +16,7 @@ class RelationProcessor(
     val modules: RelationBuilder with RelationComparator with Strengthener with StructuralSize
   ) extends Processor with Solvable {
 
-  val name: String = "Relation Processor"
+  val name: String = "Relation Processor " + modules.comparisonMethod
 
   def run(problem: Problem) = {
     reporter.debug("- Strengthening postconditions")