1 ; COMMAND-LINE: --rewrite-rules --quiet
2 ;; try to solve datatypes with rewriterules
7 (declare-sort elt 0) ;; we suppose that elt is infinite
10 (declare-fun nil1 () list)
11 (declare-fun nil2 () list)
12 (declare-fun cons (elt list) list)
17 (declare-fun inj1 (list) elt)
18 (assert (forall ((?e elt) (?l list))
19 (! (! (=> true (=> true (= (inj1 (cons ?e ?l)) ?e))) :pattern ((cons ?e ?l)) ) :rewrite-rule) ))
21 (declare-fun inj2 (list) list)
22 (assert (forall ((?e elt) (?l list))
23 (! (! (=> true (=> true (= (inj2 (cons ?e ?l)) ?l))) :pattern ((cons ?e ?l)) ) :rewrite-rule) ))
28 (declare-fun proj1 (list) elt)
29 (assert (forall ((?e elt) (?l list))
30 (! (= (proj1 (cons ?e ?l)) ?e) :rewrite-rule) ))
32 (declare-fun proj2 (list) list)
33 (assert (forall ((?e elt) (?l list))
34 (! (= (proj2 (cons ?e ?l)) ?l) :rewrite-rule) ))
38 (declare-fun iscons (list) Bool)
39 (assert (= (iscons nil1) false))
40 (assert (= (iscons nil2) false))
41 (assert (forall ((?e elt) (?l list))
42 (! (! (=> true (=> true (= (iscons (cons ?e ?l)) true))) :pattern ((cons ?e ?l)) ) :rewrite-rule) ))
44 (assert (forall ((?l list))
45 (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj1 ?l)) ) :rewrite-rule) ))
46 (assert (forall ((?l list))
47 (! (! (=> true (=> (iscons ?l) (= ?l (cons (proj1 ?l) (proj2 ?l))))) :pattern ((proj2 ?l)) ) :rewrite-rule) ))
50 (declare-fun isnil1 (list) Bool)
51 (assert (= (isnil1 nil1) true))
52 (assert (= (isnil1 nil2) false))
53 (assert (forall ((?e elt) (?l list))
54 (! (= (isnil1 (cons ?e ?l)) false) :rewrite-rule) ))
55 (assert (forall ((?l list))
56 (! (=> true (=> (isnil1 ?l) (= ?l nil1))) :rewrite-rule) ))
58 (declare-fun isnil2 (list) Bool)
59 (assert (= (isnil2 nil1) false))
60 (assert (= (isnil2 nil2) true))
61 (assert (forall ((?e elt) (?l list))
62 (! (= (isnil2 (cons ?e ?l)) false) :rewrite-rule) ))
63 (assert (forall ((?l list))
64 (! (=> true (=> (isnil2 ?l) (= ?l nil2))) :rewrite-rule) ))
67 (assert (forall ((?l list))
68 (! (=> (isnil1 ?l) (and (not (isnil2 ?l)) (not (iscons ?l))) ) :rewrite-rule) ))
70 (assert (forall ((?l list))
71 (! (=> (isnil2 ?l) (and (not (isnil1 ?l)) (not (iscons ?l))) ) :rewrite-rule) ))
73 (assert (forall ((?l list))
74 (! (=> (iscons ?l) (and (not (isnil1 ?l)) (not (isnil2 ?l))) ) :rewrite-rule) ))
79 (assert (forall ((?l list))
80 (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj1 ?l)) ) :rewrite-rule) ))
81 (assert (forall ((?l list))
82 (! (! (=> true (or (isnil1 ?l) (isnil2 ?l) (iscons ?l))) :pattern ((proj2 ?l)) ) :rewrite-rule) ))
86 (assert (forall ((?l list))
87 (! (=> (not (iscons ?l)) (or (isnil1 ?l) (isnil2 ?l))) :rewrite-rule) ))
93 (declare-fun e () elt)
94 (declare-fun l1 () list)
95 (declare-fun l2 () list)
98 (assert (not (=> (iscons l1) (=> (= (proj2 l1) (proj2 l2)) (= l1 (cons (proj1 l2) (proj2 l2)))))))