blob: 4fe8221abf836fc0e873a5cb02c8065478fac121 (
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
|
; EXPECT: unsat
(set-logic ALL)
(set-info :status unsat)
(declare-datatypes ((List 1)) ((par (T) ((cons (head T) (tail (List T))) (nil)))))
(declare-datatypes ((KV 0)) (((kv (key Int) (value Int)) (nilKV))))
(declare-fun mapper ((List Int)) (List KV))
(assert
(forall
((input (List Int)))
(ite
(= input (as nil (List Int)))
(= (as nil (List KV)) (mapper input))
(= (cons (kv 0 (head input)) (mapper (tail input))) (mapper input))
)
)
)
(declare-fun reduce ((List KV)) Int)
(assert
(forall
((inputk (List KV)))
(ite
(= inputk (as nil (List KV)))
(= 0 (reduce inputk))
(= (+ (value (head inputk)) (reduce (tail inputk))) (reduce inputk))
)
)
)
(declare-fun sum ((List Int)) Int)
(assert
(forall
((input (List Int)))
(ite
(= input (as nil (List Int)))
(= 0 (sum input))
(= (+ (head input) (sum (tail input))) (sum input))
)
)
)
(assert
(not (= (sum (cons 0 (as nil (List Int)))) (reduce (mapper (cons 0 (as nil (List Int)))))))
)
(check-sat)
|
