-
Notifications
You must be signed in to change notification settings - Fork 8
/
z3-noserver.scm
95 lines (86 loc) · 2.93 KB
/
z3-noserver.scm
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
(define z3-counter-check-sat 0)
(define z3-counter-get-model 0)
(define read-sat
(lambda (fn)
(let ([p (open-input-file fn)])
(let ([r (read p)])
(close-input-port p)
(eq? r 'sat)))))
(define call-z3
(lambda (xs)
(let ([p (open-output-file "out.smt" 'replace)])
(for-each (lambda (x) (fprintf p "~a\n" x)) xs)
(close-output-port p)
(system "perl -i -pe 's/#t/true/g' out.smt")
(system "perl -i -pe 's/#f/false/g' out.smt")
(system "perl -i -pe 's/bitvec-/#b/g' out.smt")
(let ((r (system "z3 out.smt >out.txt")))
(system "perl -i -pe 's/#b/bitvec-/g' out.txt")
(if (not (= r 0))
(error 'call-z3 "error in z3 out.smt > out.txt"))))))
(define check-sat
(lambda (xs)
(call-z3 (append xs '((check-sat) (exit))))
(set! z3-counter-check-sat (+ z3-counter-check-sat 1))
(read-sat "out.txt")))
(define read-model
(lambda (fn)
(let ([p (open-input-file fn)])
(let ([r (read p)])
(if (eq? r 'sat)
(let ([m (read p)])
(close-input-port p)
(map (lambda (x)
(cons (cadr x)
(if (null? (caddr x))
(let ([r (cadddr (cdr x))])
(cond
((eq? r 'false) #f)
((eq? r 'true) #t)
((and (pair? (cadddr x)) (eq? (cadr (cadddr x)) 'BitVec)) r)
(else (eval r))))
`(lambda ,(map car (caddr x)) ,(cadddr (cdr x))))))
(cdr m)))
(begin
(close-input-port p)
#f))))))
(define get-model
(lambda (xs)
(call-z3 (append xs '((check-sat) (get-model) (exit))))
(set! z3-counter-get-model (+ z3-counter-get-model 1))
(read-model "out.txt")))
(define neg-model
(lambda (model)
(cons
'assert
(list
(cons
'or
(map
(lambda (xv)
`(not (= ,(car xv) ,(cdr xv))))
model))))))
(define check-model-unique
(lambda (xs model)
(let ([r
(check-sat
(append xs (list (neg-model model))))])
(not r))))
(define get-all-models
(lambda (xs ms)
(let* ([ys (append xs (map neg-model ms))])
(if (not (check-sat ys))
(reverse ms)
(get-all-models xs (cons (get-model ys) ms))))))
(define get-next-model
(lambda (xs ms)
(let* ([ms (map (lambda (m)
(filter (lambda (x) ; ignoring functions
(or (number? (cdr x))
(symbol? (cdr x)) ; for bitvectors
)) m))
ms)])
(if (member '() ms) #f ; if we're skipping a model, let us stop
(let ([ys (append xs (map neg-model ms))])
(and (check-sat ys)
(get-model ys)))))))