Cross-compilation for Scala 3.0, with some changes for Inox

The small changes are brought to help migrate Inox to Scala 3

Author: mario-bucev

.gitignore

@@ -6,6 +6,8 @@ target
 .metals
 .bloop
 .vscode
+.idea
+.bsp
 project/.bloop
 project/metals.sbt
-project/project
+project/project

.larabot.conf

@@ -1,5 +1,5 @@
 commands = [
-    "sbt -batch ++2.12.13 it:test"
+    "sbt -batch it:test"
 ]
 
 trusted = [

build.sbt

@@ -4,23 +4,22 @@ git.useGitDescribe := true
 
 scalacOptions ++= Seq("-unchecked", "-deprecation", "-feature")
 
-javaOptions in IntegrationTest ++= Seq("-Xss128M")
+IntegrationTest / javaOptions ++= Seq("-Xss128M")
 
-fork in IntegrationTest := true
+IntegrationTest / fork := true
 
-libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.7"
-libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.7" % "test"
+libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.7" % "test;it"
 
 
-logBuffered in IntegrationTest := false
+IntegrationTest / logBuffered := false
 
-parallelExecution in Test := true
+Test / parallelExecution := true
 
 lazy val commonSettings = Seq(
   organization := "com.regblanc",
   name := "scala-smtlib",
-  scalaVersion := "2.12.13",
-  crossScalaVersions := Seq("2.10.7", "2.11.12", "2.12.8", "2.12.13", "2.13.0", "2.13.5")
+  scalaVersion := "2.13.6",
+  crossScalaVersions := Seq("3.0.2")
 )
 
 lazy val root = (project in file(".")).
@@ -30,7 +29,7 @@ lazy val root = (project in file(".")).
 
 publishMavenStyle := true
 
-publishArtifact in Test := false
+Test / publishArtifact := false
 
 pomIncludeRepository := { _ => false }
 

project/build.properties

@@ -1 +1 @@
-sbt.version=1.3.0
+sbt.version=1.5.5

src/it/scala/smtlib/it/TestHelpers.scala

@@ -44,19 +44,18 @@ trait TestHelpers {
   def getCVC4Interpreter: Interpreter = CVC4Interpreter.buildDefault
 
   def isZ3Available: Boolean = try {
-    val output: String = "z3 -help".!! 
+    val _: String = "z3 -help".!!
     true
   } catch {
-    case (_: Exception) => false
+    case _: Exception => false
   }
 
   def isCVC4Available: Boolean = try {
-    val output: String = "cvc4".!!
+    // Make sure to pass a dummy option to cvc4, otherwise it starts in interactive mode (and does not exit)
+    val _: String = "cvc4 --version".!!
     true
   } catch {
-    case (e: Exception) => {
-      false
-    }
+    case _: Exception => false
   }
 
   def executeZ3(file: File)(f: (String) => Unit): Unit = {

src/main/scala/smtlib/interpreters/CVC4Interpreter.scala

@@ -1,16 +1,22 @@
 package smtlib
 package interpreters
 
-import trees.Terms._
+import smtlib.lexer.Lexer
+import smtlib.parser.Parser
+import smtlib.printer.{Printer, RecursivePrinter}
 import trees.Commands._
-import trees.CommandsResponses._
 
-class CVC4Interpreter(executable: String, args: Array[String], tailPrinter: Boolean = false)
-  extends ProcessInterpreter(executable, args, tailPrinter) {
+import java.io.BufferedReader
+
+class CVC4Interpreter(executable: String,
+                      args: Array[String],
+                      printer: Printer = RecursivePrinter,
+                      parserCtor: BufferedReader => Parser = out => new Parser(new Lexer(out)))
+  extends ProcessInterpreter(executable, args, printer, parserCtor) {
 
   printer.printCommand(SetOption(PrintSuccess(true)), in)
   in.write("\n")
-  in.flush
+  in.flush()
   parser.parseGenResponse
 
 }

src/main/scala/smtlib/interpreters/ProcessInterpreter.scala

@@ -10,17 +10,20 @@ import printer._
 
 import java.io._
 
-abstract class ProcessInterpreter(protected val process: Process, tailPrinter: Boolean) extends Interpreter {
+abstract class ProcessInterpreter private(override val printer: Printer,
+                                          override val parser: Parser,
+                                          protected val process: Process,
+                                          protected val in: BufferedWriter,
+                                          protected val out: BufferedReader) extends Interpreter {
 
-  def this(executable: String, args: Array[String], tailPrinter: Boolean = false) = {
-    this(java.lang.Runtime.getRuntime.exec((executable :: args.toList).mkString(" ")), tailPrinter)
-  }
-
-  lazy val in = new BufferedWriter(new OutputStreamWriter(process.getOutputStream))
-  lazy val out = new BufferedReader(new InputStreamReader(process.getInputStream))
+  private def this(printer: Printer, otherArgs: (Parser, Process, BufferedWriter, BufferedReader)) =
+    this(printer, otherArgs._1, otherArgs._2, otherArgs._3, otherArgs._4)
 
-  lazy val parser: Parser = new Parser(new Lexer(out))
-  lazy val printer: Printer = if (tailPrinter) TailPrinter else RecursivePrinter
+  def this(executable: String,
+           args: Array[String],
+           printer: Printer = RecursivePrinter,
+           parserCtor: BufferedReader => Parser = out => new Parser(new Lexer(out))) =
+    this(printer, ProcessInterpreter.ctorHelper(executable, args, parserCtor))
 
   def parseResponseOf(cmd: SExpr): SExpr = cmd match {
     case CheckSat() => parser.parseCheckSatResponse
@@ -98,17 +101,16 @@ abstract class ProcessInterpreter(protected val process: Process, tailPrinter: B
   override def interrupt(): Unit = synchronized {
     kill()
   }
+}
 
-  /*
-   * Manos, greatest hack:
-   * Process.destroyForcibly is only available on java8,
-   * Using the implicit conversion, if compiled with java7
-   * we will fallback to Process.destroy. If compiled on java8,
-   * it will ignore the implicit conversion as the method exists,
-   * and call the native Process.destroyForcibly.
-   */
-  private implicit class Java8Process(process: Process) {
-    def destroyForcibly() = process.destroy
+object ProcessInterpreter {
+  private def ctorHelper(executable: String,
+                         args: Array[String],
+                         parserCtor: BufferedReader => Parser): (Parser, Process, BufferedWriter, BufferedReader) = {
+    val process = java.lang.Runtime.getRuntime.exec((executable :: args.toList).mkString(" "))
+    val in = new BufferedWriter(new OutputStreamWriter(process.getOutputStream))
+    val out = new BufferedReader(new InputStreamReader(process.getInputStream))
+    val parser = parserCtor(out)
+    (parser, process, in, out)
   }
-
-}
+}

src/main/scala/smtlib/interpreters/Z3Interpreter.scala

@@ -2,14 +2,21 @@ package smtlib
 package interpreters
 
 import trees.Commands._
-import printer.RecursivePrinter
+import printer.{Printer, RecursivePrinter}
+import smtlib.lexer.Lexer
+import smtlib.parser.Parser
 
-class Z3Interpreter(executable: String, args: Array[String], tailPrinter: Boolean = false)
-  extends ProcessInterpreter(executable, args, tailPrinter) {
+import java.io.BufferedReader
+
+class Z3Interpreter(executable: String,
+                    args: Array[String],
+                    printer: Printer = RecursivePrinter,
+                    parserCtor: BufferedReader => Parser = out => new Parser(new Lexer(out)))
+  extends ProcessInterpreter(executable, args, printer, parserCtor) {
 
   printer.printCommand(SetOption(PrintSuccess(true)), in)
   in.write("\n")
-  in.flush
+  in.flush()
   parser.parseGenResponse
 
 }

src/test/scala/smtlib/parser/CommandsParserTests.scala

@@ -402,7 +402,7 @@ class CommandsParserTests extends AnyFunSuite with TimeLimits {
 
     {
       val declareSort = parseUniqueCmd("(declare-sort A 3)")
-    assert(parseUniqueCmd("(declare-sort A 3)") === DeclareSort("A", 3))
+      assert(parseUniqueCmd("(declare-sort A 3)") === DeclareSort("A", 3))
       val DeclareSort(a, n) = declareSort
       assert(declareSort.getPos === Position(1,1))
       assert(a.getPos === Position(1,15))