Drop outdated support for Yices (emina#189).

REA1 · Apr 16, 2021 · 9f6322c · 9f6322c
1 parent 3432d95
commit 9f6322c
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 186 deletions.
diff --git a/rosette/guide/scribble/datatypes/solvers+solutions.scrbl b/rosette/guide/scribble/datatypes/solvers+solutions.scrbl
@@ -3,7 +3,7 @@
 @(require (for-label 
            rosette/solver/solver rosette/solver/solution 
            rosette/solver/smt/z3 rosette/solver/smt/cvc4
-           rosette/solver/smt/boolector rosette/solver/smt/yices 
+           rosette/solver/smt/boolector 
            rosette/base/form/define rosette/query/query 
            rosette/base/core/term (only-in rosette/base/base bv?)
            (only-in rosette/base/base assert) 
@@ -21,7 +21,6 @@
                    rosette/solver/solution
                    rosette/solver/smt/z3
                    rosette/solver/smt/cvc4
-                   rosette/solver/smt/yices
                    rosette/solver/smt/boolector
                    #:use-sources 
                    (rosette/query/finitize
@@ -30,7 +29,6 @@
                     rosette/solver/solution
                     rosette/solver/smt/z3
                     rosette/solver/smt/cvc4
-                    rosette/solver/smt/yices
                     rosette/solver/smt/boolector)]
 
 A @deftech{solver} is an automatic reasoning engine, used to answer 
@@ -281,37 +279,6 @@ 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{Yices}
-
-@defmodule[rosette/solver/smt/yices #:no-declare]
-
-@defproc*[([(yices [#:path path (or/c path-string? #f) #f]
-                   [#:logic logic symbol? 'ALL]
-                   [#:options options (hash/c symbol? any/c) (hash)]) solver?]
-           [(yices? [v any/c]) boolean?])]{
-
-Returns a @racket[solver?] wrapper for the @hyperlink["http://yices.csl.sri.com/"]{Yices} solver from SRI.
-
-To use this solver, download and install Yices (version 2.6.0 or later),
-and either add the @tt{yices-smt2} executable to your @tt{PATH}
-or pass the path to the executable as the optional @racket[path] argument.
-
-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['ALL].
-
-The @racket[options] argument provides additional options that are sent to Yices
-via the @tt{set-option} SMT command.
-For example, setting @racket[options] to @racket[(hash ':random-seed 5)]
-will send the command @tt{(set-option :random-seed 5)} to Yices prior to solving.
-}
-
-@defproc[(yices-available?) boolean?]{
-Returns true if the Yices 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?]),

diff --git a/rosette/solver/smt/yices.rkt b/rosette/solver/smt/yices.rkt
diff --git a/test/all-rosette-tests.rkt b/test/all-rosette-tests.rkt
@@ -3,7 +3,7 @@
 (require (only-in rosette solver-features current-solver) "base/solver.rkt"
          rosette/lib/roseunit
          rosette/solver/smt/z3 rosette/solver/smt/cvc4 
-         rosette/solver/smt/boolector rosette/solver/smt/yices
+         rosette/solver/smt/boolector 
          "config.rkt")
 
 (error-print-width default-error-print-width)
@@ -80,10 +80,6 @@
   (when (boolector-available?)
     (printf "===== Running Boolector tests =====\n")
     (run-tests-with-solver boolector))
-
-  (when (yices-available?)
-    (printf "===== Running Yices tests =====\n")
-    (run-tests-with-solver yices))
 )
 
 (module+ test