Bitwuzla (#16)

* add bitwuzla support

* add bitwuzla in the CI

* Update install solvers script to the one from Inox (+bitwuzla)

* Define bitwuzla test executors

* Filter tests for bitwuzla by compatibility

---------

Co-authored-by: Sankalp Gambhir <[email protected]>

Author: agilot

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

@@ -16,6 +16,8 @@ jobs:
       Z3_VER: 4.15.1
       CVC4_VER: 1.8
       CVC5_VER: 1.2.1
+      BITWUZLA_VER: 0.8.2
+      INSTALL_SOLVERS: 1
     steps:
     - name: Checkout
       uses: actions/checkout@v4
@@ -31,11 +33,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

@@ -1,48 +1,102 @@
 #!/usr/bin/env sh
 
+if [ "$INSTALL_SOLVERS" != "1" ]; then
+  echo "Skipping solver installation"
+  exit 0
+fi
+
+INFO_MSG="[INFO]"
+WARN_MSG="\033[33m[WARNING]\033[0m"
+ERROR_MSG="\033[1;31m[ERROR]\033[0m"
+
+# curl command with default flags
+CURL='curl -L -s -C -'
+
 TEMP_DIR="$(pwd)/temp"
 SOLVERS_DIR=${1:-"$(pwd)/solvers"}
 
+# check for set version or default to known working (for script) versions
 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
 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/;')
+Z3_LIBC_NAME=$(uname -s | tr '[:upper:]' '[:lower:]' | sed 's/darwin/osx/;s/linux/glibc/;')
+
+# os names as used by CVC5 builds
+CVC5_OS_NAME=$(uname -s | tr '[:upper:]' '[:lower:]' | sed 's/darwin/macOS/;s/linux/Linux/;')
 
 mkdir -p "$SOLVERS_DIR"
 mkdir -p "$TEMP_DIR"
+
+reset_temp_dir() {
+  rm -rf "$TEMP_DIR"
+  mkdir -p "$TEMP_DIR"
+}
+
+echo "$INFO_MSG Installing Solvers to $SOLVERS_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" 
+echo "$INFO_MSG Installing cvc5 (v${CVC5_VER})"
+
+$CURL "https://github.com/cvc5/cvc5/releases/download/cvc5-${CVC5_VER}/cvc5-${CVC5_OS_NAME}-${ARCH}-static.zip" --output "$TEMP_DIR/cvc5.zip"
+unzip -q "$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
+reset_temp_dir
+
+# CVC4
+echo "$INFO_MSG Installing CVC4 (v${CVC4_VER})"
+
+if [ "$CVC5_OS_NAME" = "macOS" ]; then
+  echo "$WARN_MSG CVC4 installation on macOS; defaulting to only build available (x86_64 v1.8)"
+  $CURL "https://github.com/CVC4/CVC4-archived/releases/download/1.8/cvc4-1.8-macos-opt" --output "$SOLVERS_DIR/cvc4"
+elif [ "$CVC5_OS_NAME" = "Linux" ]; then
+  $CURL "https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-${CVC4_VER}-x86_64-linux-opt" --output "$SOLVERS_DIR/cvc4"
+else
+  echo "$ERROR_MSG CVC4 installation not supported on unknown OS: $CVC5_OS_NAME"
+  exit 1
+fi
 chmod +x "$SOLVERS_DIR/cvc4"
 
+reset_temp_dir
+
 # z3
-mkdir -p "$TEMP_DIR"
-Z3_FILE_PREFIX="z3-${Z3_VER}-${SHORT_ARCH}-${LIBC_NAME}"
+echo "$INFO_MSG Installing Z3 (v${Z3_VER})"
+
+# z3 release file names contain libc versions in them, which makes them hard to
+# guess. Just get the correct one via the GitHub release API.
+Z3_FILE_PREFIX="z3-${Z3_VER}-${SHORT_ARCH}-${Z3_LIBC_NAME}" # followed by -<libcversion>.zip
 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
+  $CURL "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" 
+$CURL "${Z3_URL}" --output "$TEMP_DIR/z3.zip"
+unzip -q "$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
+# Bitwuzla
+echo "$INFO_MSG Installing Bitwuzla (v${BITWUZLA_VER})"
+
+mkdir -p "$TEMP_DIR"
+$CURL -L https://github.com/bitwuzla/bitwuzla/releases/download/${BITWUZLA_VER}/Bitwuzla-Linux-x86_64-static.zip --output "$TEMP_DIR/bitwuzla.zip"
+unzip -q "$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 "$INFO_MSG Solvers Installed"
+exit 0

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

@@ -12,6 +12,12 @@ import parser.Parser
 import lexer.Lexer
 import printer.RecursivePrinter
 import interpreters._
+import smtlib.trees.Commands.*
+import smtlib.trees.Terms.Term
+import smtlib.trees.Tree
+import smtlib.trees.TreesOps
+import smtlib.theories.FixedSizeBitVectors.BitVectorSort
+import smtlib.theories.FloatingPoint.FloatingPointSort
 
 /** Provide helper functions to test solver interfaces and files.
   *
@@ -43,6 +49,7 @@ trait TestHelpers {
   def getZ3Interpreter: Interpreter = Z3Interpreter.buildDefault
   def getCVC4Interpreter: Interpreter = CVC4Interpreter.buildDefault
   def getCVC5Interpreter: Interpreter = CVC5Interpreter.buildDefault
+  def getBitwuzlaInterpreter: Interpreter = BitwuzlaInterpreter.buildDefault
 
   def isZ3Available: Boolean = try {
     val _: String = "z3 -help".!!
@@ -67,6 +74,13 @@ trait TestHelpers {
     case _: Exception => false
   }
 
+  def isBitwuzlaAvailable: Boolean = try {
+    val _: String = "bitwuzla --version".!!
+    true
+  } catch {
+    case _: Exception => false
+  }
+
   def executeZ3(file: File)(f: (String) => Unit): Unit = {
     Seq("z3", "-smt2", file.getPath) ! ProcessLogger(f, s => ())
   }
@@ -79,5 +93,47 @@ trait TestHelpers {
     Seq("cvc5", "--lang", "smt", file.getPath) ! ProcessLogger(f, s => ())
   }
 
+  def executeBitwuzla(file: File)(f: (String) => Unit): Unit = {
+    Seq("bitwuzla", "-v", "0", "--lang", "--smt2", file.getPath) ! ProcessLogger(f, s => ())
+  }
+
+  ////////////////////////////////////////////////////////////////
+  // Solver specific helpers
+
+  /**
+  * Is test in the fragment supported by bitwuzla?
+  * 
+  * May not contain ints, reals, arrays, ADTs
+  *
+  */
+  def testIsBitwuzlaCompatible(cmds: Seq[Command], formula: Term): Boolean =
+    def isCompat(term: Term): Boolean =
+      def violatingTerm(term: Tree, children: Seq[Boolean]): Boolean = {
+        import smtlib.theories.*
+        term match
+          case FixedSizeBitVectors.BitVectorConstant(_, _) => false // internally contains IntNumeral, but in a valid place
+          case Ints.NumeralLit(_) => true
+          case Reals.DecimalLit(_) => true
+          case FixedSizeBitVectors.Int2BV(_, _) => true
+          case FixedSizeBitVectors.BV2Nat(_) => true
+          // this is enough to rule out the current problematic tests, 
+          // but may need refinement
+          case _ => children.contains(true)
+      }
+      !TreesOps.fold(violatingTerm)(term)
+    
+    def compatibleCommand(cmd: Command): Boolean =
+      cmd match
+        case DeclareFun(_, paramSorts, sort) => (sort +: paramSorts).forall {
+            case BitVectorSort(_) => true
+            case FloatingPointSort(_, _) => true
+            case _ => false
+        }
+        case DeclareSort(_, _) => false
+        case DeclareDatatypes(_) => false
+        case Assert(term) => isCompat(term)
+        case _ => true // may need refinement
+    cmds.forall(compatibleCommand) && (isCompat(formula))
+
 }
 

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

