added yices2

vcanumalla · Nov 30, 2023 · cd7c074 · cd7c074
1 parent 01cf9f3
commit cd7c074
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 15 deletions.
diff --git a/test/all-rosette-tests.rkt b/test/all-rosette-tests.rkt
@@ -7,8 +7,8 @@
          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)
 
 
@@ -77,24 +77,27 @@
 
 
 (define (slow-tests)
-  ; (when (cvc4-available?)
-  ;   (printf "===== Running CVC4 tests =====\n")
-  ;   (run-tests-with-solver cvc4))
+  (when (cvc4-available?)
+    (printf "===== Running CVC4 tests =====\n")
+    (run-tests-with-solver cvc4))
 
-  ; (when (boolector-available?)
-  ;   (printf "===== Running Boolector tests =====\n")
-  ;   (run-tests-with-solver boolector))
+  (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 (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))
+  (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

diff --git a/test/base/bitvector.rkt b/test/base/bitvector.rkt
@@ -1,12 +1,15 @@
 #lang racket
 
 (require rackunit rackunit/text-ui racket/generator (rename-in rackunit [check-exn rackunit/check-exn])
-         rosette/solver/solution 
+         rosette/solver/solution
+        ;  (only-in rosette solver-features current-solver) "solver.rkt"
+        ;  rosette/solver/smt/yices-smt2
          rosette/lib/roseunit rosette/solver/smt/boolector
          racket/fixnum 
          rosette/base/core/term
          rosette/base/core/bool
          rosette/base/core/result
+        ;  rosette/solver/smt/server
          (except-in rosette/base/core/bitvector bv)
          (only-in rosette/base/core/bitvector [bv @bv])
          rosette/base/core/polymorphic rosette/base/core/merge 
@@ -26,7 +29,7 @@
 (define maxval+1 (expt 2 (sub1 (bitvector-size BV)))) 
 (define maxval (sub1 maxval+1))
 (define (bv v [t BV]) (@bv v t))
-
+; (output-smt "output-debug/")
 (define-syntax-rule (check-exn e ...)
   (begin
     (rackunit/check-exn e ...)