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,34 @@ 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 --prefix=$PWD/out/ &&
+          make &&
+          make install &&
+          popd &&
+          cp yices2/out/bin/yices-smt2 bin/yices-smt2
       - name: Install Rosette
         run: raco pkg install --auto --name rosette
       - name: Compile Rosette tests

rosette/guide/scribble/datatypes/solvers+solutions.scrbl

@@ -4,6 +4,10 @@
            rosette/solver/solver rosette/solver/solution 
            rosette/solver/smt/z3 rosette/solver/smt/cvc4
            rosette/solver/smt/boolector 
+           rosette/solver/smt/bitwuzla
+           rosette/solver/smt/cvc5
+           rosette/solver/smt/stp
+           rosette/solver/smt/yices
            rosette/base/form/define rosette/query/query 
            rosette/base/core/term (only-in rosette/base/base bv?)
            (only-in rosette/base/base assert) 
@@ -22,14 +26,22 @@
                    rosette/solver/smt/z3
                    rosette/solver/smt/cvc4
                    rosette/solver/smt/boolector
+                   rosette/solver/smt/bitwuzla
+                   rosette/solver/smt/cvc5
+                   rosette/solver/smt/stp
+                   rosette/solver/smt/yices
                    #:use-sources 
                    (rosette/query/finitize
                     rosette/query/query
                     rosette/solver/solver
                     rosette/solver/solution
                     rosette/solver/smt/z3
                     rosette/solver/smt/cvc4
-                    rosette/solver/smt/boolector)]
+                    rosette/solver/smt/boolector
+                    rosette/solver/smt/bitwuzla
+                    rosette/solver/smt/cvc5
+                    rosette/solver/smt/stp
+                    rosette/solver/smt/yices)]
 
 A @deftech{solver} is an automatic reasoning engine, used to answer 
 @seclink["sec:queries"]{queries} about Rosette programs.  The result of
