blob: b5bc63d92fd7efd68bc5cbbcb916ebb5846b6a2c (
plain)
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
|
(declare forall (! s sort
(! t (term s)
(! f formula
formula))))
;This program recursively checks the instantiation.
;Composite terms (such as "apply _ _ ...") are handled recursively.
;Then, if ti and t are equal, we return true. Otherwise, we first verify that t is the variable for which ti is substitued (ifmarked). if this is the case, ti should be equal to k.
(program is_inst_t ((ti term) (t term) (k term)) bool
(match t
((apply s1 s2 t1 t2)
(match ti
((apply si1 si2 ti1 ti2)
(match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))
(default ff)))
((a_var_bv n v) (ifequal ti t tt (ifmarked v (ifequal ti k tt ff) ff)))
(default (ifequal ti t tt (ifmarked t (ifequal ti k tt ff) ff)))))
(program is_inst_f ((fi formula) (f formula) (k term)) bool
(match f
((and f1 f2) (match fi
((and fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
(default ff)))
((or f1 f2) (match fi
((or fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
(default ff)))
((impl f1 f2) (match fi
((impl fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
(default ff)))
((not f1) (match fi
((not fi1) (is_inst_f fi1 f1 k))
(default ff)))
((iff f1 f2) (match fi
((iff fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
(default ff)))
((xor f1 f2) (match fi
((xor fi1 fi2) (match (is_inst_f fi1 f1 k) (tt (is_inst_f fi2 f2 k)) (ff ff)))
(default ff)))
((ifte f1 f2 f3) (match fi
((ifte fi1 fi2 fi3) (match (is_inst_f fi1 f1 k)
(tt (match (is_inst_f fi2 f2 k) (tt (is_inst_f fi3 f3 k)) (ff ff)))
(ff ff)))
(default ff)))
((= s t1 t2) (match fi
((= s ti1 ti2) (match (is_inst_t ti1 t1 k) (tt (is_inst_t ti2 t2 k)) (ff ff)))
(default ff)))
((forall s t1 f1) (match fi
((forall s ti1 fi1) (is_inst_f fi1 f1 k))
(default ff)))
(default ff)))
(program is_inst ((fi formula) (f formula) (t term) (k term)) bool
(match t
((a_var_bv n v) (do (markvar v)
(let f1 (is_inst_f fi f k)
(do (markvar v) f1))))
(default (do (markvar t)
(let f1 (is_inst_f fi f k)
(do (markvar t) f1))))
)
)
(declare skolem
(! s sort
(! t (term s)
(! f formula
(! p (th_holds (not (forall s t f)))
(! u (! k (term s)
(! fi formula
(! p1 (th_holds (not fi))
(! r (^ (is_inst fi f t k) tt)
(holds cln)))))
(holds cln)))))))
(declare inst
(! s sort
(! t (term s)
(! f formula
(! k (term s)
(! fi formula
(! p (th_holds (forall s t f))
(! r (^ (is_inst fi f t k) tt)
(! u (! p1 (th_holds fi)
(holds cln))
(holds cln))))))))))
|
