diff --git a/build.sbt b/build.sbt index 3159baa76..b22d2f998 100644 --- a/build.sbt +++ b/build.sbt @@ -2,7 +2,7 @@ lazy val commonSettings = Seq( name := "Princess", organization := "uuverifiers", - version := "unstable-SNAPSHOT", + version := "2022-07-01", homepage := Some(url("https://philipp.ruemmer.org/princess.shtml")), licenses := Seq("BSD-3-Clause" -> url("https://opensource.org/licenses/BSD-3-Clause")), scmInfo := Some(ScmInfo( diff --git a/src/ap/CmdlMain.scala b/src/ap/CmdlMain.scala index d6d6e2cfd..d7fa2a331 100644 --- a/src/ap/CmdlMain.scala +++ b/src/ap/CmdlMain.scala @@ -50,7 +50,7 @@ import ap.util.{Debug, Seqs, Timeout} object CmdlMain { - val version = "unstable build" + val version = "2022-07-01" /** * Flag to enable stack traces being fully printed, for problems diff --git a/src/ap/proof/tree/RandomDataSource.scala b/src/ap/proof/tree/RandomDataSource.scala index 16f52268d..95428aa23 100644 --- a/src/ap/proof/tree/RandomDataSource.scala +++ b/src/ap/proof/tree/RandomDataSource.scala @@ -3,7 +3,7 @@ * arithmetic with uninterpreted predicates. * * - * Copyright (C) 2017 Philipp Ruemmer + * Copyright (C) 2017-2022 Philipp Ruemmer * * Redistribution and use in source and binary forms, with or without * modification, are permitted provided that the following conditions are met: @@ -63,6 +63,12 @@ abstract class RandomDataSource { */ def nextInt(bound : Int) : Int + /** + * Pick a random elements of the given sequence. + */ + def pick[A](objects : IndexedSeq[A]) : A = + objects(nextInt(objects.size)) + /** * Shuffle the given sequence */ @@ -79,6 +85,15 @@ abstract class RandomDataSource { } } + /** + * Shuffle the given sequence + */ + def shuffleSeq[A](seq : Seq[A]) : Seq[A] = { + val buf = seq.toBuffer + shuffle(buf) + buf.toIndexedSeq + } + /** * Shuffle the given sequence, and return the new ordering */