Bitwuzla

.github/workflows/scala-smtlib-CI.yml

@@ -16,6 +16,7 @@ jobs:
       Z3_VER: 4.15.1
       CVC4_VER: 1.8
       CVC5_VER: 1.2.1
+      BITWUZLA_VER: 0.8.2
     steps:
     - name: Checkout
       uses: actions/checkout@v4
@@ -31,11 +32,11 @@ jobs:
         ./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
+      run: ./scripts/install_solvers.sh $GITHUB_WORKSPACE/.local/bin $Z3_VER $CVC4_VER $CVC5_VER $BITWUZLA_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
+      run: cvc5 --version && z3 --version && cvc4 --version && bitwuzla --version
     - name: Run Tests
       run: sbt -Dtest-parallelism=10 -batch test
     - name: Run integration tests

.gitignore

@@ -10,4 +10,5 @@ target
 .bsp
 project/.bloop
 project/metals.sbt
-project/project
+project/project
+.DS_Store

scripts/install_solvers.sh

@@ -6,6 +6,7 @@ SOLVERS_DIR=${1:-"$(pwd)/solvers"}
 Z3_VER=${2:-"4.15.1"}
 CVC4_VER=${3:-"1.8"}
 CVC5_VER=${4:-"1.2.1"}
+BITWUZLA_VER=${5:-"0.8.2"}
 
 ARCH=$(uname -m)
 # short arch name as used by z3 builds
@@ -44,5 +45,14 @@ mv "$Z3_DIR/bin/z3" "$SOLVERS_DIR/z3"
 chmod +x "$SOLVERS_DIR/z3"
 rm -rf "$TEMP_DIR"
 
+# Bitwuzla
+mkdir -p "$TEMP_DIR"
+wget -c https://github.com/bitwuzla/bitwuzla/releases/download/${BITWUZLA_VER}/Bitwuzla-Linux-x86_64-static.zip -O "$TEMP_DIR/bitwuzla.zip" -q
+unzip "$TEMP_DIR/bitwuzla.zip" -d "$TEMP_DIR" 
+BITWUZLA_DIR=$(find "$TEMP_DIR" -mindepth 1 -maxdepth 1 -type d -name "*Bitwuzla*")
+mv "$BITWUZLA_DIR/bin/bitwuzla" "$SOLVERS_DIR/bitwuzla"
+chmod +x "$SOLVERS_DIR/bitwuzla"
+rm -rf "$TEMP_DIR"
+
 echo "************** Solvers Installed **************"
 exit 0

src/main/scala/smtlib/interpreters/BitwuzlaInterpreter.scala

@@ -0,0 +1,34 @@
+package smtlib
+package interpreters
+
+import smtlib.lexer.Lexer
+import smtlib.parser.Parser
+import smtlib.printer.{Printer, RecursivePrinter}
+import trees.Commands._
+
+import java.io.BufferedReader
+
+class BitwuzlaInterpreter(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()
+  parser.parseGenResponse
+
+}
+
+object BitwuzlaInterpreter {
+
+  def buildDefault: BitwuzlaInterpreter = {
+    val executable = "bitwuzla"
+    val args = Array("-v", "0",
+                     "--produce-models",
+                     "--lang", "smt2")
+    new BitwuzlaInterpreter(executable, args)
+  }
+
+}