Skip to content

Commit

Permalink
WIP
Browse files Browse the repository at this point in the history
  • Loading branch information
@sorawee
sorawee committed Nov 10, 2022
1 parent 194387e commit 8d22354
Show file tree
Hide file tree
Showing 5 changed files with 412 additions and 114 deletions.
203 changes: 95 additions & 108 deletions rosette/base/core/term-cache.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@
term-cache-weak?
make-term-cache
make-weak-term-cache
term-cache-clear!
term-cache-ref
term-cache-set!
term-cache-count
Expand All @@ -14,15 +13,17 @@

(require racket/match)

(struct term-cache (weak? nullary unary binary ternary nary))
(struct term-cache (nullary unary binary ternary nary))

(define-values (prop:term-cachable term-cachable? term-cachable-ref)
(make-struct-type-property 'term-cachable))

(define (term-cache-weak? x)
(and (hash? x) (hash-ephemeron? x)))

(define (make-term-cache [assocs '()])
(define out
(term-cache #f
(make-hasheq)
(term-cache (make-hasheq)
(make-hasheq)
(make-hasheq)
(make-hasheq)
Expand All @@ -31,127 +32,113 @@
(term-cache-set! out (car pair) (cdr pair)))
out)

(define (make-weak-term-cache [assocs '()])
(define out
(term-cache #t
(make-ephemeron-hasheq)
(make-ephemeron-hasheq)
(make-ephemeron-hasheq)
(make-ephemeron-hasheq)
(make-ephemeron-hash)))
(for ([pair (in-list assocs)])
(term-cache-set! out (car pair) (cdr pair)))
out)

(define (term-cache-clear! h)
(match-define (term-cache _ nullary unary binary ternary nary) h)
(hash-clear! nullary)
(hash-clear! unary)
(hash-clear! binary)
(hash-clear! ternary)
(hash-clear! nary))
(define make-weak-term-cache make-ephemeron-hash)

(define (term-like? x)
(or (term-cachable? x) (syntax? x) (fixnum? x) (boolean? x) (procedure? x)))

(define (term-cache-ref h k default)
(define (proc) (if (procedure? default) (default) default))
(match-define (term-cache _ nullary unary binary ternary nary) h)
(match k
[_
#:when (term-like? k)
(hash-ref nullary k proc)]
[(list op a)
#:when (and (term-like? op) (term-like? a))
(match (hash-ref unary op #f)
[#f (proc)]
[h (hash-ref h a proc)])]
[(list op a b)
#:when (and (term-like? op) (term-like? a) (term-like? b))
(match (hash-ref binary op #f)
[#f (proc)]
[h
(match (hash-ref h a #f)
(match h
[(term-cache nullary unary binary ternary nary)
(match k
[_
#:when (term-like? k)
(hash-ref nullary k proc)]
[(list op a)
#:when (and (term-like? op) (term-like? a))
(match (hash-ref unary op #f)
[#f (proc)]
[h (hash-ref h a proc)])]
[(list op a b)
#:when (and (term-like? op) (term-like? a) (term-like? b))
(match (hash-ref binary op #f)
[#f (proc)]
[h (hash-ref h b proc)])])]
[(list op a b c)
#:when (and (term-like? op) (term-like? a) (term-like? b) (term-like? c))
(match (hash-ref ternary op #f)
[#f (proc)]
[h
(match (hash-ref h a #f)
[h
(match (hash-ref h a #f)
[#f (proc)]
[h (hash-ref h b proc)])])]
[(list op a b c)
#:when (and (term-like? op) (term-like? a) (term-like? b) (term-like? c))
(match (hash-ref ternary op #f)
[#f (proc)]
[h
(match (hash-ref h b #f)
(match (hash-ref h a #f)
[#f (proc)]
[h (hash-ref h c proc)])])])]
[_ (hash-ref nary k proc)]))
[h
(match (hash-ref h b #f)
[#f (proc)]
[h (hash-ref h c proc)])])])]
[_ (hash-ref nary k proc)])]
[_ (hash-ref h k proc)]))

(define (term-cache-set! h k v)
(match-define (term-cache weak? nullary unary binary ternary nary) h)
(define make-eq (if weak? make-hasheq make-ephemeron-hasheq))
(match k
[_
#:when (term-like? k)
(hash-set! nullary k v)]
[(list op a)
#:when (and (term-like? op) (term-like? a))
(hash-set! (hash-ref! unary op make-eq) a v)]
[(list op a b)
#:when (and (term-like? op) (term-like? a) (term-like? b))
(hash-set! (hash-ref! (hash-ref! binary op make-eq) a make-eq) b v)]
[(list op a b c)
#:when (and (term-like? op) (term-like? a) (term-like? b) (term-like? c))
(hash-set! (hash-ref! (hash-ref! (hash-ref! ternary op make-eq) a make-eq) b make-eq) c v)]
[_ (hash-set! nary k v)]))
(match h
[(term-cache nullary unary binary ternary nary)
(match k
[_
#:when (term-like? k)
(hash-set! nullary k v)]
[(list op a)
#:when (and (term-like? op) (term-like? a))
(hash-set! (hash-ref! unary op make-hasheq) a v)]
[(list op a b)
#:when (and (term-like? op) (term-like? a) (term-like? b))
(hash-set! (hash-ref! (hash-ref! binary op make-hasheq) a make-hasheq) b v)]
[(list op a b c)
#:when (and (term-like? op) (term-like? a) (term-like? b) (term-like? c))
(hash-set! (hash-ref! (hash-ref! (hash-ref! ternary op make-hasheq) a make-hasheq) b make-hasheq) c v)]
[_ (hash-set! nary k v)])]
[_ (hash-set! h k v)]))

(define (term-cache-count h)
(match-define (term-cache _ nullary unary binary ternary nary) h)
(+ (hash-count nullary)
(for/sum ([(_ h) (in-hash unary)])
(hash-count h))
(for/sum ([(_ h) (in-hash binary)])
(for/sum ([(_ h) (in-hash h)])
(hash-count h)))
(for/sum ([(_ h) (in-hash ternary)])
(for/sum ([(_ h) (in-hash h)])
(for/sum ([(_ h) (in-hash h)])
(hash-count h))))
(hash-count nary)))
(match h
[(term-cache nullary unary binary ternary nary)
(+ (hash-count nullary)
(for/sum ([(_ h) (in-hash unary)])
(hash-count h))
(for/sum ([(_ h) (in-hash binary)])
(for/sum ([(_ h) (in-hash h)])
(hash-count h)))
(for/sum ([(_ h) (in-hash ternary)])
(for/sum ([(_ h) (in-hash h)])
(for/sum ([(_ h) (in-hash h)])
(hash-count h))))
(hash-count nary))]
[_ (hash-count h)]))

(define (term-cache-copy h)
(match-define (term-cache weak? nullary unary binary ternary nary) h)
(term-cache weak?
(hash-copy nullary)
(hash-copy unary)
(hash-copy binary)
(hash-copy ternary)
(hash-copy nary)))
(match h
[(term-cache nullary unary binary ternary nary)
(term-cache (hash-copy nullary)
(hash-copy unary)
(hash-copy binary)
(hash-copy ternary)
(hash-copy nary))]
[_ (hash-copy h)]))

(define (term-cache-copy-clear h)
(match-define (term-cache weak? nullary unary binary ternary nary) h)
(term-cache weak?
(hash-copy-clear nullary)
(hash-copy-clear unary)
(hash-copy-clear binary)
(hash-copy-clear ternary)
(hash-copy-clear nary)))
(cond
[(term-cache-weak? h) (make-weak-term-cache)]
[else (make-term-cache)]))

(define (term-cache->hash h)
(match-define (term-cache _ nullary unary binary ternary nary) h)
(define h* (hash-copy nary))
(for ([(k v) (in-hash nullary)])
(hash-set! h* k v))
(for ([(op h) (in-hash unary)])
(for ([(a v) (in-hash h)])
(hash-set! h* (list op a) v)))
(for ([(op h) (in-hash binary)])
(for ([(a h) (in-hash h)])
(for ([(b v) (in-hash h)])
(hash-set! h* (list op a b) v))))
(for ([(op h) (in-hash ternary)])
(for ([(a h) (in-hash h)])
(for ([(b h) (in-hash h)])
(for ([(c v) (in-hash h)])
(hash-set! h* (list op a b c) v)))))
h*)
(match h
[(term-cache nullary unary binary ternary nary)
(define h* (hash-copy nary))
(for ([(k v) (in-hash nullary)])
(hash-set! h* k v))
(for ([(op h) (in-hash unary)])
(for ([(a v) (in-hash h)])
(hash-set! h* (list op a) v)))
(for ([(op h) (in-hash binary)])
(for ([(a h) (in-hash h)])
(for ([(b v) (in-hash h)])
(hash-set! h* (list op a b) v))))
(for ([(op h) (in-hash ternary)])
(for ([(a h) (in-hash h)])
(for ([(b h) (in-hash h)])
(for ([(c v) (in-hash h)])
(hash-set! h* (list op a b c) v)))))
h*]
[_ h]))
8 changes: 3 additions & 5 deletions rosette/base/core/term.rkt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -28,7 +28,7 @@
; it clears all terms reachable from the given set of leaf terms.
(define (clear-terms! [terms #f])
(if (false? terms)
(term-cache-clear! (current-terms))
(current-terms (term-cache-copy-clear (current-terms)))
(let ([cache (term-cache->hash (current-terms))]
[evicted (list->mutable-set terms)])
(for ([t (in-list terms)])
Expand All @@ -42,10 +42,8 @@
(hash-remove! cache (term-val t))
(set-add! evicted t))
(loop)))
(current-terms ((if (term-cache-weak? (current-terms))
make-term-cache
make-weak-term-cache)
(hash->list cache))))))
(unless (term-cache-weak? (current-terms))
(current-terms (make-term-cache (hash->list cache)))))))

; Sets the current term cache to a garbage-collected (weak) hash.
; The setting preserves all reachable terms from (current-terms).
Expand Down
84 changes: 84 additions & 0 deletions test/base/smt.rkt
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
#lang rosette

(require rackunit rackunit/text-ui rosette/lib/roseunit)

(define (extract fml)
(define-values (in out) (make-pipe))
(parameterize ([output-smt out])
(solve (assert fml)))
(close-output-port out)

;; drop 5 for
;; (reset)
;; (set-option :auto-config true)
;; (set-option :produce-unsat-cores false)
;; (set-option :smt.mbqi.max_iterations 10000000)
;; (set-option :smt.relevancy 2)
;;
;; drop-right 7 for
;; (check-sat)
;; (get-model)
;; and the other 5 mentioned above

(drop-right (drop (port->list read in) 5) 7))

(define smt-tests
(test-suite+
"SMT tests"

;; a dummy call so that next tests start with (reset)
(solve #t)

(define-symbolic a b c d integer?)

(check-equal?
(extract (<= a b))
'((declare-fun c0 () Int)
(declare-fun c1 () Int)
(define-fun e2 () Bool (<= c0 c1))
(assert e2)))

(check-equal?
(extract (<= (+ a b) (- c)))
'((declare-fun c0 () Int)
(declare-fun c1 () Int)
(define-fun e2 () Int (+ c0 c1))
(declare-fun c3 () Int)
(define-fun e4 () Int (- c3))
(define-fun e5 () Bool (<= e2 e4))
(assert e5)))

(check-equal?
(extract (<= (+ a b) (- (+ a b))))
'((declare-fun c0 () Int)
(declare-fun c1 () Int)
(define-fun e2 () Int (+ c0 c1))
(define-fun e3 () Int (- e2))
(define-fun e4 () Bool (<= e2 e3))
(assert e4)))

(check-equal?
(extract (<= (+ a b c d) (- (+ a b c d))))
'((declare-fun c0 () Int)
(declare-fun c1 () Int)
(declare-fun c2 () Int)
(declare-fun c3 () Int)
(define-fun e4 () Int (+ c0 c1 c2 c3))
(define-fun e5 () Int (- e4))
(define-fun e6 () Bool (<= e4 e5))
(assert e6)))

(check-equal?
(extract (<= (if (= a b) c d) (if (= a b) d c)))
'((declare-fun c0 () Int)
(declare-fun c1 () Int)
(define-fun e2 () Bool (= c0 c1))
(declare-fun c3 () Int)
(declare-fun c4 () Int)
(define-fun e5 () Int (ite e2 c3 c4))
(define-fun e6 () Int (ite e2 c4 c3))
(define-fun e7 () Bool (<= e5 e6))
(assert e7)))))

(module+ test
(time (run-tests smt-tests)))
Loading

0 comments on commit 8d22354

Please sign in to comment.