Support for cvc5 and upgrade to Scala 3.3

Author: mario-bucev

build.sbt

@@ -8,7 +8,7 @@ IntegrationTest / javaOptions ++= Seq("-Xss128M")
 
 IntegrationTest / fork := true
 
-libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.7" % "test;it"
+libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.15" % "test;it"
 
 
 IntegrationTest / logBuffered := false
@@ -18,8 +18,7 @@ Test / parallelExecution := true
 lazy val commonSettings = Seq(
   organization := "com.regblanc",
   name := "scala-smtlib",
-  scalaVersion := "2.13.6",
-  crossScalaVersions := Seq("3.0.2")
+  scalaVersion := "3.3.0",
 )
 
 lazy val root = (project in file(".")).

project/build.properties

@@ -1 +1 @@
-sbt.version=1.5.6
+sbt.version=1.7.3

src/it/scala/smtlib/it/SmtLibRunnerTests.scala

@@ -18,40 +18,70 @@ import interpreters._
   *
   * Compare the result of running command by command with an interpreter against
   * running the corresponding executable directly on the .smt2 files.
-  *
-  * TODO: proper way to display warning when not all tests are run because of not found executables.
   */
 class SmtLibRunnerTests extends AnyFunSuite with TestHelpers {
 
   filesInResourceDir("regression/smtlib/solving/all", _.endsWith(".smt2")).foreach(file => {
+    val z3Test = s"With Z3: SMTLIB benchmark ${file.getPath}"
     if(isZ3Available) {
-      test("With Z3: SMTLIB benchmark: " + file.getPath) {
+      test(z3Test) {
         compareWithInterpreter(executeZ3)(getZ3Interpreter, file)
       }
+    } else {
+      ignore(z3Test) {}
     }
+
+    val cvc4Test = s"With CVC4: SMTLIB benchmark ${file.getPath}"
     if(isCVC4Available) {
-      test("With CVC4: SMTLIB benchmark: " + file.getPath) {
+      test(cvc4Test) {
         compareWithInterpreter(executeCVC4)(getCVC4Interpreter, file)
       }
+    } else {
+      ignore(cvc4Test) {}
+    }
+
+    val cvc5Test = s"With cvc5: SMTLIB benchmark ${file.getPath}"
+    if (isCVC5Available) {
+      test(cvc5Test) {
+        compareWithInterpreter(executeCVC5)(getCVC5Interpreter, file)
+      }
+    } else {
+      ignore(cvc5Test) {}
     }
   })
 
-  if(isZ3Available) {
-    filesInResourceDir("regression/smtlib/solving/z3", _.endsWith(".smt2")).foreach(file => {
-      test("With Z3: SMTLIB benchmark: " + file.getPath) {
+  // Z3-specific
+  filesInResourceDir("regression/smtlib/solving/z3", _.endsWith(".smt2")).foreach(file => {
+    val z3Test = "With Z3: SMTLIB benchmark: " + file.getPath
+    if (isZ3Available) {
+      test(z3Test) {
         compareWithInterpreter(executeZ3)(getZ3Interpreter, file)
       }
-    })
-  }
+    } else {
+      ignore(z3Test) {}
+    }
+  })
 
-  if(isCVC4Available) {
-    filesInResourceDir("regression/smtlib/solving/cvc4", _.endsWith(".smt2")).foreach(file => {
-      test("With CVC4: SMTLIB benchmark: " + file.getPath) {
+  // CVC-specifc
+  filesInResourceDir("regression/smtlib/solving/cvc4", _.endsWith(".smt2")).foreach(file => {
+    val cvc4Test = "With CVC4: SMTLIB benchmark: " + file.getPath
+    if (isCVC4Available) {
+      test(cvc4Test) {
         compareWithWant(getCVC4Interpreter, file, new File(file.getPath + ".want"))
       }
-    })
-  }
+    } else {
+      ignore(cvc4Test) {}
+    }
 
+    val cvc5Test = "With cvc5: SMTLIB benchmark: " + file.getPath
+    if (isCVC5Available) {
+      test(cvc5Test) {
+        compareWithWant(getCVC5Interpreter, file, new File(file.getPath + ".want"))
+      }
+    } else {
+      ignore(cvc5Test) {}
+    }
+  })
 
   def compareWithInterpreter(executable: (File) => (String => Unit) => Unit)
                             (interpreter: Interpreter, file: File) = {
@@ -79,9 +109,5 @@ class SmtLibRunnerTests extends AnyFunSuite with TestHelpers {
       assert(expected.trim === res.replace('\n', ' ').trim)
     }
     assert(parser.parseCommand === null)
-    intercept[smtlib.parser.Parser.UnexpectedEOFException] {
-      // There shouldn't be anything left on the interpreter parser (the solver process).
-      interpreter.parser.parseSExpr
-    }
   }
 }

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

@@ -25,11 +25,11 @@ trait TestHelpers {
   private val all: String => Boolean = (s: String) => true
   private val resourceDirHard = "src/it/resources/"
 
-  def filesInResourceDir(dir : String, filter : String=>Boolean = all) : Iterable[File] = {    
+  def filesInResourceDir(dir : String, filter : String=>Boolean = all) : Iterable[File] = {
     val d = this.getClass.getClassLoader.getResource(dir)
 
     val asFile = if(d == null || d.getProtocol != "file") {
-      // We are in Eclipse. The only way we are saved is by hard-coding the path               
+      // We are in Eclipse. The only way we are saved is by hard-coding the path
       new File(resourceDirHard + dir)
     } else new File(d.toURI())
 
@@ -39,17 +39,18 @@ trait TestHelpers {
     else
       files.filter(f => filter(f.getPath()))
   }
-  
+
   def getZ3Interpreter: Interpreter = Z3Interpreter.buildDefault
   def getCVC4Interpreter: Interpreter = CVC4Interpreter.buildDefault
+  def getCVC5Interpreter: Interpreter = CVC5Interpreter.buildDefault
 
   def isZ3Available: Boolean = try {
     val _: String = "z3 -help".!!
     true
   } catch {
     case _: Exception => false
   }
-  
+
   def isCVC4Available: Boolean = try {
     // Make sure to pass a dummy option to cvc4, otherwise it starts in interactive mode (and does not exit)
     val _: String = "cvc4 --version".!!
@@ -58,6 +59,14 @@ trait TestHelpers {
     case _: Exception => false
   }
 
+  def isCVC5Available: Boolean = try {
+    // Ditto for cvc5
+    val _: String = "cvc5 --version".!!
+    true
+  } catch {
+    case _: Exception => false
+  }
+
   def executeZ3(file: File)(f: (String) => Unit): Unit = {
     Seq("z3", "-smt2", file.getPath) ! ProcessLogger(f, s => ())
   }
@@ -66,5 +75,9 @@ trait TestHelpers {
     Seq("cvc4", "--lang", "smt", file.getPath) ! ProcessLogger(f, s => ())
   }
 
+  def executeCVC5(file: File)(f: (String) => Unit): Unit = {
+    Seq("cvc5", "--lang", "smt", file.getPath) ! ProcessLogger(f, s => ())
+  }
+
 }
 

src/it/scala/smtlib/it/TheoriesBuilderTests.scala

@@ -1,52 +1,62 @@
 package smtlib
 package it
 
-import scala.sys.process._
-
 import org.scalatest.funsuite.AnyFunSuite
-
-import java.io.File
-import java.io.FileReader
-
-import interpreters._
-
-import trees.Terms._
-import trees.Commands._
-import trees.CommandsResponses._
+import smtlib.trees.Commands._
+import smtlib.trees.CommandsResponses._
+import smtlib.trees.Terms._
 
 
 /** Checks that formula build with theories module are correctly handled by solvers */
 class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
 
+  def mkTest(formula: Term, expectedStatus: Status, prefix: String): Unit = mkTest(Nil, formula, expectedStatus, prefix)
 
-  def mkTest(formula: Term, expectedStatus: Status, prefix: String) = {
-
-    if(isZ3Available) {
-      test(prefix + ": with Z3") {
-        val z3Interpreter = getZ3Interpreter
-        val assertion = Assert(formula)
-        assert(z3Interpreter.eval(assertion) === Success)
-        val res = z3Interpreter.eval(CheckSat())
+  def mkTest(cmds: List[Command], formula: Term, expectedStatus: Status, prefix: String): Unit = {
+    def runAndCheck(mkInterp: => Interpreter): Unit = {
+      val interp = mkInterp
+      for (cmd <- cmds) {
+        val res = interp.eval(cmd)
         res match {
-          case CheckSatStatus(status) => assert(status === expectedStatus)
-          case res => assert(false, "expected a check sat status, but got: " + res)
+          case Success => ()
+          case other => fail(s"expected a success, but got: $other")
         }
       }
+      val assertion = Assert(formula)
+      assert(interp.eval(assertion) === Success)
+      val res = interp.eval(CheckSat())
+      res match {
+        case CheckSatStatus(status) => assert(status === expectedStatus)
+        case other => fail(s"expected a check sat status, but got: $other")
+      }
     }
 
-    if(isCVC4Available) {
-      test(prefix + ": with CVC4") {
-        val cvc4Interpreter = getCVC4Interpreter
-        val assertion = Assert(formula)
-        assert(cvc4Interpreter.eval(assertion) === Success)
-        val res = cvc4Interpreter.eval(CheckSat())
-        res match {
-          case CheckSatStatus(status) => assert(status === expectedStatus)
-          case res => assert(false, "expected a check sat status, but got: " + res)
-        }
+    val z3Test = prefix + ": with Z3"
+    if (isZ3Available) {
+      test(z3Test) {
+        runAndCheck(getZ3Interpreter)
+      }
+    } else {
+      ignore(z3Test) {}
+    }
+
+    val cvc4Test = prefix + ": with CVC4"
+    if (isCVC4Available) {
+      test(cvc4Test) {
+        runAndCheck(getCVC4Interpreter)
       }
+    } else {
+      ignore(cvc4Test) {}
     }
 
+    val cvc5Test = prefix + ": with cvc5"
+    if (isCVC5Available) {
+      test(cvc5Test) {
+        runAndCheck(getCVC5Interpreter)
+      }
+    } else {
+      ignore(cvc5Test) {}
+    }
   }
 
 
@@ -146,8 +156,8 @@ class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
 
   {
     import theories.Core.Equals
-    import theories.Ints.NumeralLit
     import theories.FixedSizeBitVectors._
+    import theories.Ints.NumeralLit
     val theoryString = "Theory of Bit Vectors"
     var counter = 0
     def uniqueName(): String = {
@@ -214,4 +224,69 @@ class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
     val f20 = Equals(Mul(BitVectorConstant(1, 32), BitVectorConstant(2, 32), BitVectorConstant(3, 32), BitVectorConstant(4, 32)), BitVectorConstant(24, 32))
     mkTest(f20, SatStatus, uniqueName())
   }
+
+  {
+    import theories.Core._
+    import theories.Ints._
+    val theoryADTs = "Theory of ADTs"
+    var counter = 0
+
+    def uniqueName(): String = {
+      counter += 1
+      "%d - %s".format(counter, theoryADTs)
+    }
+
+    val list = SSymbol("MyList")
+    val listSort = Sort(Identifier(list))
+    val nil = SSymbol("Nil")
+    val cons = SSymbol("Cons")
+    val head = SSymbol("head")
+    val tail = SSymbol("tail")
+    val listCtors = List(
+      Constructor(nil, Seq.empty),
+      Constructor(cons, Seq((head, IntSort()), (tail, listSort)))
+    )
+
+    def consApp(hd: Term, tl: Term): Term =
+      FunctionApplication(
+        QualifiedIdentifier(Identifier(cons), Some(listSort)),
+        Seq(hd, tl)
+      )
+
+    def nilApp: Term =
+      QualifiedIdentifier(Identifier(nil), Some(listSort))
+
+    val x = QualifiedIdentifier(Identifier(SSymbol("x")), Some(IntSort()))
+    val y = QualifiedIdentifier(Identifier(SSymbol("y")), Some(IntSort()))
+    val z = QualifiedIdentifier(Identifier(SSymbol("z")), Some(listSort))
+    val a = QualifiedIdentifier(Identifier(SSymbol("a")), Some(IntSort()))
+    val b = QualifiedIdentifier(Identifier(SSymbol("b")), Some(IntSort()))
+    val c = QualifiedIdentifier(Identifier(SSymbol("c")), Some(IntSort()))
+
+    val ids = Seq(x, y, z, a, b, c)
+    val idsDecls = ids.map(id => DeclareFun(id.id.symbol, Seq.empty, id.sort.get))
+
+    mkTest(
+      List(DeclareDatatypes(List((list, listCtors)))) ++ idsDecls,
+      Equals(
+        consApp(x, consApp(y, z)),
+        consApp(a, consApp(b, consApp(c, nilApp)))
+      ),
+      SatStatus,
+      uniqueName()
+    )
+
+    mkTest(
+      List(DeclareDatatypes(List((list, listCtors)))) ++ idsDecls,
+      And(
+        Equals(
+          consApp(x, consApp(y, z)),
+          consApp(a, consApp(b, consApp(c, nilApp)))
+        ),
+        Not(Equals(z, consApp(c, nilApp)))
+      ),
+      UnsatStatus,
+      uniqueName()
+    )
+  }
 }

src/main/scala/smtlib/Interpreter.scala

@@ -40,29 +40,25 @@ object Interpreter {
   import java.io.BufferedReader
   import java.io.File
 
-  def execute(script: Script)(implicit interpreter: Interpreter): Unit = {
+  def execute(script: Script)(using interpreter: Interpreter): Unit = {
     for(cmd <- script.commands)
       interpreter.eval(cmd)
   }
 
-  def execute(scriptReader: Reader)(implicit interpreter: Interpreter): Unit = {
-    val parser = new Parser(new lexer.Lexer(scriptReader))
-    val cmd: Command = null
-    do {
-      val cmd = parser.parseCommand
-      if(cmd != null)
-        interpreter.eval(cmd)
-    } while(cmd != null)
-  }
+  def execute(scriptReader: Reader)(using Interpreter): Unit =
+    execute(new Parser(new lexer.Lexer(scriptReader)))
 
-  def execute(file: File)(implicit interpreter: Interpreter): Unit = {
-    val parser = new Parser(new lexer.Lexer(new BufferedReader(new FileReader(file))))
-    var cmd: Command = null
-    do {
-      cmd = parser.parseCommand
+  def execute(file: File)(using Interpreter): Unit =
+    execute(new Parser(new lexer.Lexer(new BufferedReader(new FileReader(file)))))
+
+  private def execute(parser: Parser)(using interpreter: Interpreter): Unit = {
+    // do-while, Scala 3 style
+    // See https://docs.scala-lang.org/scala3/reference/dropped-features/do-while.html
+    while ({
+      val cmd = parser.parseCommand
       if(cmd != null)
         interpreter.eval(cmd)
-    } while(cmd != null)
+      cmd != null
+    }) () // This trailing () is important! If we remove it, it messes with the next statement
   }
-
 }