blob: d3e54e0af6a2aafabca2fb171a16ade77caa5372 (
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
|
; COMMAND-LINE: --quant-ind --conjecture-gen
; EXPECT: unsat
(set-logic UFDTLIA)
(set-info :status unsat)
(declare-datatypes ((Nat 0)) (((succ (pred Nat)) (zero))
))
(declare-datatypes ((Lst 0)) (((cons (head Nat) (tail Lst)) (nil))
))
(declare-datatypes ((Tree 0)) (((node (data Nat) (left Tree) (right Tree)) (leaf))
))
(declare-datatypes ((Pair 0)(ZLst 0)) (((mkpair (first Nat) (second Nat)))
((zcons (zhead Pair) (ztail ZLst)) (znil))
))
(declare-fun P (Nat) Bool)
(declare-fun f (Nat) Nat)
(declare-fun less (Nat Nat) Bool)
(declare-fun plus (Nat Nat) Nat)
(declare-fun minus (Nat Nat) Nat)
(declare-fun mult (Nat Nat) Nat)
(declare-fun nmax (Nat Nat) Nat)
(declare-fun nmin (Nat Nat) Nat)
(declare-fun nat-to-int (Nat) Int)
(declare-fun append (Lst Lst) Lst)
(declare-fun len (Lst) Nat)
(declare-fun drop (Nat Lst) Lst)
(declare-fun take (Nat Lst) Lst)
(declare-fun count (Nat Lst) Nat)
(declare-fun last (Lst) Nat)
(declare-fun butlast (Lst) Lst)
(declare-fun mem (Nat Lst) Bool)
(declare-fun delete (Nat Lst) Lst)
(declare-fun rev (Lst) Lst)
(declare-fun lmap (Lst) Lst)
(declare-fun filter (Lst) Lst)
(declare-fun dropWhile (Lst) Lst)
(declare-fun takeWhile (Lst) Lst)
(declare-fun ins1 (Nat Lst) Lst)
(declare-fun insort (Nat Lst) Lst)
(declare-fun sorted (Lst) Bool)
(declare-fun sort (Lst) Lst)
(declare-fun zip (Lst Lst) ZLst)
(declare-fun zappend (ZLst ZLst) ZLst)
(declare-fun zdrop (Nat ZLst) ZLst)
(declare-fun ztake (Nat ZLst) ZLst)
(declare-fun zrev (ZLst) ZLst)
(declare-fun mirror (Tree) Tree)
(declare-fun height (Tree) Nat)
(define-fun leq ((x Nat) (y Nat)) Bool (or (= x y) (less x y)))
(assert (forall ((x Nat)) (>= (nat-to-int x) 0) ))
(assert (forall ((x Nat) (y Nat)) (=> (= (nat-to-int x) (nat-to-int y)) (= x y)) ))
(assert (= (nat-to-int zero) 0))
(assert (forall ((x Nat)) (= (nat-to-int (succ x)) (+ 1 (nat-to-int x))) ))
(assert (forall ((x Nat)) (= (less x zero) false) ))
(assert (forall ((x Nat)) (= (less zero (succ x)) true) ))
(assert (forall ((x Nat) (y Nat)) (= (less (succ x) (succ y)) (less x y)) ))
(assert (forall ((x Nat) (y Nat)) (= (less x y) (< (nat-to-int x) (nat-to-int y))) ))
(assert (= (len nil) zero))
(assert (forall ((x Nat) (y Lst)) (= (len (cons x y)) (succ (len y))) ))
(assert (forall ((i Nat)) (= (insort i nil) (cons i nil)) ))
(assert (forall ((i Nat) (x Nat) (y Lst)) (= (insort i (cons x y)) (ite (less i x) (cons i (cons x y)) (cons x (insort i y)))) ))
(assert (= (sort nil) nil))
(assert (forall ((x Nat) (y Lst)) (= (sort (cons x y)) (insort x (sort y))) ))
(assert (not (forall ((l Lst)) (= (len (sort l)) (len l)) )))
(check-sat)
(exit)
|
