diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 99e2465120173fc72ed3e55d30606d5280fbfc50..d69bdbf94e608fed2a7d8fb3a2a60b1c0bd5f276 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -881,7 +881,7 @@ object ExprOps {
val subTests = subps.zipWithIndex.map{case (p, i) => rec(tupleSelect(in, i+1, subps.size), p)}
and(bind(ob, in) +: subTests: _*)
- case up@UnapplyPattern(ob, fd, subps) =>
+ case up @ UnapplyPattern(ob, fd, subps) =>
def someCase(e: Expr) = {
// In the case where unapply returns a Some, it is enough that the subpatterns match
andJoin(unwrapTuple(e, subps.size) zip subps map { case (ex, p) => rec(ex, p).setPos(p) }).setPos(e)
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index a45c4ee59a0bf518f320769286b00b95ce2fc42a..532d96d44ff00e8530b59e4728dfb34a0edfa3f9 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -331,7 +331,7 @@ object Expressions {
// Hacky, but ok
lazy val optionType = unapplyFun.returnType.asInstanceOf[AbstractClassType]
lazy val Seq(noneType, someType) = optionType.knownCCDescendants.sortBy(_.fields.size)
- lazy val someValue = someType.fields.head
+ lazy val someValue = someType.classDef.fields.head
// Pattern match unapply(scrut)
// In case of None, return noneCase.
// In case of Some(v), return someCase(v).
diff --git a/src/main/scala/leon/purescala/MethodLifting.scala b/src/main/scala/leon/purescala/MethodLifting.scala
index 8cfae30d2ebfa070ceb5f50fb58e1eab1c70ccd6..2014739eaa3fba0c84ce10685087262e7e227872 100644
--- a/src/main/scala/leon/purescala/MethodLifting.scala
+++ b/src/main/scala/leon/purescala/MethodLifting.scala
@@ -27,7 +27,7 @@ object MethodLifting extends TransformationPhase {
// Common for both cases
val ct = ccd.typed
val binder = FreshIdentifier(ccd.id.name.toLowerCase, ct, true)
- val fBinders = ct.fields.map{ f => f.id -> f.id.freshen }.toMap
+ val fBinders = (ccd.fieldsIds zip ct.fields).map(p => p._1 -> p._2.id.freshen).toMap
def subst(e: Expr): Expr = e match {
case CaseClassSelector(`ct`, This(`ct`), i) =>
Variable(fBinders(i)).setPos(e)
@@ -37,19 +37,19 @@ object MethodLifting extends TransformationPhase {
e
}
- ccd.methods.find( _.id == fdId).map { m =>
+ ccd.methods.find(_.id == fdId).map { m =>
// Ancestor's method is a method in the case class
- val subPatts = ct.fields map (f => WildcardPattern(Some(fBinders(f.id))))
+ val subPatts = ccd.fields map (f => WildcardPattern(Some(fBinders(f.id))))
val patt = CaseClassPattern(Some(binder), ct, subPatts)
val newE = simplePreTransform(subst)(breakDown(m.fullBody))
val cse = SimpleCase(patt, newE).setPos(newE)
(List(cse), true)
- } orElse ccd.fields.find( _.id == fdId).map { f =>
+ } orElse ccd.fields.find(_.id == fdId).map { f =>
// Ancestor's method is a case class argument in the case class
- val subPatts = ct.fields map (fld =>
+ val subPatts = ccd.fields map (fld =>
if (fld.id == f.id)
WildcardPattern(Some(fBinders(f.id)))
else
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index ed8e75fbf79bcd8ea5016863ed845134ff59bc62..cc54bdd6c1b904c9aa4c419460ef011e674e5f53 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -630,6 +630,84 @@ trait SMTLIBTarget extends Interruptible {
/* Translate an SMTLIB term back to a Leon Expr */
protected def fromSMT(t: Term, otpe: Option[TypeTree] = None)(implicit lets: Map[SSymbol, Term], letDefs: Map[SSymbol, DefineFun]): Expr = {
+ object EQ {
+ def unapply(t: Term): Option[(Term, Term)] = t match {
+ case Core.Equals(e1, e2) => Some((e1, e2))
+ case FunctionApplication(f, Seq(e1, e2)) if f.toString == "=" => Some((e1, e2))
+ case _ => None
+ }
+ }
+
+ object AND {
+ def unapply(t: Term): Option[Seq[Term]] = t match {
+ case Core.And(e1, e2) => Some(Seq(e1, e2))
+ case FunctionApplication(SimpleSymbol(SSymbol("and")), args) => Some(args)
+ case _ => None
+ }
+ def apply(ts: Seq[Term]): Term = ts match {
+ case Seq() => throw new IllegalArgumentException
+ case Seq(t) => t
+ case _ => FunctionApplication(SimpleSymbol(SSymbol("and")), ts)
+ }
+ }
+
+ object Num {
+ def unapply(t: Term): Option[BigInt] = t match {
+ case SNumeral(n) => Some(n)
+ case FunctionApplication(f, Seq(SNumeral(n))) if f.toString == "-" => Some(-n)
+ case _ => None
+ }
+ }
+
+ def extractLambda(n: BigInt, ft: FunctionType): Expr = {
+ val FunctionType(from, to) = ft
+ lambdas.getB(ft) match {
+ case None => simplestValue(ft)
+ case Some(dynLambda) => letDefs.get(dynLambda) match {
+ case None => simplestValue(ft)
+ case Some(DefineFun(SMTFunDef(a, SortedVar(dispatcher, dkind) +: args, rkind, body))) =>
+ val d = symbolToQualifiedId(dispatcher)
+ def dispatch(t: Term): Term = t match {
+ case Core.ITE(EQ(di, Num(ni)), thenn, elze) if di == d =>
+ if (ni == n) thenn else dispatch(elze)
+ case Core.ITE(AND(EQ(di, Num(ni)) +: rest), thenn, elze) if di == d =>
+ if (ni == n) Core.ITE(AND(rest), thenn, dispatch(elze)) else dispatch(elze)
+ case _ => t
+ }
+
+ def extract(t: Term): Expr = {
+ def recCond(term: Term, index: Int): Seq[Expr] = term match {
+ case AND(es) =>
+ es.foldLeft(Seq.empty[Expr]) { case (seq, e) => seq ++ recCond(e, index + seq.size) }
+ case EQ(e1, e2) =>
+ recCond(e2, index)
+ case _ => Seq(fromSMT(term, from(index)))
+ }
+
+ def recCases(term: Term, matchers: Seq[Expr]): Seq[(Seq[Expr], Expr)] = term match {
+ case Core.ITE(cond, thenn, elze) =>
+ val cs = recCond(cond, matchers.size)
+ recCases(thenn, matchers ++ cs) ++ recCases(elze, matchers)
+ case AND(es) if to == BooleanType =>
+ Seq((matchers ++ recCond(term, matchers.size)) -> BooleanLiteral(true))
+ case EQ(e1, e2) if to == BooleanType =>
+ Seq((matchers ++ recCond(term, matchers.size)) -> BooleanLiteral(true))
+ case _ => Seq(matchers -> fromSMT(term, to))
+ }
+
+ val cases = recCases(t, Seq.empty)
+ val (default, rest) = cases.partition(_._1.isEmpty)
+ val leonDefault = if (default.isEmpty && to == BooleanType) BooleanLiteral(false) else default.head._2
+ PartialLambda(rest.filter(_._1.size == from.size), Some(leonDefault), ft)
+ }
+
+ val lambdaTerm = dispatch(body)
+ val lambda = extract(lambdaTerm)
+ lambda
+ }
+ }
+ }
+
// Use as much information as there is, if there is an expected type, great, but it might not always be there
(t, otpe) match {
case (_, Some(UnitType)) =>
@@ -663,79 +741,8 @@ trait SMTLIBTarget extends Interruptible {
}
}
- case (SNumeral(n), Some(ft @ FunctionType(from, to))) =>
- val dynLambda = lambdas.toB(ft)
- val DefineFun(SMTFunDef(a, SortedVar(dispatcher, dkind) +: args, rkind, body)) = letDefs(dynLambda)
-
- object EQ {
- def unapply(t: Term): Option[(Term, Term)] = t match {
- case Core.Equals(e1, e2) => Some((e1, e2))
- case FunctionApplication(f, Seq(e1, e2)) if f.toString == "=" => Some((e1, e2))
- case _ => None
- }
- }
-
- object AND {
- def unapply(t: Term): Option[Seq[Term]] = t match {
- case Core.And(e1, e2) => Some(Seq(e1, e2))
- case FunctionApplication(SimpleSymbol(SSymbol("and")), args) => Some(args)
- case _ => None
- }
- def apply(ts: Seq[Term]): Term = ts match {
- case Seq() => throw new IllegalArgumentException
- case Seq(t) => t
- case _ => FunctionApplication(SimpleSymbol(SSymbol("and")), ts)
- }
- }
-
- object Num {
- def unapply(t: Term): Option[BigInt] = t match {
- case SNumeral(n) => Some(n)
- case FunctionApplication(f, Seq(SNumeral(n))) if f.toString == "-" => Some(-n)
- case _ => None
- }
- }
-
- val d = symbolToQualifiedId(dispatcher)
- def dispatch(t: Term): Term = t match {
- case Core.ITE(EQ(di, Num(ni)), thenn, elze) if di == d =>
- if (ni == n) thenn else dispatch(elze)
- case Core.ITE(AND(EQ(di, Num(ni)) +: rest), thenn, elze) if di == d =>
- if (ni == n) Core.ITE(AND(rest), thenn, dispatch(elze)) else dispatch(elze)
- case _ => t
- }
-
- def extract(t: Term): Expr = {
- def recCond(term: Term, index: Int): Seq[Expr] = term match {
- case AND(es) =>
- es.foldLeft(Seq.empty[Expr]) { case (seq, e) => seq ++ recCond(e, index + seq.size) }
- case EQ(e1, e2) =>
- recCond(e2, index)
- case _ => Seq(fromSMT(term, from(index)))
- }
-
- def recCases(term: Term, matchers: Seq[Expr]): Seq[(Seq[Expr], Expr)] = term match {
- case Core.ITE(cond, thenn, elze) =>
- val cs = recCond(cond, matchers.size)
- recCases(thenn, matchers ++ cs) ++ recCases(elze, matchers)
- case AND(es) if to == BooleanType =>
- Seq((matchers ++ recCond(term, matchers.size)) -> BooleanLiteral(true))
- case EQ(e1, e2) if to == BooleanType =>
- Seq((matchers ++ recCond(term, matchers.size)) -> BooleanLiteral(true))
- case _ => Seq(matchers -> fromSMT(term, to))
- }
-
- val cases = recCases(t, Seq.empty)
- val (default, rest) = cases.partition(_._1.isEmpty)
- val leonDefault = if (default.isEmpty && to == BooleanType) BooleanLiteral(false) else default.head._2
-
- assert(rest.forall(_._1.size == from.size))
- PartialLambda(rest, Some(leonDefault), ft)
- }
-
- val lambdaTerm = dispatch(body)
- val lambda = extract(lambdaTerm)
- lambda
+ case (Num(n), Some(ft: FunctionType)) =>
+ extractLambda(n, ft)
case (SNumeral(n), Some(RealType)) =>
FractionalLiteral(n, 1)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index 334f9f0ad12820282da3569d028253662480104e..3d4a06a838a5057a693d85754bb5113e1ce7d0ae 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -76,11 +76,6 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
val n = s.name.split("!").toList.last
GenericValue(tp, n.toInt)
- // XXX: (NV) Z3 doesn't seem to produce models for uninterpreted functions that
- // don't impact satisfiability...
- case (SNumeral(n), Some(ft: FunctionType)) if !letDefs.isDefinedAt(lambdas.toB(ft)) =>
- purescala.ExprOps.simplestValue(ft)
-
case (QualifiedIdentifier(ExtendedIdentifier(SSymbol("as-array"), k: SSymbol), _), Some(tpe)) =>
if (letDefs contains k) {
// Need to recover value form function model
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index d7a3fd8fa22ac9ebeed9529aba1c17d00ca39e5a..bc6aaf207c071e694f6154fca23d128479aa50d0 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -657,9 +657,9 @@ trait AbstractZ3Solver extends Solver {
}
case ft @ FunctionType(fts, tt) => lambdas.getB(ft) match {
- case None => throw new IllegalArgumentException
+ case None => simplestValue(ft)
case Some(decl) => model.getModelFuncInterpretations.find(_._1 == decl) match {
- case None => throw new IllegalArgumentException
+ case None => simplestValue(ft)
case Some((_, mapping, elseValue)) =>
val leonElseValue = rec(elseValue, tt)
PartialLambda(mapping.flatMap { case (z3Args, z3Result) =>
@@ -738,7 +738,8 @@ trait AbstractZ3Solver extends Solver {
case _ => unsound(t, "unexpected AST")
}
}
- rec(tree, tpe)
+
+ rec(tree, normalizeType(tpe))
}
protected[leon] def softFromZ3Formula(model: Z3Model, tree: Z3AST, tpe: TypeTree) : Option[Expr] = {
diff --git a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
index 227dd691c29734e0dd85feb179f40fac15ceea7a..6b2f9e8585a98ab9677aa5f1c439b2a1afa136ef 100644
--- a/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
+++ b/src/main/scala/leon/synthesis/rules/EquivalentInputs.scala
@@ -24,7 +24,7 @@ case object EquivalentInputs extends NormalizingRule("EquivalentInputs") {
val ccSubsts = for (IsInstanceOf(s, cct: CaseClassType) <- instanceOfs) yield {
- val fieldsVals = (for (f <- cct.fields) yield {
+ val fieldsVals = (for (f <- cct.classDef.fields) yield {
val id = f.id
clauses.find {
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index bbd87b999e653a943598915e7d2e38a9aba20bff..3f7be09f145d2768ff00f8573f078d6e90bc1b2d 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -34,7 +34,7 @@ trait Solvable extends Processor {
val sizeUnit : UnitDef = UnitDef(FreshIdentifier("$size"),Seq(sizeModule))
val newProgram : Program = program.copy( units = sizeUnit :: program.units)
- SolverFactory.getFromSettings(context, newProgram).withTimeout(1000.millisecond)
+ SolverFactory.getFromSettings(context, newProgram).withTimeout(10.seconds)
}
type Solution = (Option[Boolean], Map[Identifier, Expr])
diff --git a/src/test/resources/regression/verification/purescala/invalid/Unapply1.scala b/src/test/resources/regression/verification/purescala/invalid/Unapply1.scala
index 20ff95383b4f7042b0eba32fcc4e5c8b0cea3680..674ca7c69fa29333755d8908f707ae9931d20bf2 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Unapply1.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Unapply1.scala
@@ -6,10 +6,14 @@ object Unap1 {
}
object Unapply1 {
+
+ sealed abstract class Bool
+ case class True() extends Bool
+ case class False() extends Bool
- def bar: Boolean = { (42, false, ()) match {
- case Unap1(_, b) if b => b
+ def bar: Bool = { (42, False().asInstanceOf[Bool], ()) match {
+ case Unap1(_, b) if b == True() => b
case Unap1((), b) => b
- }} ensuring { res => res }
+ }} ensuring { res => res == True() }
}
diff --git a/src/test/resources/regression/verification/purescala/invalid/Unapply2.scala b/src/test/resources/regression/verification/purescala/invalid/Unapply2.scala
index ae4167c20026f0e926494af6cf3a11f25e9399e5..7efd6e220fd1c7fcd08fbaa5b7016bf6801e151f 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Unapply2.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Unapply2.scala
@@ -5,7 +5,12 @@ object Unap2 {
}
object Unapply {
- def bar: Boolean = { (42, false, ()) match {
- case Unap2(_, b) if b => b
- }} ensuring { res => res }
+
+ sealed abstract class Bool
+ case class True() extends Bool
+ case class False() extends Bool
+
+ def bar: Bool = { (42, False().asInstanceOf[Bool], ()) match {
+ case Unap2(_, b) if b == True() => b
+ }} ensuring { res => res == True() }
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Unapply.scala b/src/test/resources/regression/verification/purescala/valid/Unapply.scala
index 941b1f370d740204e8fa850a9d5e5a787b1c401e..1885837d990c32185a42c1232a53de48c3935340 100644
--- a/src/test/resources/regression/verification/purescala/valid/Unapply.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Unapply.scala
@@ -5,8 +5,18 @@ object Unap {
}
object Unapply {
- def bar: Boolean = { (42, true, ()) match {
- case Unap(_, b) if b => b
- case Unap((), b) => !b
- }} ensuring { res => res }
+
+ sealed abstract class Bool
+ case class True() extends Bool
+ case class False() extends Bool
+
+ def not(b: Bool): Bool = b match {
+ case True() => False()
+ case False() => True()
+ }
+
+ def bar: Bool = { (42, True().asInstanceOf[Bool], ()) match {
+ case Unap(_, b) if b == True() => b
+ case Unap((), b) => not(b)
+ }} ensuring { res => res == True() }
}