Merge branch 'epfl-lara:master' into master

agilot · web-flow · commit e656833ad230 · 2025-08-07T17:16:17.000+02:00
diff --git a/.github/workflows/scala-smtlib-CI.yml b/.github/workflows/scala-smtlib-CI.yml
@@ -0,0 +1,44 @@
+name: scala-smtlib CI
+on: [push, pull_request]
+jobs:
+  tests:
+    # the CI is small enough that we can run on draft PRs as well without issue
+    # if: github.event.pull_request.draft == false
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        java-version: [ 17, 21 ]
+    env:
+      # define Java options for both official sbt and sbt-extras
+      JAVA_OPTS: -Xss64M -Xms1024M -Xmx8G
+      JVM_OPTS:  -Xss64M -Xms1024M -Xmx8G
+      # solver versions to test against
+      Z3_VER: 4.15.1
+      CVC4_VER: 1.8
+      CVC5_VER: 1.2.1
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v4
+      with:
+        submodules: recursive
+    - name: Setup JDK
+      uses: actions/setup-java@v4
+      with:
+        distribution: temurin
+        java-version: ${{ matrix.java-version }}
+    - name: Install and unpack sbt
+      run: |
+        ./scripts/install_sbt.sh
+        echo "PATH=./sbt/bin/:$PATH" >> "$GITHUB_ENV"
+    - name: Install solvers
+      run: ./scripts/install_solvers.sh $GITHUB_WORKSPACE/.local/bin $Z3_VER $CVC4_VER $CVC5_VER
+    - name: Add solvers to PATH
+      run: echo "$GITHUB_WORKSPACE/.local/bin" >> $GITHUB_PATH
+    - name: Test solvers availability
+      run: cvc5 --version && z3 --version && cvc4 --version
+    - name: Run Tests
+      run: sbt -Dtest-parallelism=10 -batch test
+    - name: Run integration tests
+      run: sbt -Dtest-parallelism=10 -batch it:test
+    - name: Clean up
+      run: rm -rf $JAVA_OPTS_TMP_DIR
diff --git a/build.sbt b/build.sbt
@@ -18,7 +18,7 @@ Test / parallelExecution := true
 lazy val commonSettings = Seq(
   organization := "com.regblanc",
   name := "scala-smtlib",
-  scalaVersion := "3.3.0",
+  scalaVersion := "3.7.0",
 )
 
 lazy val root = (project in file(".")).
