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
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; SMT syntax and semantics (not theory-specific)
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; depends on sat.plf
(declare formula type)
(declare th_holds (! f formula type))
; standard logic definitions
(declare true formula)
(declare false formula)
(define formula_op1
(! f formula
formula))
(define formula_op2
(! f1 formula
(! f2 formula
formula)))
(define formula_op3
(! f1 formula
(! f2 formula
(! f3 formula
formula))))
(declare not formula_op1)
(declare and formula_op2)
(declare or formula_op2)
(declare impl formula_op2)
(declare iff formula_op2)
(declare xor formula_op2)
(declare ifte formula_op3)
; terms
(declare sort type)
(declare term (! t sort type)) ; declared terms in formula
; standard definitions for =, ite, let and flet
(declare = (! s sort
(! x (term s)
(! y (term s)
formula))))
(declare ite (! s sort
(! f formula
(! t1 (term s)
(! t2 (term s)
(term s))))))
(declare let (! s sort
(! t (term s)
(! f (! v (term s) formula)
formula))))
(declare flet (! f1 formula
(! f2 (! v formula formula)
formula)))
; We view applications of predicates as terms of sort "Bool".
; Such terms can be injected as atomic formulas using "p_app".
(declare Bool sort) ; the special sort for predicates
(declare p_app (! x (term Bool) formula)) ; propositional application of term
; boolean terms
(declare t_true (term Bool))
(declare t_false (term Bool))
(declare t_t_neq_f
(th_holds (not (= Bool t_true t_false))))
(declare pred_eq_t
(! x (term Bool)
(! u (th_holds (p_app x))
(th_holds (= Bool x t_true)))))
(declare pred_eq_f
(! x (term Bool)
(! u (th_holds (not (p_app x)))
(th_holds (= Bool x t_false)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; CNF Clausification
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; binding between an LF var and an (atomic) formula
(declare atom (! v var (! p formula type)))
; binding between two LF vars
(declare bvatom (! sat_v var (! bv_v var type)))
(declare decl_atom
(! f formula
(! u (! v var
(! a (atom v f)
(holds cln)))
(holds cln))))
;; declare atom enhanced with mapping
;; between SAT prop variable and BVSAT prop variable
(declare decl_bvatom
(! f formula
(! u (! v var
(! bv_v var
(! a (atom v f)
(! bva (atom bv_v f)
(! vbv (bvatom v bv_v)
(holds cln))))))
(holds cln))))
; clausify a formula directly
(declare clausify_form
(! f formula
(! v var
(! a (atom v f)
(! u (th_holds f)
(holds (clc (pos v) cln)))))))
(declare clausify_form_not
(! f formula
(! v var
(! a (atom v f)
(! u (th_holds (not f))
(holds (clc (neg v) cln)))))))
(declare clausify_false
(! u (th_holds false)
(holds cln)))
(declare th_let_pf
(! f formula
(! u (th_holds f)
(! u2 (! v (th_holds f) (holds cln))
(holds cln)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; Natural deduction rules : used for CNF
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; for eager bit-blasting
(declare iff_symm
(! f formula
(th_holds (iff f f))))
;; contradiction
(declare contra
(! f formula
(! r1 (th_holds f)
(! r2 (th_holds (not f))
(th_holds false)))))
; truth
(declare truth (th_holds true))
;; not not
(declare not_not_intro
(! f formula
(! u (th_holds f)
(th_holds (not (not f))))))
(declare not_not_elim
(! f formula
(! u (th_holds (not (not f)))
(th_holds f))))
;; or elimination
(declare or_elim_1
(! f1 formula
(! f2 formula
(! u1 (th_holds (not f1))
(! u2 (th_holds (or f1 f2))
(th_holds f2))))))
(declare or_elim_2
(! f1 formula
(! f2 formula
(! u1 (th_holds (not f2))
(! u2 (th_holds (or f1 f2))
(th_holds f1))))))
(declare not_or_elim
(! f1 formula
(! f2 formula
(! u2 (th_holds (not (or f1 f2)))
(th_holds (and (not f1) (not f2)))))))
;; and elimination
(declare and_elim_1
(! f1 formula
(! f2 formula
(! u (th_holds (and f1 f2))
(th_holds f1)))))
(declare and_elim_2
(! f1 formula
(! f2 formula
(! u (th_holds (and f1 f2))
(th_holds f2)))))
(declare not_and_elim
(! f1 formula
(! f2 formula
(! u2 (th_holds (not (and f1 f2)))
(th_holds (or (not f1) (not f2)))))))
;; impl elimination
(declare impl_intro (! f1 formula
(! f2 formula
(! i1 (! u (th_holds f1)
(th_holds f2))
(th_holds (impl f1 f2))))))
(declare impl_elim
(! f1 formula
(! f2 formula
(! u2 (th_holds (impl f1 f2))
(th_holds (or (not f1) f2))))))
(declare not_impl_elim
(! f1 formula
(! f2 formula
(! u (th_holds (not (impl f1 f2)))
(th_holds (and f1 (not f2)))))))
;; iff elimination
(declare iff_elim_1
(! f1 formula
(! f2 formula
(! u1 (th_holds (iff f1 f2))
(th_holds (or (not f1) f2))))))
(declare iff_elim_2
(! f1 formula
(! f2 formula
(! u1 (th_holds (iff f1 f2))
(th_holds (or f1 (not f2)))))))
(declare not_iff_elim
(! f1 formula
(! f2 formula
(! u2 (th_holds (not (iff f1 f2)))
(th_holds (iff f1 (not f2)))))))
; xor elimination
(declare xor_elim_1
(! f1 formula
(! f2 formula
(! u1 (th_holds (xor f1 f2))
(th_holds (or (not f1) (not f2)))))))
(declare xor_elim_2
(! f1 formula
(! f2 formula
(! u1 (th_holds (xor f1 f2))
(th_holds (or f1 f2))))))
(declare not_xor_elim
(! f1 formula
(! f2 formula
(! u2 (th_holds (not (xor f1 f2)))
(th_holds (iff f1 f2))))))
;; ite elimination
(declare ite_elim_1
(! a formula
(! b formula
(! c formula
(! u2 (th_holds (ifte a b c))
(th_holds (or (not a) b)))))))
(declare ite_elim_2
(! a formula
(! b formula
(! c formula
(! u2 (th_holds (ifte a b c))
(th_holds (or a c)))))))
(declare ite_elim_3
(! a formula
(! b formula
(! c formula
(! u2 (th_holds (ifte a b c))
(th_holds (or b c)))))))
(declare not_ite_elim_1
(! a formula
(! b formula
(! c formula
(! u2 (th_holds (not (ifte a b c)))
(th_holds (or (not a) (not b))))))))
(declare not_ite_elim_2
(! a formula
(! b formula
(! c formula
(! u2 (th_holds (not (ifte a b c)))
(th_holds (or a (not c))))))))
(declare not_ite_elim_3
(! a formula
(! b formula
(! c formula
(! u2 (th_holds (not (ifte a b c)))
(th_holds (or (not b) (not c))))))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;
; For theory lemmas
; - make a series of assumptions and then derive a contradiction (or false)
; - then the assumptions yield a formula like "v1 -> v2 -> ... -> vn -> false"
; - In CNF, it becomes a clause: "~v1, ~v2, ..., ~vn"
;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare ast
(! v var
(! f formula
(! C clause
(! r (atom v f) ;this is specified
(! u (! o (th_holds f)
(holds C))
(holds (clc (neg v) C))))))))
(declare asf
(! v var
(! f formula
(! C clause
(! r (atom v f)
(! u (! o (th_holds (not f))
(holds C))
(holds (clc (pos v) C))))))))
;; Bitvector lemma constructors to assume
;; the unit clause containing the assumptions
;; it also requires the mapping between bv_v and v
;; The resolution proof proving false will use bv_v as the definition clauses use bv_v
;; but the Problem clauses in the main SAT solver will use v so the learned clause is in terms of v
(declare bv_asf
(! v var
(! bv_v var
(! f formula
(! C clause
(! r (atom v f) ;; passed in
(! x (bvatom v bv_v) ; establishes the equivalence of v to bv_
(! u (! o (holds (clc (neg bv_v) cln)) ;; l binding to be used in proof
(holds C))
(holds (clc (pos v) C))))))))))
(declare bv_ast
(! v var
(! bv_v var
(! f formula
(! C clause
(! r (atom v f) ; this is specified
(! x (bvatom v bv_v) ; establishes the equivalence of v to bv_v
(! u (! o (holds (clc (pos bv_v) cln))
(holds C))
(holds (clc (neg v) C))))))))))
;; Example:
;;
;; Given theory literals (F1....Fn), and an input formula A of the form (th_holds (or F1 (or F2 .... (or F{n-1} Fn))))).
;;
;; We introduce atoms (a1,...,an) to map boolean literals (v1,...,vn) top literals (F1,...,Fn).
;; Do this at the beginning of the proof:
;;
;; (decl_atom F1 (\ v1 (\ a1
;; (decl_atom F2 (\ v2 (\ a2
;; ....
;; (decl_atom Fn (\ vn (\ an
;;
;; A is then clausified by the following proof:
;;
;;(satlem _ _
;;(asf _ _ _ a1 (\ l1
;;(asf _ _ _ a2 (\ l2
;;...
;;(asf _ _ _ an (\ ln
;;(clausify_false
;;
;; (contra _
;; (or_elim_1 _ _ l{n-1}
;; ...
;; (or_elim_1 _ _ l2
;; (or_elim_1 _ _ l1 A))))) ln)
;;
;;))))))) (\ C
;;
;; We now have the free variable C, which should be the clause (v1 V ... V vn).
;;
;; Polarity of literals should be considered, say we have A of the form (th_holds (or (not F1) (or F2 (not F3)))).
;; Where necessary, we use "ast" instead of "asf", introduce negations by "not_not_intro" for pattern matching, and flip
;; the arguments of contra:
;;
;;(satlem _ _
;;(ast _ _ _ a1 (\ l1
;;(asf _ _ _ a2 (\ l2
;;(ast _ _ _ a3 (\ l3
;;(clausify_false
;;
;; (contra _ l3
;; (or_elim_1 _ _ l2
;; (or_elim_1 _ _ (not_not_intro l1) A))))
;;
;;))))))) (\ C
;;
;; C should be the clause (~v1 V v2 V ~v3 )
|
