Update websynth to use CVC4 for testing for now.

jamestiotio · Dec 10, 2020 · 57034f5 · 57034f5
1 parent f1acc83
commit 57034f5
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 2 deletions.
diff --git a/sdsl/websynth/websynthlib.rkt b/sdsl/websynth/websynthlib.rkt
@@ -1,8 +1,18 @@
 #lang rosette
 
-(require "dom.rkt")
+(require "dom.rkt" (rename-in rosette [solve rosette/solve]))
 (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))
 

diff --git a/test/all-sdsl-tests.rkt b/test/all-sdsl-tests.rkt
@@ -5,7 +5,7 @@
 (error-print-width 4)
 
 (test-groups [test fast] 
- ;"../sdsl/websynth/test/all-tests.rkt"         ; WebSynth
+ "../sdsl/websynth/test/all-tests.rkt"         ; WebSynth
  "../sdsl/bv/test/all-tests.rkt"               ; BV
  (submod "../sdsl/ifc/test.rkt")               ; IFC tests
  (submod "../sdsl/synthcl/test/all-tests.rkt") ; SynthCL tests