From d7f8c8b0cdf60d6241990a083861a7dfb9bdf8cb Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Fri, 11 Oct 2024 16:09:14 +0200 Subject: [PATCH 1/8] add flatmap to set --- frontends/library/stainless/lang/Set.scala | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/frontends/library/stainless/lang/Set.scala b/frontends/library/stainless/lang/Set.scala index a299eecf7..8da2ba422 100644 --- a/frontends/library/stainless/lang/Set.scala +++ b/frontends/library/stainless/lang/Set.scala @@ -36,6 +36,11 @@ object Set { new Set(set.theSet.map(f)) } + @extern @pure + def flatMap[B](f: A => Set[B]): Set[B] = { + new Set(set.theSet.flatMap(f(_).theSet)) + } + @extern @pure def mapPost1[B](f: A => B)(a: A): Unit = { () From ff2043d0477ec7c87834a8f70f0bd8749f4d9d6e Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Fri, 11 Oct 2024 16:25:59 +0200 Subject: [PATCH 2/8] add flatmap postcondition --- frontends/library/stainless/lang/Set.scala | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/frontends/library/stainless/lang/Set.scala b/frontends/library/stainless/lang/Set.scala index 8da2ba422..f9e491621 100644 --- a/frontends/library/stainless/lang/Set.scala +++ b/frontends/library/stainless/lang/Set.scala @@ -36,15 +36,10 @@ object Set { new Set(set.theSet.map(f)) } - @extern @pure - def flatMap[B](f: A => Set[B]): Set[B] = { - new Set(set.theSet.flatMap(f(_).theSet)) - } - @extern @pure def mapPost1[B](f: A => B)(a: A): Unit = { () - }.ensuring { _ => + }.ensuring { _ => !set.contains(a) || map[B](f).contains(f(a)) } @@ -52,10 +47,22 @@ object Set { def mapPost2[B](f: A => B)(b: B): A = { require(map[B](f).contains(b)) (??? : A) - }.ensuring { (a:A) => + }.ensuring { (a:A) => b == f(a) && set.contains(a) } + @extern @pure + def flatMap[B](f: A => Set[B]): Set[B] = { + new Set(set.theSet.flatMap(f(_).theSet)) + } + + @extern @pure + def flatMapPost[B](f: A => B)(b: B) = { + (??? : A) + }.ensuring { _ => + flatMap(f).contains(b) == set.exists(a => f(a).contains(b)) + } + @extern @pure def filter(p: A => Boolean): Set[A] = { new Set(set.theSet.filter(p)) From d0dc10d7430cad39f338efa04b5762fe21fbee59 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Mon, 14 Oct 2024 15:32:28 +0200 Subject: [PATCH 3/8] update set --- frontends/library/stainless/lang/Set.scala | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/frontends/library/stainless/lang/Set.scala b/frontends/library/stainless/lang/Set.scala index f9e491621..a7fbc75e4 100644 --- a/frontends/library/stainless/lang/Set.scala +++ b/frontends/library/stainless/lang/Set.scala @@ -57,7 +57,7 @@ object Set { } @extern @pure - def flatMapPost[B](f: A => B)(b: B) = { + def flatMapPost[B](f: A => Set[B])(b: B) = { (??? : A) }.ensuring { _ => flatMap(f).contains(b) == set.exists(a => f(a).contains(b)) @@ -126,4 +126,7 @@ sealed case class Set[T](theSet: scala.collection.immutable.Set[T]) { def contains(a: T): Boolean = theSet.contains(a) def subsetOf(b: Set[T]): Boolean = theSet.subsetOf(b.theSet) + + def exists(p: T => Boolean): Boolean = theSet.exists(p) + def forall(p: T => Boolean): Boolean = theSet.forall(p) } From 0897b252b8ef9c432e37d382cdddf1604b119b2c Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Wed, 16 Oct 2024 11:11:57 +0200 Subject: [PATCH 4/8] Move forall and exists to the SetOps class --- frontends/library/stainless/lang/Set.scala | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/frontends/library/stainless/lang/Set.scala b/frontends/library/stainless/lang/Set.scala index a7fbc75e4..9a7462aa2 100644 --- a/frontends/library/stainless/lang/Set.scala +++ b/frontends/library/stainless/lang/Set.scala @@ -31,6 +31,17 @@ object Set { @library implicit class SetOps[A](val set: Set[A]) extends AnyVal { + + @extern @pure + def exists(p: A => Boolean): Boolean = { + set.theSet.exists(p) + } + + @extern @pure + def forall(p: A => Boolean): Boolean = { + set.theSet.forall(p) + } + @extern @pure def map[B](f: A => B): Set[B] = { new Set(set.theSet.map(f)) @@ -126,7 +137,4 @@ sealed case class Set[T](theSet: scala.collection.immutable.Set[T]) { def contains(a: T): Boolean = theSet.contains(a) def subsetOf(b: Set[T]): Boolean = theSet.subsetOf(b.theSet) - - def exists(p: T => Boolean): Boolean = theSet.exists(p) - def forall(p: T => Boolean): Boolean = theSet.forall(p) } From ce2004e9b1b461d077cfe97376ac766391efa844 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Wed, 16 Oct 2024 11:21:57 +0200 Subject: [PATCH 5/8] move to extension methods instead of implicit class --- frontends/library/stainless/lang/Set.scala | 44 +++++++++++----------- 1 file changed, 21 insertions(+), 23 deletions(-) diff --git a/frontends/library/stainless/lang/Set.scala b/frontends/library/stainless/lang/Set.scala index 9a7462aa2..6ec686ba3 100644 --- a/frontends/library/stainless/lang/Set.scala +++ b/frontends/library/stainless/lang/Set.scala @@ -23,38 +23,36 @@ object Set { new Set(set) } - @extern @pure @library - def mkString[A](set: Set[A], infix: String)(format: A => String): String = { - set.theSet.map(format).toList.sorted.mkString(infix) - } - - @library - implicit class SetOps[A](val set: Set[A]) extends AnyVal { + // @extern @pure @library + // def mkString[A](set: Set[A], infix: String)(format: A => String): String = { + // set.theSet.map(format).toList.sorted.mkString(infix) + // } + extension[A](set: Set[A]) { - @extern @pure + @library @extern @pure def exists(p: A => Boolean): Boolean = { set.theSet.exists(p) } - @extern @pure + @library @extern @pure def forall(p: A => Boolean): Boolean = { set.theSet.forall(p) } - @extern @pure + @library @extern @pure def map[B](f: A => B): Set[B] = { new Set(set.theSet.map(f)) } - @extern @pure + @library @extern @pure def mapPost1[B](f: A => B)(a: A): Unit = { () }.ensuring { _ => !set.contains(a) || map[B](f).contains(f(a)) } - @extern @pure + @library @extern @pure def mapPost2[B](f: A => B)(b: B): A = { require(map[B](f).contains(b)) (??? : A) @@ -62,52 +60,52 @@ object Set { b == f(a) && set.contains(a) } - @extern @pure + @library @extern @pure def flatMap[B](f: A => Set[B]): Set[B] = { new Set(set.theSet.flatMap(f(_).theSet)) } - @extern @pure + @library @extern @pure def flatMapPost[B](f: A => Set[B])(b: B) = { (??? : A) }.ensuring { _ => - flatMap(f).contains(b) == set.exists(a => f(a).contains(b)) + set.flatMap(f).contains(b) == set.exists(a => f(a).contains(b)) } - @extern @pure + @library @extern @pure def filter(p: A => Boolean): Set[A] = { new Set(set.theSet.filter(p)) } - @extern @pure + @library @extern @pure def filterPost(p: A => Boolean)(a: A): Unit = { () }.ensuring (_ => filter(p).contains(a) == (p(a) && set.contains(a))) - @extern @pure + @library @extern @pure def withFilter(p: A => Boolean): Set[A] = { new Set(set.theSet.filter(p)) } - @extern @pure + @library @extern @pure def withFilterPost(p: A => Boolean)(a: A): Unit = { () }.ensuring(_ => withFilter(p).contains(a) == (p(a) && set.contains(a))) - @extern @pure + @library @extern @pure def toList: List[A] = { List.fromScala(set.theSet.toList) }.ensuring(res => ListOps.noDuplicate(res) && res.content == set) - @extern @pure + @library @extern @pure def toListPost(a:A): Unit = { () }.ensuring(_ => toList.contains(a) == set.contains(a)) - @extern @pure + @library @extern @pure def toScala: ScalaSet[A] = set.theSet - @extern @pure + @library @extern @pure def mkString(infix: String)(format: A => String): String = { set.theSet.map(format).toList.sorted.mkString(infix) } From 58468a0a817777525be20d5a211e6a7ab408e977 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Wed, 16 Oct 2024 13:42:04 +0200 Subject: [PATCH 6/8] new timeout for sat precond test --- .../stainless/verification/SatPrecondVerificationSuite.scala | 2 ++ 1 file changed, 2 insertions(+) diff --git a/frontends/common/src/it/scala/stainless/verification/SatPrecondVerificationSuite.scala b/frontends/common/src/it/scala/stainless/verification/SatPrecondVerificationSuite.scala index e1dc44ca1..18edadc8e 100644 --- a/frontends/common/src/it/scala/stainless/verification/SatPrecondVerificationSuite.scala +++ b/frontends/common/src/it/scala/stainless/verification/SatPrecondVerificationSuite.scala @@ -46,7 +46,9 @@ class SatPrecondVerificationSuite extends VerificationComponentTestSuite { inox.optSelectedSolvers(Set(solver)), inox.solvers.optCheckModels(true), evaluators.optCodeGen(codeGen), + inox.optTimeout(4.seconds), inox.solvers.unrolling.optFeelingLucky(codeGen)) ++ seq + } } yield conf } From 8dc93f41a84cc604608f2c9770ab93e755826c61 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Wed, 16 Oct 2024 14:48:19 +0200 Subject: [PATCH 7/8] new big timeout --- .../stainless/verification/SatPrecondVerificationSuite.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontends/common/src/it/scala/stainless/verification/SatPrecondVerificationSuite.scala b/frontends/common/src/it/scala/stainless/verification/SatPrecondVerificationSuite.scala index 18edadc8e..447f3d653 100644 --- a/frontends/common/src/it/scala/stainless/verification/SatPrecondVerificationSuite.scala +++ b/frontends/common/src/it/scala/stainless/verification/SatPrecondVerificationSuite.scala @@ -46,7 +46,7 @@ class SatPrecondVerificationSuite extends VerificationComponentTestSuite { inox.optSelectedSolvers(Set(solver)), inox.solvers.optCheckModels(true), evaluators.optCodeGen(codeGen), - inox.optTimeout(4.seconds), + inox.optTimeout(30.seconds), inox.solvers.unrolling.optFeelingLucky(codeGen)) ++ seq } From 7e167f8d315b14fc28bb4d6fecefbe30f1e708f7 Mon Sep 17 00:00:00 2001 From: Samuel Chassot Date: Wed, 16 Oct 2024 16:11:19 +0200 Subject: [PATCH 8/8] ignore sat-precondition/valid/SATPrecond4 with Princess --- .../stainless/verification/SatPrecondVerificationSuite.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/frontends/common/src/it/scala/stainless/verification/SatPrecondVerificationSuite.scala b/frontends/common/src/it/scala/stainless/verification/SatPrecondVerificationSuite.scala index 447f3d653..62aea8d9a 100644 --- a/frontends/common/src/it/scala/stainless/verification/SatPrecondVerificationSuite.scala +++ b/frontends/common/src/it/scala/stainless/verification/SatPrecondVerificationSuite.scala @@ -19,7 +19,7 @@ class SatPrecondVerificationSuite extends VerificationComponentTestSuite { Set() private val ignorePrincess: Set[String] = ignoreCommon ++ - Set() + Set("sat-precondition/valid/SATPrecond4") private val ignoreCodegen: Set[String] = Set() @@ -46,7 +46,7 @@ class SatPrecondVerificationSuite extends VerificationComponentTestSuite { inox.optSelectedSolvers(Set(solver)), inox.solvers.optCheckModels(true), evaluators.optCodeGen(codeGen), - inox.optTimeout(30.seconds), + inox.optTimeout(3.seconds), inox.solvers.unrolling.optFeelingLucky(codeGen)) ++ seq }