Skip to content

Commit

Permalink
version number
Browse files Browse the repository at this point in the history
  • Loading branch information
pruemmer committed Nov 2, 2022
1 parent 31630dc commit b8280e7
Show file tree
Hide file tree
Showing 3 changed files with 10 additions and 6 deletions.
6 changes: 3 additions & 3 deletions build.sbt
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
lazy val commonSettings = Seq(
name := "Princess",
organization := "uuverifiers",
version := "2022-07-01",
version := "2022-11-03",
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(
Expand Down Expand Up @@ -42,7 +42,7 @@ lazy val commonSettings = Seq(
),
description := "Princess is a theorem prover (aka SMT Solver) for Presburger arithmetic, uninterpreted predicates, and various other theories.",
scalaVersion := "2.11.12",
crossScalaVersions := Seq("2.11.12", "2.12.16"),
crossScalaVersions := Seq("2.11.12", "2.12.17"),
fork in run := true,
cancelable in Global := true,
publishTo := Some(Resolver.file("file", new File( "/tmp/shared-repo" )) )
Expand Down Expand Up @@ -93,7 +93,7 @@ lazy val root = (project in file(".")).
"-language:implicitConversions,postfixOps,reflectiveCalls"),
scalacOptions += (scalaVersion map { sv => sv match {
case "2.11.12" => "-optimise"
case "2.12.16" => "-opt:_"
case "2.12.17" => "-opt:_"
}}).value,
//
libraryDependencies +=
Expand Down
2 changes: 1 addition & 1 deletion src/ap/CmdlMain.scala
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ import ap.util.{Debug, Seqs, Timeout}

object CmdlMain {

val version = "unstable"
val version = "2022-11-03"

/**
* Flag to enable stack traces being fully printed, for problems
Expand Down
8 changes: 6 additions & 2 deletions src/ap/theories/ExtArray.scala
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,10 @@ object ExtArray {

private val instances = new MHashMap[(Seq[Sort], Sort), ExtArray]

/**
* Get a unique instance of the array theory with the given index
* and element sorts.
*/
def apply(indexSorts : Seq[Sort], objSort : Sort) : ExtArray = synchronized {
instances.getOrElseUpdate((indexSorts, objSort),
new ExtArray(indexSorts, objSort))
Expand Down Expand Up @@ -266,8 +270,8 @@ object ExtArray {
/**
* Theory of extensional arrays.
*/
class ExtArray private (val indexSorts : Seq[Sort],
val objSort : Sort) extends Theory {
class ExtArray (val indexSorts : Seq[Sort],
val objSort : Sort) extends Theory {
import ExtArray.{AC, AbstractArray}

private val infiniteIndex = indexSorts exists (_.cardinality.isEmpty)
Expand Down

0 comments on commit b8280e7

Please sign in to comment.