Drop current-oracle and oracle.

jamestiotio · Feb 17, 2021 · c185cf7 · c185cf7
1 parent b4f6ae1
commit c185cf7
Show file tree

Hide file tree

Showing 8 changed files with 20 additions and 54 deletions.
diff --git a/rosette/base/base.rkt b/rosette/base/base.rkt
@@ -9,7 +9,7 @@
   "core/procedure.rkt" "core/equality.rkt" "core/distinct.rkt" "core/reflect.rkt"  
   "adt/box.rkt" "adt/list.rkt" "adt/vector.rkt" 
   "struct/struct.rkt" "struct/generics.rkt"
-  "form/state.rkt" "form/define.rkt" "form/control.rkt" "form/module.rkt" "form/app.rkt") 
+  "form/define.rkt" "form/control.rkt" "form/module.rkt" "form/app.rkt") 
 
 (provide
   (rename-out [@|| ||]) ; The character sequence || does not play nicely with the filtered-out form.
@@ -92,8 +92,6 @@
      struct struct-field-index define/generic define-struct
      ; struct/generics.rkt
      @define-generics @make-struct-type-property
-     ; form/state.rkt
-     current-oracle oracle oracle? 
      ; form/define.rkt
      define-symbolic define-symbolic*
      ; form/control.rkt

diff --git a/rosette/base/form/define.rkt b/rosette/base/form/define.rkt
@@ -1,7 +1,7 @@
 #lang racket
 
 (require syntax/parse (for-syntax syntax/parse racket)
-         "../core/term.rkt" "state.rkt")
+         "../core/term.rkt")
 
 (provide define-symbolic define-symbolic*)
 
@@ -27,12 +27,17 @@
     [(_ var:id ...+ type)
      #'(begin (define-symbolic var type) ...)]))
 
+(define current-index (make-parameter 0))
+
+(define (index!)
+  (define idx (current-index))
+  (current-index (add1 idx))
+  idx)
+
 (define-syntax (define-symbolic* stx)
   (syntax-parse stx
-    [(_ [var:id oracle] type)
-     #'(define var (constant (list #'var (oracle #'var)) type))]
     [(_ var:id type)
-     #'(define-symbolic* [var (current-oracle)] type)]
+     #'(define var (constant (list #'var (index!)) type))]
     [(_ var:id type #:length k)
      #:declare k (expr/c #'natural? #:name "length argument")
      #'(define var

diff --git a/rosette/base/form/state.rkt b/rosette/base/form/state.rkt
diff --git a/rosette/lib/roseunit.rkt b/rosette/lib/roseunit.rkt
@@ -5,7 +5,7 @@
 (require rosette/base/core/result
          (only-in rosette 
                   clear-state!
-                  current-bitwidth current-oracle oracle
+                  current-bitwidth
                   with-vc with-terms terms
                   solution? sat? unsat?))
 (require (for-syntax syntax/parse))
@@ -72,10 +72,9 @@
                     #:after after
                     (with-normal-or-fail
                       (with-terms 
-                        (parameterize ([current-bitwidth (current-bitwidth)]
-                                       [current-oracle (oracle (current-oracle))])
+                        (parameterize ([current-bitwidth (current-bitwidth)])
                           test ...))))])
-           (let ([rts (rosette-test-suite features ts (terms) (current-bitwidth) (oracle (current-oracle)))])
+           (let ([rts (rosette-test-suite features ts (terms) (current-bitwidth))])
              (set-box! discovered-tests (append (unbox discovered-tests) (list rts)))
              ts)))]))
 
@@ -85,30 +84,28 @@
 ; A test should only be run if the current-solver satisfies the test's feature list.
 (define discovered-tests (box '()))
 (define executed-tests (mutable-seteq))
-(struct rosette-test-suite (features ts terms bitwidth oracle) #:transparent)
+(struct rosette-test-suite (features ts terms bitwidth) #:transparent)
 
 
 ; Run all discovered tests that the given list of features satisfies.
 ; Only tests that actually require features are run.
 (define (run-solver-specific-tests [features '()])
   (for ([rts (in-list (unbox discovered-tests))])
-    (match-define (rosette-test-suite feats ts trms bw o) rts)
+    (match-define (rosette-test-suite feats ts trms bw) rts)
     (when (and (not (null? feats)) (for/and ([f feats]) (member f features)))
       (with-terms trms
-        (parameterize ([current-bitwidth bw]
-                       [current-oracle (oracle o)])
+        (parameterize ([current-bitwidth bw])
           (set-add! executed-tests rts)
           (time (run-tests ts)))))))
 
 ; The same as run-all-discovered-tests, but only for tests
 ; that require no features.
 (define (run-generic-tests)
   (for ([rts (in-list (unbox discovered-tests))])
-    (match-define (rosette-test-suite feats ts trms bw o) rts)
+    (match-define (rosette-test-suite feats ts trms bw) rts)
     (when (null? feats)
       (with-terms trms
-        (parameterize ([current-bitwidth bw]
-                       [current-oracle (oracle o)])
+        (parameterize ([current-bitwidth bw])
           (set-add! executed-tests rts)
           (time (run-tests ts)))))))
 

diff --git a/rosette/safe.rkt b/rosette/safe.rkt
@@ -22,7 +22,6 @@
 
 (define (clear-state!)
   (current-bitwidth #f)
-  (current-oracle (oracle))
   (clear-vc!)
   (clear-terms!)
   (current-solver (z3)))

diff --git a/sdsl/bv/lang/form.rkt b/sdsl/bv/lang/form.rkt
@@ -2,7 +2,6 @@
 
 (require "program.rkt" "core.rkt" "fragment.rkt" "log.rkt"
          rosette/query/eval
-         rosette/base/form/state
          rosette/solver/solution
          (only-in rosette/base/core/term with-terms)
          (for-syntax racket/syntax))
@@ -29,7 +28,7 @@
      #'(synthesize-fragment (id param ...) #:implements spec #:library lib-expr #:minbv 4)]
     [(_ (id param ...) #:implements spec #:library lib-expr #:minbv minbv)
      #`(with-terms
-         (parameterize ([current-oracle (oracle)])
+         (begin
            (bv-info "synthesizing ~a" #'id)
            (define impl (prog* #,(length (syntax->list #'(param ...))) lib-expr))
            (define-values (val cpu real gc) (time-apply ∃∀-solve (list impl spec minbv)))     

diff --git a/sdsl/ifc/verify.rkt b/sdsl/ifc/verify.rkt
@@ -40,8 +40,7 @@
 ;     (or/c EENI-witness? #t))
 (define (verify-EENI* start end ≈ prog [k #f] [verbose? #f])
   (with-terms
-    (parameterize ([current-bitwidth 5]
-                   [current-oracle (oracle)])
+    (parameterize ([current-bitwidth 5])
 
       (define p (prog))
 

diff --git a/sdsl/synthcl/lang/queries.rkt b/sdsl/synthcl/lang/queries.rkt
@@ -26,7 +26,6 @@
            (expected?)
            (with-terms 
              (parameterize ([current-bitwidth 32]
-                            [current-oracle (oracle (current-oracle))]
                             [current-output-port (query-output-port)])
                (printf "Verifying ~a\n" (source-of #'verify))
                (time 
@@ -69,7 +68,6 @@
            (expected?)
            (with-terms 
              (parameterize ([current-bitwidth bw]
-                            [current-oracle (oracle (current-oracle))]
                             [current-output-port (query-output-port)])
                (printf "Synthesizing ~a\n" (source-of #'synthesize))
                (define-values (id ...)