@@ -6,7 +6,6 @@ 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 {
 
@@ -57,6 +56,15 @@ class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
     } else {
       ignore(cvc5Test) {}
     }
+
+    val bitwuzlaTest = prefix + ": with Bitwuzla"
+    if (isBitwuzlaAvailable && testIsBitwuzlaCompatible(cmds, formula)) {
+      test(bitwuzlaTest) {
+        runAndCheck(getBitwuzlaInterpreter)
+      }
+    } else {
+      ignore(bitwuzlaTest) {}
+    }
   }
 
 
@@ -221,8 +229,8 @@ class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
     val f18 = Equals(Add(BitVectorConstant(1, 32), BitVectorConstant(2, 32), BitVectorConstant(3, 32), BitVectorConstant(4, 32)), BitVectorConstant(10, 32))
     mkTest(f18, SatStatus, uniqueName())
 
-    val f20 = Equals(Mul(BitVectorConstant(1, 32), BitVectorConstant(2, 32), BitVectorConstant(3, 32), BitVectorConstant(4, 32)), BitVectorConstant(24, 32))
-    mkTest(f20, SatStatus, uniqueName())
+    val f19 = Equals(Mul(BitVectorConstant(1, 32), BitVectorConstant(2, 32), BitVectorConstant(3, 32), BitVectorConstant(4, 32)), BitVectorConstant(24, 32))
+    mkTest(f19, SatStatus, uniqueName())
   }
 
   {

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)
+  }
+
+}