diff --git a/project/build.properties b/project/build.properties
@@ -1 +1 @@
-sbt.version=1.7.3
+sbt.version=1.11.1
diff --git a/scripts/install_sbt.sh b/scripts/install_sbt.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env sh
+
+SBT_VER="$(grep 'sbt.version' project/build.properties | cut -d= -f2)"
+if [ -z "$SBT_VER" ]; then
+  echo "sbt.version not found in project/build.properties"
+  exit 1
+fi
+wget -c https://github.com/sbt/sbt/releases/download/v${SBT_VER}/sbt-${SBT_VER}.tgz -q
+tar xfz "sbt-${SBT_VER}.tgz"
diff --git a/scripts/install_solvers.sh b/scripts/install_solvers.sh
@@ -0,0 +1,48 @@
+#!/usr/bin/env sh
+
+TEMP_DIR="$(pwd)/temp"
+SOLVERS_DIR=${1:-"$(pwd)/solvers"}
+
+Z3_VER=${2:-"4.15.1"}
+CVC4_VER=${3:-"1.8"}
+CVC5_VER=${4:-"1.2.1"}
+
+ARCH=$(uname -m)
+# short arch name as used by z3 builds
+SHORT_ARCH=$(uname -m | sed 's/x86_64/x64/;s/aarch64/arm64/;')
+
+# libc linked against z3
+# (glibc for Linux, osx for macOS)
+LIBC_NAME=$(uname -s | tr '[:upper:]' '[:lower:]' | sed 's/darwin/osx/;s/linux/glibc/;')
+
+mkdir -p "$SOLVERS_DIR"
+mkdir -p "$TEMP_DIR"
+# cvc5
+wget -c "https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VER}/cvc5-Linux-${ARCH}-static.zip" -O "$TEMP_DIR/cvc5.zip" -q
+unzip "$TEMP_DIR/cvc5.zip" -d "$TEMP_DIR" 
+CVC5_DIR=$(find "$TEMP_DIR" -mindepth 1 -maxdepth 1 -type d -name "*cvc5*")
+mv "$CVC5_DIR/bin/cvc5" "$SOLVERS_DIR/cvc5"
+chmod +x "$SOLVERS_DIR/cvc5"
+rm -rf "$TEMP_DIR"
+
+# # CVC4
+wget -c "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-${CVC4_VER}-x86_64-linux-opt" -O "$SOLVERS_DIR/cvc4" -q
+chmod +x "$SOLVERS_DIR/cvc4"
+
+# z3
+mkdir -p "$TEMP_DIR"
+Z3_FILE_PREFIX="z3-${Z3_VER}-${SHORT_ARCH}-${LIBC_NAME}"
+Z3_URL=$(
+  curl -s "https://api.github.com/repos/Z3Prover/z3/releases/tags/z3-${Z3_VER}" | # get release info
+  grep "browser_download_url.*${Z3_FILE_PREFIX}" | #| # find url for the correct build
+  sed 's/^.*: //;s/^"//;s/"$//' # strip non-url
+)
+wget -c "${Z3_URL}" -O "$TEMP_DIR/z3.zip" -q
+unzip "$TEMP_DIR/z3.zip" -d "$TEMP_DIR" 
+Z3_DIR=$(find "$TEMP_DIR" -mindepth 1 -maxdepth 1 -type d -name "*z3*")
+mv "$Z3_DIR/bin/z3" "$SOLVERS_DIR/z3"
+chmod +x "$SOLVERS_DIR/z3"
+rm -rf "$TEMP_DIR"
+
+echo "************** Solvers Installed **************"
+exit 0
diff --git a/src/main/scala/smtlib/common/Positions.scala b/src/main/scala/smtlib/common/Positions.scala
@@ -32,7 +32,7 @@ case class Position(line: Int, col: Int) extends Ordered[Position] {
   */
 trait Positioned {
 
-  private[this] var _pos: Option[Position] = None
+  private var _pos: Option[Position] = None
 
   def setPos(pos: Position): this.type = {
     _pos = Some(pos)
diff --git a/src/main/scala/smtlib/interpreters/ProcessInterpreter.scala b/src/main/scala/smtlib/interpreters/ProcessInterpreter.scala
@@ -130,7 +130,7 @@ object ProcessInterpreter {
   private def ctorHelper(executable: String,
                          args: Array[String],
                          parserCtor: BufferedReader => Parser): (Parser, Process, BufferedWriter, BufferedReader, BufferedReader) = {
-    val process = java.lang.Runtime.getRuntime.exec((executable :: args.toList).mkString(" "))
+    val process = java.lang.Runtime.getRuntime.exec(executable +: args)
     val in = new BufferedWriter(new OutputStreamWriter(process.getOutputStream))
     val out = new BufferedReader(new InputStreamReader(process.getInputStream))
     val err = new BufferedReader(new InputStreamReader(process.getErrorStream))
diff --git a/src/main/scala/smtlib/parser/ParserCommands.scala b/src/main/scala/smtlib/parser/ParserCommands.scala
@@ -7,7 +7,7 @@ import trees.Commands._
 
 import scala.collection.mutable.ListBuffer
 
-trait ParserCommands { this: ParserCommon with ParserTerms =>
+trait ParserCommands { this: ParserCommon & ParserTerms =>
 
   import Parser._
 
diff --git a/src/main/scala/smtlib/parser/ParserCommandsResponses.scala b/src/main/scala/smtlib/parser/ParserCommandsResponses.scala
@@ -7,7 +7,7 @@ import trees.CommandsResponses._
 
 import scala.collection.mutable.ListBuffer
 
-trait ParserCommandsResponses { this: ParserCommon with ParserTerms with ParserCommands =>
+trait ParserCommandsResponses { this: ParserCommon & ParserTerms & ParserCommands =>
 
   import Parser._
 
diff --git a/src/main/scala/smtlib/parser/ParserCommon.scala b/src/main/scala/smtlib/parser/ParserCommon.scala
@@ -164,7 +164,7 @@ trait ParserCommon {
       case Tokens.StringLitKind => parseString
       case Tokens.SymbolLitKind => parseSymbol
       case Tokens.OParen => parseSList
-      case _ => expected(peekToken, attributeValuesTokenKinds:_*)
+      case _ => expected(peekToken, attributeValuesTokenKinds*)
     }
   }
   def tryParseAttributeValue: Option[AttributeValue] = {
diff --git a/src/main/scala/smtlib/theories/FixedSizeBitVectors.scala b/src/main/scala/smtlib/theories/FixedSizeBitVectors.scala
@@ -48,7 +48,7 @@ object FixedSizeBitVectors {
       case QualifiedIdentifier(
         Identifier(SSymbol(cst), Seq(SNumeral(size))),
         None
-      ) if cst startsWith "bv" =>
+      ) if cst `startsWith` "bv" =>
         Some(BigInt(cst drop 2) -> size)
 
       case _ => None
diff --git a/src/main/scala/smtlib/trees/TermsOps.scala b/src/main/scala/smtlib/trees/TermsOps.scala
@@ -22,7 +22,7 @@ object TermsOps {
     * @return the new sort after applying the mapping
     */
   def postMap(f: (Sort) => Option[Sort])(sort: Sort): Sort = {
-    val rec = postMap(f) _
+    val rec = postMap(f)
     val Sort(id, subSorts) = sort
 
     val recSorts = subSorts.map(rec)
@@ -51,7 +51,7 @@ object TermsOps {
     * @note this operation can diverge if f is not well formed
     */
   def preMap(f: (Sort) => Option[Sort])(sort: Sort): Sort = {
-    val rec = preMap(f) _
+    val rec = preMap(f)
     val newSort = f(sort).getOrElse(sort)
     val Sort(id, subSorts) = newSort
 
@@ -65,22 +65,22 @@ object TermsOps {
 
 
   def postTraversal(f: (Sort) => Unit)(sort: Sort): Unit = {
-    val rec = postTraversal(f) _
+    val rec = postTraversal(f)
     val Sort(_, subSorts) = sort
     subSorts.foreach(rec)
     f(sort)
   }
 
   def preTraversal(f: (Sort) => Unit)(sort: Sort): Unit = {
-    val rec = preTraversal(f) _
+    val rec = preTraversal(f)
     val Sort(_, subSorts) = sort
     f(sort)
     subSorts.foreach(rec)
   }
 
 
   def fold[T](f: (Sort, Seq[T]) => T)(sort: Sort): T = {
-    val rec = fold(f) _
+    val rec = fold(f)
     val Sort(_, ss) = sort
     f(sort, ss.map(rec))
   }
diff --git a/src/main/scala/smtlib/trees/Trees.scala b/src/main/scala/smtlib/trees/Trees.scala
@@ -81,7 +81,7 @@ object Terms {
 
   case class SList(sexprs: List[SExpr]) extends SExpr with AttributeValue
   object SList {
-    def apply(sexprs: SExpr*): SList = SList(List(sexprs:_*))
+    def apply(sexprs: SExpr*): SList = SList(List(sexprs*))
   }
   case class SKeyword(name: String) extends SExpr
   case class SSymbol(name: String) extends SExpr with AttributeValue with Index
diff --git a/src/test/scala/smtlib/theories/StringsTests.scala b/src/test/scala/smtlib/theories/StringsTests.scala
@@ -136,22 +136,22 @@ class StringsTests extends AnyFunSuite with Matchers {
     }
 
 
-    "\"abc\"" shouldParseTo
+    "\"abc\"" `shouldParseTo`
     StringLit("abc")
 
-    "(str.++ \"a\" \"bc\" )" shouldParseTo
+    "(str.++ \"a\" \"bc\" )" `shouldParseTo`
     Concat(StringLit("a"), StringLit("bc"))
 
-    "(str.++ \"a\" \"bc\" \"def\" )" shouldParseTo
+    "(str.++ \"a\" \"bc\" \"def\" )" `shouldParseTo`
     Concat(StringLit("a"), StringLit("bc"), StringLit("def"))
 
-    "(str.len \"abcd\")" shouldParseTo
+    "(str.len \"abcd\")" `shouldParseTo`
     Length(StringLit("abcd"))
 
-    "(str.at \"abcd\" 1)" shouldParseTo
+    "(str.at \"abcd\" 1)" `shouldParseTo`
     At(StringLit("abcd"), NumeralLit(1))
 
-    "(str.substr \"abcdef\" 2 5)" shouldParseTo
+    "(str.substr \"abcdef\" 2 5)" `shouldParseTo`
     Substring(StringLit("abcdef"), NumeralLit(2), NumeralLit(5))
   }
 }

Original file line number	Diff line number	Diff line change
`@@ -18,7 +18,7 @@ Test / parallelExecution := true`
`18`	`18`	`lazy val commonSettings = Seq(`
`19`	`19`	`organization := "com.regblanc",`
`20`	`20`	`name := "scala-smtlib",`
`21`		`- scalaVersion := "3.3.0",`
	`21`	`+ scalaVersion := "3.7.0",`
`22`	`22`	`)`
`23`	`23`
`24`	`24`	`lazy val root = (project in file(".")).`
Original file line number	Diff line number	Diff line change
`@@ -1 +1 @@`
`1`		`-sbt.version=1.7.3`
	`1`	`+sbt.version=1.11.1`
Original file line number	Diff line number	Diff line change
`@@ -164,7 +164,7 @@ trait ParserCommon {`
`164`	`164`	`case Tokens.StringLitKind => parseString`
`165`	`165`	`case Tokens.SymbolLitKind => parseSymbol`
`166`	`166`	`case Tokens.OParen => parseSList`
`167`		`- case _ => expected(peekToken, attributeValuesTokenKinds:_*)`
	`167`	`+ case _ => expected(peekToken, attributeValuesTokenKinds*)`
`168`	`168`	`}`
`169`	`169`	`}`
`170`	`170`	`def tryParseAttributeValue: Option[AttributeValue] = {`