-
Notifications
You must be signed in to change notification settings - Fork 0
/
smt.scm
170 lines (151 loc) · 5.03 KB
/
smt.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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
(define-module (smt)
#:export (smt-assert
smt-check-sat
smt-comment
smt-const
smt-distinct
smt-fun
smt-get-model
smt-maximize
smt-minimize
smt-quoted-symbol
smt-push
smt-pop
smt-record
smt-scalar
smt-sort
with-current-assertion-set))
(define *bug-report* "https://github.com/edoput/guile-smt/issues")
(define-syntax smt-assert
(syntax-rules ()
((_ e)
(begin
(display `(assert ,e))
(newline)))
;; TODO add the ability to set the smt
;; keyword to this assertion
((_ e name)
(begin
(display `(assert ,e))
(newline)))))
(define-syntax smt-sort
(syntax-rules ()
((_ name)
(begin
(display `(declare-sort ,name 0))
(newline)))
((_ name e)
(begin
(display `(define-sort ,name () ,e))
(newline)))
((_ name parameters e)
(begin
(display `(define-sort ,name (,@parameters) ,@e))
(newline)))))
(define-syntax smt-fun
(syntax-rules ()
((_ name input-sort output-sort)
(begin
(display `(declare-fun ,name (,@input-sort) ,output-sort))
(newline)))
((_ name input-sort output-sort e)
(begin
(display `(define-fun ,name (,@input-sort) ,output-sort
e))
(newline)))))
(define-syntax smt-const
(syntax-rules ()
((_ name sort)
(begin
(display `(declare-const ,name ,sort))
(newline)))))
(define-syntax smt-minimize
(syntax-rules ()
((_ e)
(begin
(display `(minimize ,e))
(newline)))))
(define-syntax smt-maximize
(syntax-rules ()
((_ e)
(begin
(display `(maximize ,e))
(newline)))))
(define smt-distinct
(lambda v
`(distinct ,@v)))
(define-syntax smt-scalar
(syntax-rules ()
((_ name v)
(begin
(display `(declare-datatypes () ((,name ,@v))))
(newline)))))
; (_ name params v)
; (begin
; (display `(declare-datatypes (,@params) ((,name ,@v))))
; (newline)))))
(define-syntax smt-record
(syntax-rules ()
((_ name fields)
(begin
(display
`(declare-datatypes ()
((,name (
,(string-append "mk-" (symbol->string name))
,@fields)))))
(newline)))
((_ name fields types)
(begin
(display
`(declare-datatypes ,(list types)
((,name (
,(string-append "mk-" (symbol->string name))
,@fields)))))
(newline)))))
(define-syntax with-current-assertion-set
(syntax-rules ()
((_ e)
(let ((n (length e)))
(smt-push n e)
(smt-pop n)))))
(define-syntax smt-push
(syntax-rules ()
((_ n)
(begin
(display `(push ,n))
(newline)))))
(define smt-pop
(lambda (n)
(display `(pop ,n))
(newline)))
(define-syntax make-symbol
(syntax-rules ()
((_ e) (symbol->string e))
((_ e1 e2 ...)
(string-append
(symbol->string e1)
"-"
(make-symbol e2 ...)))))
; return the representation for a new SMT quoted symbol
(define-syntax smt-quoted-symbol
(syntax-rules ()
((_ e) (string-append "|" (symbol->string e) "|"))
((_ e1 ...)
(string-append "|" (make-symbol e1 ...) "|"))))
; insert a comment in the resulting SMT file
(define-syntax smt-comment
(syntax-rules ()
((_ e1 ...)
(begin (display (string-append "; " e1 ...))(newline)))))
; insert the check-sat command in the resulting SMT file
(define smt-check-sat
(lambda ()
(newline)
(display '(check-sat))
(newline)))
; insert the get-model command in the resulting SMT file
(define smt-get-model
(lambda ()
(newline)
(display '(get-model))
(newline)))