forked from emina/rosette
-
Notifications
You must be signed in to change notification settings - Fork 0
/
all-rosette-tests.rkt
105 lines (87 loc) · 2.5 KB
/
all-rosette-tests.rkt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
#lang racket
(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/cvc5
rosette/solver/smt/bitwuzla
rosette/solver/smt/stp
rosette/solver/smt/yices-smt2
"config.rkt")
(error-print-width default-error-print-width)
; Require all the modules with tests. No tests will actually run,
; because the modules have no (interesting) top level, but we need
; to clear-state! between each module.
(define-syntax-rule (require-all-tests path ...)
(run-all-tests path ...))
(require-all-tests
"base/type.rkt"
"base/term.rkt"
"base/bool.rkt"
"base/merge.rkt"
"base/store.rkt"
"base/vc.rkt"
"base/eval-guarded.rkt"
"base/list.rkt"
"base/vector.rkt"
"base/bvseq.rkt"
"base/forall.rkt"
"base/bitvector.rkt"
"base/bvlib.rkt"
"base/equality.rkt"
"base/uninterpreted.rkt"
"base/real.rkt"
"base/quantified.rkt"
"base/finitize.rkt"
"base/distinct.rkt"
"base/generics.rkt"
"base/push-pop.rkt"
"base/optimize-order.rkt"
"base/reflect.rkt"
"base/decode.rkt"
"query/solve.rkt"
"query/verify.rkt"
"query/synthesize.rkt"
"query/solve+.rkt"
"query/synthax.rkt"
"query/grammar.rkt"
"query/optimize.rkt"
"lib/destruct.rkt"
"profile/test.rkt"
"trace/test.rkt")
(define (run-tests-with-solver solver%)
(let ([slvr (solver%)])
(parameterize ([current-solver slvr][solver slvr])
(run-solver-specific-tests (solver-features slvr)))))
(define (fast-tests)
(printf "===== Running generic tests =====\n")
(run-generic-tests)
(printf "===== Running Z3 tests =====\n")
(run-tests-with-solver z3)
(check-all-tests-executed)
)
(module+ fast
(fast-tests))
(define (slow-tests)
(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 (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 (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
(fast-tests)
(slow-tests))