diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 71920325e88979042fd7add19cd4f7b45edcca21..8f79149b9eb3290209ede19c6b7afb11410af3f0 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -231,7 +231,7 @@ class CompilationUnit(val ctx: LeonContext,
else GenericValue(tp, id).copiedFrom(gv)
case (set: runtime.Set, SetType(b)) =>
- finiteSet(set.getElements.asScala.map(jvmToExpr(_, b)).toSet, b)
+ FiniteSet(set.getElements.asScala.map(jvmToExpr(_, b)).toSet, b)
case (map: runtime.Map, MapType(from, to)) =>
val pairs = map.getElements.asScala.map { entry =>
@@ -239,7 +239,7 @@ class CompilationUnit(val ctx: LeonContext,
val v = jvmToExpr(entry.getValue, to)
(k, v)
}
- finiteMap(pairs.toSeq, from, to)
+ FiniteMap(pairs.toSeq, from, to)
case (lambda: runtime.Lambda, _: FunctionType) =>
val cls = lambda.getClass
diff --git a/src/main/scala/leon/datagen/VanuatooDataGen.scala b/src/main/scala/leon/datagen/VanuatooDataGen.scala
index 4b48a2ac576c7ce3aed6280bb9c8a8e74d58721f..c4100ceef464368de733a11ca9b67f2a5c3226b4 100644
--- a/src/main/scala/leon/datagen/VanuatooDataGen.scala
+++ b/src/main/scala/leon/datagen/VanuatooDataGen.scala
@@ -79,7 +79,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
Constructor[Expr, TypeTree](
(1 to size).map(i => sub).toList,
st,
- s => finiteSet(s.toSet, sub),
+ s => FiniteSet(s.toSet, sub),
st.toString+"@"+size
)
}
@@ -99,7 +99,7 @@ class VanuatooDataGen(ctx: LeonContext, p: Program) extends DataGenerator {
val cs = for (size <- List(0, 1, 2, 5)) yield {
val subs = (1 to size).flatMap(i => List(from, to)).toList
- Constructor[Expr, TypeTree](subs, mt, s => finiteMap(s.grouped(2).map(t => (t(0), t(1))).toSeq, from, to), mt.toString+"@"+size)
+ Constructor[Expr, TypeTree](subs, mt, s => FiniteMap(s.grouped(2).map(t => (t(0), t(1))).toSeq, from, to), mt.toString+"@"+size)
}
constructors += mt -> cs
cs
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 77e74b5303816b6b0a6a56c3e4e646762a0cc335..ff2e8309103d117aa8738c20803e485547186561 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -399,7 +399,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
(e(s1), e(s2)) match {
case (f@FiniteSet(els1, _),FiniteSet(els2, _)) =>
val SetType(tpe) = f.getType
- finiteSet(els1 ++ els2, tpe)
+ FiniteSet(els1 ++ els2, tpe)
case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
}
@@ -408,7 +408,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (f @ FiniteSet(els1, _), FiniteSet(els2, _)) => {
val newElems = els1 intersect els2
val SetType(tpe) = f.getType
- finiteSet(newElems, tpe)
+ FiniteSet(newElems, tpe)
}
case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
}
@@ -418,7 +418,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
case (f @ FiniteSet(els1, _),FiniteSet(els2, _)) => {
val SetType(tpe) = f.getType
val newElems = els1 -- els2
- finiteSet(newElems, tpe)
+ FiniteSet(newElems, tpe)
}
case (le,re) => throw EvalError(typeErrorMsg(le, s1.getType))
}
@@ -439,7 +439,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
}
case f @ FiniteSet(els, base) =>
- finiteSet(els.map(e), base)
+ FiniteSet(els.map(e), base)
case l @ Lambda(_, _) =>
val mapping = variablesOf(l).map(id => id -> e(Variable(id))).toMap
@@ -477,7 +477,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
)
case f @ FiniteMap(ss, kT, vT) =>
- finiteMap(ss.map{ case (k, v) => (e(k), e(v)) }.distinct, kT, vT)
+ FiniteMap(ss.map{ case (k, v) => (e(k), e(v)) }.distinct, kT, vT)
case g @ MapGet(m,k) => (e(m), e(k)) match {
case (FiniteMap(ss, _, _), e) => ss.find(_._1 == e) match {
@@ -491,7 +491,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
val filtered1 = ss1.filterNot(s1 => ss2.exists(s2 => s2._1 == s1._1))
val newSs = filtered1 ++ ss2
val MapType(kT, vT) = u.getType
- finiteMap(newSs, kT, vT)
+ FiniteMap(newSs, kT, vT)
}
case (l, r) => throw EvalError(typeErrorMsg(l, m1.getType))
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 362b225ce37d041255d867407f9eab159fbeca60..0c81ec1d4f9a387355958f8700fabb8c4c55e43c 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1410,10 +1410,10 @@ trait CodeExtraction extends ASTExtractors {
outOfSubsetError(tr, "Some map elements could not be extracted as Tuple2")
}
- finiteMap(singletons, extractType(tptFrom), extractType(tptTo))
+ FiniteMap(singletons, extractType(tptFrom), extractType(tptTo))
case ExFiniteSet(tpt, args) =>
- finiteSet(args.map(extractTree).toSet, extractType(tpt))
+ FiniteSet(args.map(extractTree).toSet, extractType(tpt))
case ExCaseClassConstruction(tpt, args) =>
extractType(tpt) match {
@@ -1695,7 +1695,7 @@ trait CodeExtraction extends ASTExtractors {
ElementOfSet(a2, a1)
case (IsTyped(a1, SetType(b1)), "isEmpty", List()) =>
- Equals(a1, finiteSet(Set(), b1))
+ Equals(a1, FiniteSet(Set(), b1))
// Multiset methods
case (IsTyped(a1, MultisetType(b1)), "++", List(IsTyped(a2, MultisetType(b2)))) if b1 == b2 =>
diff --git a/src/main/scala/leon/purescala/Constructors.scala b/src/main/scala/leon/purescala/Constructors.scala
index 2c15bdaf386c427365faac434fe64aacd5c6c949..ce97e591284b460008bcd882fa17283b5b890828 100644
--- a/src/main/scala/leon/purescala/Constructors.scala
+++ b/src/main/scala/leon/purescala/Constructors.scala
@@ -187,19 +187,11 @@ object Constructors {
case _ => Implies(lhs, rhs)
}
- def finiteSet(els: Set[Expr], tpe: TypeTree) = {
- FiniteSet(els, tpe)
- }
-
def finiteMultiset(els: Seq[Expr], tpe: TypeTree) = {
if (els.isEmpty) EmptyMultiset(tpe)
else NonemptyMultiset(els)
}
- def finiteMap(els: Seq[(Expr, Expr)], keyType: TypeTree, valueType: TypeTree) = {
- FiniteMap(els, keyType, valueType)
- }
-
def finiteArray(els: Seq[Expr]): Expr = {
require(els.nonEmpty)
finiteArray(els, None, Untyped) // Untyped is not correct, but will not be used anyway
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index a80cdb41c4e144ef847e06f935125568602450cc..b3bd13f5d380c8955d7068d02ee761aac6b30ed9 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1948,18 +1948,25 @@ object ExprOps {
}
def isListLiteral(e: Expr): Option[(TypeTree, List[Expr])] = e match {
- case CaseClass(cct, args) =>
- programOf(cct.classDef) flatMap { p =>
- val lib = p.library
- if (Some(cct.classDef) == lib.Nil) {
- Some((cct.tps.head, Nil))
- } else if (Some(cct.classDef) == lib.Cons) {
- isListLiteral(args(1)).map { case (_, t) =>
- (cct.tps.head, args.head :: t)
- }
- } else None
- }
- case _ => None
+ case CaseClass(CaseClassType(classDef, Seq(tp)), Nil) =>
+ for {
+ p <- programOf(classDef)
+ leonNil <- p.library.Nil
+ if classDef == leonNil
+ } yield {
+ (tp, Nil)
+ }
+ case CaseClass(CaseClassType(classDef, Seq(tp)), Seq(hd, tl)) =>
+ for {
+ p <- programOf(classDef)
+ leonCons <- p.library.Cons
+ if classDef == leonCons
+ (_, tlElems) <- isListLiteral(tl)
+ } yield {
+ (tp, hd :: tlElems)
+ }
+ case _ =>
+ None
}
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 9fb28e66d21877d0ab88441d6fa586c684ea85ab..c363c60ba1568a8129f755eca985b9f02f5a2fa0 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -13,7 +13,7 @@ object Extractors {
object UnaryOperator {
def unapply(expr: Expr) : Option[(Expr,(Expr)=>Expr)] = expr match {
- case Not(t) => Some((t,Not(_)))
+ case Not(t) => Some((t,not))
case UMinus(t) => Some((t,UMinus))
case BVUMinus(t) => Some((t,BVUMinus))
case BVNot(t) => Some((t,BVNot))
@@ -45,7 +45,7 @@ object Extractors {
LetDef(fd, body)
}
))
- case Equals(t1,t2) => Some((t1,t2,Equals.apply))
+ case Equals(t1,t2) => Some((t1,t2,Equals))
case Implies(t1,t2) => Some((t1,t2, implies))
case Plus(t1,t2) => Some((t1,t2,Plus))
case Minus(t1,t2) => Some((t1,t2,Minus))
@@ -78,15 +78,15 @@ object Extractors {
case MultisetUnion(t1,t2) => Some((t1,t2,MultisetUnion))
case MultisetPlus(t1,t2) => Some((t1,t2,MultisetPlus))
case MultisetDifference(t1,t2) => Some((t1,t2,MultisetDifference))
- case mg@MapGet(t1,t2) => Some((t1,t2, (t1, t2) => MapGet(t1, t2).setPos(mg)))
+ case mg@MapGet(t1,t2) => Some((t1,t2, MapGet))
case MapUnion(t1,t2) => Some((t1,t2,MapUnion))
case MapDifference(t1,t2) => Some((t1,t2,MapDifference))
case MapIsDefinedAt(t1,t2) => Some((t1,t2, MapIsDefinedAt))
case ArraySelect(t1, t2) => Some((t1, t2, ArraySelect))
- case Let(binders, e, body) => Some((e, body, (e: Expr, b: Expr) => Let(binders, e, b)))
+ case Let(binder, e, body) => Some((e, body, let(binder, _, _)))
case Require(pre, body) => Some((pre, body, Require))
- case Ensuring(body, post) => Some((body, post, (b: Expr, p: Expr) => Ensuring(b, p)))
- case Assert(const, oerr, body) => Some((const, body, (c: Expr, b: Expr) => Assert(c, oerr, b)))
+ case Ensuring(body, post) => Some((body, post, Ensuring))
+ case Assert(const, oerr, body) => Some((const, body, Assert(_, oerr, _)))
case (ex: BinaryExtractable) => ex.extract
case _ => None
}
@@ -102,9 +102,9 @@ object Extractors {
case Seq(pred) => Choose(pred, None)
case Seq(pred, impl) => Choose(pred, Some(impl))
}))
- case fi @ FunctionInvocation(fd, args) => Some((args, as => FunctionInvocation(fd, as).setPos(fi)))
- case mi @ MethodInvocation(rec, cd, tfd, args) => Some((rec +: args, as => MethodInvocation(as.head, cd, tfd, as.tail).setPos(mi)))
- case fa @ Application(caller, args) => Some(caller +: args, as => application(as.head, as.tail).setPos(fa))
+ case fi @ FunctionInvocation(fd, args) => Some((args, FunctionInvocation(fd, _)))
+ case mi @ MethodInvocation(rec, cd, tfd, args) => Some((rec +: args, as => MethodInvocation(as.head, cd, tfd, as.tail)))
+ case fa @ Application(caller, args) => Some(caller +: args, as => application(as.head, as.tail))
case CaseClass(cd, args) => Some((args, CaseClass(cd, _)))
case And(args) => Some((args, and))
case Or(args) => Some((args, or))
@@ -136,11 +136,11 @@ object Extractors {
}
case NonemptyArray(elems, None) =>
val all = elems.map(_._2).toSeq
- Some(( all, finiteArray _ ))
- case Tuple(args) => Some((args, Tuple))
+ Some(( all, finiteArray))
+ case Tuple(args) => Some((args, tupleWrap))
case IfExpr(cond, thenn, elze) => Some((
- Seq(cond, thenn, elze),
- (as: Seq[Expr]) => IfExpr(as(0), as(1), as(2))
+ Seq(cond, thenn, elze),
+ { case Seq(c,t,e) => IfExpr(c,t,e) }
))
case MatchExpr(scrut, cases) => Some((
scrut +: cases.flatMap {
@@ -166,7 +166,7 @@ object Extractors {
case GuardedCase(b, _, _) => i+=2; GuardedCase(b, es(i-1), es(i-2))
}
- Passes(in, out, newcases)
+ passes(in, out, newcases)
}}
))
case (ex: NAryExtractable) => ex.extract
@@ -181,35 +181,19 @@ object Extractors {
object StringLiteral {
def unapply(e: Expr): Option[String] = e match {
case CaseClass(cct, args) =>
- DefOps.programOf(cct.classDef) flatMap { p =>
- val lib = p.library
-
- if (Some(cct.classDef) == lib.String) {
- isListLiteral(args.head) match {
- case Some((_, chars)) =>
- val str = chars.map {
- case CharLiteral(c) => Some(c)
- case _ => None
- }
-
- if (str.forall(_.isDefined)) {
- Some(str.flatten.mkString)
- } else {
- None
- }
- case _ =>
- None
-
- }
- } else {
- None
- }
+ for {
+ p <- DefOps.programOf(cct.classDef)
+ libS <- p.library.String
+ if cct.classDef == libS
+ (_, chars) <- isListLiteral(args.head)
+ if chars.forall(_.isInstanceOf[CharLiteral])
+ } yield {
+ chars.collect{ case CharLiteral(c) => c }.mkString
}
case _ =>
None
}
}
-
object TopLevelOrs { // expr1 AND (expr2 AND (expr3 AND ..)) => List(expr1, expr2, expr3)
def unapply(e: Expr): Option[Seq[Expr]] = e match {
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
index f43e4bd831c16cb87a1eb671261e438ee5b5e33c..dfe6df71419ff6b9fc817fe3525b72335a3cad5f 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4Solver.scala
@@ -88,15 +88,15 @@ class SMTLIBCVC4Solver(context: LeonContext, program: Program) extends SMTLIBSol
finiteLambda(dflt, mapping :+ (fromSMT(key, tupleTypeWrap(from)) -> fromSMT(elem, to)), from)
case (FunctionApplication(SimpleSymbol(SSymbol("singleton")), elems), SetType(base)) =>
- finiteSet(elems.map(fromSMT(_, base)).toSet, base)
+ FiniteSet(elems.map(fromSMT(_, base)).toSet, base)
case (FunctionApplication(SimpleSymbol(SSymbol("insert")), elems), SetType(base)) =>
val selems = elems.init.map(fromSMT(_, base))
val FiniteSet(se, _) = fromSMT(elems.last, tpe)
- finiteSet(se ++ selems, base)
+ FiniteSet(se ++ selems, base)
case (FunctionApplication(SimpleSymbol(SSymbol("union")), elems), SetType(base)) =>
- finiteSet(elems.map(fromSMT(_, tpe) match {
+ FiniteSet(elems.map(fromSMT(_, tpe) match {
case FiniteSet(elems, _) => elems
}).flatten.toSet, base)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index b5560fb0b4d5861ed226d63c74407c3a4392eaa0..722e2566afadeb49e980c77b73747c24a9683414 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -159,7 +159,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
}
require(r.keyTpe == base, s"Type error in solver model, expected $base, found ${r.keyTpe}")
- finiteSet(r.elems.keySet, base)
+ FiniteSet(r.elems.keySet, base)
case RawArrayType(from, to) =>
r
@@ -180,7 +180,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
case (k, CaseClass(leonSome, Seq(x))) => Some(k -> x)
case (k, _) => None
}.toSeq
- finiteMap(elems, from, to)
+ FiniteMap(elems, from, to)
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 fe7b0fec729419f29fbbe346c38fe3e7a14dca40..3959e2265f67ac446faf4e2d4ea81fd8f617b562 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -714,7 +714,7 @@ trait AbstractZ3Solver
case (k, _) => None
}.toSeq
- finiteMap(elems, from, to)
+ FiniteMap(elems, from, to)
}
@@ -732,7 +732,7 @@ trait AbstractZ3Solver
case None => throw new IllegalArgumentException
case Some(set) =>
val elems = set.map(e => rec(e, dt))
- finiteSet(elems, dt)
+ FiniteSet(elems, dt)
}
case _ =>
diff --git a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
index 3752b228c2bf2c6b84c7445f2c22b6628e2c9380..ebb4bb8faf22ddd1bf25a5b0ab26cbaea41d2add 100644
--- a/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
+++ b/src/main/scala/leon/synthesis/utils/ExpressionGrammar.scala
@@ -124,7 +124,7 @@ object ExpressionGrammars {
case st @ SetType(base) =>
List(
- Generator(List(base), { case elems => finiteSet(elems.toSet, base) }),
+ Generator(List(base), { case elems => FiniteSet(elems.toSet, base) }),
Generator(List(st, st), { case Seq(a, b) => SetUnion(a, b) }),
Generator(List(st, st), { case Seq(a, b) => SetIntersection(a, b) }),
Generator(List(st, st), { case Seq(a, b) => SetDifference(a, b) })
@@ -177,8 +177,8 @@ object ExpressionGrammars {
case st @ SetType(base) =>
List(
- Generator(List(base), { case elems => finiteSet(elems.toSet, base) }),
- Generator(List(base, base), { case elems => finiteSet(elems.toSet, base) })
+ Generator(List(base), { case elems => FiniteSet(elems.toSet, base) }),
+ Generator(List(base, base), { case elems => FiniteSet(elems.toSet, base) })
)
case UnitType =>
diff --git a/src/test/resources/regression/verification/purescala/invalid/Array4.scala b/src/test/resources/regression/verification/purescala/invalid/Array4.scala
index 4e630cd428758454bc00f9e5355e502939839ad3..d7875d9b3ea09be869429c801fe59716213aac3a 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Array4.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Array4.scala
@@ -6,7 +6,7 @@ object Array4 {
def foo(a: Array[Int]): Int = {
val tmp = a.updated(0, 0)
- 42
+ tmp(0)
}
}