diff --git a/library/collection/List.scala b/library/collection/List.scala
index c9ebac9d3590d9b4831097342d556022a9ced95b..f4ab47a45ee75e571242c6b7bf72cbd8ec35e270 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -8,8 +8,8 @@ import leon.annotation._
@library
sealed abstract class List[T] {
- def size: Int = (this match {
- case Nil() => 0
+ def size: BigInt = (this match {
+ case Nil() => BigInt(0)
case Cons(h, t) => 1 + t.size
}) ensuring (_ >= 0)
@@ -43,9 +43,9 @@ sealed abstract class List[T] {
}
}
- def apply(index: Int): T = {
+ def apply(index: BigInt): T = {
require(0 <= index && index < size)
- if (index == 0) {
+ if (index == BigInt(0)) {
head
} else {
tail(index-1)
@@ -68,27 +68,27 @@ sealed abstract class List[T] {
}
} ensuring (res => (res.size == size) && (res.content == content))
- def take(i: Int): List[T] = (this, i) match {
+ def take(i: BigInt): List[T] = (this, i) match {
case (Nil(), _) => Nil()
case (Cons(h, t), i) =>
- if (i == 0) {
+ if (i == BigInt(0)) {
Nil()
} else {
Cons(h, t.take(i-1))
}
}
- def drop(i: Int): List[T] = (this, i) match {
+ def drop(i: BigInt): List[T] = (this, i) match {
case (Nil(), _) => Nil()
case (Cons(h, t), i) =>
- if (i == 0) {
+ if (i == BigInt(0)) {
Cons(h, t)
} else {
t.drop(i-1)
}
}
- def slice(from: Int, to: Int): List[T] = {
+ def slice(from: BigInt, to: BigInt): List[T] = {
require(from < to && to < size && from >= 0)
drop(from).take(to-from)
}
@@ -104,7 +104,7 @@ sealed abstract class List[T] {
}
}
- private def chunk0(s: Int, l: List[T], acc: List[T], res: List[List[T]], s0: Int): List[List[T]] = l match {
+ private def chunk0(s: BigInt, l: List[T], acc: List[T], res: List[List[T]], s0: BigInt): List[List[T]] = l match {
case Nil() =>
if (acc.size > 0) {
res :+ acc
@@ -112,14 +112,14 @@ sealed abstract class List[T] {
res
}
case Cons(h, t) =>
- if (s0 == 0) {
+ if (s0 == BigInt(0)) {
chunk0(s, l, Nil(), res :+ acc, s)
} else {
chunk0(s, t, acc :+ h, res, s0-1)
}
}
- def chunks(s: Int): List[List[T]] = {
+ def chunks(s: BigInt): List[List[T]] = {
require(s > 0)
chunk0(s, this, Nil(), Nil(), s)
@@ -165,7 +165,7 @@ sealed abstract class List[T] {
Nil()
}
- def pad(s: Int, e: T): List[T] = (this, s) match {
+ def pad(s: BigInt, e: T): List[T] = (this, s) match {
case (_, s) if s <= 0 =>
this
case (Nil(), s) =>
@@ -174,7 +174,7 @@ sealed abstract class List[T] {
Cons(h, t.pad(s-1, e))
}
- def find(e: T): Option[Int] = this match {
+ def find(e: T): Option[BigInt] = this match {
case Nil() => None()
case Cons(h, t) =>
if (h == e) {
@@ -194,7 +194,7 @@ sealed abstract class List[T] {
Cons[T](h, t.init)
case Nil() =>
Nil[T]()
- }) ensuring ( (r: List[T]) => ((r.size < this.size) || (this.size == 0)) )
+ }) ensuring ( (r: List[T]) => ((r.size < this.size) || (this.size == BigInt(0))) )
def lastOption: Option[T] = this match {
case Cons(h, t) =>
@@ -230,7 +230,7 @@ sealed abstract class List[T] {
Cons(Nil(), Nil())
}
- def count(e: T): Int = this match {
+ def count(e: T): BigInt = this match {
case Cons(h, t) =>
if (h == e) {
1 + t.count(e)
@@ -238,7 +238,7 @@ sealed abstract class List[T] {
t.count(e)
}
case Nil() =>
- 0
+ BigInt(0)
}
def evenSplit: (List[T], List[T]) = {
@@ -246,10 +246,10 @@ sealed abstract class List[T] {
(take(c), drop(c))
}
- def insertAt(pos: Int, l: List[T]): List[T] = {
+ def insertAt(pos: BigInt, l: List[T]): List[T] = {
if(pos < 0) {
insertAt(size + pos, l)
- } else if(pos == 0) {
+ } else if(pos == BigInt(0)) {
l ++ this
} else {
this match {
@@ -261,10 +261,10 @@ sealed abstract class List[T] {
}
}
- def replaceAt(pos: Int, l: List[T]): List[T] = {
+ def replaceAt(pos: BigInt, l: List[T]): List[T] = {
if(pos < 0) {
replaceAt(size + pos, l)
- } else if(pos == 0) {
+ } else if(pos == BigInt(0)) {
l ++ this.drop(l.size)
} else {
this match {
@@ -276,7 +276,7 @@ sealed abstract class List[T] {
}
}
- def rotate(s: Int): List[T] = {
+ def rotate(s: BigInt): List[T] = {
if (s < 0) {
rotate(size+s)
} else {
@@ -304,19 +304,19 @@ object ListOps {
case Nil() => Nil()
}
- def isSorted(ls: List[Int]): Boolean = ls match {
+ def isSorted(ls: List[BigInt]): Boolean = ls match {
case Nil() => true
case Cons(_, Nil()) => true
case Cons(h1, Cons(h2, _)) if(h1 > h2) => false
case Cons(_, t) => isSorted(t)
}
- def sorted(ls: List[Int]): List[Int] = ls match {
+ def sorted(ls: List[BigInt]): List[BigInt] = ls match {
case Cons(h, t) => insSort(sorted(t), h)
case Nil() => Nil()
}
- def insSort(ls: List[Int], v: Int): List[Int] = ls match {
+ def insSort(ls: List[BigInt], v: BigInt): List[BigInt] = ls match {
case Nil() => Cons(v, Nil())
case Cons(h, t) =>
if (v <= h) {
@@ -333,7 +333,7 @@ case class Nil[T]() extends List[T]
@library
object ListSpecs {
- def snocIndex[T](l : List[T], t : T, i : Int) : Boolean = {
+ def snocIndex[T](l : List[T], t : T, i : BigInt) : Boolean = {
require(0 <= i && i < l.size + 1)
// proof:
(l match {
@@ -344,7 +344,7 @@ object ListSpecs {
((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
}.holds
- def reverseIndex[T](l : List[T], i : Int) : Boolean = {
+ def reverseIndex[T](l : List[T], i : BigInt) : Boolean = {
require(0 <= i && i < l.size)
(l match {
case Nil() => true
@@ -353,11 +353,11 @@ object ListSpecs {
(l.reverse.apply(i) == l.apply(l.size - 1 - i))
}.holds
- def appendIndex[T](l1 : List[T], l2 : List[T], i : Int) : Boolean = {
+ def appendIndex[T](l1 : List[T], l2 : List[T], i : BigInt) : Boolean = {
require(0 <= i && i < l1.size + l2.size)
(l1 match {
case Nil() => true
- case Cons(x,xs) => if (i==0) true else appendIndex[T](xs,l2,i-1)
+ case Cons(x,xs) => if (i==BigInt(0)) true else appendIndex[T](xs,l2,i-1)
}) &&
((l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)))
}.holds
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index 8a548ecdb009a6bb4c89cbca5b66dc85353b91dd..dbca0c5de0d920cf2b2528fe23c8b52d1123bb11 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -84,6 +84,7 @@ trait CodeGeneration {
/** Return the respective JVM type from a Leon type */
def typeToJVM(tpe : TypeTree) : String = tpe match {
case Int32Type => "I"
+ case IntegerType => "I"
case BooleanType => "Z"
@@ -118,6 +119,7 @@ trait CodeGeneration {
/** Return the respective boxed JVM type from a Leon type */
def typeToJVMBoxed(tpe : TypeTree) : String = tpe match {
case Int32Type => s"L$BoxedIntClass;"
+ case IntegerType => s"L$BoxedIntClass;"
case BooleanType | UnitType => s"L$BoxedBoolClass;"
case CharType => s"L$BoxedCharClass;"
case other => typeToJVM(other)
@@ -190,7 +192,7 @@ trait CodeGeneration {
mkExpr(bodyWithPost, ch)(Locals(newMapping, Map.empty, Map.empty, isStatic))
funDef.returnType match {
- case Int32Type | BooleanType | UnitType =>
+ case IntegerType | Int32Type | BooleanType | UnitType =>
ch << IRETURN
case _ : ClassType | _ : TupleType | _ : SetType | _ : MapType | _ : ArrayType | _ : FunctionType | _ : TypeParameter =>
@@ -218,7 +220,7 @@ trait CodeGeneration {
mkExpr(d, ch)
val slot = ch.getFreshVar
val instr = i.getType match {
- case Int32Type | CharType | BooleanType | UnitType => IStore(slot)
+ case IntegerType | Int32Type | CharType | BooleanType | UnitType => IStore(slot)
case _ => AStore(slot)
}
ch << instr
@@ -226,6 +228,8 @@ trait CodeGeneration {
case IntLiteral(v) =>
ch << Ldc(v)
+ case InfiniteIntegerLiteral(v) =>
+ ch << Ldc(v.toInt)
case CharLiteral(v) =>
ch << Ldc(v)
@@ -562,6 +566,9 @@ trait CodeGeneration {
ch << InvokeSpecial(afName, constructorName, consSig)
// Arithmetic
+ /*
+ * TODO: Correct code generation for infinite precision operations
+ */
case Plus(l, r) =>
mkExpr(l, ch)
mkExpr(r, ch)
@@ -591,6 +598,37 @@ trait CodeGeneration {
mkExpr(e, ch)
ch << INEG
+ //BV arithmetic
+ case BVPlus(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << IADD
+
+ case BVMinus(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << ISUB
+
+ case BVTimes(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << IMUL
+
+ case BVDivision(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << IDIV
+
+ case BVModulo(l, r) =>
+ mkExpr(l, ch)
+ mkExpr(r, ch)
+ ch << IREM
+
+ case BVUMinus(e) =>
+ mkExpr(e, ch)
+ ch << INEG
+
+
case ArrayLength(a) =>
mkExpr(a, ch)
ch << ARRAYLENGTH
@@ -602,6 +640,7 @@ trait CodeGeneration {
case Untyped => throw CompilationException("Cannot compile untyped array access.")
case CharType => CALOAD
case Int32Type => IALOAD
+ case IntegerType => IALOAD
case BooleanType => BALOAD
case _ => AALOAD
})
@@ -613,6 +652,7 @@ trait CodeGeneration {
val storeInstr = a.getType match {
case ArrayType(CharType) => ch << NewArray.primitive("T_CHAR"); CASTORE
case ArrayType(Int32Type) => ch << NewArray.primitive("T_INT"); IASTORE
+ case ArrayType(IntegerType) => ch << NewArray.primitive("T_INT"); IASTORE
case ArrayType(BooleanType) => ch << NewArray.primitive("T_BOOLEAN"); BASTORE
case ArrayType(other) => ch << NewArray(typeToJVM(other)); AASTORE
case other => throw CompilationException("Cannot compile finite array expression whose type is %s.".format(other))
@@ -637,6 +677,7 @@ trait CodeGeneration {
val storeInstr = a.getType match {
case ArrayType(CharType) => ch << NewArray.primitive("T_CHAR"); CASTORE
case ArrayType(Int32Type) => ch << NewArray.primitive("T_INT"); IASTORE
+ case ArrayType(IntegerType) => ch << NewArray.primitive("T_INT"); IASTORE
case ArrayType(BooleanType) => ch << NewArray.primitive("T_BOOLEAN"); BASTORE
case ArrayType(other) => ch << NewArray(typeToJVM(other)); AASTORE
case other => throw CompilationException("Cannot compile finite array expression whose type is %s.".format(other))
@@ -719,6 +760,10 @@ trait CodeGeneration {
ch << New(BoxedIntClass) << DUP
mkExpr(e, ch)
ch << InvokeSpecial(BoxedIntClass, constructorName, "(I)V")
+ case IntegerType =>
+ ch << New(BoxedIntClass) << DUP
+ mkExpr(e, ch)
+ ch << InvokeSpecial(BoxedIntClass, constructorName, "(I)V")
case BooleanType | UnitType =>
ch << New(BoxedBoolClass) << DUP
@@ -746,6 +791,8 @@ trait CodeGeneration {
tpe match {
case Int32Type =>
ch << New(BoxedIntClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedIntClass, constructorName, "(I)V")
+ case IntegerType =>
+ ch << New(BoxedIntClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedIntClass, constructorName, "(I)V")
case BooleanType | UnitType =>
ch << New(BoxedBoolClass) << DUP_X1 << SWAP << InvokeSpecial(BoxedBoolClass, constructorName, "(Z)V")
@@ -764,6 +811,8 @@ trait CodeGeneration {
tpe match {
case Int32Type =>
ch << CheckCast(BoxedIntClass) << InvokeVirtual(BoxedIntClass, "intValue", "()I")
+ case IntegerType =>
+ ch << CheckCast(BoxedIntClass) << InvokeVirtual(BoxedIntClass, "intValue", "()I")
case BooleanType | UnitType =>
ch << CheckCast(BoxedBoolClass) << InvokeVirtual(BoxedBoolClass, "booleanValue", "()Z")
@@ -834,7 +883,7 @@ trait CodeGeneration {
mkExpr(l, ch)
mkExpr(r, ch)
l.getType match {
- case Int32Type | BooleanType | UnitType | CharType =>
+ case Int32Type | IntegerType | BooleanType | UnitType | CharType =>
ch << If_ICmpEq(thenn) << Goto(elze)
case _ =>
@@ -894,7 +943,7 @@ trait CodeGeneration {
case None => locals.varToLocal(id) match {
case Some(slot) =>
val instr = id.getType match {
- case Int32Type | CharType | BooleanType | UnitType => ILoad(slot)
+ case IntegerType | Int32Type | CharType | BooleanType | UnitType => ILoad(slot)
case _ => ALoad(slot)
}
ch << instr
@@ -985,7 +1034,7 @@ trait CodeGeneration {
ch << Label(initLabel) // return lzy
//newValue
lzy.returnType match {
- case Int32Type | BooleanType | UnitType | CharType =>
+ case Int32Type | IntegerType | BooleanType | UnitType | CharType =>
// Since the underlying field only has boxed types, we have to unbox them to return them
mkUnbox(lzy.returnType, ch)(NoLocals(isStatic))
ch << IRETURN
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 5bf34b1f70f3bd0b3ec4e52b3eb9713a17fc7685..b24a5f0f91406a732c99f30cdb3ba86fb9f2606c 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -125,6 +125,8 @@ class CompilationUnit(val ctx: LeonContext,
def exprToJVM(e: Expr)(implicit monitor : LeonCodeGenRuntimeMonitor): AnyRef = e match {
case IntLiteral(v) =>
new java.lang.Integer(v)
+ case InfiniteIntegerLiteral(v) =>
+ new java.lang.Integer(v.toInt)
case BooleanLiteral(v) =>
new java.lang.Boolean(v)
@@ -184,6 +186,8 @@ class CompilationUnit(val ctx: LeonContext,
def jvmToExpr(e: AnyRef, tpe: TypeTree): Expr = (e, tpe) match {
case (i: Integer, Int32Type) =>
IntLiteral(i.toInt)
+ case (i: Integer, IntegerType) =>
+ InfiniteIntegerLiteral(i.toInt)
case (b: java.lang.Boolean, BooleanType) =>
BooleanLiteral(b.booleanValue)
@@ -284,7 +288,7 @@ class CompilationUnit(val ctx: LeonContext,
mkExpr(e, ch)(Locals(newMapping, Map.empty, Map.empty, true))
e.getType match {
- case Int32Type | BooleanType =>
+ case IntegerType | Int32Type | BooleanType =>
ch << IRETURN
case UnitType | _: TupleType | _: SetType | _: MapType | _: AbstractClassType | _: CaseClassType | _: ArrayType | _: FunctionType | _: TypeParameter =>
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 6adab6929b9bac530248f97f769fb53c8e53e4a4..e40af01e948f6fc0f6c15bd182fc6f6e091e7b87 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -23,11 +23,17 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
i -> Constructor[Expr, TypeTree](List(), Int32Type, s => IntLiteral(i), ""+i)
}).toMap
+ val bigInts = (for (i <- Set(0, 1, 2, 3)) yield {
+ i -> Constructor[Expr, TypeTree](List(), IntegerType, s => InfiniteIntegerLiteral(i), ""+i)
+ }).toMap
+
val booleans = (for (b <- Set(true, false)) yield {
b -> Constructor[Expr, TypeTree](List(), BooleanType, s => BooleanLiteral(b), ""+b)
}).toMap
def intConstructor(i: Int) = ints(i)
+
+ def bigIntConstructor(i: Int) = bigInts(i)
def boolConstructor(b: Boolean) = booleans(b)
@@ -133,6 +139,9 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
case (i: Integer, Int32Type) =>
(cPattern(intConstructor(i), List()), true)
+ case (i: Integer, IntegerType) =>
+ (cPattern(bigIntConstructor(i), List()), true)
+
case (b: java.lang.Boolean, BooleanType) =>
(cPattern(boolConstructor(b), List()), true)
@@ -256,7 +265,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
}).flatten
- val gen = new StubGenerator[Expr, TypeTree]((ints.values ++ booleans.values).toSeq,
+ val gen = new StubGenerator[Expr, TypeTree]((ints.values ++ bigInts.values ++ booleans.values).toSeq,
Some(getConstructors _),
treatEmptyStubsAsChildless = true)
@@ -274,7 +283,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
return new Iterator[Seq[Expr]] {
var total = 0
- var found = 0;
+ var found = 0
var theNext: Option[Seq[Expr]] = None
@@ -294,6 +303,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
def computeNext(): Option[Seq[Expr]] = {
+ //return None
while(total < maxEnumerated && found < maxValid && it.hasNext && !interrupted.get) {
val model = it.next.asInstanceOf[Tuple]
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index fa0148b5df985576caa41bddb661d5c26477e0bb..1d060afb63c140889ac5e3dfeb69e83261ad2fd7 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -229,63 +229,106 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
}
case Plus(l,r) =>
+ (e(l), e(r)) match {
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => InfiniteIntegerLiteral(i1 + i2)
+ case (le,re) => throw EvalError(typeErrorMsg(le, IntegerType))
+ }
+
+ case Minus(l,r) =>
+ (e(l), e(r)) match {
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => InfiniteIntegerLiteral(i1 - i2)
+ case (le,re) => throw EvalError(typeErrorMsg(le, IntegerType))
+ }
+
+ case BVPlus(l,r) =>
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 + i2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
- case Minus(l,r) =>
+ case BVMinus(l,r) =>
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 - i2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
case UMinus(ex) =>
+ e(ex) match {
+ case InfiniteIntegerLiteral(i) => InfiniteIntegerLiteral(-i)
+ case re => throw EvalError(typeErrorMsg(re, IntegerType))
+ }
+
+ case BVUMinus(ex) =>
e(ex) match {
case IntLiteral(i) => IntLiteral(-i)
case re => throw EvalError(typeErrorMsg(re, Int32Type))
}
case Times(l,r) =>
+ (e(l), e(r)) match {
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => InfiniteIntegerLiteral(i1 * i2)
+ case (le,re) => throw EvalError(typeErrorMsg(le, IntegerType))
+ }
+
+ case Division(l,r) =>
+ (e(l), e(r)) match {
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) =>
+ if(i2 != 0) InfiniteIntegerLiteral(i1 / i2) else throw RuntimeError("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 != 0) InfiniteIntegerLiteral(i1 % i2) else throw RuntimeError("Modulo by 0.")
+ case (le,re) => throw EvalError(typeErrorMsg(le, IntegerType))
+ }
+
+ case BVTimes(l,r) =>
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 * i2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
- case Division(l,r) =>
+ case BVDivision(l,r) =>
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) =>
if(i2 != 0) IntLiteral(i1 / i2) else throw RuntimeError("Division by 0.")
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
- case Modulo(l,r) =>
+ case BVModulo(l,r) =>
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) =>
if(i2 != 0) IntLiteral(i1 % i2) else throw RuntimeError("Modulo by 0.")
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
+
case LessThan(l,r) =>
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 < i2)
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 < i2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
case GreaterThan(l,r) =>
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 > i2)
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 > i2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
case LessEquals(l,r) =>
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 <= i2)
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 <= i2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
case GreaterEquals(l,r) =>
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 >= i2)
+ case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 >= i2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
@@ -332,6 +375,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case f @ FiniteSet(els) => FiniteSet(els.map(e(_))).setType(f.getType)
case i @ IntLiteral(_) => i
+ case i @ InfiniteIntegerLiteral(_) => i
case b @ BooleanLiteral(_) => b
case u @ UnitLiteral() => u
case l @ Lambda(_, _) => l
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 0424350cf2ae76a1f4e1a9b08d3c95faa156e484..8f9f8b0b7c0e8eec1ac28b6a5b48d3be9bb6735f 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -36,12 +36,15 @@ trait ASTExtractors {
protected lazy val function4TraitSym = classFromName("scala.Function4")
protected lazy val function5TraitSym = classFromName("scala.Function5")
protected lazy val byNameSym = classFromName("scala.<byname>")
+ protected lazy val bigIntSym = classFromName("scala.math.BigInt")
def isTuple2(sym : Symbol) : Boolean = sym == tuple2Sym
def isTuple3(sym : Symbol) : Boolean = sym == tuple3Sym
def isTuple4(sym : Symbol) : Boolean = sym == tuple4Sym
def isTuple5(sym : Symbol) : Boolean = sym == tuple5Sym
+ def isBigIntSym(sym : Symbol) : Boolean = getResolvedTypeSym(sym) == bigIntSym
+
def isByNameSym(sym : Symbol) : Boolean = getResolvedTypeSym(sym) == byNameSym
// Resolve type aliases
@@ -88,6 +91,8 @@ trait ASTExtractors {
val tpe = t.tpe.widen
tpe =:= IntClass.tpe
}
+
+ def hasBigIntType(t : Tree) = isBigIntSym(t.tpe.typeSymbol)
object ExtractorHelpers {
@@ -214,6 +219,24 @@ trait ASTExtractors {
}
}
+ object ExBigIntLiteral {
+ def unapply(tree: Tree): Option[Int] = tree match {
+ case Apply(ExSelected("scala", "package", "BigInt", "apply"), (n: Literal) :: Nil) =>
+ Some(n.value.intValue)
+ case _ =>
+ None
+ }
+ }
+
+
+ object ExIntToBigInt {
+ def unapply(tree: Tree): Option[Tree] = tree match {
+ case Apply(ExSelected("math", "BigInt", "int2bigInt"), tree :: Nil) => Some(tree)
+ case _ => None
+ }
+ }
+
+
object ExListLiteral {
def unapply(tree: Apply): Option[(Tree, List[Tree])] = tree match {
case Apply(
@@ -714,6 +737,13 @@ trait ASTExtractors {
}
object ExUMinus {
+ def unapply(tree: Select): Option[Tree] = tree match {
+ case Select(t, n) if (n == nme.UNARY_- && hasBigIntType(t)) => Some(t)
+ case _ => None
+ }
+ }
+
+ object ExBVUMinus {
def unapply(tree: Select): Option[Tree] = tree match {
case Select(t, n) if (n == nme.UNARY_- && hasIntType(t)) => Some(t)
case _ => None
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 369be0adfbba6ba4dfba7e7229c41785c8ccb4dc..8b63ff7318f6b414715e851bcf8c661021f966a0 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1204,6 +1204,20 @@ trait CodeExtraction extends ASTExtractors {
val newValueRec = extractTree(newValue)
ArrayUpdate(lhsRec, indexRec, newValueRec)
+ case ExBigIntLiteral(n) => {
+ InfiniteIntegerLiteral(BigInt(n))
+ }
+
+ case ExIntToBigInt(tree) => {
+ val rec = extractTree(tree)
+ rec match {
+ case IntLiteral(n) =>
+ InfiniteIntegerLiteral(BigInt(n))
+ case _ =>
+ IntToBigInt(rec)
+ }
+ }
+
case ExInt32Literal(v) =>
IntLiteral(v)
@@ -1314,6 +1328,7 @@ trait CodeExtraction extends ASTExtractors {
case ExNot(e) => Not(extractTree(e))
case ExUMinus(e) => UMinus(extractTree(e))
+ case ExBVUMinus(e) => BVUMinus(extractTree(e))
case ExEquals(l, r) =>
val rl = extractTree(l)
@@ -1457,6 +1472,8 @@ trait CodeExtraction extends ASTExtractors {
CaseClass(CaseClassType(libraryCaseClass(str.pos, "leon.lang.string.String"), Seq()), Seq(charList))
+
+
case c @ ExCall(rec, sym, tps, args) =>
val rrec = rec match {
case t if (defsToDefs contains sym) && !isMethod(sym) =>
@@ -1499,21 +1516,43 @@ trait CodeExtraction extends ASTExtractors {
case (a1, "!=", List(a2)) =>
Not(Equals(a1, a2))
+ //BigInt methods
+ case (IsTyped(a1, IntegerType), "+", List(IsTyped(a2, IntegerType))) =>
+ Plus(a1, a2)
+ case (IsTyped(a1, IntegerType), "-", List(IsTyped(a2, IntegerType))) =>
+ Minus(a1, a2)
+ case (IsTyped(a1, IntegerType), "*", List(IsTyped(a2, IntegerType))) =>
+ Times(a1, a2)
+ case (IsTyped(a1, IntegerType), "%", List(IsTyped(a2, IntegerType))) =>
+ Modulo(a1, a2)
+ case (IsTyped(a1, IntegerType), "/", List(IsTyped(a2, IntegerType))) =>
+ Division(a1, a2)
+ case (IsTyped(a1, IntegerType), ">", List(IsTyped(a2, IntegerType))) =>
+ GreaterThan(a1, a2)
+ case (IsTyped(a1, IntegerType), ">=", List(IsTyped(a2, IntegerType))) =>
+ GreaterEquals(a1, a2)
+ case (IsTyped(a1, IntegerType), "<", List(IsTyped(a2, IntegerType))) =>
+ LessThan(a1, a2)
+ case (IsTyped(a1, IntegerType), "<=", List(IsTyped(a2, IntegerType))) =>
+ LessEquals(a1, a2)
+ case (IsTyped(a1, IntegerType), "<=", List(IsTyped(a2, IntegerType))) =>
+ LessEquals(a1, a2)
+
// Int methods
case (IsTyped(a1, Int32Type), "+", List(IsTyped(a2, Int32Type))) =>
- Plus(a1, a2)
+ BVPlus(a1, a2)
case (IsTyped(a1, Int32Type), "-", List(IsTyped(a2, Int32Type))) =>
- Minus(a1, a2)
+ BVMinus(a1, a2)
case (IsTyped(a1, Int32Type), "*", List(IsTyped(a2, Int32Type))) =>
- Times(a1, a2)
+ BVTimes(a1, a2)
case (IsTyped(a1, Int32Type), "%", List(IsTyped(a2, Int32Type))) =>
- Modulo(a1, a2)
+ BVModulo(a1, a2)
case (IsTyped(a1, Int32Type), "/", List(IsTyped(a2, Int32Type))) =>
- Division(a1, a2)
+ BVDivision(a1, a2)
case (IsTyped(a1, Int32Type), ">", List(IsTyped(a2, Int32Type))) =>
GreaterThan(a1, a2)
@@ -1642,6 +1681,9 @@ trait CodeExtraction extends ASTExtractors {
case tpe if tpe == NothingClass.tpe =>
Untyped
+ case TypeRef(_, sym, _) if isBigIntSym(sym) =>
+ IntegerType
+
case TypeRef(_, sym, btt :: Nil) if isSetTraitSym(sym) =>
SetType(extractType(btt))
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index f2cd6bc079b83e5eb8f4dc24ddaf0bf98c89ad87..a62521d84f17c91e62039514a3bb2a200080c79f 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -18,6 +18,7 @@ object Extractors {
def unapply(expr: Expr) : Option[(Expr,(Expr)=>Expr)] = expr match {
case Not(t) => Some((t,Not(_)))
case UMinus(t) => Some((t,UMinus))
+ case BVUMinus(t) => Some((t,BVUMinus))
case SetCardinality(t) => Some((t,SetCardinality))
case MultisetCardinality(t) => Some((t,MultisetCardinality))
case MultisetToSet(t) => Some((t,MultisetToSet))
@@ -51,6 +52,11 @@ object Extractors {
case GreaterThan(t1,t2) => Some((t1,t2,GreaterThan))
case LessEquals(t1,t2) => Some((t1,t2,LessEquals))
case GreaterEquals(t1,t2) => Some((t1,t2,GreaterEquals))
+ case BVPlus(t1,t2) => Some((t1,t2,BVPlus))
+ 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 ElementOfSet(t1,t2) => Some((t1,t2,ElementOfSet))
case SubsetOf(t1,t2) => Some((t1,t2,SubsetOf))
case SetIntersection(t1,t2) => Some((t1,t2,SetIntersection))
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 8127e0af690531b2f1dd8af443661b9411ad24ed..baa1a2c203f941d782213b136b33a8fb24969c55 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -269,8 +269,10 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case Not(Equals(l, r)) => optP { p"$l \u2260 $r" }
case Implies(l,r) => optP { p"$l ==> $r" }
case UMinus(expr) => p"-$expr"
+ case BVUMinus(expr) => p"-$expr"
case Equals(l,r) => optP { p"$l == $r" }
case IntLiteral(v) => p"$v"
+ case InfiniteIntegerLiteral(v) => p"BigInt($v)"
case CharLiteral(v) => p"$v"
case BooleanLiteral(v) => p"$v"
case StringLiteral(s) => p""""$s""""
@@ -341,6 +343,11 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case GreaterThan(l,r) => optP { p"$l > $r" }
case LessEquals(l,r) => optP { p"$l <= $r" }
case GreaterEquals(l,r) => optP { p"$l >= $r" }
+ case BVPlus(l,r) => optP { p"$l + $r" }
+ 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 FiniteSet(rs) => p"{${rs.toSeq}}"
case FiniteMultiset(rs) => p"{|$rs|)"
case EmptyMultiset(_) => p"\u2205"
@@ -379,7 +386,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
s match {
case IntLiteral(length) => {
if(es.size == length) {
- val orderedElements = es.toSeq.sortWith((e1, e2) => e1._1 < e2._1)
+ val orderedElements = es.toSeq.sortWith((e1, e2) => e1._1 < e2._1).map(el => el._2)
p"Array($orderedElements)"
} else if(length < 10) {
val elems = (0 until length).map(i =>
@@ -487,6 +494,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe
case Untyped => p"<untyped>"
case UnitType => p"Unit"
case Int32Type => p"Int"
+ case IntegerType => p"BigInt"
case CharType => p"Char"
case BooleanType => p"Boolean"
case ArrayType(bt) => p"Array[$bt]"
@@ -697,8 +705,8 @@ 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 | _: Minus | _: SetUnion| _: SetDifference | BinaryMethodCall(_, "+" | "-", _)) => 6
- case (_: Times | _: Division | _: Modulo | BinaryMethodCall(_, "*" | "/", _)) => 7
+ case (_: Plus | _: BVPlus | _: Minus | _: BVMinus | _: SetUnion| _: SetDifference | BinaryMethodCall(_, "+" | "-", _)) => 6
+ case (_: Times | _: BVTimes | _: Division | _: BVDivision | _: Modulo | _: BVModulo | BinaryMethodCall(_, "*" | "/", _)) => 7
case _ => 7
}
diff --git a/src/main/scala/leon/purescala/TreeNormalizations.scala b/src/main/scala/leon/purescala/TreeNormalizations.scala
index 2f080d93e6f617d6dce1258e6407a1d129d95cc3..3558ad5984eae73f95a7b00ab6d8ea870ac73fc1 100644
--- a/src/main/scala/leon/purescala/TreeNormalizations.scala
+++ b/src/main/scala/leon/purescala/TreeNormalizations.scala
@@ -24,34 +24,34 @@ object TreeNormalizations {
//assume the expr is a literal (mult of constants and variables) with degree one
def extractCoef(e: Expr): (Expr, Identifier) = {
var id: Option[Identifier] = None
- var coef = 1
+ var coef: BigInt = 1
def rec(e: Expr): Unit = e match {
- case IntLiteral(i) => coef = coef*i
+ case InfiniteIntegerLiteral(i) => coef = coef*i
case Variable(id2) => if(id.isEmpty) id = Some(id2) else throw NonLinearExpressionException("multiple variable")
case Times(e1, e2) => rec(e1); rec(e2)
}
rec(e)
assert(!id.isEmpty)
- (IntLiteral(coef), id.get)
+ (InfiniteIntegerLiteral(coef), id.get)
}
def containsId(e: Expr, id: Identifier): Boolean = e match {
case Times(e1, e2) => containsId(e1, id) || containsId(e2, id)
- case IntLiteral(_) => false
+ case InfiniteIntegerLiteral(_) => false
case Variable(id2) => id == id2
case err => throw NonLinearExpressionException("unexpected in containsId: " + err)
}
def group(es: Seq[Expr], id: Identifier): Expr = {
- val totalCoef = es.foldLeft(0)((acc, e) => {
- val (IntLiteral(i), id2) = extractCoef(e)
+ val totalCoef = es.foldLeft(BigInt(0))((acc, e) => {
+ val (InfiniteIntegerLiteral(i), id2) = extractCoef(e)
assert(id2 == id)
acc + i
})
- Times(IntLiteral(totalCoef), Variable(id))
+ Times(InfiniteIntegerLiteral(totalCoef), Variable(id))
}
var exprs: Seq[Expr] = expandedForm(expr)
@@ -64,7 +64,7 @@ object TreeNormalizations {
res(index+1) = coef
}}
- res(0) = simplifyArithmetic(exprs.foldLeft[Expr](IntLiteral(0))(Plus(_, _)))
+ res(0) = simplifyArithmetic(exprs.foldLeft[Expr](InfiniteIntegerLiteral(0))(Plus(_, _)))
res
}
@@ -78,11 +78,11 @@ object TreeNormalizations {
//do not keep the evaluation order
def expandedForm(expr: Expr): Seq[Expr] = expr match {
case Plus(es1, es2) => expandedForm(es1) ++ expandedForm(es2)
- case Minus(e1, e2) => expandedForm(e1) ++ expandedForm(e2).map(Times(IntLiteral(-1), _): Expr)
- case UMinus(e) => expandedForm(e).map(Times(IntLiteral(-1), _): Expr)
+ case Minus(e1, e2) => expandedForm(e1) ++ expandedForm(e2).map(Times(InfiniteIntegerLiteral(-1), _): Expr)
+ case UMinus(e) => expandedForm(e).map(Times(InfiniteIntegerLiteral(-1), _): Expr)
case Times(es1, es2) => multiply(expandedForm(es1), expandedForm(es2))
- case v@Variable(_) if v.getType == Int32Type => Seq(v)
- case n@IntLiteral(_) => Seq(n)
+ case v@Variable(_) if v.getType == IntegerType => Seq(v)
+ case n@InfiniteIntegerLiteral(_) => Seq(n)
case err => throw NonLinearExpressionException("unexpected in expandedForm: " + err)
}
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index a0313c5dc878fa0f46a9348ccfbbdb02cc45b755..1a256bc82cc197514403703bdd52173aed42e30a 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -998,6 +998,7 @@ object TreeOps {
*/
def simplestValue(tpe: TypeTree) : Expr = tpe match {
case Int32Type => IntLiteral(0)
+ case IntegerType => InfiniteIntegerLiteral(0)
case CharType => CharLiteral('a')
case BooleanType => BooleanLiteral(false)
case UnitType => UnitLiteral()
@@ -1295,7 +1296,7 @@ object TreeOps {
} else {
None
}
- case Untyped | BooleanType | Int32Type | UnitType | TypeParameter(_) => None
+ case Untyped | BooleanType | Int32Type | IntegerType | UnitType | TypeParameter(_) => None
}
var idMap = Map[Identifier, Identifier]()
@@ -1430,45 +1431,45 @@ object TreeOps {
*/
def simplifyArithmetic(expr: Expr): Expr = {
def simplify0(expr: Expr): Expr = (expr match {
- case Plus(IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 + i2)
- case Plus(IntLiteral(0), e) => e
- case Plus(e, IntLiteral(0)) => e
+ case Plus(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => InfiniteIntegerLiteral(i1 + i2)
+ case Plus(InfiniteIntegerLiteral(zero), e) if zero == BigInt(0) => e
+ case Plus(e, InfiniteIntegerLiteral(zero)) if zero == BigInt(0) => e
case Plus(e1, UMinus(e2)) => Minus(e1, e2)
- case Plus(Plus(e, IntLiteral(i1)), IntLiteral(i2)) => Plus(e, IntLiteral(i1+i2))
- case Plus(Plus(IntLiteral(i1), e), IntLiteral(i2)) => Plus(IntLiteral(i1+i2), e)
+ case Plus(Plus(e, InfiniteIntegerLiteral(i1)), InfiniteIntegerLiteral(i2)) => Plus(e, InfiniteIntegerLiteral(i1+i2))
+ case Plus(Plus(InfiniteIntegerLiteral(i1), e), InfiniteIntegerLiteral(i2)) => Plus(InfiniteIntegerLiteral(i1+i2), e)
- case Minus(e, IntLiteral(0)) => e
- case Minus(IntLiteral(0), e) => UMinus(e)
- case Minus(IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 - i2)
+ case Minus(e, InfiniteIntegerLiteral(zero)) if zero == BigInt(0) => e
+ case Minus(InfiniteIntegerLiteral(zero), e) if zero == BigInt(0) => UMinus(e)
+ case Minus(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => InfiniteIntegerLiteral(i1 - i2)
case Minus(e1, UMinus(e2)) => Plus(e1, e2)
case Minus(e1, Minus(UMinus(e2), e3)) => Plus(e1, Plus(e2, e3))
- case UMinus(IntLiteral(x)) => IntLiteral(-x)
+ case UMinus(InfiniteIntegerLiteral(x)) => InfiniteIntegerLiteral(-x)
case UMinus(UMinus(x)) => x
case UMinus(Plus(UMinus(e1), e2)) => Plus(e1, UMinus(e2))
case UMinus(Minus(e1, e2)) => Minus(e2, e1)
- case Times(IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 * i2)
- case Times(IntLiteral(1), e) => e
- case Times(IntLiteral(-1), e) => UMinus(e)
- case Times(e, IntLiteral(1)) => e
- case Times(IntLiteral(0), _) => IntLiteral(0)
- case Times(_, IntLiteral(0)) => IntLiteral(0)
- case Times(IntLiteral(i1), Times(IntLiteral(i2), t)) => Times(IntLiteral(i1*i2), t)
- case Times(IntLiteral(i1), Times(t, IntLiteral(i2))) => Times(IntLiteral(i1*i2), t)
- case Times(IntLiteral(i), UMinus(e)) => Times(IntLiteral(-i), e)
- case Times(UMinus(e), IntLiteral(i)) => Times(e, IntLiteral(-i))
- case Times(IntLiteral(i1), Division(e, IntLiteral(i2))) if i2 != 0 && i1 % i2 == 0 => Times(IntLiteral(i1/i2), e)
-
- case Division(IntLiteral(i1), IntLiteral(i2)) if i2 != 0 => IntLiteral(i1 / i2)
- case Division(e, IntLiteral(1)) => e
+ case Times(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => InfiniteIntegerLiteral(i1 * i2)
+ case Times(InfiniteIntegerLiteral(one), e) if one == BigInt(1) => e
+ case Times(InfiniteIntegerLiteral(mone), e) if mone == BigInt(-1) => UMinus(e)
+ case Times(e, InfiniteIntegerLiteral(one)) if one == BigInt(1) => e
+ case Times(InfiniteIntegerLiteral(zero), _) if zero == BigInt(0) => InfiniteIntegerLiteral(0)
+ case Times(_, InfiniteIntegerLiteral(zero)) if zero == BigInt(0) => InfiniteIntegerLiteral(0)
+ case Times(InfiniteIntegerLiteral(i1), Times(InfiniteIntegerLiteral(i2), t)) => Times(InfiniteIntegerLiteral(i1*i2), t)
+ case Times(InfiniteIntegerLiteral(i1), Times(t, InfiniteIntegerLiteral(i2))) => Times(InfiniteIntegerLiteral(i1*i2), t)
+ case Times(InfiniteIntegerLiteral(i), UMinus(e)) => Times(InfiniteIntegerLiteral(-i), e)
+ case Times(UMinus(e), InfiniteIntegerLiteral(i)) => Times(e, InfiniteIntegerLiteral(-i))
+ case Times(InfiniteIntegerLiteral(i1), Division(e, InfiniteIntegerLiteral(i2))) if i2 != BigInt(0) && i1 % i2 == BigInt(0) => Times(InfiniteIntegerLiteral(i1/i2), e)
+
+ case Division(InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) if i2 != BigInt(0) => InfiniteIntegerLiteral(i1 / i2)
+ case Division(e, InfiniteIntegerLiteral(one)) if one == BigInt(1) => e
//here we put more expensive rules
//btw, I know those are not the most general rules, but they lead to good optimizations :)
case Plus(UMinus(Plus(e1, e2)), e3) if e1 == e3 => UMinus(e2)
case Plus(UMinus(Plus(e1, e2)), e3) if e2 == e3 => UMinus(e1)
- case Minus(e1, e2) if e1 == e2 => IntLiteral(0)
- case Minus(Plus(e1, e2), Plus(e3, e4)) if e1 == e4 && e2 == e3 => IntLiteral(0)
+ case Minus(e1, e2) if e1 == e2 => InfiniteIntegerLiteral(0)
+ case Minus(Plus(e1, e2), Plus(e3, e4)) if e1 == e4 && e2 == e3 => InfiniteIntegerLiteral(0)
case Minus(Plus(e1, e2), Plus(Plus(e3, e4), e5)) if e1 == e4 && e2 == e3 => UMinus(e5)
//default
@@ -1899,8 +1900,8 @@ object TreeOps {
val expr0 = try {
val freeVars: Array[Identifier] = variablesOf(expr).toArray
val coefs: Array[Expr] = TreeNormalizations.linearArithmeticForm(expr, freeVars)
- coefs.toList.zip(IntLiteral(1) :: freeVars.toList.map(Variable(_))).foldLeft[Expr](IntLiteral(0))((acc, t) => {
- if(t._1 == IntLiteral(0)) acc else Plus(acc, Times(t._1, t._2))
+ coefs.toList.zip(InfiniteIntegerLiteral(1) :: freeVars.toList.map(Variable(_))).foldLeft[Expr](InfiniteIntegerLiteral(0))((acc, t) => {
+ if(t._1 == InfiniteIntegerLiteral(0)) acc else Plus(acc, Times(t._1, t._2))
})
} catch {
case _: Throwable =>
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 5879c42da0a7d30fde9fcb669c0766d4edc6db28..eeb15220ff7a5ed27d7579bf8f0a9c8cb5ab4e01 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -255,6 +255,9 @@ object Trees {
case class IntLiteral(value: Int) extends Literal[Int] {
val getType = Int32Type
}
+ case class InfiniteIntegerLiteral(value: BigInt) extends Literal[BigInt] {
+ val getType = IntegerType
+ }
case class BooleanLiteral(value: Boolean) extends Literal[Boolean] {
val getType = BooleanType
@@ -307,22 +310,28 @@ object Trees {
/* Arithmetic */
case class Plus(lhs: Expr, rhs: Expr) extends Expr {
- val getType = Int32Type
+ require(lhs.getType == IntegerType && rhs.getType == IntegerType)
+ val getType = IntegerType
}
case class Minus(lhs: Expr, rhs: Expr) extends Expr {
- val getType = Int32Type
+ require(lhs.getType == IntegerType && rhs.getType == IntegerType)
+ val getType = IntegerType
}
case class UMinus(expr: Expr) extends Expr {
- val getType = Int32Type
+ require(expr.getType == IntegerType)
+ val getType = IntegerType
}
case class Times(lhs: Expr, rhs: Expr) extends Expr {
- val getType = Int32Type
+ require(lhs.getType == IntegerType && rhs.getType == IntegerType)
+ val getType = IntegerType
}
case class Division(lhs: Expr, rhs: Expr) extends Expr {
- val getType = Int32Type
+ require(lhs.getType == IntegerType && rhs.getType == IntegerType)
+ val getType = IntegerType
}
case class Modulo(lhs: Expr, rhs: Expr) extends Expr {
- val getType = Int32Type
+ require(lhs.getType == IntegerType && rhs.getType == IntegerType)
+ val getType = IntegerType
}
case class LessThan(lhs: Expr, rhs: Expr) extends Expr {
val getType = BooleanType
@@ -337,6 +346,36 @@ object Trees {
val getType = BooleanType
}
+ /* Bit-vector arithmetic */
+ case class BVPlus(lhs: Expr, rhs: Expr) extends Expr {
+ require(lhs.getType == Int32Type && rhs.getType == Int32Type)
+ val getType = Int32Type
+ }
+ case class BVMinus(lhs: Expr, rhs: Expr) extends Expr {
+ require(lhs.getType == Int32Type && rhs.getType == Int32Type)
+ val getType = Int32Type
+ }
+ case class BVUMinus(expr: Expr) extends Expr {
+ require(expr.getType == Int32Type)
+ val getType = Int32Type
+ }
+ case class BVTimes(lhs: Expr, rhs: Expr) extends Expr {
+ require(lhs.getType == Int32Type && rhs.getType == Int32Type)
+ val getType = Int32Type
+ }
+ case class BVDivision(lhs: Expr, rhs: Expr) extends Expr {
+ require(lhs.getType == Int32Type && rhs.getType == Int32Type)
+ val getType = Int32Type
+ }
+ case class BVModulo(lhs: Expr, rhs: Expr) extends Expr {
+ require(lhs.getType == Int32Type && rhs.getType == Int32Type)
+ val getType = Int32Type
+ }
+
+ case class IntToBigInt(expr: Expr) extends Expr {
+ val getType = Int32Type
+ }
+
/* Set expressions */
case class FiniteSet(elements: Set[Expr]) extends Expr with MutableTyped {
val tpe = if (elements.isEmpty) None else leastUpperBound(elements.toSeq.map(_.getType))
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 2cc6591ca6d4ad1dd0cd2b37eceb675d264b69d5..05c90501e95f62dc5c7020b22ffd0260223a8df0 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -56,9 +56,12 @@ object TypeTrees {
case object Untyped extends TypeTree
case object BooleanType extends TypeTree
- case object Int32Type extends TypeTree
case object UnitType extends TypeTree
case object CharType extends TypeTree
+ case object IntegerType extends TypeTree
+
+ case class BitVectorType(size: Int) extends TypeTree
+ case object Int32Type extends TypeTree
case class TypeParameter(id: Identifier) extends TypeTree {
def freshen = TypeParameter(id.freshen)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index f754744b271f96e8c125bc0d955477c70a97d5a0..0c69b047b7190194f32bfd74b962c8b2583728df 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -95,7 +95,8 @@ trait SMTLIBTarget {
sorts.cachedB(tpe) {
tpe match {
case BooleanType => Core.BoolSort()
- case Int32Type => Ints.IntSort()
+ case IntegerType => Ints.IntSort()
+ case Int32Type => FixedSizeBitVectors.BitVectorSort(32)
case CharType => FixedSizeBitVectors.BitVectorSort(32)
case RawArrayType(from, to) =>
@@ -331,7 +332,8 @@ trait SMTLIBTarget {
declareVariable(FreshIdentifier("Unit").setType(UnitType))
- case IntLiteral(i) => if (i > 0) Ints.NumeralLit(i) else Ints.Neg(Ints.NumeralLit(-i))
+ case InfiniteIntegerLiteral(i) => if (i > 0) Ints.NumeralLit(i) else Ints.Neg(Ints.NumeralLit(-i))
+ case IntLiteral(i) => FixedSizeBitVectors.BitVectorLit(Hexadecimal.fromInt(i))
case CharLiteral(c) => FixedSizeBitVectors.BitVectorLit(Hexadecimal.fromInt(c.toInt))
case BooleanLiteral(v) => Core.BoolConst(v)
case StringLiteral(s) => SString(s)
@@ -452,10 +454,27 @@ trait SMTLIBTarget {
case (_: Times) => Ints.Mul(toSMT(a), toSMT(b))
case (_: Division) => Ints.Div(toSMT(a), toSMT(b))
case (_: Modulo) => Ints.Mod(toSMT(a), toSMT(b))
- case (_: LessThan) => Ints.LessThan(toSMT(a), toSMT(b))
- case (_: LessEquals) => Ints.LessEquals(toSMT(a), toSMT(b))
- case (_: GreaterThan) => Ints.GreaterThan(toSMT(a), toSMT(b))
- case (_: GreaterEquals) => Ints.GreaterEquals(toSMT(a), toSMT(b))
+ case (_: LessThan) => a.getType match {
+ case Int32Type => FixedSizeBitVectors.SLessThan(toSMT(a), toSMT(b))
+ case IntegerType => Ints.LessThan(toSMT(a), toSMT(b))
+ }
+ case (_: LessEquals) => a.getType match {
+ case Int32Type => FixedSizeBitVectors.SLessEquals(toSMT(a), toSMT(b))
+ case IntegerType => Ints.LessEquals(toSMT(a), toSMT(b))
+ }
+ case (_: GreaterThan) => a.getType match {
+ case Int32Type => FixedSizeBitVectors.SGreaterThan(toSMT(a), toSMT(b))
+ case IntegerType => Ints.GreaterThan(toSMT(a), toSMT(b))
+ }
+ case (_: GreaterEquals) => a.getType match {
+ case Int32Type => FixedSizeBitVectors.SGreaterEquals(toSMT(a), toSMT(b))
+ case IntegerType => Ints.GreaterEquals(toSMT(a), toSMT(b))
+ }
+ case (_: BVPlus) => FixedSizeBitVectors.Add(toSMT(a), toSMT(b))
+ case (_: BVMinus) => FixedSizeBitVectors.Sub(toSMT(a), toSMT(b))
+ case (_: BVTimes) => FixedSizeBitVectors.Mul(toSMT(a), toSMT(b))
+ case (_: BVDivision) => FixedSizeBitVectors.SDiv(toSMT(a), toSMT(b))
+ case (_: BVModulo) => FixedSizeBitVectors.SRem(toSMT(a), toSMT(b))
case _ => reporter.fatalError("Unhandled binary "+e)
}
@@ -490,8 +509,8 @@ trait SMTLIBTarget {
case (SHexadecimal(h), CharType) =>
CharLiteral(h.toInt.toChar)
- case (SNumeral(n), Int32Type) =>
- IntLiteral(n.toInt)
+ case (SNumeral(n), IntegerType) =>
+ InfiniteIntegerLiteral(n)
case (Core.True(), BooleanType) => BooleanLiteral(true)
case (Core.False(), BooleanType) => BooleanLiteral(false)
@@ -556,8 +575,8 @@ trait SMTLIBTarget {
app match {
case "-" =>
args match {
- case List(a) => UMinus(fromSMT(a, Int32Type))
- case List(a, b) => Minus(fromSMT(a, Int32Type), fromSMT(b, Int32Type))
+ case List(a) => UMinus(fromSMT(a, IntegerType))
+ case List(a, b) => Minus(fromSMT(a, IntegerType), fromSMT(b, IntegerType))
}
case _ =>
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index dfe0784197c0763915aa58529e686dd66e3a2f21..f73c0ae11e506e664e52204cf4f7e5b68b191eac 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -377,14 +377,16 @@ trait AbstractZ3Solver
)
)
- sorts += Int32Type -> z3.mkIntSort
+ //TODO: mkBitVectorType
+ sorts += Int32Type -> z3.mkBVSort(32)
+ sorts += IntegerType -> z3.mkIntSort
sorts += BooleanType -> z3.mkBoolSort
sorts += UnitType -> us
unitValue = unitCons()
- val intSetSort = typeToSort(SetType(Int32Type))
- val intSort = typeToSort(Int32Type)
+ val intSetSort = typeToSort(SetType(IntegerType))
+ val intSort = typeToSort(IntegerType)
intSetMinFun = z3.mkFreshFuncDecl("setMin", Seq(intSetSort), intSort)
intSetMaxFun = z3.mkFreshFuncDecl("setMax", Seq(intSetSort), intSort)
@@ -404,7 +406,7 @@ trait AbstractZ3Solver
// assumes prepareSorts has been called....
protected[leon] def typeToSort(oldtt: TypeTree): Z3Sort = normalizeType(oldtt) match {
- case Int32Type | BooleanType | UnitType =>
+ case Int32Type | BooleanType | UnitType | IntegerType =>
sorts.toZ3(oldtt)
case act: AbstractClassType =>
@@ -563,6 +565,7 @@ trait AbstractZ3Solver
case Not(Equals(l, r)) => z3.mkDistinct(rec(l), rec(r))
case Not(e) => z3.mkNot(rec(e))
case IntLiteral(v) => z3.mkInt(v, typeToSort(Int32Type))
+ case InfiniteIntegerLiteral(v) => z3.mkNumeral(v.toString, typeToSort(IntegerType))
case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse()
case UnitLiteral() => unitValue
case Equals(l, r) => z3.mkEq(rec( l ), rec( r ) )
@@ -572,10 +575,29 @@ trait AbstractZ3Solver
case Division(l, r) => z3.mkDiv(rec(l), rec(r))
case Modulo(l, r) => z3.mkMod(rec(l), rec(r))
case UMinus(e) => z3.mkUnaryMinus(rec(e))
- case LessThan(l, r) => z3.mkLT(rec(l), rec(r))
- case LessEquals(l, r) => z3.mkLE(rec(l), rec(r))
- case GreaterThan(l, r) => z3.mkGT(rec(l), rec(r))
- case GreaterEquals(l, r) => z3.mkGE(rec(l), rec(r))
+ 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 BVUMinus(e) => z3.mkBVNeg(rec(e))
+ case LessThan(l, r) => l.getType match {
+ case IntegerType => z3.mkLT(rec(l), rec(r))
+ case Int32Type => z3.mkBVSlt(rec(l), rec(r))
+ }
+ case LessEquals(l, r) => l.getType match {
+ case IntegerType => z3.mkLE(rec(l), rec(r))
+ case Int32Type => z3.mkBVSle(rec(l), rec(r))
+ }
+ case GreaterThan(l, r) => l.getType match {
+ case IntegerType => z3.mkGT(rec(l), rec(r))
+ case Int32Type => z3.mkBVSgt(rec(l), rec(r))
+ }
+ case GreaterEquals(l, r) => l.getType match {
+ case IntegerType => z3.mkGE(rec(l), rec(r))
+ case Int32Type => z3.mkBVSge(rec(l), rec(r))
+ }
+
case c @ CaseClass(ct, args) =>
typeToSort(ct) // Making sure the sort is defined
val constructor = adtConstructors(ct)
@@ -668,9 +690,10 @@ trait AbstractZ3Solver
val default = oDefault.getOrElse(simplestValue(base))
- val ar = z3.mkConstArray(typeToSort(base), rec(default))
- val u = elems.foldLeft(ar)((array, el) =>
- z3.mkStore(array, rec(IntLiteral(el._1)), rec(el._2)))
+ val ar = z3.mkConstArray(typeToSort(Int32Type), rec(default))
+ val u = elems.foldLeft(ar)((array, el) => {
+ z3.mkStore(array, rec(IntLiteral(el._1)), rec(el._2))
+ })
meta.cons(u, rec(length))
case gv @ GenericValue(tp, id) =>
@@ -696,7 +719,29 @@ trait AbstractZ3Solver
val sort = z3.getSort(t)
kind match {
- case Z3NumeralIntAST(Some(v)) => IntLiteral(v)
+ case Z3NumeralIntAST(Some(v)) => {
+ val leading = t.toString.substring(0, 2 min t.toString.size)
+ if(leading == "#x") {
+ _root_.smtlib.common.Hexadecimal.fromString(t.toString.substring(2)) match {
+ case Some(hexa) => IntLiteral(hexa.toInt)
+ case None => {
+ println("Z3NumeralIntAST with None: " + t)
+ throw new CantTranslateException(t)
+ }
+ }
+ } else {
+ InfiniteIntegerLiteral(v)
+ }
+ }
+ case Z3NumeralIntAST(None) => {
+ _root_.smtlib.common.Hexadecimal.fromString(t.toString.substring(2)) match {
+ case Some(hexa) => IntLiteral(hexa.toInt)
+ case None => {
+ println("Z3NumeralIntAST with None: " + t)
+ throw new CantTranslateException(t)
+ }
+ }
+ }
case Z3AppAST(decl, args) =>
val argsSize = args.size
if(argsSize == 0 && (variables containsZ3 t)) {
@@ -729,13 +774,21 @@ trait AbstractZ3Solver
case LeonType(at @ ArrayType(dt)) =>
assert(args.size == 2)
- val IntLiteral(length) = rec(args(1))
+ val length = rec(args(1)) match {
+ case InfiniteIntegerLiteral(length) => length.toInt
+ case IntLiteral(length) => length
+ case _ => throw new CantTranslateException(t)
+ }
model.getArrayValue(args(0)) match {
case None => throw new CantTranslateException(t)
case Some((map, elseZ3Value)) =>
val elseValue = rec(elseZ3Value)
var valuesMap = map.map { case (k,v) =>
- val IntLiteral(index) = rec(k)
+ val index = rec(k) match {
+ case InfiniteIntegerLiteral(index) => index.toInt
+ case IntLiteral(index) => index
+ case _ => throw new CantTranslateException(t)
+ }
(index -> rec(v))
}
@@ -850,7 +903,7 @@ trait AbstractZ3Solver
}
}
}
- case Z3NumeralIntAST(Some(v)) => IntLiteral(v)
+ case Z3NumeralIntAST(Some(v)) => InfiniteIntegerLiteral(v)
case _ => throw e
}
diff --git a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
index 5953fc422598d19de8fb774a3064a607d78cea93..1bdb9fe6ad22b91357e9c3cfa46cf0a29515f079 100644
--- a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
+++ b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
@@ -24,6 +24,7 @@ trait Z3ModelReconstruction {
expectedType match {
case BooleanType => model.evalAs[Boolean](z3ID).map(BooleanLiteral(_))
case Int32Type => model.evalAs[Int](z3ID).map(IntLiteral(_))
+ case IntegerType => model.evalAs[Int](z3ID).map(InfiniteIntegerLiteral(_))
case other => model.eval(z3ID) match {
case None => None
case Some(t) => softFromZ3Formula(model, t)
diff --git a/src/main/scala/leon/synthesis/Algebra.scala b/src/main/scala/leon/synthesis/Algebra.scala
index 757c4c83c12f32b0e3d4d24e2db32bf06b735310..474d6e90e2bd4b2277cad21ca22ce7cea8705ac9 100644
--- a/src/main/scala/leon/synthesis/Algebra.scala
+++ b/src/main/scala/leon/synthesis/Algebra.scala
@@ -19,6 +19,12 @@ object Algebra {
((a - r)/b, r)
}
+ def remainder(x: BigInt, y: BigInt) = ((x % y) + y.abs) % y.abs
+ def divide(a: BigInt, b: BigInt): (BigInt, BigInt) = {
+ val r = remainder(a, b)
+ ((a - r)/b, r)
+ }
+
def gcd(a: Int, b: Int): Int = {
val (na, nb) = (a.abs, b.abs)
def gcd0(a: Int, b: Int): Int = {
@@ -54,6 +60,41 @@ object Algebra {
}
}
+ def gcd(a: BigInt, b: BigInt): BigInt = {
+ val (na, nb) = (a.abs, b.abs)
+ def gcd0(a: BigInt, b: BigInt): BigInt = {
+ require(a >= b)
+ if(b == 0) a else gcd0(b, a % b)
+ }
+ if(na > nb) gcd0(na, nb) else gcd0(nb, na)
+ }
+
+ def gcd(a1: BigInt, a2: BigInt, a3: BigInt, as: BigInt*): BigInt = {
+ var tmp = gcd(a1, a2)
+ tmp = gcd(tmp, a3)
+ var i = 0
+ while(i < as.size) {
+ tmp = gcd(tmp, as(i))
+ i += 1
+ }
+ tmp
+ }
+
+ def gcd(as: Seq[BigInt]): BigInt = {
+ require(as.length >= 1)
+ if(as.length == 1)
+ as(0).abs
+ else {
+ var tmp = gcd(as(0), as(1))
+ var i = 2
+ while(i < as.size) {
+ tmp = gcd(tmp, as(i))
+ i += 1
+ }
+ tmp
+ }
+ }
+
def lcm(a: Int, b: Int): Int = {
val (na, nb) = (a.abs, b.abs)
na*nb/gcd(a, b)
@@ -85,6 +126,37 @@ object Algebra {
}
}
+ def lcm(a: BigInt, b: BigInt): BigInt = {
+ val (na, nb) = (a.abs, b.abs)
+ na*nb/gcd(a, b)
+ }
+
+ def lcm(a1: BigInt, a2: BigInt, a3: BigInt, as: BigInt*): BigInt = {
+ var tmp = lcm(a1, a2)
+ tmp = lcm(tmp, a3)
+ var i = 0
+ while(i < as.size) {
+ tmp = lcm(tmp, as(i))
+ i += 1
+ }
+ tmp
+ }
+
+ def lcm(as: Seq[BigInt]): BigInt = {
+ require(as.length >= 1)
+ if(as.length == 1)
+ as(0).abs
+ else {
+ var tmp = lcm(as(0), as(1))
+ var i = 2
+ while(i < as.size) {
+ tmp = lcm(tmp, as(i))
+ i += 1
+ }
+ tmp
+ }
+ }
+
//return (x, y) such that ax + by = gcd(a, b)
def extendedEuclid(a: Int, b: Int): (Int, Int) = {
def rec(a: Int, b: Int): (Int, Int) = {
@@ -101,6 +173,21 @@ object Algebra {
else if(a < 0 && b < 0) {val (x, y) = rec(-a, -b); (-x, -y)}
else sys.error("shouldn't have forgot a case here")
}
+ def extendedEuclid(a: BigInt, b: BigInt): (BigInt, BigInt) = {
+ def rec(a: BigInt, b: BigInt): (BigInt, BigInt) = {
+ require(a >= 0 && b >= 0)
+ if(b == 0) (1, 0) else {
+ val (q, r) = divide(a, b)
+ val (s, t) = extendedEuclid(b, r)
+ (t, s - q * t)
+ }
+ }
+ if(a >= 0 && b >= 0) rec(a, b)
+ else if(a < 0 && b >= 0) {val (x, y) = rec(-a, b); (-x, y)}
+ else if(a >= 0 && b < 0) {val (x, y) = rec(a, -b); (x, -y)}
+ else if(a < 0 && b < 0) {val (x, y) = rec(-a, -b); (-x, -y)}
+ else sys.error("shouldn't have forgot a case here")
+ }
//val that the sol vector with the term in the equation
diff --git a/src/main/scala/leon/synthesis/LinearEquations.scala b/src/main/scala/leon/synthesis/LinearEquations.scala
index 6c91c40f59e62a60e2b5666725239e9928ad9671..a9dd5ff9a30d42902857b1ae77b12a3c6ac44e26 100644
--- a/src/main/scala/leon/synthesis/LinearEquations.scala
+++ b/src/main/scala/leon/synthesis/LinearEquations.scala
@@ -17,32 +17,32 @@ object LinearEquations {
//return a mapping for each of the n variables in (pre, map, freshVars)
def elimVariable(evaluator: Evaluator, as: Set[Identifier], normalizedEquation: List[Expr]): (Expr, List[Expr], List[Identifier]) = {
require(normalizedEquation.size > 1)
- require(normalizedEquation.tail.forall{case IntLiteral(i) if i != 0 => true case _ => false})
+ require(normalizedEquation.tail.forall{case InfiniteIntegerLiteral(i) if i != 0 => true case _ => false})
val t: Expr = normalizedEquation.head
- val coefsVars: List[Int] = normalizedEquation.tail.map{case IntLiteral(i) => i}
+ val coefsVars: List[BigInt] = normalizedEquation.tail.map{case InfiniteIntegerLiteral(i) => i}
val orderedParams: Array[Identifier] = as.toArray
- val coefsParams: List[Int] = linearArithmeticForm(t, orderedParams).map{case IntLiteral(i) => i}.toList
+ val coefsParams: List[BigInt] = linearArithmeticForm(t, orderedParams).map{case InfiniteIntegerLiteral(i) => i}.toList
//val coefsParams: List[Int] = if(coefsParams0.head == 0) coefsParams0.tail else coefsParams0
- val d: Int = gcd((coefsParams ++ coefsVars).toSeq)
+ val d: BigInt = gcd((coefsParams ++ coefsVars).toSeq)
if(coefsVars.size == 1) {
val coef = coefsVars.head
- (Equals(Modulo(t, IntLiteral(coef)), IntLiteral(0)), List(UMinus(Division(t, IntLiteral(coef)))), List())
+ (Equals(Modulo(t, InfiniteIntegerLiteral(coef)), InfiniteIntegerLiteral(0)), List(UMinus(Division(t, InfiniteIntegerLiteral(coef)))), List())
} else if(d > 1) {
- val newCoefsParams: List[Expr] = coefsParams.map(i => IntLiteral(i/d) : Expr)
- val newT = newCoefsParams.zip(IntLiteral(1)::orderedParams.map(Variable(_)).toList).foldLeft[Expr](IntLiteral(0))((acc, p) => Plus(acc, Times(p._1, p._2)))
- elimVariable(evaluator, as, newT :: normalizedEquation.tail.map{case IntLiteral(i) => IntLiteral(i/d) : Expr})
+ val newCoefsParams: List[Expr] = coefsParams.map(i => InfiniteIntegerLiteral(i/d) : Expr)
+ val newT = newCoefsParams.zip(InfiniteIntegerLiteral(1)::orderedParams.map(Variable(_)).toList).foldLeft[Expr](InfiniteIntegerLiteral(0))((acc, p) => Plus(acc, Times(p._1, p._2)))
+ elimVariable(evaluator, as, newT :: normalizedEquation.tail.map{case InfiniteIntegerLiteral(i) => InfiniteIntegerLiteral(i/d) : Expr})
} else {
- val basis: Array[Array[Int]] = linearSet(evaluator, as, normalizedEquation.tail.map{case IntLiteral(i) => i}.toArray)
+ val basis: Array[Array[BigInt]] = linearSet(evaluator, as, normalizedEquation.tail.map{case InfiniteIntegerLiteral(i) => i}.toArray)
val (pre, sol) = particularSolution(as, normalizedEquation)
- val freshVars: Array[Identifier] = basis(0).map(_ => FreshIdentifier("v", true).setType(Int32Type))
+ val freshVars: Array[Identifier] = basis(0).map(_ => FreshIdentifier("v", true).setType(IntegerType))
val tbasis = basis.transpose
assert(freshVars.size == tbasis.size)
val basisWithFreshVars: Array[Array[Expr]] = freshVars.zip(tbasis).map{
- case (lambda, column) => column.map((i: Int) => Times(IntLiteral(i), Variable(lambda)): Expr)
+ case (lambda, column) => column.map((i: BigInt) => Times(InfiniteIntegerLiteral(i), Variable(lambda)): Expr)
}.transpose
- val combinationBasis: Array[Expr] = basisWithFreshVars.map((v: Array[Expr]) => v.foldLeft[Expr](IntLiteral(0))((acc, e) => Plus(acc, e)))
+ val combinationBasis: Array[Expr] = basisWithFreshVars.map((v: Array[Expr]) => v.foldLeft[Expr](InfiniteIntegerLiteral(0))((acc, e) => Plus(acc, e)))
assert(combinationBasis.size == sol.size)
val subst: List[Expr] = sol.zip(combinationBasis.toList).map(p => Plus(p._1, p._2): Expr)
@@ -58,9 +58,9 @@ object LinearEquations {
//Intuitively, we are building a "basis" for the "vector space" of solutions (although we are over
//integers, so it is not a vector space).
//we are returning a matrix where the columns are the vectors
- def linearSet(evaluator: Evaluator, as: Set[Identifier], coef: Array[Int]): Array[Array[Int]] = {
+ def linearSet(evaluator: Evaluator, as: Set[Identifier], coef: Array[BigInt]): Array[Array[BigInt]] = {
- val K = Array.ofDim[Int](coef.size, coef.size-1)
+ val K = Array.ofDim[BigInt](coef.size, coef.size-1)
for(i <- 0 until K.size) {
for(j <- 0 until K(i).size) {
if(i < j)
@@ -71,11 +71,11 @@ object LinearEquations {
}
}
for(j <- 0 until K.size - 1) {
- val (_, sols) = particularSolution(as, IntLiteral(coef(j)*K(j)(j)) :: coef.drop(j+1).map(IntLiteral(_)).toList)
+ val (_, sols) = particularSolution(as, InfiniteIntegerLiteral(coef(j)*K(j)(j)) :: coef.drop(j+1).map(InfiniteIntegerLiteral(_)).toList)
var i = 0
while(i < sols.size) {
// seriously ???
- K(i+j+1)(j) = evaluator.eval(sols(i)).asInstanceOf[EvaluationResults.Successful].value.asInstanceOf[IntLiteral].value
+ K(i+j+1)(j) = evaluator.eval(sols(i)).asInstanceOf[EvaluationResults.Successful].value.asInstanceOf[InfiniteIntegerLiteral].value
i += 1
}
}
@@ -96,16 +96,16 @@ object LinearEquations {
//return a particular solution to t + c1x + c2y = 0, with (pre, (x0, y0))
def particularSolution(as: Set[Identifier], t: Expr, c1: Expr, c2: Expr): (Expr, (Expr, Expr)) = {
- val (IntLiteral(i1), IntLiteral(i2)) = (c1, c2)
+ val (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) = (c1, c2)
val (v1, v2) = extendedEuclid(i1, i2)
val d = gcd(i1, i2)
- val pre = Equals(Modulo(t, IntLiteral(d)), IntLiteral(0))
+ val pre = Equals(Modulo(t, InfiniteIntegerLiteral(d)), InfiniteIntegerLiteral(0))
(pre,
(
- UMinus(Times(IntLiteral(v1), Division(t, IntLiteral(d)))),
- UMinus(Times(IntLiteral(v2), Division(t, IntLiteral(d))))
+ UMinus(Times(InfiniteIntegerLiteral(v1), Division(t, InfiniteIntegerLiteral(d)))),
+ UMinus(Times(InfiniteIntegerLiteral(v2), Division(t, InfiniteIntegerLiteral(d))))
)
)
}
@@ -114,9 +114,9 @@ object LinearEquations {
def particularSolution(as: Set[Identifier], normalizedEquation: List[Expr]): (Expr, List[Expr]) = {
require(normalizedEquation.size >= 2)
val t: Expr = normalizedEquation.head
- val coefs: List[Int] = normalizedEquation.tail.map{case IntLiteral(i) => i}
+ val coefs: List[BigInt] = normalizedEquation.tail.map{case InfiniteIntegerLiteral(i) => i}
val d = gcd(coefs.toSeq)
- val pre = Equals(Modulo(t, IntLiteral(d)), IntLiteral(0))
+ val pre = Equals(Modulo(t, InfiniteIntegerLiteral(d)), InfiniteIntegerLiteral(0))
if(normalizedEquation.size == 2) {
(pre, List(UMinus(Division(t, normalizedEquation(1)))))
@@ -125,8 +125,8 @@ object LinearEquations {
(pre, List(w1, w2))
} else {
val gamma1: Expr = normalizedEquation(1)
- val coefs: List[Int] = normalizedEquation.drop(2).map{case IntLiteral(i) => i}
- val gamma2: Expr = IntLiteral(gcd(coefs.toSeq))
+ val coefs: List[BigInt] = normalizedEquation.drop(2).map{case InfiniteIntegerLiteral(i) => i}
+ val gamma2: Expr = InfiniteIntegerLiteral(gcd(coefs.toSeq))
val (_, (w1, w)) = particularSolution(as, t, gamma1, gamma2)
val (_, sols) = particularSolution(as, UMinus(Times(w, gamma2)) :: normalizedEquation.drop(2))
(pre, w1 :: sols)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 10b8e6ef51f781a6767c41c4db4d1e0693c4ea24..399e045a537e1522be519773532e8b66555ee7fc 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -50,8 +50,8 @@ object Rules {
DetupleInput,
ADTSplit,
InlineHoles,
- IntegerEquation,
- IntegerInequalities,
+ //IntegerEquation,
+ //IntegerInequalities,
IntInduction,
InnerCaseSplit,
//new OptimisticInjection(_),
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index 3a744c42c0b04c7a9f899748195c9ee5e84c6843..6d989c4ef4126e8391a47a9fa048fcd7d8efd92b 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -9,6 +9,18 @@ import purescala.TypeTrees._
import purescala.Common._
import purescala.Definitions._
import utils.Helpers._
+import purescala.TypeTrees._
+import purescala.TreeOps._
+import purescala.DefOps._
+import purescala.TypeTreeOps._
+import purescala.Extractors._
+import purescala.ScalaPrinter
+
+import scala.collection.mutable.{Map=>MutableMap}
+
+import evaluators._
+import datagen._
+import codegen.CodeGenParams
import utils._
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index 54ce95e5e83d1a7e76cf08b0f9589c3f6aeefa50..a71574fdaf243c388014f0c73c1f49773e512db1 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -18,7 +18,7 @@ case object InequalitySplit extends Rule("Ineq. Split.") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
val solver = SimpleSolverAPI(hctx.sctx.fastSolverFactory)
- val candidates = p.as.filter(_.getType == Int32Type).combinations(2).toList.filter {
+ val candidates = p.as.filter(_.getType == IntegerType).combinations(2).toList.filter {
case List(a1, a2) =>
val toValLT = implies(p.pc, LessThan(Variable(a1), Variable(a2)))
diff --git a/src/main/scala/leon/synthesis/rules/IntInduction.scala b/src/main/scala/leon/synthesis/rules/IntInduction.scala
index ae0567bd3a2e0ab53bd9208a181674a27b057cd8..15c19915d02269358ea4c98c6910f09389c568e6 100644
--- a/src/main/scala/leon/synthesis/rules/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/rules/IntInduction.scala
@@ -15,7 +15,7 @@ import purescala.Definitions._
case object IntInduction extends Rule("Int Induction") {
def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
p.as match {
- case List(IsTyped(origId, Int32Type)) =>
+ case List(IsTyped(origId, IntegerType)) =>
val tpe = tupleTypeWrap(p.xs.map(_.getType))
val inductOn = FreshIdentifier(origId.name, true).setType(origId.getType)
@@ -27,12 +27,12 @@ case object IntInduction extends Rule("Int Induction") {
val newPhi = subst(origId -> Variable(inductOn), p.phi)
val newPc = subst(origId -> Variable(inductOn), p.pc)
val newWs = subst(origId -> Variable(inductOn), p.ws)
- val postCondGT = substAll(postXsMap + (origId -> Minus(Variable(inductOn), IntLiteral(1))), p.phi)
- val postCondLT = substAll(postXsMap + (origId -> Plus(Variable(inductOn), IntLiteral(1))), p.phi)
+ val postCondGT = substAll(postXsMap + (origId -> Minus(Variable(inductOn), InfiniteIntegerLiteral(1))), p.phi)
+ val postCondLT = substAll(postXsMap + (origId -> Plus(Variable(inductOn), InfiniteIntegerLiteral(1))), p.phi)
- val subBase = Problem(List(), subst(origId -> IntLiteral(0), p.ws), subst(origId -> IntLiteral(0), p.pc), subst(origId -> IntLiteral(0), p.phi), p.xs)
- val subGT = Problem(inductOn :: postXs, newWs, and(GreaterThan(Variable(inductOn), IntLiteral(0)), postCondGT, newPc), newPhi, p.xs)
- val subLT = Problem(inductOn :: postXs, newWs, and(LessThan(Variable(inductOn), IntLiteral(0)), postCondLT, newPc), newPhi, p.xs)
+ val subBase = Problem(List(), subst(origId -> InfiniteIntegerLiteral(0), p.ws), subst(origId -> InfiniteIntegerLiteral(0), p.pc), subst(origId -> InfiniteIntegerLiteral(0), p.phi), p.xs)
+ val subGT = Problem(inductOn :: postXs, newWs, and(GreaterThan(Variable(inductOn), InfiniteIntegerLiteral(0)), postCondGT, newPc), newPhi, p.xs)
+ val subLT = Problem(inductOn :: postXs, newWs, and(LessThan(Variable(inductOn), InfiniteIntegerLiteral(0)), postCondLT, newPc), newPhi, p.xs)
val onSuccess: List[Solution] => Option[Solution] = {
case List(base, gt, lt) =>
@@ -41,9 +41,9 @@ case object IntInduction extends Rule("Int Induction") {
// allow invalid programs.
None
} else {
- val preIn = or(and(Equals(Variable(inductOn), IntLiteral(0)), base.pre),
- and(GreaterThan(Variable(inductOn), IntLiteral(0)), gt.pre),
- and(LessThan(Variable(inductOn), IntLiteral(0)), lt.pre))
+ val preIn = or(and(Equals(Variable(inductOn), InfiniteIntegerLiteral(0)), base.pre),
+ and(GreaterThan(Variable(inductOn), InfiniteIntegerLiteral(0)), gt.pre),
+ and(LessThan(Variable(inductOn), InfiniteIntegerLiteral(0)), lt.pre))
val preOut = subst(inductOn -> Variable(origId), preIn)
val newFun = new FunDef(FreshIdentifier("rec", true), Nil, tpe, Seq(ValDef(inductOn, inductOn.getType)),DefType.MethodDef)
@@ -53,11 +53,11 @@ case object IntInduction extends Rule("Int Induction") {
newFun.postcondition = Some((idPost, letTuple(p.xs.toSeq, Variable(idPost), p.phi)))
newFun.body = Some(
- IfExpr(Equals(Variable(inductOn), IntLiteral(0)),
+ IfExpr(Equals(Variable(inductOn), InfiniteIntegerLiteral(0)),
base.toExpr,
- IfExpr(GreaterThan(Variable(inductOn), IntLiteral(0)),
- letTuple(postXs, FunctionInvocation(newFun.typed, Seq(Minus(Variable(inductOn), IntLiteral(1)))), gt.toExpr)
- , letTuple(postXs, FunctionInvocation(newFun.typed, Seq(Plus(Variable(inductOn), IntLiteral(1)))), lt.toExpr)))
+ IfExpr(GreaterThan(Variable(inductOn), InfiniteIntegerLiteral(0)),
+ letTuple(postXs, FunctionInvocation(newFun.typed, Seq(Minus(Variable(inductOn), InfiniteIntegerLiteral(1)))), gt.toExpr)
+ , letTuple(postXs, FunctionInvocation(newFun.typed, Seq(Plus(Variable(inductOn), InfiniteIntegerLiteral(1)))), lt.toExpr)))
)
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index 97687c4250153f1424c00cf38fce707f1854e165..ac3f47b1798902582ac6c09ac79fbfd44a755cfd 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -81,18 +81,30 @@ object ExpressionGrammars {
Generator(List(BooleanType), { case Seq(a) => Not(a) }),
Generator(List(BooleanType, BooleanType), { case Seq(a, b) => And(a, b) }),
Generator(List(BooleanType, BooleanType), { case Seq(a, b) => LeonOr(a, b) }),
- Generator(List(Int32Type, Int32Type), { case Seq(a, b) => LessThan(a, b) }),
- Generator(List(Int32Type, Int32Type), { case Seq(a, b) => LessEquals(a, b) }),
+ Generator(List(Int32Type, Int32Type), { case Seq(a, b) => LessThan(a, b) }),
+ Generator(List(Int32Type, Int32Type), { case Seq(a, b) => LessEquals(a, b) }),
Generator(List(Int32Type, Int32Type ), { case Seq(a, b) => Equals(a, b) }),
+ Generator(List(IntegerType, IntegerType), { case Seq(a, b) => LessThan(a, b) }),
+ Generator(List(IntegerType, IntegerType), { case Seq(a, b) => LessEquals(a, b) }),
+ Generator(List(IntegerType, IntegerType), { case Seq(a, b) => Equals(a, b) }),
Generator(List(BooleanType, BooleanType), { case Seq(a, b) => Equals(a, b) })
)
case Int32Type =>
List(
Generator(Nil, { _ => IntLiteral(0) }),
Generator(Nil, { _ => IntLiteral(1) }),
- Generator(List(Int32Type, Int32Type), { case Seq(a,b) => Plus(a, b) }),
- Generator(List(Int32Type, Int32Type), { case Seq(a,b) => Minus(a, b) }),
- Generator(List(Int32Type, Int32Type), { case Seq(a,b) => Times(a, b) })
+ Generator(List(Int32Type, Int32Type), { case Seq(a,b) => BVPlus(a, b) }),
+ Generator(List(Int32Type, Int32Type), { case Seq(a,b) => BVMinus(a, b) }),
+ Generator(List(Int32Type, Int32Type), { case Seq(a,b) => BVTimes(a, b) })
+ )
+
+ case IntegerType =>
+ List(
+ Generator(Nil, { _ => InfiniteIntegerLiteral(0) }),
+ Generator(Nil, { _ => InfiniteIntegerLiteral(1) }),
+ Generator(List(IntegerType, IntegerType), { case Seq(a,b) => Plus(a, b) }),
+ Generator(List(IntegerType, IntegerType), { case Seq(a,b) => Minus(a, b) }),
+ Generator(List(IntegerType, IntegerType), { case Seq(a,b) => Times(a, b) })
)
case TupleType(stps) =>
@@ -137,6 +149,12 @@ object ExpressionGrammars {
Generator(Nil, { _ => IntLiteral(1) }),
Generator(Nil, { _ => IntLiteral(-1) })
)
+ case IntegerType =>
+ List(
+ Generator(Nil, { _ => InfiniteIntegerLiteral(0) }),
+ Generator(Nil, { _ => InfiniteIntegerLiteral(1) }),
+ Generator(Nil, { _ => InfiniteIntegerLiteral(-1) })
+ )
case tp@TypeParameter(_) =>
for (ind <- (1 to 3).toList) yield
@@ -263,8 +281,8 @@ object ExpressionGrammars {
def intVariations(gl: L, e : Expr): Seq[(L, Gen)] = {
Seq(
- gl -> Generator(Nil, { _ => Minus(e, IntLiteral(1))} ),
- gl -> Generator(Nil, { _ => Plus (e, IntLiteral(1))} )
+ gl -> Generator(Nil, { _ => BVMinus(e, IntLiteral(1))} ),
+ gl -> Generator(Nil, { _ => BVPlus (e, IntLiteral(1))} )
)
}
diff --git a/src/main/scala/leon/termination/ChainComparator.scala b/src/main/scala/leon/termination/ChainComparator.scala
index 68f5f97a2908fcb3e3079692ee553a14f3d0cb72..f1d146e7dca987900714948fef9eebc9ab1d649a 100644
--- a/src/main/scala/leon/termination/ChainComparator.scala
+++ b/src/main/scala/leon/termination/ChainComparator.scala
@@ -194,7 +194,7 @@ trait ChainComparator { self : StructuralSize with TerminationChecker =>
def numericConverging(e1: Expr, e2s: Seq[(Seq[Expr], Expr)], cluster: Set[Chain]) : Seq[Expr] = flatType(e1.getType).toSeq.flatMap {
recons => recons(e1) match {
- case e if e.getType == Int32Type =>
+ case e if e.getType == IntegerType =>
val endpoint = numericEndpoint(e, cluster)
val uppers = if (endpoint == UpperBoundEndpoint || endpoint == AnyEndpoint) {
diff --git a/src/main/scala/leon/termination/StructuralSize.scala b/src/main/scala/leon/termination/StructuralSize.scala
index 25965c4ad6c71a9fa09c41a3ca5df674d0885f69..e1f8f8b3cf423e1d83f2776983d828feb6a5f6d7 100644
--- a/src/main/scala/leon/termination/StructuralSize.scala
+++ b/src/main/scala/leon/termination/StructuralSize.scala
@@ -34,12 +34,12 @@ trait StructuralSize {
case None =>
val argument = ValDef(FreshIdentifier("x", true).setType(argumentType), argumentType)
val formalTParams = typeParams.map(TypeParameterDef(_))
- val fd = new FunDef(FreshIdentifier("size", true), formalTParams, Int32Type, Seq(argument), DefType.MethodDef)
+ val fd = new FunDef(FreshIdentifier("size", true), formalTParams, IntegerType, Seq(argument), DefType.MethodDef)
sizeCache(argumentType) = fd
val body = simplifyLets(matchToIfThenElse(matchExpr(argument.toVariable, cases(argumentType))))
- val postId = FreshIdentifier("res", false).setType(Int32Type)
- val postcondition = GreaterThan(Variable(postId), IntLiteral(0))
+ val postId = FreshIdentifier("res", false).setType(IntegerType)
+ val postcondition = GreaterThan(Variable(postId), InfiniteIntegerLiteral(0))
fd.body = Some(body)
fd.postcondition = Some(postId, postcondition)
@@ -52,7 +52,7 @@ trait StructuralSize {
val arguments = c.fields.map(vd => FreshIdentifier(vd.id.name).setType(vd.tpe))
val argumentPatterns = arguments.map(id => WildcardPattern(Some(id)))
val sizes = arguments.map(id => size(Variable(id)))
- val result = sizes.foldLeft[Expr](IntLiteral(1))(Plus(_,_))
+ val result = sizes.foldLeft[Expr](InfiniteIntegerLiteral(1))(Plus(_,_))
purescala.Extractors.SimpleCase(CaseClassPattern(None, c, argumentPatterns), result)
}
@@ -65,8 +65,8 @@ trait StructuralSize {
FunctionInvocation(TypedFunDef(fd, ct.tps), Seq(expr))
case TupleType(argTypes) => argTypes.zipWithIndex.map({
case (_, index) => size(tupleSelect(expr, index + 1))
- }).foldLeft[Expr](IntLiteral(0))(Plus(_,_))
- case _ => IntLiteral(0)
+ }).foldLeft[Expr](InfiniteIntegerLiteral(0))(Plus(_,_))
+ case _ => InfiniteIntegerLiteral(0)
}
}
diff --git a/src/test/resources/regression/synthesis/List/Insert.scala b/src/test/resources/regression/synthesis/List/Insert.scala
index 13c1294d7000c4b8fce4fbe229a3a5b54ea27790..0a2cb88b0efa17ab1498b71bac764c55504c1f96 100644
--- a/src/test/resources/regression/synthesis/List/Insert.scala
+++ b/src/test/resources/regression/synthesis/List/Insert.scala
@@ -9,9 +9,9 @@ object Insert {
case class Cons(head: Int, tail: List) extends List
case object Nil extends List
- def size(l: List) : Int = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ def size(l: List) : BigInt = (l match {
+ case Nil => BigInt(0)
+ case Cons(_, t) => size(t) + 1
}) ensuring(res => res >= 0)
def content(l: List): Set[Int] = l match {
diff --git a/src/test/resources/regression/termination/valid/Fibonacci.scala b/src/test/resources/regression/termination/valid/Fibonacci.scala
index feabb8aff313a4cfd91f5a2cf75f2ab764dc0917..e859a2c3d8c80ce169081d49f72938201d2dfa38 100644
--- a/src/test/resources/regression/termination/valid/Fibonacci.scala
+++ b/src/test/resources/regression/termination/valid/Fibonacci.scala
@@ -1,7 +1,7 @@
/* Copyright 2009-2014 EPFL, Lausanne */
object Fibonacci {
- def fib(x: Int) : Int = {
+ def fib(x: BigInt) : BigInt = {
require(x >= 0)
if(x < 2) {
x
@@ -12,6 +12,6 @@ object Fibonacci {
// requires that fib is universally quantified to work...
def check() : Boolean = {
- fib(5) == 5
+ fib(5) == BigInt(5)
} ensuring(_ == true)
}
diff --git a/src/test/resources/regression/termination/valid/Numeric1.scala b/src/test/resources/regression/termination/valid/Numeric1.scala
index 07218fa520f9373717b9e3eed3d363db7367a505..7015bf71e3297131940b175e4034fdb9715f2aaf 100644
--- a/src/test/resources/regression/termination/valid/Numeric1.scala
+++ b/src/test/resources/regression/termination/valid/Numeric1.scala
@@ -4,10 +4,7 @@ import leon.lang._
object Numeric {
- def f1(x: Int): Int = f2(x - 2)
+ def f1(x: BigInt): BigInt = f2(x - 2)
- def f2(x: Int): Int = if (x < 0) 0 else f1(x + 1)
+ def f2(x: BigInt): BigInt = if (x < 0) 0 else f1(x + 1)
}
-
-
-// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/purescala/invalid/AddingNegativeNumbers.scala b/src/test/resources/regression/verification/purescala/invalid/AddingNegativeNumbers.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a8c1433b1b0eb8e86b575453141d910fe4dc39cc
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/AddingNegativeNumbers.scala
@@ -0,0 +1,10 @@
+package test.resources.regression.verification.purescala.invalid
+
+object AddingNegativeNumbers {
+
+ def additionOverflow(x: Int, y: Int): Int = {
+ require(x <= 0 && y <= 0)
+ x + y
+ } ensuring(_ <= 0)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/AddingPositiveNumbers.scala b/src/test/resources/regression/verification/purescala/invalid/AddingPositiveNumbers.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d5f1b2825f17083409b2f5474fc0d3d331e7ff1e
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/AddingPositiveNumbers.scala
@@ -0,0 +1,11 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object AddingPositiveNumbers {
+
+ //this should overflow with bit vectors
+ def additionOverflow(x: Int, y: Int): Int = {
+ require(x >= 0 && y >= 0)
+ x + y
+ } ensuring(_ >= 0)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/Choose1.scala b/src/test/resources/regression/verification/purescala/invalid/Choose1.scala
index 20d5885231c38d0ea858152d112fe43e5e546f23..8ff2e7dcb81701d0113f96a98268426e7c0ba071 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Choose1.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Choose1.scala
@@ -9,8 +9,8 @@ object Choose1 {
case class Cons(head: Int, tail: List) extends List
case class Nil() extends List
- def size(l: List) : Int = (l match {
- case Nil() => 0
+ def size(l: List) : BigInt = (l match {
+ case Nil() => BigInt(0)
case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
@@ -19,10 +19,10 @@ object Choose1 {
case Cons(x, xs) => Set(x) ++ content(xs)
}
- def listOfSize(i: Int): List = {
+ def listOfSize(i: BigInt): List = {
require(i >= 0)
- if (i == 0) {
+ if (i == BigInt(0)) {
Nil()
} else {
choose { (res: List) => size(res) == i-1 }
@@ -30,7 +30,7 @@ object Choose1 {
} ensuring ( size(_) == i )
- def listOfSize2(i: Int): List = {
+ def listOfSize2(i: BigInt): List = {
require(i >= 0)
if (i > 0) {
diff --git a/src/test/resources/regression/verification/purescala/invalid/Generics.scala b/src/test/resources/regression/verification/purescala/invalid/Generics.scala
index 04421e7549b02d573b86093803879344881c7526..1c8566937e7c3a1c56edaf62aa6bfb4a7db9a099 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Generics.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Generics.scala
@@ -7,8 +7,8 @@ object Generics1 {
case class Cons[A](head: A, tail: List[A]) extends List[A]
case class Nil[B]() extends List[B]
- def size[T](l: List[T]): Int = (l match {
- case Nil() => 0
+ def size[T](l: List[T]): BigInt = (l match {
+ case Nil() => BigInt(0)
case Cons(h, t) => 1+size(t)
})ensuring { _ > 0 }
diff --git a/src/test/resources/regression/verification/purescala/invalid/Generics2.scala b/src/test/resources/regression/verification/purescala/invalid/Generics2.scala
index 0376cfaf21e557ce82e03877bf7decdfde00b0b3..56dc25fd4fd8573039deab177c4e88f536475579 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Generics2.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Generics2.scala
@@ -7,8 +7,8 @@ object Generics1 {
case class Cons[A](head: A, tail: List[A]) extends List[A]
case class Nil[B]() extends List[B]
- def size[T](l: List[T]): Int = (l match {
- case Nil() => 0
+ def size[T](l: List[T]): BigInt = (l match {
+ case Nil() => BigInt(0)
case Cons(h, t) => 1+size(t)
})ensuring { _ >= 0 }
diff --git a/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala b/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala
index 5fd06d36a53f3b41ffde13fff37044afc50734ec..8f4d88aa28398d441f5ac9179d8a548fd516646a 100644
--- a/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala
@@ -13,8 +13,8 @@ object InsertionSort {
case class Some(value: Int) extends OptInt
case class None() extends OptInt
- def size(l : List) : Int = (l match {
- case Nil() => 0
+ def size(l : List) : BigInt = (l match {
+ case Nil() => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
diff --git a/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala b/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
index bca6e6a76bbe862f63d4016a0e6db6073cba6443..afa46acd20e5fdfcab9a6b91a04d46b6cd8b883c 100644
--- a/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
@@ -16,13 +16,13 @@ object ListOperations {
sealed abstract class IntPair
case class IP(fst: Int, snd: Int) extends IntPair
- def size(l: List) : Int = (l match {
- case Nil() => 0
+ def size(l: List) : BigInt = (l match {
+ case Nil() => BigInt(0)
case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
- def iplSize(l: IntPairList) : Int = (l match {
- case IPNil() => 0
+ def iplSize(l: IntPairList) : BigInt = (l match {
+ case IPNil() => BigInt(0)
case IPCons(_, xs) => 1 + iplSize(xs)
}) ensuring(_ >= 0)
@@ -39,8 +39,8 @@ object ListOperations {
}
} ensuring(iplSize(_) == size(l1))
- def sizeTailRec(l: List) : Int = sizeTailRecAcc(l, 0)
- def sizeTailRecAcc(l: List, acc: Int) : Int = {
+ def sizeTailRec(l: List) : BigInt = sizeTailRecAcc(l, 0)
+ def sizeTailRecAcc(l: List, acc: BigInt) : BigInt = {
require(acc >= 0)
l match {
case Nil() => acc
@@ -58,7 +58,7 @@ object ListOperations {
}
def sizeAndContent(l: List) : Boolean = {
- size(l) == 0 || content(l) != Set.empty[Int]
+ size(l) == BigInt(0) || content(l) != Set.empty[Int]
}.holds
def drunk(l : List) : List = (l match {
diff --git a/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala b/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala
index 148512d000bf452ca3c284d9fd57670318eb6b87..1a75c77190cdea1c49aedf0d63491ee08db1e943 100644
--- a/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala
@@ -22,8 +22,8 @@ object RedBlackTree {
case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
}
- def size(t: Tree) : Int = (t match {
- case Empty() => 0
+ def size(t: Tree) : BigInt = (t match {
+ case Empty() => BigInt(0)
case Node(_, l, v, r) => size(l) + 1 + size(r)
}) ensuring(_ >= 0)
diff --git a/src/test/resources/regression/verification/purescala/valid/AddingPositiveNumbers.scala b/src/test/resources/regression/verification/purescala/valid/AddingPositiveNumbers.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ad5efa8794a974e620fe5c0ea936380a36dd562b
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/AddingPositiveNumbers.scala
@@ -0,0 +1,11 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+object AddingPositiveNumbers {
+
+ //this should not overflow
+ def additionSound(x: BigInt, y: BigInt): BigInt = {
+ require(x >= 0 && y >= 0)
+ x + y
+ } ensuring(_ >= 0)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala b/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
index 0c7d2170f77ebb4e338dc3840d3ac750b0f0f9f2..1f74ed4b12933352dedeb22dadff0f1d1121f19d 100644
--- a/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
+++ b/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
@@ -12,8 +12,8 @@ object AmortizedQueue {
sealed abstract class AbsQueue
case class Queue(front : List, rear : List) extends AbsQueue
- def size(list : List) : Int = (list match {
- case Nil() => 0
+ def size(list : List) : BigInt = (list match {
+ case Nil() => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
diff --git a/src/test/resources/regression/verification/purescala/valid/Anonymous.scala b/src/test/resources/regression/verification/purescala/valid/Anonymous.scala
index b8d3235ccf5e817d0202b0f8de3145d977e1989f..d69b1f8423c3ae681527e2a49fb75d6c54672b4f 100644
--- a/src/test/resources/regression/verification/purescala/valid/Anonymous.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Anonymous.scala
@@ -1,9 +1,9 @@
import leon.lang._
object Anonymous {
- def test(x: Int) = {
+ def test(x: BigInt) = {
require(x > 0)
- val i = (a: Int) => a + 1
+ val i = (a: BigInt) => a + 1
i(x) + i(2)
} ensuring { res => res > 0 }
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Asserts1.scala b/src/test/resources/regression/verification/purescala/valid/Asserts1.scala
index abbd39d5e8f88244891e20f763f7ccd150fcf839..0851ba5adf9eaa3b80a73fe263b904e93fc474da 100644
--- a/src/test/resources/regression/verification/purescala/valid/Asserts1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Asserts1.scala
@@ -4,7 +4,7 @@ import leon._
object Operators {
- def foo(a: Int): Int = {
+ def foo(a: BigInt): BigInt = {
require(a > 0)
{
@@ -17,7 +17,7 @@ object Operators {
_ > a
}
- def bar(a: Int): Int = {
+ def bar(a: BigInt): BigInt = {
require(a > 0)
{
diff --git a/src/test/resources/regression/verification/purescala/valid/Choose1.scala b/src/test/resources/regression/verification/purescala/valid/Choose1.scala
index 2b033c809ca1e5c71ad9c7592aa4482ab13ef083..da4b4e7752a7a4a6fcbd21c72533e0312c18cb73 100644
--- a/src/test/resources/regression/verification/purescala/valid/Choose1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Choose1.scala
@@ -9,8 +9,8 @@ object Choose1 {
case class Cons(head: Int, tail: List) extends List
case class Nil() extends List
- def size(l: List) : Int = (l match {
- case Nil() => 0
+ def size(l: List) : BigInt = (l match {
+ case Nil() => BigInt(0)
case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
@@ -19,10 +19,10 @@ object Choose1 {
case Cons(x, xs) => Set(x) ++ content(xs)
}
- def listOfSize(i: Int): List = {
+ def listOfSize(i: BigInt): List = {
require(i >= 0)
- if (i == 0) {
+ if (i == BigInt(0)) {
Nil()
} else {
choose { (res: List) => size(res) == i }
@@ -30,7 +30,7 @@ object Choose1 {
} ensuring ( size(_) == i )
- def listOfSize2(i: Int): List = {
+ def listOfSize2(i: BigInt): List = {
require(i >= 0)
if (i > 0) {
diff --git a/src/test/resources/regression/verification/purescala/valid/Generics.scala b/src/test/resources/regression/verification/purescala/valid/Generics.scala
index 2820d5a5cfe8791584a187787e564e84d8a280ba..7e1b2359f35b7b197738397782b20d0a73a32df6 100644
--- a/src/test/resources/regression/verification/purescala/valid/Generics.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Generics.scala
@@ -7,8 +7,8 @@ object Generics1 {
case class Cons[A](head: A, tail: List[A]) extends List[A]
case class Nil[B]() extends List[B]
- def size[T](l: List[T]): Int = (l match {
- case Nil() => 0
+ def size[T](l: List[T]): BigInt = (l match {
+ case Nil() => BigInt(0)
case Cons(h, t) => 1+size(t)
})ensuring { _ >= 0 }
diff --git a/src/test/resources/regression/verification/purescala/valid/Generics2.scala b/src/test/resources/regression/verification/purescala/valid/Generics2.scala
index 5bd3627d49d9b1a86dcb604da915bf3237bfaf1f..3ad9b7df9a5090a1abfa268f3bdbcbd7a57f2119 100644
--- a/src/test/resources/regression/verification/purescala/valid/Generics2.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Generics2.scala
@@ -7,10 +7,10 @@ object Generics1 {
case class Cons[A](head: A, tail: List[A]) extends List[A]
case class Nil[B]() extends List[B]
- def size[T](l: List[T]): Int = (l match {
- case Nil() => 0
- case Cons(h, t) => 1+size(t)
- })ensuring { _ >= 0 }
+ def size[T](l: List[T]): BigInt = (l match {
+ case Nil() => BigInt(0)
+ case Cons(h, t) => size(t) + BigInt(1)
+ }) ensuring((res: BigInt) => res >= BigInt(0))
def content[T](l: List[T]): Set[T] = l match {
case Nil() => Set()
@@ -21,7 +21,7 @@ object Generics1 {
Cons(a, l)
} ensuring { res => (size(res) == size(l) + 1) && (content(res) == content(l) ++ Set(a))}
- def insertInt(a: Int, l: List[Int]): List[Int] = {
+ def insertInt(a: BigInt, l: List[BigInt]): List[BigInt] = {
insert(a,l)
} ensuring { res => (size(res) == size(l) + 1) && (content(res) == content(l) ++ Set(a))}
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Heap.scala b/src/test/resources/regression/verification/purescala/valid/Heap.scala
index f70934816ca4b437b4cb08bded8bc6d586499ca0..f1464e8bcfbacf1b4ea2bc721e104d9309a98b44 100644
--- a/src/test/resources/regression/verification/purescala/valid/Heap.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Heap.scala
@@ -7,25 +7,25 @@ object Heaps {
/*~~~~~~~~~~~~~~~~~~~~~~~*/
/* Data type definitions */
/*~~~~~~~~~~~~~~~~~~~~~~~*/
- private case class Node(rank : Int, elem : Int, nodes : Heap)
+ private case class Node(rank : BigInt, elem : BigInt, nodes : Heap)
sealed abstract class Heap
private case class Nodes(head : Node, tail : Heap) extends Heap
private case object Empty extends Heap
sealed abstract class OptInt
- case class Some(value : Int) extends OptInt
+ case class Some(value : BigInt) extends OptInt
case object None extends OptInt
/*~~~~~~~~~~~~~~~~~~~~~~~*/
/* Abstraction functions */
/*~~~~~~~~~~~~~~~~~~~~~~~*/
- def heapContent(h : Heap) : Set[Int] = h match {
- case Empty => Set.empty[Int]
+ def heapContent(h : Heap) : Set[BigInt] = h match {
+ case Empty => Set.empty[BigInt]
case Nodes(n, ns) => nodeContent(n) ++ heapContent(ns)
}
- def nodeContent(n : Node) : Set[Int] = n match {
+ def nodeContent(n : Node) : Set[BigInt] = n match {
case Node(_, e, h) => Set(e) ++ heapContent(h)
}
@@ -78,13 +78,13 @@ object Heaps {
/*~~~~~~~~~~~~~~~~*/
def empty() : Heap = {
Empty
- } ensuring(res => heapContent(res) == Set.empty[Int])
+ } ensuring(res => heapContent(res) == Set.empty[BigInt])
def isEmpty(h : Heap) : Boolean = {
(h == Empty)
- } ensuring(res => res == (heapContent(h) == Set.empty[Int]))
+ } ensuring(res => res == (heapContent(h) == Set.empty[BigInt]))
- def insert(e : Int, h : Heap) : Heap = {
+ def insert(e : BigInt, h : Heap) : Heap = {
insertNode(Node(0, e, Empty), h)
} ensuring(res => heapContent(res) == heapContent(h) ++ Set(e))
diff --git a/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
index 820e9717857ecb98e3d5034d2de90a15b4a9cde9..a3120a9bc9e728ab5a6f352d649b64e9c67e761c 100644
--- a/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
+++ b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
@@ -13,8 +13,8 @@ object InsertionSort {
case class Some(value: Int) extends OptInt
case class None() extends OptInt
- def size(l : List) : Int = (l match {
- case Nil() => 0
+ def size(l : List) : BigInt = (l match {
+ case Nil() => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
diff --git a/src/test/resources/regression/verification/purescala/valid/ListOperations.scala b/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
deleted file mode 100644
index fb6b11d94c35c33ab4293712697906f2b91b46d3..0000000000000000000000000000000000000000
--- a/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
+++ /dev/null
@@ -1,105 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import scala.collection.immutable.Set
-import leon.annotation._
-import leon.lang._
-
-object ListOperations {
- sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil() extends List
-
- sealed abstract class IntPairList
- case class IPCons(head: IntPair, tail: IntPairList) extends IntPairList
- case class IPNil() extends IntPairList
-
- sealed abstract class IntPair
- case class IP(fst: Int, snd: Int) extends IntPair
-
- def size(l: List) : Int = (l match {
- case Nil() => 0
- case Cons(_, t) => 1 + size(t)
- }) ensuring(res => res >= 0)
-
- def iplSize(l: IntPairList) : Int = (l match {
- case IPNil() => 0
- case IPCons(_, xs) => 1 + iplSize(xs)
- }) ensuring(_ >= 0)
-
- def zip(l1: List, l2: List) : IntPairList = {
- // try to comment this and see how pattern-matching becomes
- // non-exhaustive and post-condition fails
- require(size(l1) == size(l2))
-
- l1 match {
- case Nil() => IPNil()
- case Cons(x, xs) => l2 match {
- case Cons(y, ys) => IPCons(IP(x, y), zip(xs, ys))
- }
- }
- } ensuring(iplSize(_) == size(l1))
-
- def sizeTailRec(l: List) : Int = sizeTailRecAcc(l, 0)
- def sizeTailRecAcc(l: List, acc: Int) : Int = {
- require(acc >= 0)
- l match {
- case Nil() => acc
- case Cons(_, xs) => sizeTailRecAcc(xs, acc+1)
- }
- } ensuring(res => res == size(l) + acc)
-
- def sizesAreEquiv(l: List) : Boolean = {
- size(l) == sizeTailRec(l)
- }.holds
-
- def content(l: List) : Set[Int] = l match {
- case Nil() => Set.empty[Int]
- case Cons(x, xs) => Set(x) ++ content(xs)
- }
-
- def sizeAndContent(l: List) : Boolean = {
- size(l) == 0 || content(l) != Set.empty[Int]
- }.holds
-
- def drunk(l : List) : List = (l match {
- case Nil() => Nil()
- case Cons(x,l1) => Cons(x,Cons(x,drunk(l1)))
- }) ensuring (size(_) == 2 * size(l))
-
- def reverse(l: List) : List = reverse0(l, Nil()) ensuring(content(_) == content(l))
- def reverse0(l1: List, l2: List) : List = (l1 match {
- case Nil() => l2
- case Cons(x, xs) => reverse0(xs, Cons(x, l2))
- }) ensuring(content(_) == content(l1) ++ content(l2))
-
- def append(l1 : List, l2 : List) : List = (l1 match {
- case Nil() => l2
- case Cons(x,xs) => Cons(x, append(xs, l2))
- }) ensuring(content(_) == content(l1) ++ content(l2))
-
- @induct
- def nilAppend(l : List) : Boolean = (append(l, Nil()) == l).holds
-
- @induct
- def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
- (append(append(xs, ys), zs) == append(xs, append(ys, zs))).holds
-
- @induct
- def sizeAppend(l1 : List, l2 : List) : Boolean =
- (size(append(l1, l2)) == size(l1) + size(l2)).holds
-
- @induct
- def concat(l1: List, l2: List) : List =
- concat0(l1, l2, Nil()) ensuring(content(_) == content(l1) ++ content(l2))
-
- @induct
- def concat0(l1: List, l2: List, l3: List) : List = (l1 match {
- case Nil() => l2 match {
- case Nil() => reverse(l3)
- case Cons(y, ys) => {
- concat0(Nil(), ys, Cons(y, l3))
- }
- }
- case Cons(x, xs) => concat0(xs, l2, Cons(x, l3))
- }) ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3))
-}
diff --git a/src/test/resources/regression/verification/purescala/valid/MergeSort.scala b/src/test/resources/regression/verification/purescala/valid/MergeSort.scala
index e3714371ba6a331c705d4f71a217ef223afe6209..de8b0c32b21cca1d1cbe869fe89dd3fb70d0cece 100644
--- a/src/test/resources/regression/verification/purescala/valid/MergeSort.scala
+++ b/src/test/resources/regression/verification/purescala/valid/MergeSort.scala
@@ -23,8 +23,8 @@ object MergeSort {
case LCons(x, xs) => content(x) ++ lContent(xs)
}
- def size(list : List) : Int = (list match {
- case Nil() => 0
+ def size(list : List) : BigInt = (list match {
+ case Nil() => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
@@ -40,7 +40,7 @@ object MergeSort {
case LCons(x, xs) => isSorted(x) && lIsSorted(xs)
}
- def abs(i : Int) : Int = {
+ def abs(i : BigInt) : BigInt = {
if(i < 0) -i else i
} ensuring(_ >= 0)
diff --git a/src/test/resources/regression/verification/purescala/valid/PositiveMap.scala b/src/test/resources/regression/verification/purescala/valid/PositiveMap.scala
index 7ee05ec9cffdc9789bfe4372586c20a882a84d37..0441ec26ca74f98dec17e05e91e487f0756b78ad 100644
--- a/src/test/resources/regression/verification/purescala/valid/PositiveMap.scala
+++ b/src/test/resources/regression/verification/purescala/valid/PositiveMap.scala
@@ -3,7 +3,7 @@ import leon.lang._
object PositiveMap {
abstract class List
- case class Cons(head: Int, tail: List) extends List
+ case class Cons(head: BigInt, tail: List) extends List
case class Nil() extends List
def positive(list: List): Boolean = list match {
@@ -11,7 +11,7 @@ object PositiveMap {
case Nil() => true
}
- def positiveMap_passing_1(f: (Int) => Int, list: List): List = {
+ def positiveMap_passing_1(f: (BigInt) => BigInt, list: List): List = {
list match {
case Cons(head, tail) =>
val fh = f(head)
@@ -21,7 +21,7 @@ object PositiveMap {
}
} ensuring { res => positive(res) }
- def positiveMap_passing_2(f: (Int) => Int, list: List): List = {
+ def positiveMap_passing_2(f: (BigInt) => BigInt, list: List): List = {
list match {
case Cons(head, tail) =>
val fh = f(head)
diff --git a/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala b/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
index 15f4ba78d016836e875e3727ed89138eea152a06..841befb415c77e3609b9ad7bf28a1e760d3ce39f 100644
--- a/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
+++ b/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
@@ -11,19 +11,19 @@ object RedBlackTree {
sealed abstract class Tree
case class Empty() extends Tree
- case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+ case class Node(color: Color, left: Tree, value: BigInt, right: Tree) extends Tree
sealed abstract class OptionInt
- case class Some(v : Int) extends OptionInt
+ case class Some(v : BigInt) extends OptionInt
case class None() extends OptionInt
- def content(t: Tree) : Set[Int] = t match {
+ def content(t: Tree) : Set[BigInt] = t match {
case Empty() => Set.empty
case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
}
- def size(t: Tree) : Int = (t match {
- case Empty() => 0
+ def size(t: Tree) : BigInt = (t match {
+ case Empty() => BigInt(0)
case Node(_, l, v, r) => size(l) + 1 + size(r)
}) ensuring(_ >= 0)
@@ -50,14 +50,14 @@ object RedBlackTree {
case Empty() => true
}
- def blackHeight(t : Tree) : Int = t match {
+ def blackHeight(t : Tree) : BigInt = t match {
case Empty() => 1
case Node(Black(), l, _, _) => blackHeight(l) + 1
case Node(Red(), l, _, _) => blackHeight(l)
}
// <<insert element x into the tree t>>
- def ins(x: Int, t: Tree): Tree = {
+ def ins(x: BigInt, t: Tree): Tree = {
require(redNodesHaveBlackChildren(t) && blackBalanced(t))
t match {
case Empty() => Node(Red(),Empty(),x,Empty())
@@ -79,12 +79,12 @@ object RedBlackTree {
}
} ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res))
- def add(x: Int, t: Tree): Tree = {
+ def add(x: BigInt, t: Tree): Tree = {
require(redNodesHaveBlackChildren(t) && blackBalanced(t))
makeBlack(ins(x, t))
} ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res))
- def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ def balance(c: Color, a: Tree, x: BigInt, b: Tree): Tree = {
Node(c,a,x,b) match {
case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
diff --git a/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala b/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
index bf259ab0f480ee303c3ee27a878984fe9f488876..bd0596fbaab48f4a64309e71d019db53ed72db2a 100644
--- a/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
+++ b/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
@@ -9,8 +9,8 @@ object SearchLinkedList {
case class Cons(head : Int, tail : List) extends List
case class Nil() extends List
- def size(list : List) : Int = (list match {
- case Nil() => 0
+ def size(list : List) : BigInt = (list match {
+ case Nil() => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
@@ -19,9 +19,9 @@ object SearchLinkedList {
case Cons(x, xs) => x == elem || contains(xs, elem)
})
- def firstZero(list : List) : Int = (list match {
- case Nil() => 0
- case Cons(x, xs) => if (x == 0) 0 else firstZero(xs) + 1
+ def firstZero(list : List) : BigInt = (list match {
+ case Nil() => BigInt(0)
+ case Cons(x, xs) => if (x == 0) BigInt(0) else firstZero(xs) + 1
}) ensuring (res =>
res >= 0 && (if (contains(list, 0)) {
firstZeroAtPos(list, res)
@@ -29,14 +29,14 @@ object SearchLinkedList {
res == size(list)
}))
- def firstZeroAtPos(list : List, pos : Int) : Boolean = {
+ def firstZeroAtPos(list : List, pos : BigInt) : Boolean = {
list match {
case Nil() => false
- case Cons(x, xs) => if (pos == 0) x == 0 else x != 0 && firstZeroAtPos(xs, pos - 1)
+ case Cons(x, xs) => if (pos == BigInt(0)) x == 0 else x != 0 && firstZeroAtPos(xs, pos - 1)
}
}
- def goal(list : List, i : Int) : Boolean = {
+ def goal(list : List, i : BigInt) : Boolean = {
if(firstZero(list) == i) {
if(contains(list, 0)) {
firstZeroAtPos(list, i)
diff --git a/src/test/resources/regression/verification/xlang/invalid/Mean.scala b/src/test/resources/regression/verification/xlang/invalid/Mean.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f6e8757d5f12e82ac472e764780dce12d17a187a
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Mean.scala
@@ -0,0 +1,12 @@
+import scala.collection.immutable.Set
+import leon.annotation._
+import leon.lang._
+
+object Mean {
+
+ def meanOverflow(x: Int, y: Int): Int = {
+ require(x <= y && x >= 0 && y >= 0)
+ (x + y)/2
+ } ensuring(m => m >= x && m <= y)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Arithmetic.scala b/src/test/resources/regression/verification/xlang/valid/Arithmetic.scala
index 56baab22fe29220879459d2927fc9c667412894d..2e080a90c7245efe9490d2cf208612cc0280c271 100644
--- a/src/test/resources/regression/verification/xlang/valid/Arithmetic.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Arithmetic.scala
@@ -5,17 +5,17 @@ import leon.lang._
object Arithmetic {
/* VSTTE 2008 - Dafny paper */
- def mult(x : Int, y : Int): Int = ({
- var r = 0
+ def mult(x : BigInt, y : BigInt): BigInt = ({
+ var r: BigInt = 0
if(y < 0) {
var n = y
- (while(n != 0) {
+ (while(n != BigInt(0)) {
r = r - x
n = n + 1
}) invariant(r == x * (y - n) && 0 <= -n)
} else {
var n = y
- (while(n != 0) {
+ (while(n != BigInt(0)) {
r = r + x
n = n - 1
}) invariant(r == x * (y - n) && 0 <= n)
@@ -24,17 +24,17 @@ object Arithmetic {
}) ensuring(_ == x*y)
/* VSTTE 2008 - Dafny paper */
- def add(x : Int, y : Int): Int = ({
+ def add(x : BigInt, y : BigInt): BigInt = ({
var r = x
if(y < 0) {
var n = y
- (while(n != 0) {
+ (while(n != BigInt(0)) {
r = r - 1
n = n + 1
}) invariant(r == x + y - n && 0 <= -n)
} else {
var n = y
- (while(n != 0) {
+ (while(n != BigInt(0)) {
r = r + 1
n = n - 1
}) invariant(r == x + y - n && 0 <= n)
@@ -43,10 +43,10 @@ object Arithmetic {
}) ensuring(_ == x+y)
- def sum(n: Int): Int = {
+ def sum(n: BigInt): BigInt = {
require(n >= 0)
- var r = 0
- var i = 0
+ var r = BigInt(0)
+ var i = BigInt(0)
(while(i < n) {
i = i + 1
r = r + i
@@ -54,10 +54,10 @@ object Arithmetic {
r
} ensuring(_ >= n)
- def divide(x: Int, y: Int): (Int, Int) = {
+ def divide(x: BigInt, y: BigInt): (BigInt, BigInt) = {
require(x >= 0 && y > 0)
var r = x
- var q = 0
+ var q = BigInt(0)
(while(r >= y) {
r = r - y
q = q + 1
diff --git a/src/test/resources/regression/verification/xlang/valid/Mean.scala b/src/test/resources/regression/verification/xlang/valid/Mean.scala
new file mode 100644
index 0000000000000000000000000000000000000000..447553e95006e3430b9b22bcc88f0d0800391dbf
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Mean.scala
@@ -0,0 +1,12 @@
+import scala.collection.immutable.Set
+import leon.annotation._
+import leon.lang._
+
+object Mean {
+
+ def mean(x: Int, y: Int): Int = {
+ require(x <= y && x >= 0 && y >= 0)
+ x + (y - x)/2
+ } ensuring(m => m >= x && m <= y)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested2.scala b/src/test/resources/regression/verification/xlang/valid/Nested2.scala
index da94f93d6fee5db8ff425a8f10aa8ec23b22d7f1..35cbb861183aaff59932a3e71d4eda97bd461d3a 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested2.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested2.scala
@@ -2,10 +2,10 @@
object Nested2 {
- def foo(a: Int): Int = {
+ def foo(a: BigInt): BigInt = {
require(a >= 0)
val b = a + 2
- def rec1(c: Int): Int = {
+ def rec1(c: BigInt): BigInt = {
require(c >= 0)
b + c
}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested3.scala b/src/test/resources/regression/verification/xlang/valid/Nested3.scala
index 81b7483375b9225beab3cb486d40d1bea9a0204a..05449370531b823999b4b40683db662b457abfd2 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested3.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested3.scala
@@ -2,11 +2,11 @@
object Nested3 {
- def foo(a: Int): Int = {
+ def foo(a: BigInt): BigInt = {
require(a >= 0 && a <= 50)
val b = a + 2
val c = a + b
- def rec1(d: Int): Int = {
+ def rec1(d: BigInt): BigInt = {
require(d >= 0 && d <= 50)
val e = d + b + c
e
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested4.scala b/src/test/resources/regression/verification/xlang/valid/Nested4.scala
index cb91848ee813e4c602f73e88b65c555c5f3b8685..7b82532dfed6c5b4ced77eee01840e39a5751d83 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested4.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested4.scala
@@ -2,20 +2,20 @@
object Nested4 {
- def foo(a: Int, a2: Int): Int = {
+ def foo(a: BigInt, a2: BigInt): BigInt = {
require(a >= 0 && a <= 50)
val b = a + 2
val c = a + b
if(a2 > a) {
- def rec1(d: Int): Int = {
+ def rec1(d: BigInt): BigInt = {
require(d >= 0 && d <= 50)
val e = d + b + c + a2
e
} ensuring(_ > 0)
rec1(2)
} else {
- 5
+ BigInt(5)
}
- } ensuring(_ > 0)
+ } ensuring(x => x > 0)
}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested6.scala b/src/test/resources/regression/verification/xlang/valid/Nested6.scala
index 305870f843d9ec22b94bc5e7274d8a8cb2b8b9b5..f7bfa772fa2f31ac30efa8fd3c1be5be6813318b 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested6.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested6.scala
@@ -2,15 +2,15 @@
object Nested5 {
- def foo(a: Int): Int = {
+ def foo(a: BigInt): BigInt = {
require(a >= 0)
- def bar(b: Int): Int = {
+ def bar(b: BigInt): BigInt = {
require(b > 0)
b + 3
} ensuring(prop(a, b) && a >= 0 && _ == b + 3)
bar(2)
- } ensuring(a >= 0 && _ == 5)
+ } ensuring(a >= 0 && _ == BigInt(5))
- def prop(x: Int, y: Int): Boolean = x + y > 0
+ def prop(x: BigInt, y: BigInt): Boolean = x + y > 0
}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested7.scala b/src/test/resources/regression/verification/xlang/valid/Nested7.scala
index 2f785f083c871923c6021e29bf4f10ae7d82f5e0..4187e7b0fb31affe67314cb072be128ef386ca5b 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested7.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested7.scala
@@ -2,10 +2,10 @@
object Nested2 {
- def foo(a: Int): Int = {
+ def foo(a: BigInt): BigInt = {
require(a >= 0)
val b = a + 2
- def rec1(c: Int): Int = {
+ def rec1(c: BigInt): BigInt = {
require(c >= 0)
b + c + bar(a) + bar(b) + bar(c)
}
@@ -13,7 +13,7 @@ object Nested2 {
} ensuring(_ > 0)
- def bar(x: Int): Int = {
+ def bar(x: BigInt): BigInt = {
require(x >= 0)
x
} ensuring(_ >= 0)
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested8.scala b/src/test/resources/regression/verification/xlang/valid/Nested8.scala
index 4024de42cec25892dd26ba08a4af0b83ea921150..6bcb9050ba953d96d7ea7f9f74b9e477d989dcc6 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested8.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested8.scala
@@ -4,12 +4,12 @@ import leon.lang._
object Nested8 {
- def foo(a: Int): Int = {
+ def foo(a: BigInt): BigInt = {
require(a > 0)
- def bar(b: Int): Int = {
+ def bar(b: BigInt): BigInt = {
if(a < b) {
- def rec(c: Int): Int = {
+ def rec(c: BigInt): BigInt = {
require(c > 0)
c + b
} ensuring(_ > 0)
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested9.scala b/src/test/resources/regression/verification/xlang/valid/Nested9.scala
index 14f912137f6a38b7e8057916135f28fee3e1d2d0..148ba3a589cf1d61003bd9f79d4a7d04f994416f 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested9.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested9.scala
@@ -2,15 +2,15 @@
object Nested4 {
- def foo(a: Int, a2: Int): Int = {
+ def foo(a: BigInt, a2: BigInt): BigInt = {
require(a >= 0 && a <= 50)
val b = a + 2
val c = a + b
if(a2 > a) {
- def rec1(d: Int): Int = {
+ def rec1(d: BigInt): BigInt = {
require(d >= 0 && d <= 50)
val e = d + b + c + a2
- def rec2(f: Int): Int = {
+ def rec2(f: BigInt): BigInt = {
require(f >= c)
f + e
} ensuring(_ > 0)
@@ -18,7 +18,7 @@ object Nested4 {
} ensuring(_ > 0)
rec1(2)
} else {
- 5
+ BigInt(5)
}
} ensuring(_ > 0)
diff --git a/src/test/scala/leon/test/codegen/CodeGenTests.scala b/src/test/scala/leon/test/codegen/CodeGenTests.scala
index af02b00a9f56e09c9f8a9ebad3247ce3d8d95bf9..1e0ad3a1172c330ea22a15cee2b434535b3358de 100644
--- a/src/test/scala/leon/test/codegen/CodeGenTests.scala
+++ b/src/test/scala/leon/test/codegen/CodeGenTests.scala
@@ -104,7 +104,20 @@ class CodeGenTests extends test.LeonTestSuite {
}
}""",
IntLiteral(1)
- ),
+ ),
+
+ TestCase("simpleBigInt", """
+ object simple {
+ abstract class Abs
+ case class Conc(x : BigInt) extends Abs
+ def test = {
+ val c = Conc(1)
+ c.x
+
+ }
+ }""",
+ InfiniteIntegerLiteral(1)
+ ),
TestCase("eager", """
object eager {
@@ -158,6 +171,19 @@ class CodeGenTests extends test.LeonTestSuite {
IntLiteral(10)
),
+ TestCase("methSimpleBignt", """
+ object methSimple {
+
+ sealed abstract class Ab {
+ def f2(x : BigInt): BigInt = x + 5
+ }
+ case class Con() extends Ab { }
+
+ def test = Con().f2(5)
+ }""",
+ InfiniteIntegerLiteral(10)
+ ),
+
TestCase("methods", """
object methods {
def f1 = 4
diff --git a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
index 0dd8fe1d38ab195ddd2b7d6f0d13d86b2af6f7ea..7dd1b474266c3fb7ea6e850174deef78c0b59a93 100644
--- a/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
+++ b/src/test/scala/leon/test/evaluators/DefaultEvaluatorTests.scala
@@ -34,19 +34,32 @@ class DefaultEvaluatorTests extends leon.test.LeonTestSuite {
expectSuccessful(defaultEvaluator.eval(IntLiteral(0)), IntLiteral(0))
expectSuccessful(defaultEvaluator.eval(IntLiteral(42)), IntLiteral(42))
expectSuccessful(defaultEvaluator.eval(UnitLiteral()), UnitLiteral())
+ expectSuccessful(defaultEvaluator.eval(InfiniteIntegerLiteral(0)), InfiniteIntegerLiteral(0))
+ expectSuccessful(defaultEvaluator.eval(InfiniteIntegerLiteral(42)), InfiniteIntegerLiteral(42))
+ }
+
+ test("eval of simple bit vector arithmetic expressions") {
+ expectSuccessful(defaultEvaluator.eval(BVPlus(IntLiteral(3), IntLiteral(5))), IntLiteral(8))
+ expectSuccessful(defaultEvaluator.eval(BVPlus(IntLiteral(0), IntLiteral(5))), IntLiteral(5))
+ expectSuccessful(defaultEvaluator.eval(BVTimes(IntLiteral(3), IntLiteral(3))), IntLiteral(9))
}
test("eval of simple arithmetic expressions") {
expectSuccessful(
- defaultEvaluator.eval(Plus(IntLiteral(3), IntLiteral(5))), IntLiteral(8))
+ defaultEvaluator.eval(Plus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(5))),
+ InfiniteIntegerLiteral(8))
expectSuccessful(
- defaultEvaluator.eval(Minus(IntLiteral(7), IntLiteral(2))), IntLiteral(5))
+ defaultEvaluator.eval(Minus(InfiniteIntegerLiteral(7), InfiniteIntegerLiteral(2))),
+ InfiniteIntegerLiteral(5))
expectSuccessful(
- defaultEvaluator.eval(UMinus(IntLiteral(7))), IntLiteral(-7))
+ defaultEvaluator.eval(UMinus(InfiniteIntegerLiteral(7))),
+ InfiniteIntegerLiteral(-7))
expectSuccessful(
- defaultEvaluator.eval(Times(IntLiteral(2), IntLiteral(3))), IntLiteral(6))
+ defaultEvaluator.eval(Times(InfiniteIntegerLiteral(2), InfiniteIntegerLiteral(3))),
+ InfiniteIntegerLiteral(6))
expectSuccessful(
- defaultEvaluator.eval(Modulo(IntLiteral(10), IntLiteral(3))), IntLiteral(1))
+ defaultEvaluator.eval(Modulo(InfiniteIntegerLiteral(10), InfiniteIntegerLiteral(3))),
+ InfiniteIntegerLiteral(1))
}
test("Eval of simple boolean operations") {
@@ -146,4 +159,5 @@ class DefaultEvaluatorTests extends leon.test.LeonTestSuite {
Map(id -> IntLiteral(27))),
FiniteArray(Map(), Some(IntLiteral(27)), IntLiteral(7)))
}
+
}
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 5828635a309ca2b517fc454b13ed252cc7da30b7..5a0599b41c525a2e737540dfddd22768d98432e5 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -183,10 +183,10 @@ class EvaluatorsTests extends leon.test.LeonTestSuite {
for(e <- evaluators) {
// Some simple math.
- checkComp(e, mkCall("plus", IL(60), UMinus(IL(18))), IL(42))
+ checkComp(e, mkCall("plus", IL(60), BVUMinus(IL(18))), IL(42))
checkComp(e, mkCall("max", IL(4), IL(42)), IL(42))
- checkComp(e, mkCall("max", IL(42), UMinus(IL(42))), IL(42))
- checkComp(e, mkCall("intSqrt", UMinus(IL(1800))), IL(42))
+ checkComp(e, mkCall("max", IL(42), BVUMinus(IL(42))), IL(42))
+ checkComp(e, mkCall("intSqrt", BVUMinus(IL(1800))), IL(42))
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))
diff --git a/src/test/scala/leon/test/purescala/LikelyEq.scala b/src/test/scala/leon/test/purescala/LikelyEq.scala
index 3dd28dfc7032b569293e79cefb1feea63858914a..7fd0341232eb79a7f3e5ae91fb069388ec700ea2 100644
--- a/src/test/scala/leon/test/purescala/LikelyEq.scala
+++ b/src/test/scala/leon/test/purescala/LikelyEq.scala
@@ -50,7 +50,7 @@ trait WithLikelyEq {
var cont = true
while(i < counters.size && isEq) {
- val m: Map[Expr, Expr] = vsOrder.zip(counters).map{case (v, c) => (Variable(v), IntLiteral(c))}.toMap
+ val m: Map[Expr, Expr] = vsOrder.zip(counters).map{case (v, c) => (Variable(v), InfiniteIntegerLiteral(c))}.toMap
val ne1 = replace(m, e1)
val ne2 = replace(m, e2)
val npre = replace(m, pre)
diff --git a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
index 8c367a0cea64c914304b6007c43a0210241af7fe..fced5df182f3888a37c16227c4b1dc03e6a831a8 100644
--- a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
+++ b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
@@ -6,42 +6,43 @@ import leon._
import leon.test._
import leon.purescala.Common._
import leon.purescala.Trees._
+import leon.purescala.TypeTrees._
class LikelyEqSuite extends LeonTestSuite with WithLikelyEq {
- def i(x: Int) = IntLiteral(x)
+ def i(x: Int) = InfiniteIntegerLiteral(x)
- val xId = FreshIdentifier("x")
+ val xId = FreshIdentifier("x").setType(IntegerType)
val x = Variable(xId)
- val yId = FreshIdentifier("y")
+ val yId = FreshIdentifier("y").setType(IntegerType)
val y = Variable(yId)
- val zId = FreshIdentifier("z")
+ val zId = FreshIdentifier("z").setType(IntegerType)
val z = Variable(zId)
test("apply") {
- assert(LikelyEq(Plus(x, x), Times(IntLiteral(2), x), Set(xId)))
- assert(LikelyEq(Plus(x, x), Times(x, IntLiteral(2)), Set(xId)))
+ assert(LikelyEq(Plus(x, x), Times(i(2), x), Set(xId)))
+ assert(LikelyEq(Plus(x, x), Times(x, i(2)), Set(xId)))
assert(LikelyEq(Plus(x, y), Plus(y, x), Set(xId, yId)))
- assert(LikelyEq(Plus(Plus(x, y), y), Plus(x, Times(IntLiteral(2), y)), Set(xId, yId)))
+ assert(LikelyEq(Plus(Plus(x, y), y), Plus(x, Times(i(2), y)), Set(xId, yId)))
def defaultCompare(e1: Expr, e2: Expr) = e1 == e2
assert(LikelyEq(
- Plus(IntLiteral(2), Plus(x, y)),
- Plus(IntLiteral(3), Plus(x, z)),
+ Plus(i(2), Plus(x, y)),
+ Plus(i(3), Plus(x, z)),
Set(xId),
BooleanLiteral(true),
defaultCompare,
- Map(yId -> IntLiteral(2), zId -> IntLiteral(1)))
+ Map(yId -> i(2), zId -> i(1)))
)
assert(LikelyEq(
- Plus(x, Times(IntLiteral(2), Division(y, IntLiteral(2))))
+ Plus(x, Times(i(2), Division(y, i(2))))
, Plus(x, y)
, Set(xId, yId)
- , Equals(Modulo(y, IntLiteral(2)), IntLiteral(0))
+ , Equals(Modulo(y, i(2)), i(0))
))
}
diff --git a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
index f05a5ddef590cce7b5c2145071cc1d4332232ddc..75dd1090343521ca272e21d6a6199df844f4a5ae 100644
--- a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
@@ -13,17 +13,17 @@ import leon.purescala.TreeOps._
import leon.purescala.TreeNormalizations._
class TreeNormalizationsTests extends LeonTestSuite with WithLikelyEq {
- def i(x: Int) = IntLiteral(x)
+ def i(x: Int) = InfiniteIntegerLiteral(x)
- val xId = FreshIdentifier("x").setType(Int32Type)
+ val xId = FreshIdentifier("x").setType(IntegerType)
val x = Variable(xId)
- val yId = FreshIdentifier("y").setType(Int32Type)
+ val yId = FreshIdentifier("y").setType(IntegerType)
val y = Variable(yId)
val xs = Set(xId, yId)
- val aId = FreshIdentifier("a").setType(Int32Type)
+ val aId = FreshIdentifier("a").setType(IntegerType)
val a = Variable(aId)
- val bId = FreshIdentifier("b").setType(Int32Type)
+ val bId = FreshIdentifier("b").setType(IntegerType)
val b = Variable(bId)
val as = Set(aId, bId)
@@ -35,7 +35,7 @@ class TreeNormalizationsTests extends LeonTestSuite with WithLikelyEq {
}
def toSum(es: Seq[Expr]) = es.reduceLeft(Plus(_, _))
- def coefToSum(es: Array[Expr], vs: Array[Expr]) = (es.zip(Array[Expr](IntLiteral(1)) ++ vs)).foldLeft[Expr](IntLiteral(0))((acc, p) => Plus(acc, Times(p._1, p._2)))
+ def coefToSum(es: Array[Expr], vs: Array[Expr]) = (es.zip(Array[Expr](InfiniteIntegerLiteral(1)) ++ vs)).foldLeft[Expr](InfiniteIntegerLiteral(0))((acc, p) => Plus(acc, Times(p._1, p._2)))
test("checkSameExpr") {
checkSameExpr(Plus(x, y), Plus(y, x), xs)
@@ -80,5 +80,8 @@ class TreeNormalizationsTests extends LeonTestSuite with WithLikelyEq {
val e3 = Minus(Plus(x, i(3)), Plus(y, i(2)))
checkSameExpr(coefToSum(linearArithmeticForm(e3, xsOrder), Array(x, y)), e3, xs)
+ val e4 = Plus(Plus(i(0), i(2)), Times(i(-1), i(3)))
+ assert(linearArithmeticForm(e4, Array()) === Array(i(-1)))
+
}
}
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTests.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
index 4bcce108d9927dfd1ee430ede115511e36eb8aee..7137ebd34ad4c0245d68ebc5bc4807221134a3ab 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -41,17 +41,17 @@ class TreeOpsTests extends LeonTestSuite with WithLikelyEq {
}
- def i(x: Int) = IntLiteral(x)
+ def i(x: Int) = InfiniteIntegerLiteral(x)
- val xId = FreshIdentifier("x").setType(Int32Type)
+ val xId = FreshIdentifier("x").setType(IntegerType)
val x = Variable(xId)
- val yId = FreshIdentifier("y").setType(Int32Type)
+ val yId = FreshIdentifier("y").setType(IntegerType)
val y = Variable(yId)
val xs = Set(xId, yId)
- val aId = FreshIdentifier("a").setType(Int32Type)
+ val aId = FreshIdentifier("a").setType(IntegerType)
val a = Variable(aId)
- val bId = FreshIdentifier("b").setType(Int32Type)
+ val bId = FreshIdentifier("b").setType(IntegerType)
val b = Variable(bId)
val as = Set(aId, bId)
@@ -62,36 +62,36 @@ class TreeOpsTests extends LeonTestSuite with WithLikelyEq {
}
test("simplifyArithmetic") {
- val e1 = Plus(IntLiteral(3), IntLiteral(2))
+ val e1 = Plus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2))
checkSameExpr(e1, simplifyArithmetic(e1), Set())
- val e2 = Plus(x, Plus(IntLiteral(3), IntLiteral(2)))
+ val e2 = Plus(x, Plus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2)))
checkSameExpr(e2, simplifyArithmetic(e2), Set(xId))
- val e3 = Minus(IntLiteral(3), IntLiteral(2))
+ val e3 = Minus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2))
checkSameExpr(e3, simplifyArithmetic(e3), Set())
- val e4 = Plus(x, Minus(IntLiteral(3), IntLiteral(2)))
+ val e4 = Plus(x, Minus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2)))
checkSameExpr(e4, simplifyArithmetic(e4), Set(xId))
- val e5 = Plus(x, Minus(x, IntLiteral(2)))
+ val e5 = Plus(x, Minus(x, InfiniteIntegerLiteral(2)))
checkSameExpr(e5, simplifyArithmetic(e5), Set(xId))
- val e6 = Times(IntLiteral(9), Plus(Division(x, IntLiteral(3)), Division(x, IntLiteral(6))))
+ val e6 = Times(InfiniteIntegerLiteral(9), Plus(Division(x, InfiniteIntegerLiteral(3)), Division(x, InfiniteIntegerLiteral(6))))
checkSameExpr(e6, simplifyArithmetic(e6), Set(xId))
}
test("expandAndSimplifyArithmetic") {
- val e1 = Plus(IntLiteral(3), IntLiteral(2))
+ val e1 = Plus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2))
checkSameExpr(e1, expandAndSimplifyArithmetic(e1), Set())
- val e2 = Plus(x, Plus(IntLiteral(3), IntLiteral(2)))
+ val e2 = Plus(x, Plus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2)))
checkSameExpr(e2, expandAndSimplifyArithmetic(e2), Set(xId))
- val e3 = Minus(IntLiteral(3), IntLiteral(2))
+ val e3 = Minus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2))
checkSameExpr(e3, expandAndSimplifyArithmetic(e3), Set())
- val e4 = Plus(x, Minus(IntLiteral(3), IntLiteral(2)))
+ val e4 = Plus(x, Minus(InfiniteIntegerLiteral(3), InfiniteIntegerLiteral(2)))
checkSameExpr(e4, expandAndSimplifyArithmetic(e4), Set(xId))
- val e5 = Plus(x, Minus(x, IntLiteral(2)))
+ val e5 = Plus(x, Minus(x, InfiniteIntegerLiteral(2)))
checkSameExpr(e5, expandAndSimplifyArithmetic(e5), Set(xId))
- val e6 = Times(IntLiteral(9), Plus(Division(x, IntLiteral(3)), Division(x, IntLiteral(6))))
+ val e6 = Times(InfiniteIntegerLiteral(9), Plus(Division(x, InfiniteIntegerLiteral(3)), Division(x, InfiniteIntegerLiteral(6))))
checkSameExpr(e6, expandAndSimplifyArithmetic(e6), Set(xId))
}
@@ -124,10 +124,10 @@ class TreeOpsTests extends LeonTestSuite with WithLikelyEq {
}
test("pre and post traversal") {
- val expr = Plus(IntLiteral(1), Minus(IntLiteral(2), IntLiteral(3)))
+ val expr = Plus(InfiniteIntegerLiteral(1), Minus(InfiniteIntegerLiteral(2), InfiniteIntegerLiteral(3)))
var res = ""
def f(e: Expr): Unit = e match {
- case IntLiteral(i) => res += i
+ case InfiniteIntegerLiteral(i) => res += i
case _ : Plus => res += "P"
case _ : Minus => res += "M"
}
@@ -141,18 +141,18 @@ class TreeOpsTests extends LeonTestSuite with WithLikelyEq {
}
test("pre- and postMap") {
- val expr = Plus(IntLiteral(1), Minus(IntLiteral(2), IntLiteral(3)))
+ val expr = Plus(InfiniteIntegerLiteral(1), Minus(InfiniteIntegerLiteral(2), InfiniteIntegerLiteral(3)))
def op(e : Expr ) = e match {
- case Minus(IntLiteral(2), e2) => Some(IntLiteral(2))
- case IntLiteral(1) => Some(IntLiteral(2))
- case IntLiteral(2) => Some(IntLiteral(42))
+ case Minus(InfiniteIntegerLiteral(two), e2) if two == BigInt(2) => Some(InfiniteIntegerLiteral(2))
+ case InfiniteIntegerLiteral(one) if one == BigInt(1) => Some(InfiniteIntegerLiteral(2))
+ case InfiniteIntegerLiteral(two) if two == BigInt(2) => Some(InfiniteIntegerLiteral(42))
case _ => None
}
- assert( preMap(op, false)(expr) == Plus(IntLiteral(2), IntLiteral(2)) )
- assert( preMap(op, true )(expr) == Plus(IntLiteral(42), IntLiteral(42)) )
- assert( postMap(op, false)(expr) == Plus(IntLiteral(2), Minus(IntLiteral(42), IntLiteral(3))) )
- assert( postMap(op, true)(expr) == Plus(IntLiteral(42), Minus(IntLiteral(42), IntLiteral(3))) )
+ assert( preMap(op, false)(expr) == Plus(InfiniteIntegerLiteral(2), InfiniteIntegerLiteral(2)) )
+ assert( preMap(op, true )(expr) == Plus(InfiniteIntegerLiteral(42), InfiniteIntegerLiteral(42)) )
+ assert( postMap(op, false)(expr) == Plus(InfiniteIntegerLiteral(2), Minus(InfiniteIntegerLiteral(42), InfiniteIntegerLiteral(3))) )
+ assert( postMap(op, true)(expr) == Plus(InfiniteIntegerLiteral(42), Minus(InfiniteIntegerLiteral(42), InfiniteIntegerLiteral(3))) )
}
diff --git a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
index 0c4bd2791ed8371542f7b3918260b52914c26794..4f156461982efcaea69db1de5a0498c9f758801e 100644
--- a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
@@ -56,14 +56,14 @@ class TimeoutSolverTests extends LeonTestSuite {
assert(check(sf, BooleanLiteral(true)) === None)
assert(check(sf, BooleanLiteral(false)) === None)
- val x = Variable(FreshIdentifier("x").setType(Int32Type))
+ val x = Variable(FreshIdentifier("x").setType(IntegerType))
assert(check(sf, Equals(x, x)) === None)
}
test("TimeoutSolver 2") {
val sf = getTOSolver
- val x = Variable(FreshIdentifier("x").setType(Int32Type))
- val o = IntLiteral(1)
+ val x = Variable(FreshIdentifier("x").setType(IntegerType))
+ val o = InfiniteIntegerLiteral(1)
assert(check(sf, Equals(Plus(x, o), Plus(o, x))) === None)
assert(check(sf, Equals(Plus(x, o), x)) === None)
}
diff --git a/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala b/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
index 94ed51f643d5991cd2db73dad9cfddf37a1fb751..46f56b4e796042daa7de619b28a50837433a4fda 100644
--- a/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/UnrollingSolverTests.scala
@@ -12,14 +12,14 @@ import leon.solvers.combinators._
class UnrollingSolverTests extends LeonTestSuite {
- private val fx : Identifier = FreshIdentifier("x").setType(Int32Type)
- private val fres : Identifier = FreshIdentifier("res").setType(Int32Type)
- private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, Int32Type, ValDef(fx, Int32Type) :: Nil, DefType.MethodDef)
- fDef.body = Some(IfExpr(GreaterThan(Variable(fx), IntLiteral(0)),
- Plus(Variable(fx), FunctionInvocation(fDef.typed, Seq(Minus(Variable(fx), IntLiteral(1))))),
- IntLiteral(1)
+ private val fx : Identifier = FreshIdentifier("x").setType(IntegerType)
+ private val fres : Identifier = FreshIdentifier("res").setType(IntegerType)
+ private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx, IntegerType) :: Nil, DefType.MethodDef)
+ fDef.body = Some(IfExpr(GreaterThan(Variable(fx), InfiniteIntegerLiteral(0)),
+ Plus(Variable(fx), FunctionInvocation(fDef.typed, Seq(Minus(Variable(fx), InfiniteIntegerLiteral(1))))),
+ InfiniteIntegerLiteral(1)
))
- fDef.postcondition = Some(fres -> GreaterThan(Variable(fres), IntLiteral(0)))
+ fDef.postcondition = Some(fres -> GreaterThan(Variable(fres), InfiniteIntegerLiteral(0)))
private val program = Program(
FreshIdentifier("Minimal"),
@@ -42,6 +42,6 @@ class UnrollingSolverTests extends LeonTestSuite {
check(BooleanLiteral(true), Some(true), "'true' should always be valid")
check(BooleanLiteral(false), Some(false), "'false' should never be valid")
- check(Not(GreaterThan(FunctionInvocation(fDef.typed, Seq(Variable(FreshIdentifier("toto").setType(Int32Type)))), IntLiteral(0))),
+ check(Not(GreaterThan(FunctionInvocation(fDef.typed, Seq(Variable(FreshIdentifier("toto").setType(IntegerType)))), InfiniteIntegerLiteral(0))),
Some(false), "unrolling should enable recursive definition verification")
}
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
index bde8cc42346edb8b5c2e53821f9a153e6e94c264..c5662615ef3d7fb189cae9a86fa664af93530976 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
@@ -38,9 +38,9 @@ class FairZ3SolverTests extends LeonTestSuite {
)
// def f(fx : Int) : Int = fx + 1
- private val fx : Identifier = FreshIdentifier("x").setType(Int32Type)
- private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, Int32Type, ValDef(fx, Int32Type) :: Nil, DefType.MethodDef)
- fDef.body = Some(Plus(Variable(fx), IntLiteral(1)))
+ private val fx : Identifier = FreshIdentifier("x").setType(IntegerType)
+ private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx, IntegerType) :: Nil, DefType.MethodDef)
+ fDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
private val minimalProgram = Program(
FreshIdentifier("Minimal"),
@@ -50,8 +50,8 @@ class FairZ3SolverTests extends LeonTestSuite {
)))
)
- private val x : Expr = Variable(FreshIdentifier("x").setType(Int32Type))
- private val y : Expr = Variable(FreshIdentifier("y").setType(Int32Type))
+ private val x : Expr = Variable(FreshIdentifier("x").setType(IntegerType))
+ private val y : Expr = Variable(FreshIdentifier("y").setType(IntegerType))
private def f(e : Expr) : Expr = FunctionInvocation(fDef.typed, e :: Nil)
private val solver = SimpleSolverAPI(SolverFactory(() => new FairZ3Solver(testContext, minimalProgram)))
@@ -59,7 +59,7 @@ class FairZ3SolverTests extends LeonTestSuite {
private val tautology1 : Expr = BooleanLiteral(true)
assertValid(solver, tautology1)
- private val tautology2 : Expr = Equals(Plus(x, x), Times(IntLiteral(2), x))
+ private val tautology2 : Expr = Equals(Plus(x, x), Times(InfiniteIntegerLiteral(2), x))
assertValid(solver, tautology2)
// This one contains a function invocation but is valid regardless of its
@@ -73,11 +73,11 @@ class FairZ3SolverTests extends LeonTestSuite {
private val wrong1 : Expr = BooleanLiteral(false)
assertInvalid(solver, wrong1)
- private val wrong2 : Expr = Equals(Plus(x, x), Times(IntLiteral(3), x))
+ private val wrong2 : Expr = Equals(Plus(x, x), Times(InfiniteIntegerLiteral(3), x))
assertInvalid(solver, wrong2)
// This is true, and FairZ3Solver should know it (by inlining).
- private val unknown1 : Expr = Equals(f(x), Plus(x, IntLiteral(1)))
+ private val unknown1 : Expr = Equals(f(x), Plus(x, InfiniteIntegerLiteral(1)))
assertValid(solver, unknown1)
test("Check assumptions") {
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
index 685bea19be921c205f0a427f3269b2b36e21cfb8..5974d31a1f954e2daaf81ec238c93684ca9bd8d8 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
@@ -46,9 +46,9 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
)
// def f(fx : Int) : Int = fx + 1
- private val fx : Identifier = FreshIdentifier("x").setType(Int32Type)
- private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, Int32Type, ValDef(fx, Int32Type) :: Nil, DefType.MethodDef)
- fDef.body = Some(Plus(Variable(fx), IntLiteral(1)))
+ private val fx : Identifier = FreshIdentifier("x").setType(IntegerType)
+ private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx, IntegerType) :: Nil, DefType.MethodDef)
+ fDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
private val minimalProgram = Program(
FreshIdentifier("Minimal"),
@@ -58,8 +58,8 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
)))
)
- private val x : Expr = Variable(FreshIdentifier("x").setType(Int32Type))
- private val y : Expr = Variable(FreshIdentifier("y").setType(Int32Type))
+ private val x : Expr = Variable(FreshIdentifier("x").setType(IntegerType))
+ private val y : Expr = Variable(FreshIdentifier("y").setType(IntegerType))
private def f(e : Expr) : Expr = FunctionInvocation(fDef.typed, e :: Nil)
private val solver = SolverFactory(() => new FairZ3Solver(testContext, minimalProgram))
@@ -67,7 +67,7 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
private val tautology1 : Expr = BooleanLiteral(true)
assertValid(solver, tautology1)
- private val tautology2 : Expr = Equals(Plus(x, x), Times(IntLiteral(2), x))
+ private val tautology2 : Expr = Equals(Plus(x, x), Times(InfiniteIntegerLiteral(2), x))
assertValid(solver, tautology2)
// This one contains a function invocation but is valid regardless of its
@@ -81,11 +81,11 @@ class FairZ3SolverTestsNewAPI extends LeonTestSuite {
private val wrong1 : Expr = BooleanLiteral(false)
assertInvalid(solver, wrong1)
- private val wrong2 : Expr = Equals(Plus(x, x), Times(IntLiteral(3), x))
+ private val wrong2 : Expr = Equals(Plus(x, x), Times(InfiniteIntegerLiteral(3), x))
assertInvalid(solver, wrong2)
// This is true, and FairZ3Solver should know it (by inlining).
- private val unknown1 : Expr = Equals(f(x), Plus(x, IntLiteral(1)))
+ private val unknown1 : Expr = Equals(f(x), Plus(x, InfiniteIntegerLiteral(1)))
assertValid(solver, unknown1)
test("Check assumptions") {
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index b2214f57304b2eca5ce241a09cd8c59ed1cda637..1c4aadaa5867eac0126fd085f885508c3dffdf1f 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -39,13 +39,13 @@ class UninterpretedZ3SolverTests extends LeonTestSuite {
)
// def f(fx : Int) : Int = fx + 1
- private val fx : Identifier = FreshIdentifier("x").setType(Int32Type)
- private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, Int32Type, ValDef(fx, Int32Type) :: Nil, DefType.MethodDef)
- fDef.body = Some(Plus(Variable(fx), IntLiteral(1)))
+ private val fx : Identifier = FreshIdentifier("x").setType(IntegerType)
+ private val fDef : FunDef = new FunDef(FreshIdentifier("f"), Nil, IntegerType, ValDef(fx, IntegerType) :: Nil, DefType.MethodDef)
+ fDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
// g is a function that is not in the program (on purpose)
- private val gDef : FunDef = new FunDef(FreshIdentifier("g"), Nil, Int32Type, ValDef(fx, Int32Type) :: Nil, DefType.MethodDef)
- gDef.body = Some(Plus(Variable(fx), IntLiteral(1)))
+ private val gDef : FunDef = new FunDef(FreshIdentifier("g"), Nil, IntegerType, ValDef(fx, IntegerType) :: Nil, DefType.MethodDef)
+ gDef.body = Some(Plus(Variable(fx), InfiniteIntegerLiteral(1)))
private val minimalProgram = Program(
FreshIdentifier("Minimal"),
@@ -55,8 +55,8 @@ class UninterpretedZ3SolverTests extends LeonTestSuite {
)))
)
- private val x : Expr = Variable(FreshIdentifier("x").setType(Int32Type))
- private val y : Expr = Variable(FreshIdentifier("y").setType(Int32Type))
+ private val x : Expr = Variable(FreshIdentifier("x").setType(IntegerType))
+ private val y : Expr = Variable(FreshIdentifier("y").setType(IntegerType))
private def f(e : Expr) : Expr = FunctionInvocation(fDef.typed, e :: Nil)
private def g(e : Expr) : Expr = FunctionInvocation(gDef.typed, e :: Nil)
@@ -65,7 +65,7 @@ class UninterpretedZ3SolverTests extends LeonTestSuite {
private val tautology1 : Expr = BooleanLiteral(true)
assertValid(solver, tautology1)
- private val tautology2 : Expr = Equals(Plus(x, x), Times(IntLiteral(2), x))
+ private val tautology2 : Expr = Equals(Plus(x, x), Times(InfiniteIntegerLiteral(2), x))
assertValid(solver, tautology2)
// This one contains a function invocation but is valid regardless of its
@@ -79,14 +79,14 @@ class UninterpretedZ3SolverTests extends LeonTestSuite {
private val wrong1 : Expr = BooleanLiteral(false)
assertInvalid(solver, wrong1)
- private val wrong2 : Expr = Equals(Plus(x, x), Times(IntLiteral(3), x))
+ private val wrong2 : Expr = Equals(Plus(x, x), Times(InfiniteIntegerLiteral(3), x))
assertInvalid(solver, wrong2)
// This is true, but that solver shouldn't know it.
// However, since the uninterpreted solver is a nice backend for the unrolling solver,
// it makes more sense to allow such formulas even if they are not completely known
/*
- private val unknown1 : Expr = Equals(f(x), Plus(x, IntLiteral(1)))
+ private val unknown1 : Expr = Equals(f(x), Plus(x, InfiniteIntegerLiteral(1)))
assertUnknown(solver, unknown1)
*/
diff --git a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
index fe89ed2ab1a73c258b77962c9c73ae0c0480eac8..7e30c3d46531426ab4f74f70448fdbebec5ec230 100644
--- a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
+++ b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
@@ -16,18 +16,18 @@ import leon.synthesis.LinearEquations._
class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
- def i(x: Int) = IntLiteral(x)
+ def i(x: Int) = InfiniteIntegerLiteral(x)
- val xId = FreshIdentifier("x").setType(Int32Type)
+ val xId = FreshIdentifier("x").setType(IntegerType)
val x = Variable(xId)
- val yId = FreshIdentifier("y").setType(Int32Type)
+ val yId = FreshIdentifier("y").setType(IntegerType)
val y = Variable(yId)
- val zId = FreshIdentifier("z").setType(Int32Type)
+ val zId = FreshIdentifier("z").setType(IntegerType)
val z = Variable(zId)
- val aId = FreshIdentifier("a").setType(Int32Type)
+ val aId = FreshIdentifier("a").setType(IntegerType)
val a = Variable(aId)
- val bId = FreshIdentifier("b").setType(Int32Type)
+ val bId = FreshIdentifier("b").setType(IntegerType)
val b = Variable(bId)
def toSum(es: Seq[Expr]) = es.reduceLeft(Plus(_, _))
@@ -41,11 +41,13 @@ class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
//use some random values to check that any vector in the basis is a valid solution to
//the equation
- def checkVectorSpace(basis: Array[Array[Int]], equation: Array[Int]) {
+ def checkVectorSpace(basis: Array[Array[Int]], equation: Array[Int]): Unit =
+ checkVectorSpace(basis.map(_.map(i => BigInt(i))), equation.map(i => BigInt(i)))
+ def checkVectorSpace(basis: Array[Array[BigInt]], equation: Array[BigInt]): Unit = {
require(basis.size == basis(0).size + 1 && basis.size == equation.size)
val n = basis(0).size
- val min = -5
- val max = 5
+ val min: BigInt = -5
+ val max: BigInt = 5
val components = Array.fill(n)(min)
var counter = 0
@@ -70,16 +72,16 @@ class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
}
//val that the sol vector with the term in the equation
- def eval(sol: Array[Int], equation: Array[Int]): Int = {
+ def eval(sol: Array[BigInt], equation: Array[BigInt]): BigInt = {
require(sol.size == equation.size)
- sol.zip(equation).foldLeft(0)((acc, p) => acc + p._1 * p._2)
+ sol.zip(equation).foldLeft(BigInt(0))((acc, p) => acc + p._1 * p._2)
}
//multiply the matrix by the vector: [M1 M2 .. Mn] * [v1 .. vn] = v1*M1 + ... + vn*Mn]
- def mult(matrix: Array[Array[Int]], vector: Array[Int]): Array[Int] = {
+ def mult(matrix: Array[Array[BigInt]], vector: Array[BigInt]): Array[BigInt] = {
require(vector.size == matrix(0).size && vector.size > 0)
val tmat = matrix.transpose
- var tmp: Array[Int] = null
+ var tmp: Array[BigInt] = null
tmp = mult(vector(0), tmat(0))
var i = 1
while(i < vector.size) {
@@ -89,8 +91,8 @@ class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
tmp
}
- def mult(c: Int, v: Array[Int]): Array[Int] = v.map(_ * c)
- def add(v1: Array[Int], v2: Array[Int]): Array[Int] = {
+ def mult(c: BigInt, v: Array[BigInt]): Array[BigInt] = v.map(_ * c)
+ def add(v1: Array[BigInt], v2: Array[BigInt]): Array[BigInt] = {
require(v1.size == v2.size)
v1.zip(v2).map(p => p._1 + p._2)
}
@@ -104,60 +106,60 @@ class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
test("particularSolution basecase") {
def toExpr(es: Array[Expr]): Expr = {
val coef: Array[Expr] = es
- val vars: Array[Expr] = Array[Expr](IntLiteral(1)) ++ Array[Expr](x, y)
- es.zip(vars).foldLeft[Expr](IntLiteral(0))( (acc: Expr, p: (Expr, Expr)) => Plus(acc, Times(p._1, p._2)) )
+ val vars: Array[Expr] = Array[Expr](i(1)) ++ Array[Expr](x, y)
+ es.zip(vars).foldLeft[Expr](i(0))( (acc: Expr, p: (Expr, Expr)) => Plus(acc, Times(p._1, p._2)) )
}
val t1: Expr = Plus(a, b)
- val c1: Expr = IntLiteral(4)
- val d1: Expr = IntLiteral(22)
+ val c1: Expr = i(4)
+ val d1: Expr = i(22)
val e1: Array[Expr] = Array(t1, c1, d1)
val (pre1, (w1, w2)) = particularSolution(Set(aId, bId), t1, c1, d1)
- checkSameExpr(toExpr(e1), IntLiteral(0), Set(aId, bId), pre1, Map(xId -> w1, yId -> w2))
+ checkSameExpr(toExpr(e1), i(0), Set(aId, bId), pre1, Map(xId -> w1, yId -> w2))
- val t2: Expr = IntLiteral(-1)
- val c2: Expr = IntLiteral(1)
- val d2: Expr = IntLiteral(-1)
+ val t2: Expr = i(-1)
+ val c2: Expr = i(1)
+ val d2: Expr = i(-1)
val e2: Array[Expr] = Array(t2, c2, d2)
val (pre2, (w3, w4)) = particularSolution(Set(), t2, c2, d2)
- checkSameExpr(toExpr(e2), IntLiteral(0), Set(), pre2, Map(xId -> w3, yId -> w4))
+ checkSameExpr(toExpr(e2), i(0), Set(), pre2, Map(xId -> w3, yId -> w4))
}
test("particularSolution preprocess") {
def toExpr(es: Array[Expr], vs: Array[Expr]): Expr = {
val coef: Array[Expr] = es
- val vars: Array[Expr] = Array[Expr](IntLiteral(1)) ++ vs
- es.zip(vars).foldLeft[Expr](IntLiteral(0))( (acc: Expr, p: (Expr, Expr)) => Plus(acc, Times(p._1, p._2)) )
+ val vars: Array[Expr] = Array[Expr](i(1)) ++ vs
+ es.zip(vars).foldLeft[Expr](i(0))( (acc: Expr, p: (Expr, Expr)) => Plus(acc, Times(p._1, p._2)) )
}
val t1: Expr = Plus(a, b)
- val c1: Expr = IntLiteral(4)
- val d1: Expr = IntLiteral(22)
+ val c1: Expr = i(4)
+ val d1: Expr = i(22)
val e1: Array[Expr] = Array(t1, c1, d1)
val (pre1, s1) = particularSolution(Set(aId, bId), e1.toList)
- checkSameExpr(toExpr(e1, Array(x, y)), IntLiteral(0), Set(aId, bId), pre1, Array(xId, yId).zip(s1).toMap)
+ checkSameExpr(toExpr(e1, Array(x, y)), i(0), Set(aId, bId), pre1, Array(xId, yId).zip(s1).toMap)
val t2: Expr = Plus(a, b)
- val c2: Expr = IntLiteral(4)
- val d2: Expr = IntLiteral(22)
- val f2: Expr = IntLiteral(10)
+ val c2: Expr = i(4)
+ val d2: Expr = i(22)
+ val f2: Expr = i(10)
val e2: Array[Expr] = Array(t2, c2, d2, f2)
val (pre2, s2) = particularSolution(Set(aId, bId), e2.toList)
- checkSameExpr(toExpr(e2, Array(x, y, z)), IntLiteral(0), Set(aId, bId), pre2, Array(xId, yId, zId).zip(s2).toMap)
+ checkSameExpr(toExpr(e2, Array(x, y, z)), i(0), Set(aId, bId), pre2, Array(xId, yId, zId).zip(s2).toMap)
- val t3: Expr = Plus(a, Times(IntLiteral(2), b))
- val c3: Expr = IntLiteral(6)
- val d3: Expr = IntLiteral(24)
- val f3: Expr = IntLiteral(9)
+ val t3: Expr = Plus(a, Times(i(2), b))
+ val c3: Expr = i(6)
+ val d3: Expr = i(24)
+ val f3: Expr = i(9)
val e3: Array[Expr] = Array(t3, c3, d3, f3)
val (pre3, s3) = particularSolution(Set(aId, bId), e3.toList)
- checkSameExpr(toExpr(e3, Array(x, y, z)), IntLiteral(0), Set(aId, bId), pre3, Array(xId, yId, zId).zip(s3).toMap)
+ checkSameExpr(toExpr(e3, Array(x, y, z)), i(0), Set(aId, bId), pre3, Array(xId, yId, zId).zip(s3).toMap)
val t4: Expr = Plus(a, b)
- val c4: Expr = IntLiteral(4)
+ val c4: Expr = i(4)
val e4: Array[Expr] = Array(t4, c4)
val (pre4, s4) = particularSolution(Set(aId, bId), e4.toList)
- checkSameExpr(toExpr(e4, Array(x)), IntLiteral(0), Set(aId, bId), pre4, Array(xId).zip(s4).toMap)
+ checkSameExpr(toExpr(e4, Array(x)), i(0), Set(aId, bId), pre4, Array(xId).zip(s4).toMap)
}
@@ -166,27 +168,27 @@ class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
val evaluator = new DefaultEvaluator(testContext, Program.empty)
- val eq1 = Array(3, 4, 8)
+ val eq1 = Array[BigInt](3, 4, 8)
val basis1 = linearSet(evaluator, as, eq1)
checkVectorSpace(basis1, eq1)
- val eq2 = Array(1, 2, 3)
+ val eq2 = Array[BigInt](1, 2, 3)
val basis2 = linearSet(evaluator, as, eq2)
checkVectorSpace(basis2, eq2)
- val eq3 = Array(1, 1)
+ val eq3 = Array[BigInt](1, 1)
val basis3 = linearSet(evaluator, as, eq3)
checkVectorSpace(basis3, eq3)
- val eq4 = Array(1, 1, 2, 7)
+ val eq4 = Array[BigInt](1, 1, 2, 7)
val basis4 = linearSet(evaluator, as, eq4)
checkVectorSpace(basis4, eq4)
- val eq5 = Array(1, -1)
+ val eq5 = Array[BigInt](1, -1)
val basis5 = linearSet(evaluator, as, eq5)
checkVectorSpace(basis5, eq5)
- val eq6 = Array(1, -6, 3)
+ val eq6 = Array[BigInt](1, -6, 3)
val basis6 = linearSet(evaluator, as, eq6)
checkVectorSpace(basis6, eq6)
}
@@ -224,35 +226,35 @@ class LinearEquationsSuite extends LeonTestSuite with WithLikelyEq {
def check(t: Expr, c: List[Expr], prec: Expr, witnesses: List[Expr], freshVars: List[Identifier]) {
enumerate(freshVars.size, (vals: Array[Int]) => {
- val mapping: Map[Expr, Expr] = (freshVars.zip(vals.toList).map(t => (Variable(t._1), IntLiteral(t._2))).toMap)
- val cWithVars: Expr = c.zip(witnesses).foldLeft[Expr](IntLiteral(0)){ case (acc, (coef, wit)) => Plus(acc, Times(coef, replace(mapping, wit))) }
- checkSameExpr(Plus(t, cWithVars), IntLiteral(0), as, prec)
+ val mapping: Map[Expr, Expr] = (freshVars.zip(vals.toList).map(t => (Variable(t._1), i(t._2))).toMap)
+ val cWithVars: Expr = c.zip(witnesses).foldLeft[Expr](i(0)){ case (acc, (coef, wit)) => Plus(acc, Times(coef, replace(mapping, wit))) }
+ checkSameExpr(Plus(t, cWithVars), i(0), as, prec)
})
}
- val t1 = Minus(Times(IntLiteral(2), a), b)
- val c1 = List(IntLiteral(3), IntLiteral(4), IntLiteral(8))
+ val t1 = Minus(Times(i(2), a), b)
+ val c1 = List(i(3), i(4), i(8))
val (pre1, wit1, f1) = elimVariable(evaluator, as, t1::c1)
check(t1, c1, pre1, wit1, f1)
- val t2 = Plus(Plus(IntLiteral(0), IntLiteral(2)), Times(IntLiteral(-1), IntLiteral(3)))
- val c2 = List(IntLiteral(1), IntLiteral(-1))
+ val t2 = Plus(Plus(i(0), i(2)), Times(i(-1), i(3)))
+ val c2 = List(i(1), i(-1))
val (pre2, wit2, f2) = elimVariable(evaluator, Set(), t2::c2)
check(t2, c2, pre2, wit2, f2)
- val t3 = Minus(Times(IntLiteral(2), a), IntLiteral(3))
- val c3 = List(IntLiteral(2))
+ val t3 = Minus(Times(i(2), a), i(3))
+ val c3 = List(i(2))
val (pre3, wit3, f3) = elimVariable(evaluator, Set(aId), t3::c3)
check(t3, c3, pre3, wit3, f3)
- val t4 = Times(IntLiteral(2), a)
- val c4 = List(IntLiteral(2), IntLiteral(4))
+ val t4 = Times(i(2), a)
+ val c4 = List(i(2), i(4))
val (pre4, wit4, f4) = elimVariable(evaluator, Set(aId), t4::c4)
check(t4, c4, pre4, wit4, f4)
val t5 = Minus(a, b)
- val c5 = List(IntLiteral(-60), IntLiteral(-3600))
+ val c5 = List(i(-60), i(-3600))
val (pre5, wit5, f5) = elimVariable(evaluator, Set(aId, bId), t5::c5)
check(t5, c5, pre5, wit5, f5)
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 0296a1e5194b71bc8dbf232710a4808bccc0bc10..30fc1a4d7336d881859b2af6e5e0e0283d2d1bc2 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -199,12 +199,12 @@ object Injection {
case class Nil() extends List
// proved with unrolling=0
- def size(l: List) : Int = (l match {
- case Nil() => 0
+ def size(l: List) : BigInt = (l match {
+ case Nil() => BigInt(0)
case Cons(t) => 1 + size(t)
}) ensuring(res => res >= 0)
- def simple() = choose{out: List => size(out) == 2 }
+ def simple() = choose{out: List => size(out) == BigInt(2) }
}
"""
) {
@@ -270,16 +270,16 @@ import leon.lang.synthesis._
object SortedList {
sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
+ case class Cons(head: BigInt, tail: List) extends List
case class Nil() extends List
- def size(l: List) : Int = (l match {
- case Nil() => 0
+ def size(l: List) : BigInt = (l match {
+ case Nil() => BigInt(0)
case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
- def content(l: List): Set[Int] = l match {
- case Nil() => Set.empty[Int]
+ def content(l: List): Set[BigInt] = l match {
+ case Nil() => Set.empty[BigInt]
case Cons(i, t) => Set(i) ++ content(t)
}
@@ -294,12 +294,12 @@ object SortedList {
content(out) == content(in1) ++ content(in2)
}
- def insert(in1: List, v: Int) = choose {
+ def insert(in1: List, v: BigInt) = choose {
(out : List) =>
content(out) == content(in1) ++ Set(v)
}
- def insertSorted(in1: List, v: Int) = choose {
+ def insertSorted(in1: List, v: BigInt) = choose {
(out : List) =>
isSorted(in1) && content(out) == content(in1) ++ Set(v) && isSorted(out)
}