Add support for Bitwuzla and CVC5

.github/workflows/tests.yml

@@ -5,6 +5,8 @@ on: [push, pull_request]
 env:
   CVC4_URL: "http://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/cvc4-1.8-x86_64-linux-opt"
   BOOLECTOR_URL: "https://github.com/Boolector/boolector/archive/3.2.1.tar.gz"
+  CVC5_URL: "https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.7/cvc5-Linux"
+  BITWUZLA_URL: "https://github.com/bitwuzla/bitwuzla/archive/93a3d930f622b4cef0063215e63b7c3bd10bd663.tar.gz"
 
 jobs:
   test:
@@ -40,7 +42,22 @@ jobs:
           make &&
           popd &&
           cp boolector/build/bin/boolector bin/ &&
-          rm -rf boolector*
+          rm -rf boolector* &&
+          wget $CVC5_URL -nv -O bin/cvc5 &&
+          chmod +x bin/cvc5 &&
+          sudo apt-get update &&
+          sudo apt-get install -y ninja-build &&
+          pip3 install meson &&
+          wget $BITWUZLA_URL -nv -O bitwuzla.tar.gz &&
+          mkdir bitwuzla &&
+          tar xzf bitwuzla.tar.gz -C bitwuzla --strip-components=1 &&
+          pushd bitwuzla &&
+          ./configure.py &&
+          pushd build &&
+          ninja &&
+          popd &&
+          popd &&
+          cp bitwuzla/build/src/main/bitwuzla bin/ 
       - name: Install Rosette
         run: raco pkg install --auto --name rosette
       - name: Compile Rosette tests

rosette/solver/smt/bitwuzla.rkt

