-
- Downloads
Datatype unrolling adds support for:
- First-class functions in ADTs - ADTs with invariants - ADTs with fields that are not most general type
Showing
- src/main/scala/leon/frontends/scalac/CodeExtraction.scala 85 additions, 12 deletionssrc/main/scala/leon/frontends/scalac/CodeExtraction.scala
- src/main/scala/leon/purescala/CheckADTFieldsTypes.scala 0 additions, 29 deletionssrc/main/scala/leon/purescala/CheckADTFieldsTypes.scala
- src/main/scala/leon/purescala/Constructors.scala 1 addition, 1 deletionsrc/main/scala/leon/purescala/Constructors.scala
- src/main/scala/leon/purescala/DefOps.scala 4 additions, 2 deletionssrc/main/scala/leon/purescala/DefOps.scala
- src/main/scala/leon/purescala/Definitions.scala 29 additions, 2 deletionssrc/main/scala/leon/purescala/Definitions.scala
- src/main/scala/leon/purescala/Expressions.scala 1 addition, 1 deletionsrc/main/scala/leon/purescala/Expressions.scala
- src/main/scala/leon/purescala/MethodLifting.scala 4 additions, 0 deletionssrc/main/scala/leon/purescala/MethodLifting.scala
- src/main/scala/leon/purescala/Types.scala 3 additions, 1 deletionsrc/main/scala/leon/purescala/Types.scala
- src/main/scala/leon/solvers/templates/DatatypeManager.scala 214 additions, 0 deletionssrc/main/scala/leon/solvers/templates/DatatypeManager.scala
- src/main/scala/leon/solvers/templates/LambdaManager.scala 106 additions, 27 deletionssrc/main/scala/leon/solvers/templates/LambdaManager.scala
- src/main/scala/leon/solvers/templates/QuantificationManager.scala 13 additions, 17 deletions.../scala/leon/solvers/templates/QuantificationManager.scala
- src/main/scala/leon/solvers/templates/TemplateGenerator.scala 6 additions, 23 deletions...main/scala/leon/solvers/templates/TemplateGenerator.scala
- src/main/scala/leon/solvers/templates/TemplateManager.scala 133 additions, 81 deletionssrc/main/scala/leon/solvers/templates/TemplateManager.scala
- src/main/scala/leon/solvers/templates/UnrollingBank.scala 3 additions, 1 deletionsrc/main/scala/leon/solvers/templates/UnrollingBank.scala
- src/main/scala/leon/termination/StructuralSize.scala 1 addition, 1 deletionsrc/main/scala/leon/termination/StructuralSize.scala
- src/main/scala/leon/utils/PreprocessingPhase.scala 0 additions, 1 deletionsrc/main/scala/leon/utils/PreprocessingPhase.scala
- src/main/scala/leon/utils/SeqUtils.scala 20 additions, 2 deletionssrc/main/scala/leon/utils/SeqUtils.scala
- src/main/scala/leon/verification/InjectAsserts.scala 6 additions, 0 deletionssrc/main/scala/leon/verification/InjectAsserts.scala
- src/test/resources/regression/termination/valid/Ackermann.scala 10 additions, 0 deletions...st/resources/regression/termination/valid/Ackermann.scala
Loading
Please register or sign in to comment