Introduce Modulo as mod operator on BigInt
Refactor all existing Modulo into Remainder, as it is the correct term in Scala for the operation %. BigInt now supports `mod` operator, which gets represented as Modulo in Leon.
Showing
- src/main/java/leon/codegen/runtime/BigInt.java 4 additions, 1 deletionsrc/main/java/leon/codegen/runtime/BigInt.java
- src/main/scala/leon/codegen/CodeGeneration.scala 7 additions, 3 deletionssrc/main/scala/leon/codegen/CodeGeneration.scala
- src/main/scala/leon/evaluators/RecursiveEvaluator.scala 14 additions, 3 deletionssrc/main/scala/leon/evaluators/RecursiveEvaluator.scala
- src/main/scala/leon/frontends/scalac/CodeExtraction.scala 3 additions, 1 deletionsrc/main/scala/leon/frontends/scalac/CodeExtraction.scala
- src/main/scala/leon/purescala/Expressions.scala 11 additions, 7 deletionssrc/main/scala/leon/purescala/Expressions.scala
- src/main/scala/leon/purescala/Extractors.scala 2 additions, 1 deletionsrc/main/scala/leon/purescala/Extractors.scala
- src/main/scala/leon/purescala/PrettyPrinter.scala 7 additions, 5 deletionssrc/main/scala/leon/purescala/PrettyPrinter.scala
- src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala 5 additions, 2 deletionssrc/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
- src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala 5 additions, 2 deletionssrc/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
- src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala 20 additions, 8 deletions...st/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
- src/test/scala/leon/test/evaluators/EvaluatorsTests.scala 18 additions, 11 deletionssrc/test/scala/leon/test/evaluators/EvaluatorsTests.scala
Loading
Please register or sign in to comment