diff --git a/src/main/scala/inox/ast/Expressions.scala b/src/main/scala/inox/ast/Expressions.scala
index 24da96276d0e849df2406af807a80337cbc00a2d..e97cf4082924c6757e278d137942ca7533fbb1f1 100644
--- a/src/main/scala/inox/ast/Expressions.scala
+++ b/src/main/scala/inox/ast/Expressions.scala
@@ -152,22 +152,33 @@ trait Expressions { self: Trees =>
case class BVLiteral(value: BitSet, size: Int) extends Literal[BitSet] {
def getType(implicit s: Symbols): Type = BVType(size)
def toBigInt: BigInt = {
- val res = value.foldLeft(BigInt(0))((res, i) => res + BigInt(2).pow(i))
- if (value(size)) BigInt(2).pow(size) - res else res
+ val res = value.foldLeft(BigInt(0))((res, i) => res + BigInt(2).pow(i-1))
+ if (value(size)) res - BigInt(2).pow(size) else res
}
}
object BVLiteral {
- def apply(bi: BigInt, size: Int): BVLiteral = BVLiteral(
- (1 to size).foldLeft(BitSet.empty) { case (res, i) =>
- if ((bi & BigInt(2).pow(i)) > 0) res + i else res
- }, size)
+ def apply(bi: BigInt, size: Int): BVLiteral = {
+ def extract(bi: BigInt): BitSet = (1 to size).foldLeft(BitSet.empty) {
+ case (res, i) => if ((bi & BigInt(2).pow(i-1)) > 0) res + i else res
+ }
+
+ val bitSet = if (bi >= 0) extract(bi) else {
+ val bs = extract(-bi)
+ (1 to size).foldLeft((BitSet.empty, false)) { case ((res, seen1), i) =>
+ if (bs(i) && !seen1) (res + i, true)
+ else (if (!seen1 || bs(i)) res else res + i, seen1)
+ }._1
+ }
+
+ BVLiteral(bitSet, size)
+ }
}
object IntLiteral {
def apply(i: Int): BVLiteral = BVLiteral(BigInt(i), 32)
def unapply(e: Expr): Option[Int] = e match {
- case b @ BVLiteral(_, 32) => Some(b.toBigInt.toInt)
+ case b @ BVLiteral(bs, 32) => Some(b.toBigInt.toInt)
case _ => None
}
}
diff --git a/src/main/scala/inox/ast/Extractors.scala b/src/main/scala/inox/ast/Extractors.scala
index 9a235fa844c91600494c554632acdf3fc5bc3d6b..ffc708f585ca3bab32db116003a3f64737aee34d 100644
--- a/src/main/scala/inox/ast/Extractors.scala
+++ b/src/main/scala/inox/ast/Extractors.scala
@@ -132,7 +132,7 @@ trait TreeDeconstructor {
}
(subArgs, Seq(base), builder)
case s.FiniteMap(elems, default, kT) =>
- val subArgs = elems.flatMap { case (k, v) => Seq(k, v) }
+ val subArgs = elems.flatMap { case (k, v) => Seq(k, v) } :+ default
val builder = (as: Seq[t.Expr], kT: Seq[t.Type]) => {
def rec(kvs: Seq[t.Expr]): (Seq[(t.Expr, t.Expr)], t.Expr) = kvs match {
case Seq(k, v, t @ _*) =>
diff --git a/src/main/scala/inox/ast/GenTreeOps.scala b/src/main/scala/inox/ast/GenTreeOps.scala
index 1b8af7c4a5dc1e4b0f1af9a9f2f63a67d1759842..6584e5a43e172e49c3e21fef82cbe246567449f3 100644
--- a/src/main/scala/inox/ast/GenTreeOps.scala
+++ b/src/main/scala/inox/ast/GenTreeOps.scala
@@ -388,8 +388,11 @@ trait GenTreeOps { self =>
}
object Same {
- def unapply(tt: (Source, Source)): Option[(Source, Source)] = {
- if (tt._1.getClass == tt._2.getClass) {
+ def unapply(tt: (Source, Target))(implicit ev1: Source =:= Target, ev2: Target =:= Source): Option[(Source, Target)] = {
+ val Deconstructor(es1, recons1) = tt._1
+ val Deconstructor(es2, recons2) = ev2(tt._2)
+
+ if (es1.size == es2.size && scala.util.Try(recons2(es1.map(ev1))).toOption == Some(tt._1)) {
Some(tt)
} else {
None
diff --git a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
index 715a8d8dd25bc6d9ca239a6f1149f7aabd5e2974..d310e98b8715c3a727774fd27e95fd190a26628b 100644
--- a/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/inox/evaluators/RecursiveEvaluator.scala
@@ -225,12 +225,7 @@ trait RecursiveEvaluator
case UMinus(ex) =>
e(ex) match {
- case BVLiteral(b, s) =>
- BVLiteral((1 to s).foldLeft((BitSet.empty, false)) { case ((res, seen1), i) =>
- if (b(i) && seen1) (res + i, true)
- else if (!seen1) (res, seen1)
- else (if (!b(i)) res + i else res, seen1)
- }._1, s)
+ case b @ BVLiteral(_, s) => BVLiteral(-b.toBigInt, s)
case IntegerLiteral(i) => IntegerLiteral(-i)
case FractionLiteral(n, d) => FractionLiteral(-n, d)
case re => throw EvalError("Unexpected operation: -(" + re.asString + ")")
@@ -239,9 +234,9 @@ trait RecursiveEvaluator
case Times(l,r) =>
(e(l), e(r)) match {
case (BVLiteral(i1, s1), BVLiteral(i2, s2)) if s1 == s2 =>
- BVLiteral(i1.foldLeft(BitSet.empty) { case (res, i) =>
- res ++ shift(i2, s2, i)
- }, s1)
+ i1.foldLeft(BVLiteral(0, s1): Expr) { case (res, i) =>
+ e(Plus(res, BVLiteral(shift(i2, s2, i-1), s1)))
+ }
case (IntegerLiteral(i1), IntegerLiteral(i2)) => IntegerLiteral(i1 * i2)
case (FractionLiteral(ln, ld), FractionLiteral(rn, rd)) =>
normalizeFraction(FractionLiteral((ln * rn), (ld * rd)))
@@ -509,8 +504,8 @@ trait RecursiveEvaluator
FiniteMap(ss.map{ case (k, v) => (e(k), e(v)) }.toMap.toSeq, e(dflt), vT)
case g @ MapApply(m,k) => (e(m), e(k)) match {
- case (FiniteMap(ss, _, _), e) =>
- ss.toMap.getOrElse(e, throw RuntimeError("Key not found: " + e.asString))
+ case (FiniteMap(ss, dflt, _), e) =>
+ ss.toMap.getOrElse(e, dflt)
case (l,r) =>
throw EvalError(typeErrorMsg(l, MapType(r.getType, g.getType)))
}
diff --git a/src/test/scala/inox/ast/ExprOpsSuite.scala b/src/test/scala/inox/ast/ExprOpsSuite.scala
index 1a8c5e6157c4937e3fbc289aa6ff7dc3632a164a..b12cad3633327368b91a810ecb80f3182424bdf5 100644
--- a/src/test/scala/inox/ast/ExprOpsSuite.scala
+++ b/src/test/scala/inox/ast/ExprOpsSuite.scala
@@ -278,7 +278,6 @@ class ExprOpsSuite extends FunSuite {
val v = simplestValue(t)
assert(isSubtypeOf(v.getType, t), "SimplestValue of "+t+": "+v+":"+v.getType)
}
-
}
test("preMapWithContext") {
diff --git a/src/test/scala/inox/evaluators/EvaluatorSuite.scala b/src/test/scala/inox/evaluators/EvaluatorSuite.scala
index c0b24793489d5752ab56210abd49441838da4a98..c5db3fd3ea26c70c21f8bb244581373ed09cef72 100644
--- a/src/test/scala/inox/evaluators/EvaluatorSuite.scala
+++ b/src/test/scala/inox/evaluators/EvaluatorSuite.scala
@@ -36,6 +36,8 @@ class EvaluatorSuite extends FunSuite {
eval(e, Plus(IntLiteral(3), IntLiteral(5))) === IntLiteral(8)
eval(e, Plus(IntLiteral(0), IntLiteral(5))) === IntLiteral(5)
+ eval(e, Plus(IntLiteral(1), IntLiteral(-2))) === IntLiteral(-1)
+ eval(e, Plus(IntLiteral(Int.MaxValue), IntLiteral(1))) === IntLiteral(Int.MinValue)
eval(e, Times(IntLiteral(3), IntLiteral(3))) === IntLiteral(9)
}
@@ -229,7 +231,7 @@ class EvaluatorSuite extends FunSuite {
eval(e, MapApply(
FiniteMap(Seq(IntLiteral(1) -> IntLiteral(2), IntLiteral(2) -> IntLiteral(4)), IntLiteral(6), Int32Type),
IntLiteral(1))
- ) === IntLiteral(4)
+ ) === IntLiteral(2)
eval(e, MapApply(
FiniteMap(Seq(IntLiteral(1) -> IntLiteral(2), IntLiteral(2) -> IntLiteral(4)), IntLiteral(6), Int32Type),