/
dllnull_len_split_dllrevs_num-2.sb.smt2
74 lines (60 loc) · 1.5 KB
/
dllnull_len_split_dllrevs_num-2.sb.smt2
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
(set-logic SHIDLIA)
(set-info :source | Songbird - https://songbird-prover.github.io/ |)
(set-info :smt-lib-version 2)
(set-info :category "crafted")
(set-info :status unsat)
;; singleton heap
(declare-sort Refnode 0)
(declare-datatypes
((node 0))
(((c_node (next Refnode) (prev Refnode)))))
(declare-heap (Refnode node))
;; heap predicates
(define-fun-rec dll_rev ((hd_7 Refnode) (p_8 Refnode) (tl_9 Refnode) (n_10 Refnode) (l_11 Int)) Bool
(or
(and
(pto hd_7 (c_node n_10 p_8))
(and
(= (- l_11 1) 0)
(= hd_7 tl_9)))
(exists
((x_12 Refnode) (k Int))
(and
(sep
(pto tl_9 (c_node n_10 x_12))
(dll_rev hd_7 p_8 x_12 tl_9 k))
(= k (- l_11 1))
(<= 1 (- l_11 1))))))
;; heap predicates
(define-fun-rec dllnull ((hd_7 Refnode) (p_8 Refnode) (l_9 Int)) Bool
(or
(and
(pto hd_7 (c_node (as nil Refnode) p_8))
(= (- l_9 1) 0))
(exists
((x_10 Refnode) (k Int))
(and
(sep
(pto hd_7 (c_node x_10 p_8))
(dllnull x_10 hd_7 k))
(= k (- l_9 1))
(<= 1 (- l_9 1))))))
(check-sat)
;; entailment: dllnull(x,y,n) & 100<=n |- (exists z,t,u,n1,n2. dll_rev(t,z,u,nil,n2) * dll_rev(x,y,z,t,n1) & n=n1+n2)
(declare-const x Refnode)
(declare-const y Refnode)
(declare-const n Int)
(assert
(and
(dllnull x y n)
(<= 100 n)))
(assert
(not
(exists
((z Refnode) (t Refnode) (u Refnode) (n1 Int) (n2 Int))
(and
(sep
(dll_rev t z u (as nil Refnode) n2)
(dll_rev x y z t n1))
(= n (+ n1 n2))))))
(check-sat)