diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index f81e359ef632021f9805a9d605f6d9ef2a20106a..51e3e8da4ef65d2bda70b5d74484df788bbc2ab3 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -7,10 +7,10 @@ import utils._
object Constructors {
import Trees._
+ import Definitions._
import TypeTreeOps._
import Common._
import TypeTrees._
- import Definitions.FunDef
def tupleSelect(t: Expr, index: Int) = t match {
case Tuple(es) =>
@@ -188,5 +188,33 @@ object Constructors {
case (l1, Implies(l2, r2)) => implies(and(l1, l2), r2)
case _ => Implies(lhs, rhs)
}
+
+ def finiteLambda(dflt: Expr, els: Seq[(Expr, Expr)], tpe: FunctionType): Lambda = {
+ val args = tpe.from.zipWithIndex.map { case (tpe, idx) =>
+ ValDef(FreshIdentifier(s"x${idx + 1}").setType(tpe), tpe)
+ }
+
+ assume(els.isEmpty || !tpe.from.isEmpty, "Can't provide finite mapping for lambda without parameters")
+
+ lazy val (tupleArgs, tupleKey) = if (tpe.from.size > 1) {
+ val tpArgs = Tuple(args.map(_.toVariable))
+ val key = (x: Expr) => x
+ (tpArgs, key)
+ } else { // note that value is lazy, so if tpe.from.size == 0, foldRight will never access (tupleArgs, tupleKey)
+ val tpArgs = args.head.toVariable
+ val key = (x: Expr) => {
+ if (isSubtypeOf(x.getType, tpe.from.head)) x
+ else if (isSubtypeOf(x.getType, TupleType(tpe.from))) x.asInstanceOf[Tuple].exprs.head
+ else throw new RuntimeException("Can't determine key tuple state : " + x + " of " + tpe)
+ }
+ (tpArgs, key)
+ }
+
+ val body = els.toSeq.foldRight(dflt) { case ((k, v), elze) =>
+ IfExpr(Equals(tupleArgs, tupleKey(k)), v, elze)
+ }
+
+ Lambda(args, body)
+ }
}
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 9e516807e9e337f6be0d2c7f3be1b7b123494e71..f2cd6bc079b83e5eb8f4dc24ddaf0bf98c89ad87 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -265,35 +265,8 @@ object Extractors {
rec(lambda.body)
}
-
- def apply(dflt: Expr, els: Seq[(Expr, Expr)], tpe: FunctionType): Lambda = {
- val args = tpe.from.zipWithIndex.map { case (tpe, idx) =>
- ValDef(FreshIdentifier(s"x${idx + 1}").setType(tpe), tpe)
- }
-
- assume(els.isEmpty || !tpe.from.isEmpty, "Can't provide finite mapping for lambda without parameters")
-
- lazy val (tupleArgs, tupleKey) = if (tpe.from.size > 1) {
- val tpArgs = Tuple(args.map(_.toVariable))
- val key = (x: Expr) => x
- (tpArgs, key)
- } else { // note that value is lazy, so if tpe.from.size == 0, foldRight will never access (tupleArgs, tupleKey)
- val tpArgs = args.head.toVariable
- val key = (x: Expr) => {
- if (isSubtypeOf(x.getType, tpe.from.head)) x
- else if (isSubtypeOf(x.getType, TupleType(tpe.from))) x.asInstanceOf[Tuple].exprs.head
- else throw new RuntimeException("Can't determine key tuple state : " + x + " of " + tpe)
- }
- (tpArgs, key)
- }
-
- val body = els.toSeq.foldRight(dflt) { case ((k, v), elze) =>
- IfExpr(Equals(tupleArgs, tupleKey(k)), v, elze)
- }
-
- Lambda(args, body)
- }
}
+
object MatchLike {
def unapply(m : MatchLike) : Option[(Expr, Seq[MatchCase], (Expr, Seq[MatchCase]) => Expr)] = {
Option(m) map { m =>
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
index 796b496474b699aae8b80a3dce6da40167a00315..6b906d64036b0fb875164b1169c75656ff064647 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Target.scala
@@ -9,6 +9,7 @@ import purescala._
import Common._
import Trees._
import Extractors._
+import Constructors._
import TypeTrees._
import TreeOps.simplestValue
@@ -55,7 +56,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
RawArrayValue(k, Map(), fromSMT(elem, v))
case (FunctionApplication(SimpleSymbol(SSymbol("__array_store_all__")), Seq(_, elem)), ft @ FunctionType(from,to)) =>
- FiniteLambda(fromSMT(elem, to), Seq.empty, ft)
+ finiteLambda(fromSMT(elem, to), Seq.empty, ft)
case (FunctionApplication(SimpleSymbol(SSymbol("store")), Seq(arr, key, elem)), RawArrayType(k,v)) =>
val RawArrayValue(_, elems, base) = fromSMT(arr, tpe)
@@ -63,7 +64,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
case (FunctionApplication(SimpleSymbol(SSymbol("store")), Seq(arr, key, elem)), ft @ FunctionType(from,to)) =>
val FiniteLambda(dflt, mapping) = fromSMT(arr, tpe)
- FiniteLambda(dflt, mapping :+ (fromSMT(key, TupleType(from)) -> fromSMT(elem, to)), ft)
+ finiteLambda(dflt, mapping :+ (fromSMT(key, TupleType(from)) -> fromSMT(elem, to)), ft)
case (FunctionApplication(SimpleSymbol(SSymbol("singleton")), elems), SetType(base)) =>
FiniteSet(elems.map(fromSMT(_, base)).toSet).setType(tpe)
@@ -82,7 +83,7 @@ trait SMTLIBCVC4Target extends SMTLIBTarget {
// some versions of CVC4 seem to generate array constants with "as const" notation instead of the __array_store_all__
// one I've witnessed up to now. Don't know why this is happening...
case (FunctionApplication(QualifiedIdentifier(SMTIdentifier(SSymbol("const"), _), _), Seq(elem)), ft @ FunctionType(from, to)) =>
- FiniteLambda(fromSMT(elem, to), Seq.empty, ft)
+ finiteLambda(fromSMT(elem, to), Seq.empty, ft)
case (FunctionApplication(QualifiedIdentifier(SMTIdentifier(SSymbol("const"), _), _), Seq(elem)), RawArrayType(k, v)) =>
RawArrayValue(k, Map(), fromSMT(elem, v))
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 4d222d4f776eb5c4313b0bdafcbfce8b6da5c68c..f754744b271f96e8c125bc0d955477c70a97d5a0 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -9,6 +9,7 @@ import Trees.{Assert => _, _}
import Extractors._
import TreeOps._
import TypeTrees._
+import Constructors._
import Definitions._
import utils.IncrementalBijection
@@ -81,7 +82,7 @@ trait SMTLIBTarget {
r
case ft @ FunctionType(from, to) =>
- FiniteLambda(r.default, r.elems.toSeq, ft)
+ finiteLambda(r.default, r.elems.toSeq, ft)
case _ =>
unsupported("Unable to extract from raw array for "+tpe)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 6e99fbfa6bfd8fc233ff32cebb2ce039f81bb294..dfe0784197c0763915aa58529e686dd66e3a2f21 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -760,7 +760,7 @@ trait AbstractZ3Solver
case Some((map, elseZ3Value)) =>
val leonElseValue = rec(elseZ3Value)
val leonMap = map.toSeq.map(p => rec(p._1) -> rec(p._2))
- FiniteLambda(leonElseValue, leonMap, tpe)
+ finiteLambda(leonElseValue, leonMap, tpe)
}
case LeonType(tpe @ SetType(dt)) =>