1; COMMAND-LINE: --rewrite-rules
2(set-logic AUFLIRA)
3
4;; DATATYPE
5;;   nat = succ(pred : nat) | zero,
6;;   list = cons(car : tree, cdr : list) | null,
7;;   tree = node(children : list) | leaf(data : nat)
8;; END;
9
10;;;;;;;;;;;
11;; nat   ;;
12;;;;;;;;;;;
13(declare-sort nat 0)
14(declare-fun zero () nat)
15(declare-fun succ (nat) nat)
16
17;;;;;;;;;;;;;;;;
18;; injective
19
20(declare-fun inj1 (nat) nat)
21(assert (forall ((?x1 nat))
22                (! (= (inj1 (succ ?x1)) ?x1) :pattern ((succ ?x1)) ) ))
23
24
25;;;;;;;;;;;;;;;;;;;;
26;; projection
27
28(declare-fun pred (nat) nat)
29(assert (forall ((?x1 nat))
30                (! (= (pred (succ ?x1)) ?x1) :pattern ((pred (succ ?x1))) ) ))
31
32(assert (= (pred zero) zero))
33
34;;;;;;;;;;;;;;;;;;;
35;; test
36(declare-fun is_succ (nat) Bool)
37(assert (= (is_succ zero) false))
38(assert (forall ((?x1 nat))
39                (! (= (is_succ (succ ?x1)) true) :pattern ((succ ?x1)) ) ))
40
41(assert (forall ((?x1 nat))
42                (! (=> (is_succ ?x1) (= ?x1 (succ (pred ?x1)))) :pattern ((is_succ ?x1) (pred ?x1)) ) ))
43
44(declare-fun is_zero (nat) Bool)
45(assert (= (is_zero zero) true))
46(assert (forall ((?x1 nat))
47                (! (=> (is_zero ?x1) (= ?x1 zero)) :pattern ((is_zero ?x1)) ) ))
48
49;;; directrr
50(assert (forall ((?x1 nat))
51                (! (= (is_succ (succ ?x1)) true) :pattern ((is_succ (succ ?x1))) ) ))
52(assert (forall ((?x1 nat))
53                (! (= (is_zero (succ ?x1)) false) :pattern ((is_zero (succ ?x1))) )))
54
55
56;;;;;;;;;;;;;;;;;;;;
57;; distinct
58(assert (forall ((?x1 nat))
59                (! (=> (is_zero ?x1) (not (is_succ ?x1)) ) :pattern ((is_zero ?x1)) ) ))
60(assert (forall ((?x1 nat))
61                (! (=> (is_succ ?x1) (not (is_zero ?x1)) ) :pattern ((is_succ ?x1)) ) ))
62(assert (forall ((?x1 nat))
63                (! (=> (not (is_zero ?x1)) (is_succ ?x1) ) :pattern ((is_zero ?x1)) ) ))
64(assert (forall ((?x1 nat))
65                (! (=> (not (is_succ ?x1)) (is_zero ?x1) ) :pattern ((is_succ ?x1)) ) ))
66
67;;;;;;;;;;;;;;;;;;;
68;; case-split
69(assert (forall ((?x1 nat))
70                (! (or (is_zero ?x1) (is_succ ?x1)) :pattern ((pred ?x1)) ) ))
71
72;;;;;;;;;;;;;;;;;;;
73;; non-cyclic
74(declare-fun size_nat (nat) Real)
75(assert (forall ((?x1 nat))
76                (! (> (size_nat (succ ?x1)) (size_nat ?x1)) :pattern ((succ ?x1)) ) ))
77
78
79
80;;;;;;;;;;;;;;;;;;;;;
81;; list and tree
82
83(declare-sort list 0)
84(declare-sort tree 0)
85
86;;;;;;;;;;;
87;; list  ;;
88;;;;;;;;;;;
89
90(declare-fun null () list)
91(declare-fun cons (tree list) list)
92
93(declare-fun node (list) tree)
94(declare-fun leaf (nat) tree)
95
96;;;;;;;;;;;;;;;;
97;; injective
98
99(declare-fun inj2 (list) tree)
100(assert (forall ((?x1 tree) (?x2 list))
101                (! (= (inj2 (cons ?x1 ?x2)) ?x1) :pattern ((cons ?x1 ?x2)) ) ))
102
103(declare-fun inj3 (list) list)
104(assert (forall ((?x1 tree) (?x2 list))
105                (! (= (inj3 (cons ?x1 ?x2)) ?x2) :pattern ((cons ?x1 ?x2)) ) ))
106
107
108;;;;;;;;;;;;;;;;;;;;
109;; projection
110
111(declare-fun car (list) tree)
112(assert (forall ((?x1 tree) (?x2 list))
113                (! (= (car (cons ?x1 ?x2)) ?x1) :pattern ((car (cons ?x1 ?x2))) ) ))
114
115(assert (= (car null) (node null)))
116
117(declare-fun cdr (list) list)
118(assert (forall ((?x1 tree) (?x2 list))
119                (! (= (cdr (cons ?x1 ?x2)) ?x2) :pattern ((cdr (cons ?x1 ?x2))) ) ))
120
121(assert (= (cdr null) null))
122
123;;;;;;;;;;;;;;;;;;;
124;; test
125(declare-fun is_cons (list) Bool)
126(assert (= (is_cons null) false))
127(assert (forall ((?x1 tree) (?x2 list))
128                (! (= (is_cons (cons ?x1 ?x2)) true) :pattern ((cons ?x1 ?x2)) ) ))
129
130(assert (forall ((?x1 list))
131                (! (=> (is_cons ?x1) (= ?x1 (cons (car ?x1) (cdr ?x1)))) :pattern ((is_cons ?x1)(car ?x1)) ) ))
132(assert (forall ((?x1 list))
133                (! (=> (is_cons ?x1) (= ?x1 (cons (car ?x1) (cdr ?x1)))) :pattern ((is_cons ?x1)(cdr ?x1)) ) ))
134
135(declare-fun is_null (list) Bool)
136(assert (= (is_null null) true))
137
138(assert (forall ((?x1 list))
139                (! (=> (is_null ?x1) (= (car ?x1) (node null))) :pattern ((is_null ?x1)(car ?x1)) )  ))
140(assert (forall ((?x1 list))
141                (! (=> (is_null ?x1) (= (cdr ?x1) null)) :pattern ((is_null ?x1)(cdr ?x1)) ) ))
142
143(assert (forall ((?x1 list))
144                (! (=> (is_null ?x1) (= ?x1 null)) :pattern ((is_null ?x1)) ) ))
145
146;;; directrr
147(assert (forall ((?x1 tree) (?x2 list))
148                (! (= (is_cons (cons ?x1 ?x2)) true) :pattern ((is_cons (cons ?x1 ?x2))) ) ))
149(assert (forall ((?x1 tree) (?x2 list))
150                (! (= (is_null (cons ?x1 ?x2)) false) :pattern ((is_null (cons ?x1 ?x2))) ) ))
151
152
153
154;;;;;;;;;;;;;;;;;;;;
155;; distinct
156(assert (forall ((?x1 list))
157                (! (=> (is_null ?x1) (not (is_cons ?x1)) ) :pattern ((is_null ?x1)) ) ))
158(assert (forall ((?x1 list))
159                (! (=> (is_cons ?x1) (not (is_null ?x1)) ) :pattern ((is_cons ?x1)) ) ))
160(assert (forall ((?x1 list))
161                (! (=> (not (is_null ?x1)) (is_cons ?x1) ) :pattern ((is_null ?x1)) ) ))
162(assert (forall ((?x1 list))
163                (! (=> (not (is_cons ?x1)) (is_null ?x1) ) :pattern ((is_cons ?x1)) ) ))
164
165;;;;;;;;;;;;;;;;;;;
166;; case-split
167(assert (forall ((?x1 list))
168            (!  (or (is_null ?x1) (is_cons ?x1)) :pattern ((car ?x1)) ) ))
169(assert (forall ((?x1 list))
170            (! (or (is_null ?x1) (is_cons ?x1)) :pattern ((cdr ?x1)) ) ))
171
172;;;;;;;;;;;;;;;
173;; tree
174
175;;;;;;;;;;;;;;;;
176;; injective
177
178(declare-fun inj4 (tree) list)
179(assert (forall ((?x1 list))
180                (! (= (inj4 (node ?x1)) ?x1) :pattern ((node ?x1)) ) ))
181
182(declare-fun inj5 (tree) nat)
183(assert (forall ((?x1 nat))
184                (!  (= (inj5 (leaf ?x1)) ?x1) :pattern ((leaf ?x1)) )  ))
185
186
187;;;;;;;;;;;;;;;;;;;;
188;; projection
189
190(declare-fun children (tree) list)
191(assert (forall ((?x1 list))
192                (! (= (children (node ?x1)) ?x1) :pattern ((children (node ?x1))) ) ))
193(assert (forall ((?x1 nat))
194                (! (= (children (leaf ?x1)) null) :pattern ((children (leaf ?x1))) ) ))
195
196
197(declare-fun data (tree) nat)
198(assert (forall ((?x1 nat))
199                (! (= (data (leaf ?x1)) ?x1) :pattern ((data (leaf ?x1))) ) ))
200(assert (forall ((?x1 list))
201                (! (= (data (node ?x1)) zero) :pattern ((data (node ?x1))) ) ))
202
203;;;;;;;;;;;;;;;;;;;
204;; test
205(declare-fun is_node (tree) Bool)
206(assert (forall ((?x1 list))
207                (! (= (is_node (node ?x1)) true) :pattern ((node ?x1)) )  ))
208
209(assert (forall ((?x1 tree))
210                (! (=> (is_node ?x1) (= ?x1 (node (children ?x1)))) :pattern ((is_node ?x1)(children ?x1)) ) ))
211
212(assert (forall ((?x1 tree))
213                (! (=> (is_node ?x1) (= (data ?x1) zero)) :pattern ((is_node ?x1)(data ?x1)) ) ))
214
215
216(declare-fun is_leaf (tree) Bool)
217(assert (forall ((?x1 nat))
218                (! (=> true (= (is_leaf (leaf ?x1)) true)) :pattern ((leaf ?x1)) ) ))
219
220(assert (forall ((?x1 tree))
221                (! (=> (is_leaf ?x1) (= ?x1 (leaf (data ?x1)))) :pattern ((is_leaf ?x1)(data ?x1)) ) ))
222(assert (forall ((?x1 tree))
223                (! (=> (is_leaf ?x1) (= (children ?x1) null)) :pattern ((is_leaf ?x1)(children ?x1)) ) ))
224
225;;; directrr
226(assert (forall ((?x1 list))
227                (! (= (is_node (node ?x1)) true) :pattern ((is_node (node ?x1))) ) ))
228(assert (forall ((?x1 list))
229                (! (= (is_leaf (node ?x1)) false) :pattern ((is_leaf (node ?x1))) ) ))
230(assert (forall ((?x1 nat))
231                (! (= (is_leaf (leaf ?x1)) true) :pattern (is_leaf (leaf ?x1)) ) ))
232(assert (forall ((?x1 nat))
233                (! (= (is_node (leaf ?x1)) false) :pattern ((is_node (leaf ?x1))) ) ))
234
235
236;;;;;;;;;;;;;;;;;;;;
237;; distinct
238(assert (forall ((?x1 tree))
239                (! (=> (is_node ?x1) (not (is_leaf ?x1)) ) :pattern ((is_node ?x1)) ) ))
240(assert (forall ((?x1 tree))
241                (! (=> (is_leaf ?x1) (not (is_node ?x1)) ) :pattern ((is_leaf ?x1)) ) ))
242(assert (forall ((?x1 tree))
243                (! (=> (not (is_node ?x1)) (is_leaf ?x1) ) :pattern ((is_node ?x1)) ) ))
244(assert (forall ((?x1 tree))
245                (! (=> (not (is_leaf ?x1)) (is_node ?x1) ) :pattern ((is_leaf ?x1)) ) ))
246
247;;;;;;;;;;;;;;;;;;;
248;; case-split
249(assert (forall ((?x1 tree))
250                (!  (or (is_node ?x1) (is_leaf ?x1)) :pattern ((children ?x1)) ) ))
251
252(assert (forall ((?x1 tree))
253                (! (or (is_node ?x1) (is_leaf ?x1)) :pattern ((data ?x1)) )  ))
254
255
256;;;;;;;;;;;;;;;;;;
257;; non-cyclic
258(declare-fun size_list (list) Real)
259(declare-fun size_tree (tree) Real)
260(assert (forall ((?x1 tree) (?x2 list))
261                (! (and (> (size_list (cons ?x1 ?x2)) (size_tree ?x1)) (> (size_list (cons ?x1 ?x2)) (size_list ?x2))) :pattern ((cons ?x1 ?x2)) ) ))
262(assert (forall ((?x1 list))
263                (! (> (size_tree (node ?x1)) (size_list ?x1)) :pattern ((node ?x1)) )  ))
264(assert (forall ((?x1 nat))
265                (! (> (size_tree (leaf ?x1)) (size_nat ?x1)) :pattern ((leaf ?x1)) ) ))
266