@@ -279,6 +291,146 @@ Returns true if the Boolector solver is available for use (i.e., Rosette can loc
 If this returns @racket[#f], @racket[(boolector)] will not succeed
 without its optional @racket[path] argument.}
 
+@subsection{Bitwuzla}
+
+@defmodule[rosette/solver/smt/bitwuzla #:no-declare]
+
+@defproc*[([(bitwuzla [#:path path (or/c path-string? #f) #f]
+                      [#:logic logic (or/c symbol? #f) #f]
+                      [#:options options (hash/c symbol? any/c) (hash)]) solver?]
+           [(bitwuzla? [v any/c]) boolean?])]{
+
+Returns a @racket[solver?] wrapper for the @hyperlink["https://bitwuzla.github.io/"]{Bitwuzla} solver.
+
+To use this solver, download prebuilt Bitwuzla or build it yourself,
+and ensure the executable is on your @tt{PATH} or pass the path to the 
+executable as the optional @racket[path] argument.
+Rosette currently tests Bitwuzla at commit 
+@tt{93a3d930f622b4cef0063215e63b7c3bd10bd663}.
+
+The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
+Specifying a logic can improve solving performance, but Rosette makes no effort to check that
+emitted constraints fall within the chosen logic. The default is @racket[#f],
+which uses Bitwuzla's default logic.
+
+The @racket[options] argument provides additional options that are sent to Bitwuzla
+via the @tt{set-option} SMT command.
+For example, setting @racket[options] to @racket[(hash ':seed 5)]
+will send the command @tt{(set-option :seed 5)} to Bitwuzla prior to solving.
+}
+
+@defproc[(bitwuzla-available?) boolean?]{
+Returns true if the Bitwuzla solver is available for use (i.e., Rosette can locate a @tt{bitwuzla} binary).
+If this returns @racket[#f], @racket[(bitwuzla)] will not succeed
+without its optional @racket[path] argument.}
+
+@subsection{CVC5}
+
+@defmodule[rosette/solver/smt/cvc5 #:no-declare]
+
+@defproc*[([(cvc5 [#:path path (or/c path-string? #f) #f]
+                  [#:logic logic (or/c symbol? #f) #f]
+                  [#:options options (hash/c symbol? any/c) (hash)]) solver?]
+           [(cvc5? [v any/c]) boolean?])]{
+
+Returns a @racket[solver?] wrapper for the @hyperlink["https://cvc5.github.io/"]{CVC5} solver.
+
+To use this solver, download prebuilt CVC5 or build it yourself,
+and ensure the executable is on your @tt{PATH} or pass the path to the 
+executable as the optional @racket[path] argument.
+Rosette currently tests CVC5 at version 1.0.7.
+
+The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
+Specifying a logic can improve solving performance, but Rosette makes no effort to check that
+emitted constraints fall within the chosen logic. The default is @racket[#f],
+which uses CVC5's default logic.
+
+The @racket[options] argument provides additional options that are sent to CVC5
+via the @tt{set-option} SMT command.
+For example, setting @racket[options] to @racket[(hash ':seed 5)]
+will send the command @tt{(set-option :seed 5)} to CVC5 prior to solving.
+}
+
+@defproc[(cvc5-available?) boolean?]{
+Returns true if the CVC5 solver is available for use (i.e., Rosette can locate a @tt{cvc5} binary).
+If this returns @racket[#f], @racket[(cvc5)] will not succeed
+without its optional @racket[path] argument.}
+
+@subsection{STP}
+
+@defmodule[rosette/solver/smt/stp #:no-declare]
+
+@defproc*[([(stp [#:path path (or/c path-string? #f) #f]
+                 [#:logic logic (or/c symbol? #f) #f]
+                 [#:options options (hash/c symbol? any/c) (hash)]) solver?]
+           [(stp? [v any/c]) boolean?])]{
+
+Returns a @racket[solver?] wrapper for the @hyperlink["https://stp.github.io/"]{STP} solver.
+
+To use this solver, download prebuilt STP or build it yourself,
+and ensure the executable is on your @tt{PATH} or pass the path to the 
+executable as the optional @racket[path] argument.
+Rosette currently tests STP at commit 
+@tt{0510509a85b6823278211891cbb274022340fa5c}.
+Note that as of December 2023, the STP version on Mac Homebrew is too old to be
+supported by Rosette.
+
+The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
+Specifying a logic can improve solving performance, but Rosette makes no effort to check that
+emitted constraints fall within the chosen logic. The default is @racket[#f],
+which uses STP's default logic.
+
+The @racket[options] argument provides additional options that are sent to STP
+via the @tt{set-option} SMT command.
+For example, setting @racket[options] to @racket[(hash ':seed 5)]
+will send the command @tt{(set-option :seed 5)} to STP prior to solving.
+}
+
+@defproc[(stp-available?) boolean?]{
+Returns true if the STP solver is available for use (i.e., Rosette can locate a @tt{stp} binary).
+If this returns @racket[#f], @racket[(stp)] will not succeed
+without its optional @racket[path] argument.}
+
+@subsection{Yices2}
+
+@defmodule[rosette/solver/smt/yices #:no-declare]
+
+@defproc*[([(yices [#:path path (or/c path-string? #f) #f]
+                   [#:logic logic (or/c symbol? #f) 'QF_BV]
+                   [#:options options (hash/c symbol? any/c) (hash)]) solver?]
+           [(yices? [v any/c]) boolean?])]{
+
+Returns a @racket[solver?] wrapper for the @hyperlink["https://yices.csl.sri.com/"]{Yices2} solver.
+
+To use this solver, download prebuilt Yices2 or build it yourself,
+and ensure the executable is on your @tt{PATH} or pass the path to the 
+executable as the optional @racket[path] argument.
+Rosette specifically uses the @tt{yices-smt2} executable, which is the Yices2
+solver with its SMTLIB2 frontend enabled.
+Note that just building (without installing) Yices2 will produce an executable
+named @tt{yices_smt2}. Running the installation step produces an executable
+with the correct name. However, it is safe to skip the installation step and
+simply rename or symlink the @tt{yices_smt2} executable to @tt{yices-smt2}.
+Rosette currently tests Yices2 at commit 
+@tt{e27cf308cffb0ecc6cc7165c10e81ca65bc303b3}.
+
+The optional @racket[logic] argument specifies an SMT logic for the solver to use (e.g., @racket['QF_BV]).
+Specifying a logic can improve solving performance, but Rosette makes no effort to check that
+emitted constraints fall within the chosen logic. Yices2 expects a logic to be
+set; Rosette defaults to @racket['QF_BV].
+
+The @racket[options] argument provides additional options that are sent to Yices2
+via the @tt{set-option} SMT command.
+For example, setting @racket[options] to @racket[(hash ':seed 5)]
+will send the command @tt{(set-option :seed 5)} to Yices2 prior to solving.
+}
+
+@defproc[(yices-available?) boolean?]{
+Returns true if the Yices2 solver is available for use (i.e., Rosette can locate a @tt{yices-smt2} binary).
+If this returns @racket[#f], @racket[(yices)] will not succeed
+without its optional @racket[path] argument.}
+
+
 @section{Solutions}
 
 A solution to a set of formulas may be satisfiable (@racket[sat?]), unsatisfiable  (@racket[unsat?]),

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.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 yices]) yices? yices-available?)
+
+(define-runtime-path yices-path (build-path ".." ".." ".." "bin" "yices-smt2"))
+(define yices-opts '("--incremental"))
+
+(define (yices-available?)
+  (not (false? (base/find-solver "yices-smt2" yices-path #f))))
+(define default-logic 'QF_BV) ;; Yices2 needs a default logic set otherwise it will error
+(define (make-yices [solver #f] #:options [options (hash)] #:logic [logic default-logic] #:path [path #f])
+  (define config
+    (cond
+      [(yices? solver)
+       (base/solver-config solver)]
+      [else
+       (define real-yices-path (base/find-solver "yices-smt2" yices-path path))
+       (when (and (false? real-yices-path) (not (getenv "PLT_PKG_BUILD_SERVICE")))
+         (error 'yices "yices-smt2 binary is not available (expected to be at ~a); try passing the #:path argument to (yices)" (path->string (simplify-path yices-path))))
+       (base/config options real-yices-path logic)]))
+  (yices (server (base/config-path config) yices-opts (base/make-send-options config)) config '() '() '() (env) '()))
+
+(struct yices base/solver ()
+  #:property prop:solver-constructor make-yices
+  #:methods gen:custom-write
+  [(define (write-proc self port mode) (fprintf port "#<yices>"))]
+  #: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
          "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-available?)
+    (printf "===== Running Yices2 tests =====\n")
+    (run-tests-with-solver yices))
 )
 
 (module+ test