Add support for STP and Yices2

.github/workflows/tests.yml

@@ -7,6 +7,8 @@ env:
   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"
+  STP_URL: "https://github.com/stp/stp/archive/0510509a85b6823278211891cbb274022340fa5c.tar.gz"
+  YICES2_URL: "https://github.com/SRI-CSL/yices2/archive/e27cf308cffb0ecc6cc7165c10e81ca65bc303b3.tar.gz"
 
 jobs:
   test:
@@ -57,7 +59,33 @@ jobs:
           ninja &&
           popd &&
           popd &&
-          cp bitwuzla/build/src/main/bitwuzla bin/ 
+          cp bitwuzla/build/src/main/bitwuzla bin/ &&
+          sudo apt-get install -y git cmake bison flex libboost-all-dev python2 perl &&
+          wget $STP_URL -nv -O stp.tar.gz &&
+          mkdir stp &&
+          tar xzf stp.tar.gz -C stp --strip-components=1 &&
+          pushd stp &&
+          ./scripts/deps/setup-gtest.sh &&
+          ./scripts/deps/setup-outputcheck.sh &&
+          ./scripts/deps/setup-cms.sh &&
+          ./scripts/deps/setup-minisat.sh &&
+          mkdir build &&
+          pushd build &&
+          cmake .. &&
+          cmake --build . &&
+          popd &&
+          popd &&
+          cp stp/build/stp bin/stp &&
+          sudo apt-get install -y gperf &&
+          wget $YICES2_URL -nv -O yices2.tar.gz &&
+          mkdir yices2 &&
+          tar xvf yices2.tar.gz -C yices2 --strip-components=1 &&
+          pushd yices2 &&
+          autoconf &&
+          ./configure &&
+          make &&
+          popd &&
+          cp yices2/build/x86_64-pc-linux-gnu-release/bin/yices_smt2 bin/yices_smt2
       - name: Install Rosette
         run: raco pkg install --auto --name rosette
       - name: Compile Rosette tests

rosette/solver/smt/stp.rkt

@@ -0,0 +1,69 @@
+#lang racket
+
+(require racket/runtime-path 
+         "server.rkt" "env.rkt" 
+         "../solver.rkt"
+         (prefix-in base/ "base-solver.rkt"))
+
+(provide (rename-out [make-stp stp]) stp? stp-available?)
+
+(define-runtime-path stp-path (build-path ".." ".." ".." "bin" "stp"))
+(define stp-opts '("--SMTLIB2"))
+
+(define (stp-available?)
+  (not (false? (base/find-solver "stp" stp-path #f))))
+
+(define (make-stp [solver #f] #:options [options (hash)] #:logic [logic #f] #:path [path #f])
+  (define config
+    (cond
+      [(stp? solver)
+       (base/solver-config solver)]
+      [else
+       (define real-stp-path (base/find-solver "stp" stp-path path))
+       (when (and (false? real-stp-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
+         (error 'stp "stp binary is not available (expected to be at ~a); try passing the #:path argument to (stp)" (path->string (simplify-path stp-path))))
+       (base/config options real-stp-path logic)]))
+  (stp (server (base/config-path config) stp-opts (base/make-send-options config)) config '() '() '() (env) '()))
+
+(struct stp base/solver ()
+  #:property prop:solver-constructor make-stp
+  #:methods gen:custom-write
+  [(define (write-proc self port mode) (fprintf port "#<stp>"))]
+  #: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)
+

rosette/solver/smt/yices-smt2.rkt

@@ -0,0 +1,69 @@
+#lang racket
+
+(require racket/runtime-path 
+         "server.rkt" "env.rkt" 
+         "../solver.rkt"
+         (prefix-in base/ "base-solver.rkt"))
+
+(provide (rename-out [make-yices-smt2 yices-smt2]) yices-smt2? yices-smt2-available?)
+
+(define-runtime-path yices-smt2-path (build-path ".." ".." ".." "bin" "yices-smt2"))
+(define yices-smt2-opts '("--incremental"))
+
+(define (yices-smt2-available?)
+  (not (false? (base/find-solver "yices-smt2" yices-smt2-path #f))))
+(define default-logic 'QF_BV) ;; YICES_2 needs a default logic set otherwise it will error
+(define (make-yices-smt2 [solver #f] #:options [options (hash)] #:logic [logic default-logic] #:path [path #f])
+  (define config
+    (cond
+      [(yices-smt2? solver)
+       (base/solver-config solver)]
+      [else
+       (define real-yices-smt2-path (base/find-solver "yices-smt2" yices-smt2-path path))
+       (when (and (false? real-yices-smt2-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
+         (error 'yices-smt2 "yices-smt2 binary is not available (expected to be at ~a); try passing the #:path argument to (yices-smt2)" (path->string (simplify-path yices-smt2-path))))
+       (base/config options real-yices-smt2-path logic)]))
+  (yices-smt2 (server (base/config-path config) yices-smt2-opts (base/make-send-options config)) config '() '() '() (env) '()))
+
+(struct yices-smt2 base/solver ()
+  #:property prop:solver-constructor make-yices-smt2
+  #:methods gen:custom-write
+  [(define (write-proc self port mode) (fprintf port "#<yices-smt2>"))]
+  #: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

@@ -6,6 +6,8 @@
          rosette/solver/smt/boolector 
          rosette/solver/smt/cvc5
          rosette/solver/smt/bitwuzla
+         rosette/solver/smt/stp
+         rosette/solver/smt/yices-smt2
          "config.rkt")
 
 (error-print-width default-error-print-width)
@@ -91,6 +93,14 @@
   (when (bitwuzla-available?)
     (printf "===== Running bitwuzla tests =====\n")
     (run-tests-with-solver bitwuzla))
+
+  (when (stp-available?)
+    (printf "===== Running stp tests =====\n")
+    (run-tests-with-solver stp))
+
+  (when (yices-smt2-available?)
+    (printf "===== Running yices-smt2 tests =====\n")
+    (run-tests-with-solver yices-smt2))
 )
 
 (module+ test