basic support for cvc4

emina · Oct 4, 2014 · 92d2ce3 · 92d2ce3
1 parent f45f4b9
commit 92d2ce3
Show file tree

Hide file tree

Showing 21 changed files with 119 additions and 74 deletions.
diff --git a/rosette/query/cegis.rkt b/rosette/query/cegis.rkt
@@ -10,7 +10,7 @@
          "../solver/solver.rkt"  
          "../solver/solution.rkt"
          "../solver/kodkod/kodkod.rkt"
-         "../solver/z3/z3.rkt")
+         "../solver/smt/z3.rkt")
 
 (provide exists-forall)
 

diff --git a/rosette/solver/kodkod/kodkod.rkt b/rosette/solver/kodkod/kodkod.rkt
@@ -9,7 +9,7 @@
 (provide kodkod% kodkod-incremental%)
 
 (define kodkod% 
-  (class* object% (solver<%> writable<%>) 
+  (class* object% (solver<%> writable<%>) (inspect (make-inspector))
 
     (define kodkod-server (new server% 
                                [initializer (thunk (kodkod-initializer #f))]

diff --git a/rosette/solver/z3/cmd.rkt → rosette/solver/smt/cmd.rkt b/rosette/solver/z3/cmd.rkt → rosette/solver/smt/cmd.rkt
@@ -51,6 +51,10 @@
        [(== true) #t]
        [(== false) #f]
        [_ (error 'decode-binding "expected 'true or 'false binding for ~a, given ~a" const val)])]
-    [(== @number?) (finitize val)]
+    [(== @number?) 
+     (match val
+       [(? number?) (finitize val)]
+       [(list _ (app symbol->string (regexp #px"bv(\\d+)" (list _ (app string->number n)))) _)
+        (finitize n)])]
     [(? enum? t) (vector-ref (enum-members t) val)]
     [other other]))
diff --git a/rosette/solver/smt/cvc4.rkt b/rosette/solver/smt/cvc4.rkt
@@ -0,0 +1,16 @@
+#lang racket
+
+(require racket/runtime-path "smt.rkt" "../common/server.rkt")
+
+(provide cvc4%)
+
+(define-runtime-path cvc4 (build-path ".." ".." ".." "bin" "cvc4"))
+
+(define cvc4%
+  (class* smt% (writable<%>) (inspect (make-inspector))
+
+    (super-new [path cvc4] 
+               [opts '("--lang=smt" "--output-lang=z3-str" "-m" "-q" "--strings-exp")])
+
+    (define/public (custom-write port) (fprintf port "cvc4%"))
+    (define/public (custom-display port) (custom-write port))))
diff --git a/rosette/solver/z3/enc.rkt → rosette/solver/smt/enc.rkt b/rosette/solver/z3/enc.rkt → rosette/solver/smt/enc.rkt
diff --git a/rosette/solver/z3/env.rkt → rosette/solver/smt/env.rkt b/rosette/solver/z3/env.rkt → rosette/solver/smt/env.rkt
diff --git a/rosette/solver/smt/smt.rkt b/rosette/solver/smt/smt.rkt
@@ -0,0 +1,52 @@
+#lang racket
+
+(require "../solver.rkt" "../solution.rkt" 
+         "../common/server.rkt" (only-in "../common/util.rkt" filter-asserts)
+         "../../config/log.rkt" "cmd.rkt" (rename-in "env.rkt" [env make-env]))
+
+(provide smt%)
+
+(define smt%
+  (class* object% (solver<%>) (inspect (make-inspector))
+    [init path]
+    [init opts]
+
+    (define server 
+      (new server% 
+           [initializer (thunk (apply subprocess #f #f #f path opts))]
+           [stderr-handler (lambda (err)
+                             (let ([expr (read err)])
+                               (unless (eof-object? expr)
+                                 (log-error [this] "~a" expr))))]))
+
+    (define asserts '())
+    (define env (make-env))
+
+    (super-new)
+
+    (define/public assert 
+      (lambda in (set! asserts (append asserts (filter-asserts in)))))
+
+    (define/public (clear) 
+      (send server shutdown)
+      (set!-values (asserts env) (values '() (make-env))))
+
+    (define/public (shutdown)  (clear))
+
+    (define/public (debug)     (error 'debug "not supported by ~a" this))      
+    (define/public (solve-all) (error 'solve-all "not supported by ~a" this))
+
+    (define/public (solve)
+      (set! asserts (remove-duplicates asserts))
+      (cond [(ormap false? asserts) (unsat)]
+            [else    
+             (parameterize ([current-log-source this])
+               (log-time [this] "compilation" : 
+                         (send server write (curry encode env asserts))
+                         (set! asserts '()))
+               (log-time [this] "solving"     : 
+                         (send server read (curry decode env))))]))))
+
+
+
+
diff --git a/rosette/solver/z3/smtlib2.rkt → rosette/solver/smt/smtlib2.rkt b/rosette/solver/z3/smtlib2.rkt → rosette/solver/smt/smtlib2.rkt
diff --git a/rosette/solver/smt/z3.rkt b/rosette/solver/smt/z3.rkt
@@ -0,0 +1,16 @@
+#lang racket
+
+(require racket/runtime-path "smt.rkt" "../common/server.rkt")
+
+(provide z3%)
+
+(define-runtime-path z3 (build-path ".." ".." ".." "bin" "z3"))
+
+(define z3%
+  (class* smt% (writable<%>) (inspect (make-inspector))
+
+    (super-new [path z3] 
+               [opts '("-smt2" "-in")])
+
+    (define/public (custom-write port) (fprintf port "z3%"))
+    (define/public (custom-display port) (custom-write port))))
diff --git a/rosette/solver/z3/z3.rkt b/rosette/solver/z3/z3.rkt
diff --git a/sdsl/fsm/demo.rkt b/sdsl/fsm/demo.rkt
@@ -8,6 +8,7 @@
            (r → end)] 
    [end : ]))
 
+(define rx #px"^c[ad]+r$")
 
 
 (define M 
@@ -22,10 +23,11 @@
    [end  : ]))
 
 ; example commands 
-(m '(c a r)) 
-(m '(c d r))
-(m '(c a d a r))
-(verify-automaton m #px"^c[ad]+r$")
-(debug-automaton m #px"^c[ad]+r$" '(c r))
-(synthesize-automaton M #px"^c[ad]+r$")
+;(m '(c a r)) 
+;(m '(c d r))
+;(m '(c a d a r))
+;(verify-automaton m #px"^c[ad]+r$")
+;(debug-automaton m #px"^c[ad]+r$" '(c r))
+;(synthesize-automaton M #px"^c[ad]+r$")
 
+(viz m)
diff --git a/sdsl/fsm/fsm.rkt b/sdsl/fsm/fsm.rkt
@@ -6,7 +6,7 @@
          verify-automaton
          debug-automaton 
          solve-automaton 
-         synthesize-automaton
+         synthesize-automaton matches?
          (rename-out [define/debug define])
          #%app #%top #%top-interaction #%module-begin #%datum
-         quote)
+         quote)
diff --git a/sdsl/fsm/query.rkt b/sdsl/fsm/query.rkt
@@ -7,7 +7,7 @@
 
 (provide define/debug debug-automaton 
          verify-automaton solve-automaton 
-         synthesize-automaton)
+         synthesize-automaton matches?)
 
 ; Returns a symbolic word of length k, drawn from the given alphabet.
 (define (word k alphabet)
@@ -23,8 +23,11 @@
 (define (word->string w)
   (apply string-append (map symbol->string w)))
 
+(define (matches? regex w)
+  (regexp-match? regex (word->string w)))
+
 (define (correct? m regex w)
-  (eq? (m w) (regexp-match? regex (word->string w))))
+  (eq? (m w) (matches? regex w)))
 
 (define (verify-automaton m regex [k 4])
   (define w (word* k (alphabet m)))

diff --git a/sdsl/ifc/verify-EENI-demo.rkt b/sdsl/ifc/verify-EENI-demo.rkt
@@ -33,7 +33,7 @@
 
 
 ; Uncomment the following two lines to use Z3 instead of Kodkod:
-;(require rosette/solver/z3/z3)
+;(require rosette/solver/smt/z3)
 ;(current-solver (new z3%))
 
 ; Shows counterexamples for bugs in basic semantics. 

diff --git a/sdsl/ifc/verify-SSNI-demo.rkt b/sdsl/ifc/verify-SSNI-demo.rkt
@@ -30,7 +30,7 @@
 
 
 ; Uncomment the following two lines to use Z3 instead of Kodkod:
-;(require rosette/solver/z3/z3)
+;(require rosette/solver/smt/z3)
 ;(current-solver (new z3%))
 
 ; Shows counterexamples for bugs in basic semantics. 

diff --git a/sdsl/synthcl/lang/main.rkt b/sdsl/synthcl/lang/main.rkt
@@ -4,7 +4,7 @@
                      (only-in rosette in-dict dict-keys)
                      (only-in "sugar.rkt" desugar)
                      (only-in "env.rkt" bind current-env [env make-env]))
-         (only-in rosette/solver/z3/z3 z3%)
+         (only-in rosette/solver/smt/z3 z3%)
          (only-in rosette/lib/meta/meta choose)
          "types.rkt" "operators.rkt" "forms.rkt" "queries.rkt"
          "builtins.rkt" "sugar.rkt")

diff --git a/sdsl/synthcl/lang/queries.rkt b/sdsl/synthcl/lang/queries.rkt
@@ -4,7 +4,7 @@
          (for-syntax (only-in racket/syntax with-syntax*))
          (only-in "forms.rkt" range :)
          (only-in rosette/lib/meta/meta print-forms)
-         (only-in rosette/solver/z3/z3 z3%)
+         (only-in rosette/solver/smt/z3 z3%)
          (prefix-in rosette/ (only-in rosette verify synthesize)))
 
 (provide verify synth)

diff --git a/sdsl/websynth/websynthlib.rkt b/sdsl/websynth/websynthlib.rkt
@@ -3,7 +3,7 @@
 (require "dom.rkt")
 (provide (except-out (all-defined-out) tag-type))
 
-(require rosette/solver/z3/z3)
+(require rosette/solver/smt/z3)
 (current-solver (new z3%))
 
 (define-syntax-rule (define-tags tags)

diff --git a/test/solver/bvsemantics.rkt b/test/solver/bvsemantics.rkt
@@ -5,7 +5,7 @@
          rosette/base/num rosette/solver/solution
          rosette/base/term rosette/base/bool rosette/base/num rosette/base/merge
          rosette/base/equality 
-         rosette/solver/kodkod/kodkod rosette/solver/z3/z3)
+         rosette/solver/kodkod/kodkod rosette/solver/smt/z3)
 
 (define kodkod (new kodkod%))
 (define z3 (new z3%))

diff --git a/test/solver/z3.rkt b/test/solver/z3.rkt
@@ -1,6 +1,6 @@
 #lang racket
 
-(require rosette/solver/z3/z3 
+(require rosette/solver/smt/z3 
          (prefix-in solve/ "solve.rkt")
          (prefix-in solve+/ "solve+.rkt"))
 

diff --git a/test/stats/all-tests.txt b/test/stats/all-tests.txt
@@ -252,3 +252,9 @@
 [2014.09.16 12:27:44] [rosette/test/all-tests.rkt run-all] [cpu=6896, real=9158, gc=1466]
 [2014.09.16 12:28:37] [rosette/test/all-tests.rkt run-z3] [cpu=34765, real=52230, gc=708]
 [2014.09.16 12:28:53] [rosette/test/all-tests.rkt run-bv] [cpu=10647, real=16905, gc=266]
+[2014.10.03 14:56:38] [rosette/test/all-tests.rkt run-all] [cpu=7160, real=9425, gc=1851]
+[2014.10.03 14:57:49] [rosette/test/all-tests.rkt run-z3] [cpu=48214, real=70926, gc=812]
+[2014.10.03 14:58:12] [rosette/test/all-tests.rkt run-bv] [cpu=13909, real=23178, gc=291]
+[2014.10.03 15:18:24] [rosette/test/all-tests.rkt run-all] [cpu=5973, real=8224, gc=685]
+[2014.10.03 15:20:13] [rosette/test/all-tests.rkt run-z3] [cpu=72339, real=108317, gc=911]
+[2014.10.03 15:20:47] [rosette/test/all-tests.rkt run-bv] [cpu=22652, real=33967, gc=2224]