From 4c6737ee0fe971f90c3f10228eca8096781dfc2f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Tue, 6 Mar 2012 15:05:17 +0100
Subject: [PATCH] added Mod operator and a nice example with isEven test
---
mytest/Even.scala | 14 ++++++++++++++
src/main/scala/leon/Evaluator.scala | 4 ++++
src/main/scala/leon/FairZ3Solver.scala | 5 +++++
src/main/scala/leon/plugin/CodeExtraction.scala | 1 +
src/main/scala/leon/plugin/Extractors.scala | 7 +++++++
src/main/scala/leon/purescala/PrettyPrinter.scala | 1 +
src/main/scala/leon/purescala/Trees.scala | 4 ++++
7 files changed, 36 insertions(+)
create mode 100644 mytest/Even.scala
diff --git a/mytest/Even.scala b/mytest/Even.scala
new file mode 100644
index 000000000..f1fdfdce4
--- /dev/null
+++ b/mytest/Even.scala
@@ -0,0 +1,14 @@
+import leon.Utils._
+
+object Even {
+
+ //def getEven: Int = {
+ // val e = epsilon((i: Int) => true)
+ // e + e
+ //}) ensuring(isEven(_))
+
+ def double(i: Int): Int = (2*i) ensuring (isEven(_))
+
+ def isEven(i: Int): Boolean = i % 2 == 0
+
+}
diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
index aec3acfa1..bd01412c2 100644
--- a/src/main/scala/leon/Evaluator.scala
+++ b/src/main/scala/leon/Evaluator.scala
@@ -167,6 +167,10 @@ object Evaluator {
case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 / i2)
case (le,re) => throw TypeErrorEx(TypeError(le, Int32Type))
}
+ case Modulo(l,r) => (rec(ctx,l), rec(ctx,r)) match {
+ case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 % i2)
+ case (le,re) => throw TypeErrorEx(TypeError(le, Int32Type))
+ }
case LessThan(l,r) => (rec(ctx,l), rec(ctx,r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 < i2)
case (le,re) => throw TypeErrorEx(TypeError(le, Int32Type))
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 390a72ee9..549f18f97 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -903,6 +903,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
case Minus(l, r) => if(USEBV) z3.mkBVSub(rec(l), rec(r)) else z3.mkSub(rec(l), rec(r))
case Times(l, r) => if(USEBV) z3.mkBVMul(rec(l), rec(r)) else z3.mkMul(rec(l), rec(r))
case Division(l, r) => if(USEBV) z3.mkBVSdiv(rec(l), rec(r)) else z3.mkDiv(rec(l), rec(r))
+ case Modulo(l, r) => if(USEBV) sys.error("I don't know what to do here!") else z3.mkMod(rec(l), rec(r))
case UMinus(e) => if(USEBV) z3.mkBVNeg(rec(e)) else z3.mkUnaryMinus(rec(e))
case LessThan(l, r) => if(USEBV) z3.mkBVSlt(rec(l), rec(r)) else z3.mkLT(rec(l), rec(r))
case LessEquals(l, r) => if(USEBV) z3.mkBVSle(rec(l), rec(r)) else z3.mkLE(rec(l), rec(r))
@@ -1112,6 +1113,10 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
assert(argsSize == 2)
Division(rargs(0), rargs(1))
}
+ case OpMod => {
+ assert(argsSize == 2)
+ Modulo(rargs(0), rargs(1))
+ }
case OpAsArray => {
assert(argsSize == 0)
throw new Exception("encountered OpAsArray")
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 1930fc7a0..f1cfeb44c 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -402,6 +402,7 @@ trait CodeExtraction extends Extractors {
case ExMinus(l, r) => Minus(rec(l), rec(r)).setType(Int32Type)
case ExTimes(l, r) => Times(rec(l), rec(r)).setType(Int32Type)
case ExDiv(l, r) => Division(rec(l), rec(r)).setType(Int32Type)
+ case ExMod(l, r) => Modulo(rec(l), rec(r)).setType(Int32Type)
case ExEquals(l, r) => {
val rl = rec(l)
val rr = rec(r)
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index ee684e97a..6985e9b8f 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -315,6 +315,13 @@ trait Extractors {
}
}
+ object ExMod {
+ def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
+ case Apply(Select(lhs, n), List(rhs)) if (n == nme.MOD) => Some((lhs,rhs))
+ case _ => None
+ }
+ }
+
object ExLocalCall {
def unapply(tree: Apply): Option[(Symbol,String,List[Tree])] = tree match {
case a @ Apply(Select(This(_), nme), args) => Some((a.symbol, nme.toString, args))
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index c5d2d7158..b28cd76c1 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -135,6 +135,7 @@ object PrettyPrinter {
case Minus(l,r) => ppBinary(sb, l, r, " - ", lvl)
case Times(l,r) => ppBinary(sb, l, r, " * ", lvl)
case Division(l,r) => ppBinary(sb, l, r, " / ", lvl)
+ case Modulo(l,r) => ppBinary(sb, l, r, " % ", lvl)
case LessThan(l,r) => ppBinary(sb, l, r, " < ", lvl)
case GreaterThan(l,r) => ppBinary(sb, l, r, " > ", lvl)
case LessEquals(l,r) => ppBinary(sb, l, r, " \u2264 ", lvl) // \leq
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 7a289934a..4d40b99a2 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -261,6 +261,9 @@ object Trees {
case class Division(lhs: Expr, rhs: Expr) extends Expr with FixedType {
val fixedType = Int32Type
}
+ case class Modulo(lhs: Expr, rhs: Expr) extends Expr with FixedType {
+ val fixedType = Int32Type
+ }
case class LessThan(lhs: Expr, rhs: Expr) extends Expr with FixedType {
val fixedType = BooleanType
}
@@ -367,6 +370,7 @@ object Trees {
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 Modulo(t1,t2) => Some((t1,t2,Modulo))
case LessThan(t1,t2) => Some((t1,t2,LessThan))
case GreaterThan(t1,t2) => Some((t1,t2,GreaterThan))
case LessEquals(t1,t2) => Some((t1,t2,LessEquals))
--
GitLab