add support for bits operations
Adds a benchmark with many cool magic tricks with bits. However, proving some of them is very costly and we could potentially look at opportunities to make the proofs go through faster.
Showing
- src/main/scala/leon/codegen/CodeGeneration.scala 34 additions, 0 deletionssrc/main/scala/leon/codegen/CodeGeneration.scala
- src/main/scala/leon/evaluators/RecursiveEvaluator.scala 42 additions, 0 deletionssrc/main/scala/leon/evaluators/RecursiveEvaluator.scala
- src/main/scala/leon/frontends/scalac/ASTExtractors.scala 7 additions, 0 deletionssrc/main/scala/leon/frontends/scalac/ASTExtractors.scala
- src/main/scala/leon/frontends/scalac/CodeExtraction.scala 14 additions, 12 deletionssrc/main/scala/leon/frontends/scalac/CodeExtraction.scala
- src/main/scala/leon/purescala/Extractors.scala 7 additions, 0 deletionssrc/main/scala/leon/purescala/Extractors.scala
- src/main/scala/leon/purescala/PrettyPrinter.scala 6 additions, 0 deletionssrc/main/scala/leon/purescala/PrettyPrinter.scala
- src/main/scala/leon/purescala/Trees.scala 22 additions, 0 deletionssrc/main/scala/leon/purescala/Trees.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala 8 additions, 0 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 7 additions, 0 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/test/resources/regression/verification/purescala/valid/BitsTricks.scala 103 additions, 0 deletions.../regression/verification/purescala/valid/BitsTricks.scala
- src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala 25 additions, 0 deletions...st/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
- testcases/verification/BitsTricks.scala 103 additions, 0 deletionstestcases/verification/BitsTricks.scala
Loading
Please register or sign in to comment