Fix MethodLifting and improvements
Make signature of IsInstanceOf consistent with other Expr's Add isInstOf Constructor Correctly handle This in instantiateType Correctly handle This in MethodLifting when it belongs to a subtype An extra unit test
Showing
- src/main/scala/leon/codegen/CodeGeneration.scala 1 addition, 1 deletionsrc/main/scala/leon/codegen/CodeGeneration.scala
- src/main/scala/leon/evaluators/RecursiveEvaluator.scala 1 addition, 1 deletionsrc/main/scala/leon/evaluators/RecursiveEvaluator.scala
- src/main/scala/leon/frontends/scalac/CodeExtraction.scala 1 addition, 1 deletionsrc/main/scala/leon/frontends/scalac/CodeExtraction.scala
- src/main/scala/leon/purescala/Constructors.scala 10 additions, 0 deletionssrc/main/scala/leon/purescala/Constructors.scala
- src/main/scala/leon/purescala/ExprOps.scala 3 additions, 3 deletionssrc/main/scala/leon/purescala/ExprOps.scala
- src/main/scala/leon/purescala/Expressions.scala 2 additions, 2 deletionssrc/main/scala/leon/purescala/Expressions.scala
- src/main/scala/leon/purescala/Extractors.scala 2 additions, 2 deletionssrc/main/scala/leon/purescala/Extractors.scala
- src/main/scala/leon/purescala/MethodLifting.scala 14 additions, 10 deletionssrc/main/scala/leon/purescala/MethodLifting.scala
- src/main/scala/leon/purescala/PrettyPrinter.scala 1 addition, 1 deletionsrc/main/scala/leon/purescala/PrettyPrinter.scala
- src/main/scala/leon/purescala/TypeOps.scala 5 additions, 2 deletionssrc/main/scala/leon/purescala/TypeOps.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala 1 addition, 1 deletionsrc/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 4 additions, 4 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/main/scala/leon/synthesis/rules/ADTDual.scala 2 additions, 2 deletionssrc/main/scala/leon/synthesis/rules/ADTDual.scala
- src/main/scala/leon/synthesis/rules/ADTInduction.scala 1 addition, 1 deletionsrc/main/scala/leon/synthesis/rules/ADTInduction.scala
- src/main/scala/leon/synthesis/rules/ADTLongInduction.scala 1 addition, 1 deletionsrc/main/scala/leon/synthesis/rules/ADTLongInduction.scala
- src/main/scala/leon/synthesis/rules/ADTSplit.scala 2 additions, 2 deletionssrc/main/scala/leon/synthesis/rules/ADTSplit.scala
- src/main/scala/leon/synthesis/rules/EquivalentInputs.scala 1 addition, 1 deletionsrc/main/scala/leon/synthesis/rules/EquivalentInputs.scala
- src/main/scala/leon/termination/SelfCallsProcessor.scala 1 addition, 1 deletionsrc/main/scala/leon/termination/SelfCallsProcessor.scala
- src/main/scala/leon/utils/TypingPhase.scala 3 additions, 3 deletionssrc/main/scala/leon/utils/TypingPhase.scala
- src/main/scala/leon/verification/InductionTactic.scala 2 additions, 2 deletionssrc/main/scala/leon/verification/InductionTactic.scala
Loading
Please register or sign in to comment