Add a key rewrite rule for => to partially evaluate default assumptio…

…ns (due to branching).
jamestiotio · Dec 12, 2020 · cf9e56c · cf9e56c
1 parent 20dcfe4
commit cf9e56c
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 12 deletions.
diff --git a/rosette/base/core/bool.rkt b/rosette/base/core/bool.rkt
@@ -86,7 +86,30 @@
 (define && (logical-connective @&& @|| #t #f))
 (define || (logical-connective @|| @&& #f #t))
 
-(define (=> x y) (|| (! x) y))
+(define (=> x y) ; (|| (! x) y))
+  (cond
+    [(equal? x y) #t]
+    [(eq? x #f) #t]
+    [(eq? y #t) #t]
+    [(eq? x #t) y]
+    [(eq? y #f) (! x)]
+    [(cancel? x y) y]
+    [else
+     (define !x (! x))
+     (match y
+       [(expression (== @||) _ ... (== x) _ ...) #t]
+       [(expression (== @||) (== !x) b) (=> x b)]
+       [(expression (== @||) b (== !x)) (=> x b)]
+       [(expression (== @&&) (== x) b) (=> x b)]
+       [(expression (== @&&) b (== x)) (=> x b)]
+       [(expression (== @&&) (expression (== @||) _ ... (== x) _ ...) b) (=> x b)]
+       [(expression (== @&&) b (expression (== @||) _ ... (== x) _ ...)) (=> x b)]
+       [(expression (== @<=>) (== x) b) (=> x b)]
+       [(expression (== @<=>) b (== x)) (=> x b)]
+       [_ (|| !x y)])]))
+
+
+
 
 (define (<=> x y) ;(|| (&& x y) (&& (! x) (! y))))))
   (cond [(equal? x y) #t]

diff --git a/sdsl/websynth/websynthlib.rkt b/sdsl/websynth/websynthlib.rkt
@@ -1,18 +1,8 @@
 #lang rosette
 
-(require "dom.rkt" (rename-in rosette [solve rosette/solve]))
+(require "dom.rkt")
 (provide (except-out (all-defined-out) tags))
 
-(require rosette/solver/smt/cvc4 rosette/solver/smt/boolector)
-
-
-(define-syntax-rule (solve e)
-  (begin
-    (current-solver (cvc4))
-    ;(current-solver (boolector))
-    ;(current-bitwidth 16)
-    (rosette/solve e)))
-
 (define-syntax-rule (define-tags ts)
   (tags ts))