@@ -0,0 +1,106 @@
+;;; Requires Bitwuzla 0.1.0 or later.
+#lang racket
+
+(require racket/runtime-path 
+         "server.rkt" "cmd.rkt" "env.rkt" 
+         "../solver.rkt" "../solution.rkt"
+         (prefix-in base/ "base-solver.rkt")
+         (only-in "../../base/core/term.rkt" term term? term-type constant? expression constant with-terms)
+         (only-in "../../base/core/bool.rkt" @boolean? @forall @exists)
+         (only-in "../../base/core/bitvector.rkt" bitvector bitvector? bv? bv bv-value @extract @sign-extend @zero-extend @bveq)
+         (only-in "../../base/core/function.rkt" function-domain function-range function? function fv)
+         (only-in "../../base/core/type.rkt" type-of)
+         (only-in "../../base/form/control.rkt" @if))
+
+(provide (rename-out [make-bitwuzla bitwuzla]) bitwuzla? bitwuzla-available?)
+
+(define-runtime-path bitwuzla-path (build-path ".." ".." ".." "bin" "bitwuzla"))
+(define bitwuzla-opts '("-m"))
+
+(define (bitwuzla-available?)
+  (not (false? (base/find-solver "bitwuzla" bitwuzla-path #f))))
+
+(define (make-bitwuzla [solver #f] #:options [options (hash)] #:logic [logic #f] #:path [path #f])
+  (define config
+    (cond
+      [(bitwuzla? solver)
+       (base/solver-config solver)]
+      [else
+       (define real-bitwuzla-path (base/find-solver "bitwuzla" bitwuzla-path path))
+       (when (and (false? real-bitwuzla-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
+         (error 'bitwuzla "bitwuzla binary is not available (expected to be at ~a); try passing the #:path argument to (bitwuzla)" (path->string (simplify-path bitwuzla-path))))
+       (base/config options real-bitwuzla-path logic)]))
+  (bitwuzla (server (base/config-path config) bitwuzla-opts (base/make-send-options config)) config '() '() '() (env) '()))
+
+(struct bitwuzla base/solver ()
+  #:property prop:solver-constructor make-bitwuzla
+  #:methods gen:custom-write
+  [(define (write-proc self port mode) (fprintf port "#<bitwuzla>"))]
+  #:methods gen:solver
+  [
+   (define (solver-features self)
+     '(qf_bv))
+
+   (define (solver-options self)
+     (base/solver-options self))
+
+   (define (solver-assert self bools)
+     (base/solver-assert self bools bitwuzla-wfcheck))
+
+   (define (solver-minimize self nums)
+     (base/solver-minimize self nums))
+
+   (define (solver-maximize self nums)
+     (base/solver-maximize self nums))
+
+   (define (solver-clear self)
+     (base/solver-clear self))
+
+   (define (solver-shutdown self)
+     (base/solver-shutdown self))
+
+   (define (solver-push self)
+     (base/solver-push self))
+
+   (define (solver-pop self [k 1])
+     (base/solver-pop self k))
+
+   (define (solver-check self [read-solution base/read-solution])
+     (base/solver-check self read-solution))
+
+   (define (solver-debug self)
+     (base/solver-debug self))])
+
+(define (set-default-options server)
+  void)
+
+
+(define (valid-type? t)
+    (or (equal? t @boolean?)
+        (bitvector? t)
+        (and (function? t)
+             (for/and ([d (in-list (function-domain t))]) (valid-type? d))
+             (valid-type? (function-range t)))))
+; Check whether a term v is well-formed for bitwuzla -- it must not mention
+; types other than bitvectors, booleans, and uninterpreted functions over those
+; types. If not, raise an exception.
+(define (bitwuzla-wfcheck v [cache (mutable-set)])
+  (unless (set-member? cache v)
+    (set-add! cache v)
+    (cond
+      [(term? v)
+       (unless (valid-type? (type-of v))
+         (error 'bitwuzla "bitwuzla does not support values of type ~v (value: ~v)" (type-of v) v))
+       (match v
+         [(expression (or (== @forall) (== @exists)) vars body)
+          (error 'bitwuzla "bitwuzla does not support quantified formulas (value: ~v)" v)]
+         [(expression (== @extract) i j e)
+          (bitwuzla-wfcheck e cache)]
+         [(expression (or (== @sign-extend) (== @zero-extend)) v t)
+          (bitwuzla-wfcheck v cache)]
+         [(expression op es ...)
+          (for ([e es]) (bitwuzla-wfcheck e cache))]
+         [_ #t])]
+      [else
+       (unless (or (boolean? v) (bv? v))
+         (error 'bitwuzla "bitwuzla does not support value (expected boolean? or bv?): ~v" v))])))

rosette/solver/smt/cvc5.rkt

@@ -0,0 +1,68 @@
+#lang racket
+
+(require racket/runtime-path 
+         "server.rkt" "env.rkt" 
+         "../solver.rkt"
+         (prefix-in base/ "base-solver.rkt"))
+
+(provide (rename-out [make-cvc5 cvc5]) cvc5? cvc5-available?)
+
+(define-runtime-path cvc5-path (build-path ".." ".." ".." "bin" "cvc5"))
+(define cvc5-opts '("-L" "smt2" "-q" "-m" "-i" "--bv-print-consts-as-indexed-symbols"))
+
+(define (cvc5-available?)
+  (not (false? (base/find-solver "cvc5" cvc5-path #f))))
+
+(define (make-cvc5 [solver #f] #:options [options (hash)] #:logic [logic #f] #:path [path #f])
+  (define config
+    (cond
+      [(cvc5? solver)
+       (base/solver-config solver)]
+      [else
+       (define real-cvc5-path (base/find-solver "cvc5" cvc5-path path))
+       (when (and (false? real-cvc5-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
+         (error 'cvc5 "cvc5 binary is not available (expected to be at ~a); try passing the #:path argument to (cvc5)" (path->string (simplify-path cvc5-path))))
+       (base/config options real-cvc5-path logic)]))
+  (cvc5 (server (base/config-path config) cvc5-opts (base/make-send-options config)) config '() '() '() (env) '()))
+
+(struct cvc5 base/solver ()
+  #:property prop:solver-constructor make-cvc5
+  #:methods gen:custom-write
+  [(define (write-proc self port mode) (fprintf port "#<cvc5>"))]
+  #:methods gen:solver
+  [
+   (define (solver-features self)
+     '(qf_bv))
+
+   (define (solver-options self)
+     (base/solver-options self))
+
+   (define (solver-assert self bools)
+     (base/solver-assert self bools))
+
+   (define (solver-minimize self nums)
+     (base/solver-minimize self nums))
+
+   (define (solver-maximize self nums)
+     (base/solver-maximize self nums))
+
+   (define (solver-clear self)
+     (base/solver-clear self))
+
+   (define (solver-shutdown self)
+     (base/solver-shutdown self))
+
+   (define (solver-push self)
+     (base/solver-push self))
+
+   (define (solver-pop self [k 1])
+     (base/solver-pop self k))
+
+   (define (solver-check self)
+     (base/solver-check self))
+
+   (define (solver-debug self)
+     (base/solver-debug self))])
+
+(define (set-default-options server)
+  void)

test/all-rosette-tests.rkt

@@ -4,6 +4,8 @@
          rosette/lib/roseunit
          rosette/solver/smt/z3 rosette/solver/smt/cvc4 
          rosette/solver/smt/boolector 
+         rosette/solver/smt/cvc5
+         rosette/solver/smt/bitwuzla
          "config.rkt")
 
 (error-print-width default-error-print-width)
@@ -80,6 +82,14 @@
   (when (boolector-available?)
     (printf "===== Running Boolector tests =====\n")
     (run-tests-with-solver boolector))
+
+  (when (cvc5-available?)
+    (printf "===== Running cvc5 tests =====\n")
+    (run-tests-with-solver cvc5))
+
+  (when (bitwuzla-available?)
+    (printf "===== Running bitwuzla tests =====\n")
+    (run-tests-with-solver bitwuzla))
 )
 
 (module+ test