<commit_before>/* Copyright 2009-2016 EPFL, Lausanne */

package leon
package termination

import purescala.Definitions._

import scala.collection.mutable.{Map => MutableMap}

class ComplexTerminationChecker(context: LeonContext, initProgram: Program) extends ProcessingPipeline(context, initProgram) {

  val name = "Complex Termination Checker"
  val description = "A modular termination checker with a few basic modules™"

  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
  }

  val modulesBV =
        new StructuralSize
       with BVRelationComparator
       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, modulesBV),
    new RelationProcessor(this, modules),
    new RelationProcessor(this, modulesLexicographic),
    //new ChainProcessor(this, modules),
    new SelfCallsProcessor(this) //,<commit_msg>(a) Added missing library annotations, (b) Added a decrease construct to specify ranking function (c) updated the extraction phase to parse the decrease construct (d) updated the fundef to store the extracted decrease construct, and added some necessary changes to the phases that create new fundefs.<commit_after>/* Copyright 2009-2016 EPFL, Lausanne */

package leon
package termination

import purescala.Definitions._

import scala.collection.mutable.{Map => MutableMap}

class ComplexTerminationChecker(context: LeonContext, initProgram: Program) extends ProcessingPipeline(context, initProgram) {

  val name = "Complex Termination Checker"
  val description = "A modular termination checker with a few basic modules™"

  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
  }

  val modulesBV =
        new StructuralSize
       with BVRelationComparator
       with ChainComparator
       with Strengthener
       with RelationBuilder
       with ChainBuilder 
  {
    val checker = ComplexTerminationChecker.this
  }

  def processors = List(
    //new DecreasesByProcessor(this),
    new RecursionProcessor(this, modules),
    // RelationProcessor is the only Processor which benefits from trying a different RelationComparator
    new RelationProcessor(this, modulesBV),
    new RelationProcessor(this, modules),
    new RelationProcessor(this, modulesLexicographic),
    //new ChainProcessor(this, modules),
    new SelfCallsProcessor(this) //,
{'fraction_non_alphanumeric': 0.05030008573878251, 'fraction_numerical': 0.004572735067162046, 'mean_word_length': 3.4929396662387675, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1339649', 'n_tokens_mistral': 920, 'n_tokens_neox': 882, 'n_words': 289}