added a procedure for explicit clearing of the term cache

vcanumalla · Aug 20, 2014 · 5c2a6f7 · 5c2a6f7
1 parent 764ec79
commit 5c2a6f7
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 3 deletions.
diff --git a/rosette/base/base.rkt b/rosette/base/base.rkt
@@ -96,7 +96,7 @@
  syntax quasisyntax unsyntax unsyntax-splicing
  syntax/loc quasisyntax/loc quote-syntax/prune
  syntax-rules syntax-id-rules
- define-syntax-rule ... _
+ define-syntax define-syntax-rule ... _ 
  local-expand expand expand-syntax expand-once
  expand-syntax-once expand-to-top-form
  expand-syntax-to-top-form

diff --git a/rosette/base/reflect.rkt b/rosette/base/reflect.rkt
@@ -9,7 +9,7 @@
          term expression constant
          term-name term-index term-op term-child  
          term=? term-origin term-track-origin
-         term-e term->datum term->list  
+         term-e term->datum term->list clear-terms!
          union? union union-contents union-guards union-values
          union-filter in-union in-union* in-union-guards in-union-values
          symbolics)

diff --git a/rosette/base/term.rkt b/rosette/base/term.rkt
@@ -23,6 +23,7 @@
  term-e            ; (-> any/c any/c)
  term->datum       ; (-> any/c any/c)
  term->list        ; (-> any/c any/c)
+ clear-terms!      ; (-> void? void?)
  (all-from-out "type.rkt"))
 
 
@@ -59,6 +60,7 @@
                 [_ #f]))
 
 (define cache (make-hash))
+(define (clear-terms!) (hash-clear! cache))
 
 (define-syntax-rule (make-term args type) 
   (let ([val args]) 

diff --git a/rosette/lib/tools/debug-angelic.rkt b/rosette/lib/tools/debug-angelic.rkt
@@ -25,7 +25,7 @@
          (parameterize ([current-oracle (oracle)]
                         [current-solution (empty-solution)]
                         [relate (lambda (relaxer val)
-                                  (if (sym=? relaxer indicator)
+                                  (if (term=? relaxer indicator)
                                       (not (equal? relaxer val))
                                       (equal? relaxer val)))])
            (solve (validator input))