Int becomes bitvector
Leon now matches Scala semantics of Int as 32 bits bit-vectors. This commits modifies the semantics of IntLiteral to be treated as 32 bits integer everywhere (solver, evaluator, ...). Introduces a new literal type, InfiniteIntegerLiteral, representing a natural integer. The front-end maps the use of BigInt to these new trees, and the solver properly handles them as mathematical integers. The behaviour of many regression tests changes due to this new semantics. In particular many of them now timeout because they are no longer proving properties over mathematical integers. This commit updates the tests to reflect this new semantics.
Showing
- library/collection/List.scala 29 additions, 29 deletionslibrary/collection/List.scala
- src/main/scala/leon/codegen/CodeGeneration.scala 54 additions, 5 deletionssrc/main/scala/leon/codegen/CodeGeneration.scala
- src/main/scala/leon/codegen/CompilationUnit.scala 5 additions, 1 deletionsrc/main/scala/leon/codegen/CompilationUnit.scala
- src/main/scala/leon/datagen/VanuatooDataGen.scala 12 additions, 2 deletionssrc/main/scala/leon/datagen/VanuatooDataGen.scala
- src/main/scala/leon/evaluators/RecursiveEvaluator.scala 47 additions, 3 deletionssrc/main/scala/leon/evaluators/RecursiveEvaluator.scala
- src/main/scala/leon/frontends/scalac/ASTExtractors.scala 30 additions, 0 deletionssrc/main/scala/leon/frontends/scalac/ASTExtractors.scala
- src/main/scala/leon/frontends/scalac/CodeExtraction.scala 47 additions, 5 deletionssrc/main/scala/leon/frontends/scalac/CodeExtraction.scala
- src/main/scala/leon/purescala/Extractors.scala 6 additions, 0 deletionssrc/main/scala/leon/purescala/Extractors.scala
- src/main/scala/leon/purescala/PrettyPrinter.scala 11 additions, 3 deletionssrc/main/scala/leon/purescala/PrettyPrinter.scala
- src/main/scala/leon/purescala/TreeNormalizations.scala 12 additions, 12 deletionssrc/main/scala/leon/purescala/TreeNormalizations.scala
- src/main/scala/leon/purescala/TreeOps.scala 29 additions, 28 deletionssrc/main/scala/leon/purescala/TreeOps.scala
- src/main/scala/leon/purescala/Trees.scala 45 additions, 6 deletionssrc/main/scala/leon/purescala/Trees.scala
- src/main/scala/leon/purescala/TypeTrees.scala 4 additions, 1 deletionsrc/main/scala/leon/purescala/TypeTrees.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala 29 additions, 10 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 68 additions, 15 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala 1 addition, 0 deletionssrc/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
- src/main/scala/leon/synthesis/Algebra.scala 87 additions, 0 deletionssrc/main/scala/leon/synthesis/Algebra.scala
- src/main/scala/leon/synthesis/LinearEquations.scala 24 additions, 24 deletionssrc/main/scala/leon/synthesis/LinearEquations.scala
- src/main/scala/leon/synthesis/Rules.scala 2 additions, 2 deletionssrc/main/scala/leon/synthesis/Rules.scala
- src/main/scala/leon/synthesis/rules/Cegis.scala 12 additions, 0 deletionssrc/main/scala/leon/synthesis/rules/Cegis.scala
Loading
Please register or sign in to comment