adjust redex-check's default strategy to ensure that it always uses the

random generator, at least some of the time

Author: rfindler

redex-doc/redex/scribblings/ref/testing.scrbl

@@ -606,11 +606,10 @@ using the @racket[match-bindings] produced by @racket[match]ing
 how @math{t} is generated:
 @itemlist[@item{@racket[language @#,ttpattern]:
                  In this case, @racket[redex-check] uses an ad hoc strategy for 
-                 generating @racket[_pattern]. For the first 10 seconds, it uses 
-                 in-order enumeration to pick terms. After that, it
-                 alternates back and forth between in-order enumeration
-                 and the ad hoc random generator. After the 10 minute mark,
-                 it switches over to using just the ad hoc random generator.}
+                 generating @racket[_pattern]. For the first half of the attempts
+                 (or only 500 if there are more than 1000 attempts) it uses
+                 in-order enumeration to pick terms. After that,
+                 it switches over to using the ad hoc random generator.}
           @item{@racket[language @#,ttpattern #:ad-hoc]:
                  In this case, @racket[redex-check] uses an ad hoc random generator
                  to generate terms that match @racket[_pattern].}

redex-lib/redex/HISTORY.txt

@@ -1,3 +1,11 @@
+v8.18
+
+  * changed redex-check's default generation strategy so that it
+    always uses random generation. Specifically, spends half of its
+    attempts on the enumerator and half on random generation when the
+    total number of attempts is 1000 or less. Otherwise it caps the
+    enumerator to 500 attempts.
+
 v8.17
 
   * render-judgment-form and judgment-form->pict are functions, making

redex-lib/redex/private/generate-term.rkt

@@ -307,11 +307,11 @@
                        keep-going?)]
                    [else
                     #`(check-one
-                       (default-generator #,lang `pattern)
+                       (default-generator #,lang `pattern att)
                        property att ret (and print? show) (or fix (λ (x) x)) term-match
                        keep-going?)])])))))))
 
-(define (default-generator lang pat)
+(define (default-generator lang pat total-attempts)
   (define ad-hoc-generator ((compile lang 'redex-check) pat))
   (define enum (pat-enumerator (compiled-lang-enum-table lang)
                                pat
@@ -323,12 +323,7 @@
      (define in-bounds (if (finite-enum? enum)
                            (λ (x) (modulo x (enum-count enum)))
                            (λ (x) x)))
-     (define start-time (current-inexact-milliseconds))
-     (define interleave-start-attempt #f)
-     (define interleave-time (+ start-time (* 1000 10))) ;; 10 seconds later
-     (define pure-random-start-attempt #f)
-     (define pure-random-time (+ start-time (* 1000 60 10))) ;; 10 minutes later
-     
+     (define random-start (min 500 (ceiling (/ total-attempts 2))))
      (λ (_size _attempt _retries)
        (define (enum-ith/fallback enum n)
          (define val (enum-ith enum n))
@@ -339,25 +334,12 @@
              ;; when the enumerator properly handles (x_!_1 ...) patterns,
              ;; then remove enum-ith/fallback and just use enum-ith
              (ad-hoc-generator _size _attempt _retries)))
-       (define now (current-inexact-milliseconds))
        (cond
-         [(<= now interleave-time)
+         [(< _attempt random-start)
           (enum-ith/fallback enum (in-bounds (- _attempt 1)))]
-         [(<= now pure-random-time)
-          (unless interleave-start-attempt (set! interleave-start-attempt _attempt))
-          (define interleave-attempt (- _attempt interleave-start-attempt))
-          (cond
-            [(odd? interleave-attempt) 
-             (ad-hoc-generator _size (/ (- interleave-attempt 1) 2) _retries)]
-            [else
-             (define enum-id (in-bounds (+ interleave-start-attempt (/ interleave-attempt 2) -1)))
-             (enum-ith/fallback enum enum-id)])]
          [else
-          (unless pure-random-start-attempt (set! pure-random-start-attempt _attempt))
           (ad-hoc-generator _size
-                            (+ (- _attempt pure-random-start-attempt)
-                               (quotient (- pure-random-start-attempt pure-random-start-attempt)
-                                         2))
+                            (- _attempt random-start)
                             _retries)]))]
     [else
      ad-hoc-generator]))