Add concrete? and symbolic? predicates for checking if a value is ful…

…ly concrete or not (emina#183).
vcanumalla · Mar 3, 2021 · fdb779a · fdb779a
1 parent 1f8c862
commit fdb779a
Show file tree

Hide file tree

Showing 5 changed files with 101 additions and 2 deletions.
diff --git a/rosette/base/base.rkt b/rosette/base/base.rkt
@@ -47,6 +47,7 @@
      @eq? @equal?
      ; core/reflect.rkt
      symbolics type? solvable? @any/c type-of type-cast for/all for*/all
+     symbolic? concrete?
      term? constant? expression? 
      term expression constant term-type
      term=? term->datum

diff --git a/rosette/base/core/reflect.rkt b/rosette/base/core/reflect.rkt
@@ -11,7 +11,7 @@
          union? union union-contents union-guards union-values
          union-filter in-union in-union* in-union-guards in-union-values
          (struct-out normal) (struct-out failed) result? result-value result-state
-         symbolics)
+         symbolics concrete? symbolic?)
 
 (define (term=? s0 s1)
   (and (term? s0) (term? s1) (equal? s0 s1)))
@@ -47,6 +47,29 @@
                    [_ (void)]))))
          (reverse result))]))
 
+(define (concrete? val)
+  (define objs (mutable-set))
+  (let all-concrete? ([val val])
+    (and (not (term? val))
+         (not (union? val))
+         (or
+          (set-member? objs val)
+          (begin
+            (set-add! objs val)
+            (match val
+              [(box v) (all-concrete? v)]
+              [(? list?) (for/and ([v val]) (all-concrete? v))]
+              [(cons x y) (and (all-concrete? x) (all-concrete? y))]
+              [(? vector?) (for/and ([v val]) (all-concrete? v))]
+              [(and (? typed?) (app get-type t))
+               (match (type-deconstruct t val)
+                 [(list (== val)) #t]
+                 [components (for/and ([v components]) (all-concrete? v))])]
+              [_ #t]))))))
+
+(define (symbolic? val) (not (concrete? val)))
+
+
 (define (term->datum val)
   (let convert ([val val] [cache (make-hash)])
     (if (hash-has-key? cache val) 

diff --git a/rosette/guide/scribble/reflection/value-reflection.scrbl b/rosette/guide/scribble/reflection/value-reflection.scrbl
@@ -5,7 +5,7 @@
            rosette/base/form/define  
            rosette/base/core/term rosette/base/core/type rosette/base/core/union
            (only-in rosette/base/base vc clear-vc! bitvector ~>)
-           (only-in rosette/base/core/reflect symbolics)
+           (only-in rosette/base/core/reflect symbolics concrete? symbolic?)
            rosette/base/core/forall racket)
           scribble/core scribble/html-properties scribble/example racket/sandbox
           "../util/lifted.rkt")
@@ -83,9 +83,26 @@ transitively contained in the given value.
 (symbolics (if (= x y) 2 #f))
 (symbolics (list y z y))
 (struct cell (value) #:transparent)
+(symbolics (list (vector (box 1) 3) (cell (cons 4 5))))
 (symbolics (list 5 (cons (box y) z) (vector (cell x) z)))]
 }
 
+@defproc[(concrete? [v any/c]) boolean?]{
+Equivalent to @racket[(null? (symbolics v))] but more efficient.
+@examples[#:eval rosette-eval
+(define-symbolic x y z integer?) 
+(concrete? x)
+(concrete? (if (= x y) 2 #f))
+(concrete? (list y z y))
+(struct cell (value) #:transparent)
+(concrete? (list (vector (box 1) 3) (cell (cons 4 5))))
+(concrete? (list 5 (cons (box y) z) (vector (cell x) z)))]              
+}
+
+@defproc[(symbolic? [v any/c]) boolean?]{
+Equivalent to @racket[(not (concrete? v))].
+}
+
 @defproc*[([(type-of [v any/c] ...+) type?])]{
 
  Returns the most specific @racket[type?] predicate that

diff --git a/test/all-rosette-tests.rkt b/test/all-rosette-tests.rkt
@@ -38,6 +38,7 @@
  "base/distinct.rkt"
  "base/generics.rkt"
  "base/push-pop.rkt"
+ "base/reflect.rkt"
  "base/decode.rkt"
  "query/solve.rkt"
  "query/verify.rkt"

diff --git a/test/base/reflect.rkt b/test/base/reflect.rkt
@@ -0,0 +1,57 @@
+#lang rosette
+
+
+(require rackunit rackunit/text-ui rosette/lib/roseunit)
+
+(define-symbolic a b boolean?)
+(define-symbolic x y z integer?)
+
+(struct triple (one two three) #:mutable #:transparent)
+
+
+(define (io)
+  (define b1 (box 1))
+  (define bx (box x))
+  (define v1 (vector 4 (list 3 2 y) bx))
+  (define v2 (vector 5 (cons (triple bx b1 6) (vector (box z) 7 (triple y x z)))))
+  (define b2 (box 0))
+  (define v3 (vector (cons (triple b2 b1 6) (vector (box z) 7 (triple y x z)))))
+  (set-box! b2 v3)
+  (define b3 (box 0))
+  (define v4 (triple (triple b3 8 9) (box 11) (list (vector 3) 5)))
+  (set-box! b3 v4)
+  (list (cons b1 null)
+        (cons #t null)
+        (cons 4 null)
+        (cons (list 1 2 (vector 5 (triple 6 7 (box 8)))) null)
+        (cons bx (list x))
+        (cons y (list y))
+        (cons (list x y z) (list x y z))
+        (cons v1 (list y x))
+        (cons v2 (list x z y))
+        (cons v3 (list z y x))
+        (cons v4 null)
+        (cons (if a (if b v4 b3) v1) (list a b y x))))
+
+(define tests:symbolics
+  (test-suite+
+   "Tests for symbolics in rosette/base/core/reflect."
+   (for ([kv (io)])
+     (check-equal? (symbolics (car kv)) (cdr kv)))))
+
+(define tests:concrete?
+  (test-suite+
+   "Tests for concrete? in rosette/base/core/reflect."
+   (for ([kv (io)])
+     (check-equal? (concrete? (car kv)) (null? (cdr kv))))))
+
+(define tests:symbolic?
+  (test-suite+
+   "Tests for symbolic? in rosette/base/core/reflect."
+   (for ([kv (io)])
+     (check-equal? (symbolic? (car kv)) (not (null? (cdr kv)))))))
+
+(module+ test
+  (time (run-tests tests:symbolics))
+  (time (run-tests tests:concrete?))
+  (time (run-tests tests:symbolic?)))