From 2bb7a742b01b27cd99e357e01d8e0cefb9e3c986 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 5 Nov 2014 17:04:45 +0100
Subject: [PATCH] Int becomes bitvector
Leon now matches Scala semantics of Int as 32 bits bit-vectors.
This commits modifies the semantics of IntLiteral to be treated
as 32 bits integer everywhere (solver, evaluator, ...).
Introduces a new literal type, InfiniteIntegerLiteral, representing
a natural integer. The front-end maps the use of BigInt to these
new trees, and the solver properly handles them as mathematical
integers.
The behaviour of many regression tests changes due to this new
semantics. In particular many of them now timeout because they
are no longer proving properties over mathematical integers. This
commit updates the tests to reflect this new semantics.
---
library/collection/List.scala | 58 ++++-----
.../scala/leon/codegen/CodeGeneration.scala | 59 ++++++++-
.../scala/leon/codegen/CompilationUnit.scala | 6 +-
.../scala/leon/datagen/VanuatooDataGen.scala | 14 ++-
.../leon/evaluators/RecursiveEvaluator.scala | 50 +++++++-
.../leon/frontends/scalac/ASTExtractors.scala | 30 +++++
.../frontends/scalac/CodeExtraction.scala | 52 +++++++-
.../scala/leon/purescala/Extractors.scala | 6 +
.../scala/leon/purescala/PrettyPrinter.scala | 14 ++-
.../leon/purescala/TreeNormalizations.scala | 24 ++--
src/main/scala/leon/purescala/TreeOps.scala | 57 ++++-----
src/main/scala/leon/purescala/Trees.scala | 51 +++++++-
src/main/scala/leon/purescala/TypeTrees.scala | 5 +-
.../leon/solvers/smtlib/SMTLIBTarget.scala | 39 ++++--
.../leon/solvers/z3/AbstractZ3Solver.scala | 83 +++++++++---
.../solvers/z3/Z3ModelReconstruction.scala | 1 +
src/main/scala/leon/synthesis/Algebra.scala | 87 +++++++++++++
.../leon/synthesis/LinearEquations.scala | 48 +++----
src/main/scala/leon/synthesis/Rules.scala | 4 +-
.../scala/leon/synthesis/rules/Cegis.scala | 12 ++
.../synthesis/rules/InequalitySplit.scala | 2 +-
.../leon/synthesis/rules/IntInduction.scala | 26 ++--
.../synthesis/utils/ExpressionGrammar.scala | 32 +++--
.../leon/termination/ChainComparator.scala | 2 +-
.../leon/termination/StructuralSize.scala | 12 +-
.../regression/synthesis/List/Insert.scala | 6 +-
.../termination/valid/Fibonacci.scala | 4 +-
.../termination/valid/Numeric1.scala | 7 +-
.../invalid/AddingNegativeNumbers.scala | 10 ++
.../invalid/AddingPositiveNumbers.scala | 11 ++
.../purescala/invalid/Choose1.scala | 10 +-
.../purescala/invalid/Generics.scala | 4 +-
.../purescala/invalid/Generics2.scala | 4 +-
.../purescala/invalid/InsertionSort.scala | 4 +-
.../purescala/invalid/ListOperations.scala | 14 +--
.../purescala/invalid/RedBlackTree.scala | 4 +-
.../valid/AddingPositiveNumbers.scala | 11 ++
.../purescala/valid/AmortizedQueue.scala | 4 +-
.../purescala/valid/Anonymous.scala | 4 +-
.../purescala/valid/Asserts1.scala | 4 +-
.../purescala/valid/Choose1.scala | 10 +-
.../purescala/valid/Generics.scala | 4 +-
.../purescala/valid/Generics2.scala | 10 +-
.../verification/purescala/valid/Heap.scala | 16 +--
.../purescala/valid/InsertionSort.scala | 4 +-
.../purescala/valid/ListOperations.scala | 105 ----------------
.../purescala/valid/MergeSort.scala | 6 +-
.../purescala/valid/PositiveMap.scala | 6 +-
.../purescala/valid/RedBlackTree.scala | 18 +--
.../purescala/valid/SearchLinkedList.scala | 16 +--
.../verification/xlang/invalid/Mean.scala | 12 ++
.../verification/xlang/valid/Arithmetic.scala | 24 ++--
.../verification/xlang/valid/Mean.scala | 12 ++
.../verification/xlang/valid/Nested2.scala | 4 +-
.../verification/xlang/valid/Nested3.scala | 4 +-
.../verification/xlang/valid/Nested4.scala | 8 +-
.../verification/xlang/valid/Nested6.scala | 8 +-
.../verification/xlang/valid/Nested7.scala | 6 +-
.../verification/xlang/valid/Nested8.scala | 6 +-
.../verification/xlang/valid/Nested9.scala | 8 +-
.../leon/test/codegen/CodeGenTests.scala | 28 ++++-
.../evaluators/DefaultEvaluatorTests.scala | 24 +++-
.../test/evaluators/EvaluatorsTests.scala | 6 +-
.../scala/leon/test/purescala/LikelyEq.scala | 2 +-
.../leon/test/purescala/LikelyEqSuite.scala | 25 ++--
.../purescala/TreeNormalizationsTests.scala | 15 ++-
.../leon/test/purescala/TreeOpsTests.scala | 54 ++++----
.../test/solvers/TimeoutSolverTests.scala | 6 +-
.../test/solvers/UnrollingSolverTests.scala | 16 +--
.../test/solvers/z3/FairZ3SolverTests.scala | 16 +--
.../solvers/z3/FairZ3SolverTestsNewAPI.scala | 16 +--
.../z3/UninterpretedZ3SolverTests.scala | 20 +--
.../test/synthesis/LinearEquationsSuite.scala | 118 +++++++++---------
.../leon/test/synthesis/SynthesisSuite.scala | 20 +--
74 files changed, 974 insertions(+), 554 deletions(-)
create mode 100644 src/test/resources/regression/verification/purescala/invalid/AddingNegativeNumbers.scala
create mode 100644 src/test/resources/regression/verification/purescala/invalid/AddingPositiveNumbers.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/AddingPositiveNumbers.scala
delete mode 100644 src/test/resources/regression/verification/purescala/valid/ListOperations.scala
create mode 100644 src/test/resources/regression/verification/xlang/invalid/Mean.scala
create mode 100644 src/test/resources/regression/verification/xlang/valid/Mean.scala
diff --git a/library/collection/List.scala b/library/collection/List.scala
index c9ebac9d3..f4ab47a45 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 8a548ecdb..dbca0c5de 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 5bf34b1f7..b24a5f0f9 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 6adab6929..e40af01e9 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 fa0148b5d..1d060afb6 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 0424350cf..8f9f8b0b7 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 369be0adf..8b63ff731 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 f2cd6bc07..a62521d84 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 8127e0af6..baa1a2c20 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 2f080d93e..3558ad598 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 a0313c5dc..1a256bc82 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 5879c42da..eeb15220f 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 2cc6591ca..05c90501e 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 f754744b2..0c69b047b 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 dfe078419..f73c0ae11 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 5953fc422..1bdb9fe6a 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 757c4c83c..474d6e90e 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 6c91c40f5..a9dd5ff9a 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 10b8e6ef5..399e045a5 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 3a744c42c..6d989c4ef 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 54ce95e5e..a71574fda 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 ae0567bd3..15c19915d 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 97687c425..ac3f47b17 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 68f5f97a2..f1d146e7d 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 25965c4ad..e1f8f8b3c 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 13c1294d7..0a2cb88b0 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 feabb8aff..e859a2c3d 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 07218fa52..7015bf71e 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 000000000..a8c1433b1
--- /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 000000000..d5f1b2825
--- /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 20d588523..8ff2e7dcb 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 04421e754..1c8566937 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 0376cfaf2..56dc25fd4 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 5fd06d36a..8f4d88aa2 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 bca6e6a76..afa46acd2 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 148512d00..1a75c7719 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 000000000..ad5efa879
--- /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 0c7d2170f..1f74ed4b1 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 b8d3235cc..d69b1f842 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 abbd39d5e..0851ba5ad 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 2b033c809..da4b4e775 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 2820d5a5c..7e1b2359f 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 5bd3627d4..3ad9b7df9 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 f70934816..f1464e8bc 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 820e97178..a3120a9bc 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 fb6b11d94..000000000
--- 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 e3714371b..de8b0c32b 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 7ee05ec9c..0441ec26c 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 15f4ba78d..841befb41 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 bf259ab0f..bd0596fba 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 000000000..f6e8757d5
--- /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 56baab22f..2e080a90c 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 000000000..447553e95
--- /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 da94f93d6..35cbb8611 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 81b748337..054493705 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 cb91848ee..7b82532df 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 305870f84..f7bfa772f 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 2f785f083..4187e7b0f 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 4024de42c..6bcb9050b 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 14f912137..148ba3a58 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 af02b00a9..1e0ad3a11 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 0dd8fe1d3..7dd1b4742 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 5828635a3..5a0599b41 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 3dd28dfc7..7fd034123 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 8c367a0ce..fced5df18 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 f05a5ddef..75dd10903 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 4bcce108d..7137ebd34 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 0c4bd2791..4f1564619 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 94ed51f64..46f56b4e7 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 bde8cc423..c5662615e 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 685bea19b..5974d31a1 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 b2214f573..1c4aadaa5 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 fe89ed2ab..7e30c3d46 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 0296a1e51..30fc1a4d7 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)
}
--
GitLab