From 08113e8da292f0a0cf682871af85bf68079fc067 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Mon, 1 Jun 2015 13:14:07 +0200
Subject: [PATCH] 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.
---
.../java/leon/codegen/runtime/BigInt.java | 5 +++-
.../scala/leon/codegen/CodeGeneration.scala | 10 +++++--
.../leon/evaluators/RecursiveEvaluator.scala | 17 +++++++++--
.../frontends/scalac/CodeExtraction.scala | 4 ++-
.../scala/leon/purescala/Expressions.scala | 18 +++++++-----
.../scala/leon/purescala/Extractors.scala | 3 +-
.../scala/leon/purescala/PrettyPrinter.scala | 12 ++++----
.../leon/solvers/smtlib/SMTLIBSolver.scala | 7 +++--
.../leon/solvers/z3/AbstractZ3Solver.scala | 7 +++--
.../evaluators/DefaultEvaluatorTests.scala | 28 +++++++++++++-----
.../test/evaluators/EvaluatorsTests.scala | 29 ++++++++++++-------
11 files changed, 96 insertions(+), 44 deletions(-)
diff --git a/src/main/java/leon/codegen/runtime/BigInt.java b/src/main/java/leon/codegen/runtime/BigInt.java
index 83de0fbb4..f2b99a6d9 100644
--- a/src/main/java/leon/codegen/runtime/BigInt.java
+++ b/src/main/java/leon/codegen/runtime/BigInt.java
@@ -40,7 +40,10 @@ public final class BigInt {
}
public BigInt mod(BigInt that) {
- return new BigInt(_underlying.mod(that.underlying()));
+ if(that.underlying().compareTo(new BigInteger("0")) < 0)
+ return new BigInt(_underlying.mod(that.underlying().negate()));
+ else
+ return new BigInt(_underlying.mod(that.underlying()));
}
public BigInt neg() {
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 4125eaddd..5d2b7fd41 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -645,12 +645,16 @@ trait CodeGeneration {
mkExpr(r, ch)
ch << InvokeVirtual(BigIntClass, "div", s"(L$BigIntClass;)L$BigIntClass;")
- //Modulo in Leon corresponds to the "rem" operator on java/Scala BigInt
- case Modulo(l, r) =>
+ case Remainder(l, r) =>
mkExpr(l, ch)
mkExpr(r, ch)
ch << InvokeVirtual(BigIntClass, "rem", s"(L$BigIntClass;)L$BigIntClass;")
+ case Modulo(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << InvokeVirtual(BigIntClass, "mod", s"(L$BigIntClass;)L$BigIntClass;")
+
case UMinus(e) =>
mkExpr(e, ch)
ch << InvokeVirtual(BigIntClass, "neg", s"()L$BigIntClass;")
@@ -676,7 +680,7 @@ trait CodeGeneration {
mkExpr(r, ch)
ch << IDIV
- case BVModulo(l, r) =>
+ case BVRemainder(l, r) =>
mkExpr(l, ch)
mkExpr(r, ch)
ch << IREM
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 86e6ef578..90ea4ace4 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -289,10 +289,21 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (le,re) => throw EvalError(typeErrorMsg(le, IntegerType))
}
+ case Remainder(l,r) =>
+ (e(l), e(r)) match {
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) =>
+ if(i2 != BigInt(0)) InfiniteIntegerLiteral(i1 % i2) else throw RuntimeError("Remainder of division by 0.")
+ case (le,re) => throw EvalError(typeErrorMsg(le, IntegerType))
+ }
case Modulo(l,r) =>
(e(l), e(r)) match {
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) =>
- if(i2 != BigInt(0)) InfiniteIntegerLiteral(i1 % i2) else throw RuntimeError("Modulo by 0.")
+ if(i2 < 0)
+ InfiniteIntegerLiteral(i1 mod (-i2))
+ else if(i2 != BigInt(0))
+ InfiniteIntegerLiteral(i1 mod i2)
+ else
+ throw RuntimeError("Modulo of division by 0.")
case (le,re) => throw EvalError(typeErrorMsg(le, IntegerType))
}
@@ -309,10 +320,10 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
- case BVModulo(l,r) =>
+ case BVRemainder(l,r) =>
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) =>
- if(i2 != 0) IntLiteral(i1 % i2) else throw RuntimeError("Modulo by 0.")
+ if(i2 != 0) IntLiteral(i1 % i2) else throw RuntimeError("Remainder of division by 0.")
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 204720092..4466dbc23 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1596,6 +1596,8 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, IntegerType), "*", List(IsTyped(a2, IntegerType))) =>
Times(a1, a2)
case (IsTyped(a1, IntegerType), "%", List(IsTyped(a2, IntegerType))) =>
+ Remainder(a1, a2)
+ case (IsTyped(a1, IntegerType), "mod", List(IsTyped(a2, IntegerType))) =>
Modulo(a1, a2)
case (IsTyped(a1, IntegerType), "/", List(IsTyped(a2, IntegerType))) =>
Division(a1, a2)
@@ -1616,7 +1618,7 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, Int32Type), "*", List(IsTyped(a2, Int32Type))) =>
BVTimes(a1, a2)
case (IsTyped(a1, Int32Type), "%", List(IsTyped(a2, Int32Type))) =>
- BVModulo(a1, a2)
+ BVRemainder(a1, a2)
case (IsTyped(a1, Int32Type), "/", List(IsTyped(a2, Int32Type))) =>
BVDivision(a1, a2)
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 2a75af65c..e852d55c0 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -326,19 +326,23 @@ object Expressions {
val getType = IntegerType
}
/*
- * Division and Modulo follows Java/Scala semantics. Division corresponds
- * to / operator on BigInt and Modulo corresponds to %. Note that in
- * Java/Scala % is rather called remainder and the "mod" operator is also
- * defined on BigInteger and differs from our Modulo. The "mod" operator
- * returns an always positive remainder, while our Modulo could return
+ * Division and Remainder follows Java/Scala semantics. Division corresponds
+ * to / operator on BigInt and Remainder corresponds to %. Note that in
+ * Java/Scala % is called remainder and the "mod" operator (Modulo in Leon) is also
+ * defined on BigInteger and differs from Remainder. The "mod" operator
+ * returns an always positive remainder, while Remainder could return
* a negative remainder. The following must hold:
*
- * Division(x, y) * y + Modulo(x, y) == x
+ * Division(x, y) * y + Remainder(x, y) == x
*/
case class Division(lhs: Expr, rhs: Expr) extends Expr {
require(lhs.getType == IntegerType && rhs.getType == IntegerType)
val getType = IntegerType
}
+ case class Remainder(lhs: Expr, rhs: Expr) extends Expr {
+ require(lhs.getType == IntegerType && rhs.getType == IntegerType)
+ val getType = IntegerType
+ }
case class Modulo(lhs: Expr, rhs: Expr) extends Expr {
require(lhs.getType == IntegerType && rhs.getType == IntegerType)
val getType = IntegerType
@@ -377,7 +381,7 @@ object Expressions {
require(lhs.getType == Int32Type && rhs.getType == Int32Type)
val getType = Int32Type
}
- case class BVModulo(lhs: Expr, rhs: Expr) extends Expr {
+ case class BVRemainder(lhs: Expr, rhs: Expr) extends Expr {
require(lhs.getType == Int32Type && rhs.getType == Int32Type)
val getType = Int32Type
}
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 249c4622e..0bacc4a72 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -52,6 +52,7 @@ object Extractors {
case Minus(t1,t2) => Some((t1,t2,Minus))
case Times(t1,t2) => Some((t1,t2,Times))
case Division(t1,t2) => Some((t1,t2,Division))
+ case Remainder(t1,t2) => Some((t1,t2,Remainder))
case Modulo(t1,t2) => Some((t1,t2,Modulo))
case LessThan(t1,t2) => Some((t1,t2,LessThan))
case GreaterThan(t1,t2) => Some((t1,t2,GreaterThan))
@@ -61,7 +62,7 @@ object Extractors {
case BVMinus(t1,t2) => Some((t1,t2,BVMinus))
case BVTimes(t1,t2) => Some((t1,t2,BVTimes))
case BVDivision(t1,t2) => Some((t1,t2,BVDivision))
- case BVModulo(t1,t2) => Some((t1,t2,BVModulo))
+ case BVRemainder(t1,t2) => Some((t1,t2,BVRemainder))
case BVAnd(t1,t2) => Some((t1,t2,BVAnd))
case BVOr(t1,t2) => Some((t1,t2,BVOr))
case BVXOr(t1,t2) => Some((t1,t2,BVXOr))
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index b274f8eda..9dbcf0989 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -357,7 +357,8 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case Minus(l,r) => optP { p"$l - $r" }
case Times(l,r) => optP { p"$l * $r" }
case Division(l,r) => optP { p"$l / $r" }
- case Modulo(l,r) => optP { p"$l % $r" }
+ case Remainder(l,r) => optP { p"$l % $r" }
+ case Modulo(l,r) => optP { p"$l mod $r" }
case LessThan(l,r) => optP { p"$l < $r" }
case GreaterThan(l,r) => optP { p"$l > $r" }
case LessEquals(l,r) => optP { p"$l <= $r" }
@@ -366,7 +367,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case BVMinus(l,r) => optP { p"$l - $r" }
case BVTimes(l,r) => optP { p"$l * $r" }
case BVDivision(l,r) => optP { p"$l / $r" }
- case BVModulo(l,r) => optP { p"$l % $r" }
+ case BVRemainder(l,r) => optP { p"$l % $r" }
case BVAnd(l,r) => optP { p"$l & $r" }
case BVOr(l,r) => optP { p"$l | $r" }
case BVXOr(l,r) => optP { p"$l ^ $r" }
@@ -741,9 +742,10 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case (_: And | BinaryMethodCall(_, "&&", _)) => 3
case (_: GreaterThan | _: GreaterEquals | _: LessEquals | _: LessThan) => 4
case (_: Equals | _: Not) => 5
- case (_: Plus | _: BVPlus | _: Minus | _: BVMinus | _: SetUnion| _: SetDifference | BinaryMethodCall(_, "+" | "-", _)) => 6
- case (_: Times | _: BVTimes | _: Division | _: BVDivision | _: Modulo | _: BVModulo | BinaryMethodCall(_, "*" | "/", _)) => 7
- case _ => 7
+ case (_: Modulo) => 6
+ case (_: Plus | _: BVPlus | _: Minus | _: BVMinus | _: SetUnion| _: SetDifference | BinaryMethodCall(_, "+" | "-", _)) => 7
+ case (_: Times | _: BVTimes | _: Division | _: BVDivision | _: Remainder | _: BVRemainder | BinaryMethodCall(_, "*" | "/", _)) => 8
+ case _ => 9
}
def requiresParentheses(ex: Tree, within: Option[Tree]): Boolean = (ex, within) match {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index ae77673d8..0ac1f11e6 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -649,10 +649,13 @@ abstract class SMTLIBSolver(val context: LeonContext,
Ints.Div(ar, br),
Ints.Neg(Ints.Div(Ints.Neg(ar), br)))
}
- case Modulo(a,b) => {
+ case Remainder(a,b) => {
val q = toSMT(Division(a, b))
Ints.Sub(toSMT(a), Ints.Mul(toSMT(b), q))
}
+ case Modulo(a,b) => {
+ Ints.Mod(toSMT(a), toSMT(b))
+ }
case LessThan(a,b) => a.getType match {
case Int32Type => FixedSizeBitVectors.SLessThan(toSMT(a), toSMT(b))
case IntegerType => Ints.LessThan(toSMT(a), toSMT(b))
@@ -677,7 +680,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
case BVMinus(a,b) => FixedSizeBitVectors.Sub(toSMT(a), toSMT(b))
case BVTimes(a,b) => FixedSizeBitVectors.Mul(toSMT(a), toSMT(b))
case BVDivision(a,b) => FixedSizeBitVectors.SDiv(toSMT(a), toSMT(b))
- case BVModulo(a,b) => FixedSizeBitVectors.SRem(toSMT(a), toSMT(b))
+ case BVRemainder(a,b) => FixedSizeBitVectors.SRem(toSMT(a), toSMT(b))
case BVAnd(a,b) => FixedSizeBitVectors.And(toSMT(a), toSMT(b))
case BVOr(a,b) => FixedSizeBitVectors.Or(toSMT(a), toSMT(b))
case BVXOr(a,b) => FixedSizeBitVectors.XOr(toSMT(a), toSMT(b))
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index d8ac22b21..e036c86eb 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -569,16 +569,19 @@ trait AbstractZ3Solver
z3.mkUnaryMinus(z3.mkDiv(z3.mkUnaryMinus(rl), rr))
)
}
- case Modulo(l, r) => {
+ case Remainder(l, r) => {
val q = rec(Division(l, r))
z3.mkSub(rec(l), z3.mkMul(rec(r), q))
}
+ case Modulo(l, r) => {
+ z3.mkMod(rec(l), rec(r))
+ }
case UMinus(e) => z3.mkUnaryMinus(rec(e))
case BVPlus(l, r) => z3.mkBVAdd(rec(l), rec(r))
case BVMinus(l, r) => z3.mkBVSub(rec(l), rec(r))
case BVTimes(l, r) => z3.mkBVMul(rec(l), rec(r))
case BVDivision(l, r) => z3.mkBVSdiv(rec(l), rec(r))
- case BVModulo(l, r) => z3.mkBVSrem(rec(l), rec(r))
+ case BVRemainder(l, r) => z3.mkBVSrem(rec(l), rec(r))
case BVUMinus(e) => z3.mkBVNeg(rec(e))
case BVNot(e) => z3.mkBVNot(rec(e))
case BVAnd(l, r) => z3.mkBVAnd(rec(l), rec(r))
diff --git a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
index b4b4540cd..ad359346a 100644
--- a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
+++ b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
@@ -79,10 +79,13 @@ class DefaultEvaluatorTests extends leon.test.LeonTestSuite {
InfiniteIntegerLiteral(6))
}
- test("Eval of division and modulo semantics for BigInt") {
+ test("Eval of division, remainder and modulo semantics for BigInt") {
expectSuccessful(
defaultEvaluator.eval(Division(InfiniteIntegerLiteral(10), InfiniteIntegerLiteral(3))),
InfiniteIntegerLiteral(3))
+ expectSuccessful(
+ defaultEvaluator.eval(Remainder(InfiniteIntegerLiteral(10), InfiniteIntegerLiteral(3))),
+ InfiniteIntegerLiteral(1))
expectSuccessful(
defaultEvaluator.eval(Modulo(InfiniteIntegerLiteral(10), InfiniteIntegerLiteral(3))),
InfiniteIntegerLiteral(1))
@@ -91,51 +94,60 @@ class DefaultEvaluatorTests extends leon.test.LeonTestSuite {
defaultEvaluator.eval(Division(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(3))),
InfiniteIntegerLiteral(0))
expectSuccessful(
- defaultEvaluator.eval(Modulo(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(3))),
+ defaultEvaluator.eval(Remainder(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(3))),
InfiniteIntegerLiteral(-1))
+ expectSuccessful(
+ defaultEvaluator.eval(Modulo(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(3))),
+ InfiniteIntegerLiteral(2))
expectSuccessful(
defaultEvaluator.eval(Division(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(-3))),
InfiniteIntegerLiteral(0))
expectSuccessful(
- defaultEvaluator.eval(Modulo(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(-3))),
+ defaultEvaluator.eval(Remainder(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(-3))),
InfiniteIntegerLiteral(-1))
+ expectSuccessful(
+ defaultEvaluator.eval(Modulo(InfiniteIntegerLiteral(-1), InfiniteIntegerLiteral(-3))),
+ InfiniteIntegerLiteral(2))
expectSuccessful(
defaultEvaluator.eval(Division(InfiniteIntegerLiteral(1), InfiniteIntegerLiteral(-3))),
InfiniteIntegerLiteral(0))
+ expectSuccessful(
+ defaultEvaluator.eval(Remainder(InfiniteIntegerLiteral(1), InfiniteIntegerLiteral(-3))),
+ InfiniteIntegerLiteral(1))
expectSuccessful(
defaultEvaluator.eval(Modulo(InfiniteIntegerLiteral(1), InfiniteIntegerLiteral(-3))),
InfiniteIntegerLiteral(1))
}
- test("Eval of division and modulo semantics for bit vectors") {
+ test("Eval of division and remainder semantics for bit vectors") {
expectSuccessful(
defaultEvaluator.eval(BVDivision(IntLiteral(10), IntLiteral(3))),
IntLiteral(3))
expectSuccessful(
- defaultEvaluator.eval(BVModulo(IntLiteral(10), IntLiteral(3))),
+ defaultEvaluator.eval(BVRemainder(IntLiteral(10), IntLiteral(3))),
IntLiteral(1))
expectSuccessful(
defaultEvaluator.eval(BVDivision(IntLiteral(-1), IntLiteral(3))),
IntLiteral(0))
expectSuccessful(
- defaultEvaluator.eval(BVModulo(IntLiteral(-1), IntLiteral(3))),
+ defaultEvaluator.eval(BVRemainder(IntLiteral(-1), IntLiteral(3))),
IntLiteral(-1))
expectSuccessful(
defaultEvaluator.eval(BVDivision(IntLiteral(-1), IntLiteral(-3))),
IntLiteral(0))
expectSuccessful(
- defaultEvaluator.eval(BVModulo(IntLiteral(-1), IntLiteral(-3))),
+ defaultEvaluator.eval(BVRemainder(IntLiteral(-1), IntLiteral(-3))),
IntLiteral(-1))
expectSuccessful(
defaultEvaluator.eval(BVDivision(IntLiteral(1), IntLiteral(-3))),
IntLiteral(0))
expectSuccessful(
- defaultEvaluator.eval(BVModulo(IntLiteral(1), IntLiteral(-3))),
+ defaultEvaluator.eval(BVRemainder(IntLiteral(1), IntLiteral(-3))),
IntLiteral(1))
}
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 20bd91732..f34d82dee 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -174,7 +174,7 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
| if(s > n) c else intSqrt0(n, c+1)
| }
| def div(x : Int, y : Int) : Int = (x / y)
- | def mod(x : Int, y : Int) : Int = (x % y)
+ | def rem(x : Int, y : Int) : Int = (x % y)
|}
|""".stripMargin
@@ -191,15 +191,15 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
checkComp(e, mkCall("div", IL(7), IL(-5)), IL(-1))
checkComp(e, mkCall("div", IL(-7), IL(5)), IL(-1))
checkComp(e, mkCall("div", IL(-7), IL(-5)), IL(1))
- checkComp(e, mkCall("mod", IL(7), IL(5)), IL(2))
- checkComp(e, mkCall("mod", IL(7), IL(-5)), IL(2))
- checkComp(e, mkCall("mod", IL(-7), IL(5)), IL(-2))
- checkComp(e, mkCall("mod", IL(-7), IL(-5)), IL(-2))
- checkComp(e, mkCall("mod", IL(-1), IL(5)), IL(-1))
+ checkComp(e, mkCall("rem", IL(7), IL(5)), IL(2))
+ checkComp(e, mkCall("rem", IL(7), IL(-5)), IL(2))
+ checkComp(e, mkCall("rem", IL(-7), IL(5)), IL(-2))
+ checkComp(e, mkCall("rem", IL(-7), IL(-5)), IL(-2))
+ checkComp(e, mkCall("rem", IL(-1), IL(5)), IL(-1))
// Things that should crash.
checkError(e, mkCall("div", IL(42), IL(0)))
- checkError(e, mkCall("mod", IL(42), IL(0)))
+ checkError(e, mkCall("rem", IL(42), IL(0)))
}
}
@@ -215,7 +215,8 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
| if(s > n) c else intSqrt0(n, c+1)
| }
| def div(x : BigInt, y : BigInt) : BigInt = (x / y)
- | def mod(x : BigInt, y : BigInt) : BigInt = (x % y)
+ | def rem(x : BigInt, y : BigInt) : BigInt = (x % y)
+ | def mod(x : BigInt, y : BigInt) : BigInt = (x mod y)
|}
|""".stripMargin
@@ -232,14 +233,20 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
checkComp(e, mkCall("div", BIL(7), BIL(-5)), BIL(-1))
checkComp(e, mkCall("div", BIL(-7), BIL(5)), BIL(-1))
checkComp(e, mkCall("div", BIL(-7), BIL(-5)), BIL(1))
+ checkComp(e, mkCall("rem", BIL(7), BIL(5)), BIL(2))
+ checkComp(e, mkCall("rem", BIL(7), BIL(-5)), BIL(2))
+ checkComp(e, mkCall("rem", BIL(-7), BIL(5)), BIL(-2))
+ checkComp(e, mkCall("rem", BIL(-7), BIL(-5)), BIL(-2))
+ checkComp(e, mkCall("rem", BIL(-1), BIL(5)), BIL(-1))
checkComp(e, mkCall("mod", BIL(7), BIL(5)), BIL(2))
checkComp(e, mkCall("mod", BIL(7), BIL(-5)), BIL(2))
- checkComp(e, mkCall("mod", BIL(-7), BIL(5)), BIL(-2))
- checkComp(e, mkCall("mod", BIL(-7), BIL(-5)), BIL(-2))
- checkComp(e, mkCall("mod", BIL(-1), BIL(5)), BIL(-1))
+ checkComp(e, mkCall("mod", BIL(-7), BIL(5)), BIL(3))
+ checkComp(e, mkCall("mod", BIL(-7), BIL(-5)), BIL(3))
+ checkComp(e, mkCall("mod", BIL(-1), BIL(5)), BIL(4))
// Things that should crash.
checkError(e, mkCall("div", BIL(42), BIL(0)))
+ checkError(e, mkCall("rem", BIL(42), BIL(0)))
checkError(e, mkCall("mod", BIL(42), BIL(0)))
}
}
--
GitLab