From e4ba453797830f2298df28e77bdab5bb00431c2c Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 10 Feb 2015 14:47:29 +0100
Subject: [PATCH] More fixes for lambda equality, got flatMap working!! Fixed
SMTLIB for z3 target
---
.../leon/solvers/smtlib/SMTLIBTarget.scala | 3 +
.../leon/solvers/smtlib/SMTLIBZ3Target.scala | 9 ++-
.../solvers/templates/LambdaManager.scala | 2 +-
.../leon/solvers/templates/Templates.scala | 9 ++-
.../purescala/valid/FlatMap.scala | 48 +++++++++++++
.../purescala/valid/FlatMap.scala.BAK | 69 -------------------
6 files changed, 64 insertions(+), 76 deletions(-)
create mode 100644 src/test/resources/regression/verification/purescala/valid/FlatMap.scala
delete mode 100644 src/test/resources/regression/verification/purescala/valid/FlatMap.scala.BAK
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index d55f225bc..7901e428f 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -78,6 +78,9 @@ trait SMTLIBTarget {
case RawArrayType(from, to) =>
r
+ case ft @ FunctionType(from, to) =>
+ 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/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
index f781cdc48..91e205c6a 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala
@@ -188,9 +188,12 @@ trait SMTLIBZ3Target extends SMTLIBTarget {
for (me <- smodel) me match {
case DefineFun(s, args, kind, e) =>
if(args.isEmpty) {
- val id = variables.toA(s)
- // EK: this is a little hack, we pass models for array functions as let-defs
- model += id -> fromSMT(e, id.getType)(Map(), modelFunDefs)
+ variables.getA(s) match {
+ case Some(id) =>
+ // EK: this is a little hack, we pass models for array functions as let-defs
+ model += id -> fromSMT(e, id.getType)(Map(), modelFunDefs)
+ case _ => // function, should be handled elsewhere
+ }
}
case _ =>
}
diff --git a/src/main/scala/leon/solvers/templates/LambdaManager.scala b/src/main/scala/leon/solvers/templates/LambdaManager.scala
index 7249313f1..d8aa9026f 100644
--- a/src/main/scala/leon/solvers/templates/LambdaManager.scala
+++ b/src/main/scala/leon/solvers/templates/LambdaManager.scala
@@ -112,7 +112,7 @@ class LambdaManager[T](encoder: TemplateEncoder[T]) {
template.contextEquality(that) match {
case None => encoder.mkNot(equals)
case Some(Seq()) => equals
- case Some(seq) => encoder.mkImplies(encoder.mkAnd(seq : _*), equals)
+ case Some(seq) => encoder.mkEquals(encoder.mkAnd(seq : _*), equals)
}
}.toSeq
}
diff --git a/src/main/scala/leon/solvers/templates/Templates.scala b/src/main/scala/leon/solvers/templates/Templates.scala
index c7e79263f..6c26fa8d8 100644
--- a/src/main/scala/leon/solvers/templates/Templates.scala
+++ b/src/main/scala/leon/solvers/templates/Templates.scala
@@ -230,7 +230,6 @@ object LambdaTemplate {
private def structuralKey[T](lambda: Lambda, dependencies: Map[Identifier, T]): (Lambda, Map[Identifier,T]) = {
def closureIds(expr: Expr): Seq[Identifier] = {
- val vars = variablesOf(expr)
val allVars : Seq[Identifier] = foldRight[Seq[Identifier]] {
(expr, idSeqs) => idSeqs.foldLeft(expr match {
case Variable(id) => Seq(id)
@@ -238,10 +237,11 @@ object LambdaTemplate {
})((acc, seq) => acc ++ seq)
} (expr)
+ val vars = variablesOf(expr)
allVars.filter(vars(_)).distinct
}
- val grouped : Map[TypeTree, Seq[Identifier]] = closureIds(lambda).groupBy(_.getType)
+ val grouped : Map[TypeTree, Seq[Identifier]] = (lambda.args.map(_.id) ++ closureIds(lambda)).groupBy(_.getType)
val subst : Map[Identifier, Identifier] = grouped.foldLeft(Map.empty[Identifier,Identifier]) { case (subst, (tpe, ids)) =>
val currentVars = typedIds(tpe)
@@ -257,7 +257,10 @@ object LambdaTemplate {
subst ++ (ids zip typedVars)
}
- val structuralLambda = replaceFromIDs(subst.mapValues(_.toVariable), lambda).asInstanceOf[Lambda]
+ val newArgs = lambda.args.map(vd => ValDef(subst(vd.id), vd.tpe))
+ val newBody = replaceFromIDs(subst.mapValues(_.toVariable), lambda.body)
+ val structuralLambda = Lambda(newArgs, newBody)
+
val newDeps = dependencies.map { case (id, idT) => subst(id) -> idT }
structuralLambda -> newDeps
diff --git a/src/test/resources/regression/verification/purescala/valid/FlatMap.scala b/src/test/resources/regression/verification/purescala/valid/FlatMap.scala
new file mode 100644
index 000000000..56f8c47e8
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/FlatMap.scala
@@ -0,0 +1,48 @@
+import leon.lang._
+import leon.collection._
+
+object FlatMap {
+
+ def append[T](l1: List[T], l2: List[T]): List[T] = l1 match {
+ case Cons(head, tail) => Cons(head, append(tail, l2))
+ case Nil() => l2
+ }
+
+ def associative_append_lemma[T](l1: List[T], l2: List[T], l3: List[T]): Boolean = {
+ append(append(l1, l2), l3) == append(l1, append(l2, l3))
+ }
+
+ def associative_append_lemma_induct[T](l1: List[T], l2: List[T], l3: List[T]): Boolean = {
+ l1 match {
+ case Nil() => associative_append_lemma(l1, l2, l3)
+ case Cons(head, tail) => associative_append_lemma(l1, l2, l3) && associative_append_lemma_induct(tail, l2, l3)
+ }
+ }.holds
+
+ def flatMap[T,U](list: List[T], f: T => List[U]): List[U] = list match {
+ case Cons(head, tail) => append(f(head), flatMap(tail, f))
+ case Nil() => Nil()
+ }
+
+ def associative_lemma[T,U,V](list: List[T], f: T => List[U], g: U => List[V]): Boolean = {
+ flatMap(flatMap(list, f), g) == flatMap(list, (x: T) => flatMap(f(x), g))
+ }
+
+ def associative_lemma_induct[T,U,V](list: List[T], flist: List[U], glist: List[V], f: T => List[U], g: U => List[V]): Boolean = {
+ associative_lemma(list, f, g) &&
+ append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) &&
+ (glist match {
+ case Cons(ghead, gtail) =>
+ associative_lemma_induct(list, flist, gtail, f, g)
+ case Nil() => flist match {
+ case Cons(fhead, ftail) =>
+ associative_lemma_induct(list, ftail, g(fhead), f, g)
+ case Nil() => list match {
+ case Cons(head, tail) => associative_lemma_induct(tail, f(head), Nil(), f, g)
+ case Nil() => true
+ }
+ }
+ })
+ }.holds
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/FlatMap.scala.BAK b/src/test/resources/regression/verification/purescala/valid/FlatMap.scala.BAK
deleted file mode 100644
index fc177bd1f..000000000
--- a/src/test/resources/regression/verification/purescala/valid/FlatMap.scala.BAK
+++ /dev/null
@@ -1,69 +0,0 @@
-import leon.lang._
-import leon.collection._
-
-object Lists5 {
-
- def append[T](l1: List[T], l2: List[T]): List[T] = l1 match {
- case Cons(head, tail) => Cons(head, append(tail, l2))
- case Nil() => l2
- }
-
- def associative_append_lemma[T](l1: List[T], l2: List[T], l3: List[T]): Boolean = {
- append(append(l1, l2), l3) == append(l1, append(l2, l3))
- }
-
- def associative_append_lemma_induct[T](l1: List[T], l2: List[T], l3: List[T]): Boolean = {
- l1 match {
- case Nil() => associative_append_lemma(l1, l2, l3)
- case Cons(head, tail) => associative_append_lemma(l1, l2, l3) && associative_append_lemma_induct(tail, l2, l3)
- }
- }.holds
-
- def flatMap[T,U](list: List[T], f: T => List[U]): List[U] = list match {
- case Cons(head, tail) => append(f(head), flatMap(tail, f))
- case Nil() => Nil()
- }
-
- def associative_lemma[T,U,V](list: List[T], f: T => List[U], g: U => List[V]): Boolean = {
- flatMap(flatMap(list, f), g) == flatMap(list, (x: T) => flatMap(f(x), g))
- }
-
- def associative_lemma_helper[T,U,V](fprev: List[U], fcur: List[U], fgprev: List[V], fgcur: List[V], tail: List[T], f: T => List[U], g: U => List[V]): Boolean = {
- val left = fcur match {
- case Cons(fhead, ftail) =>
- flatMap(append(fprev, Cons(fhead, append(ftail, flatMap(tail, f)))), g)
- case Nil() =>
- flatMap(append(fprev, flatMap(tail, f)), g)
- }
-
- val right = fgcur match {
- case Cons(fghead, fgtail) =>
- append(fgprev, Cons(fghead, append(fgtail, flatMap(tail, (x: T) => flatMap(f(x), g)))))
- case Nil() =>
- append(fgprev, flatMap(tail, (x: T) => flatMap(f(x), g)))
- }
-
- left == right && (fgcur match {
- case Cons(fghead, fgtail) => associative_lemma_helper(fprev, fcur, append(fgprev, Cons(fghead, Nil())), fgtail, tail, f, g)
- case Nil() => fcur match {
- case Cons(fhead, ftail) => associative_lemma_helper(append(fprev, Cons(fhead, Nil())), ftail, fgprev, fgcur, tail, f, g)
- case Nil() => tail match {
- case Nil() => true
- case Cons(head, tail) => f(head) match {
- case fl @ Cons(fh, ft) => associative_lemma_helper(Nil(), fl, Nil(), flatMap(fl, g), tail, f, g)
- case Nil() => associative_lemma_helper(Nil(), Nil(), Nil(), Nil(), tail, f, g)
- }
- }
- }
- })
- }
-
- def associative_lemma_induct[T,U,V](list: List[T], f: T => List[U], g: U => List[V]): Boolean = {
- list match {
- case Nil() => associative_lemma(list, f, g)
- case Cons(head, tail) =>
- associative_lemma(list, f, g) && associative_lemma_induct(tail, f, g) && associative_lemma_helper(Nil(), Nil(), Nil(), Nil(), list, f, g)
- }
- }.holds
-
-}
--
GitLab