From 66c9ec794255848bb636c90f14cf9f1068d3c72c Mon Sep 17 00:00:00 2001 From: Samuel Gruetter <samuel.gruetter@epfl.ch> Date: Tue, 2 Jun 2015 20:53:59 +0200 Subject: [PATCH] add lexicographic comparison of argument lists --- .../ComplexTerminationChecker.scala | 28 +++++++++---- .../leon/termination/RelationComparator.scala | 40 +++++++++++++++++++ .../leon/termination/RelationProcessor.scala | 2 +- 3 files changed, 62 insertions(+), 8 deletions(-) diff --git a/src/main/scala/leon/termination/ComplexTerminationChecker.scala b/src/main/scala/leon/termination/ComplexTerminationChecker.scala index 062f6af12..a1fc1d85b 100644 --- a/src/main/scala/leon/termination/ComplexTerminationChecker.scala +++ b/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) diff --git a/src/main/scala/leon/termination/RelationComparator.scala b/src/main/scala/leon/termination/RelationComparator.scala index 14121286b..65c00adb2 100644 --- a/src/main/scala/leon/termination/RelationComparator.scala +++ b/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: diff --git a/src/main/scala/leon/termination/RelationProcessor.scala b/src/main/scala/leon/termination/RelationProcessor.scala index 0fd6dd380..8169bff8c 100644 --- a/src/main/scala/leon/termination/RelationProcessor.scala +++ b/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") -- GitLab