blob: e91ef36c2527422088897ca273e02a6c01453f44 (
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
|
(set-logic AUFLIA)
(set-info :status unsat)
;; don't use a datatypes for currently focusing in uf
(declare-sort elt 0)
(declare-fun R (elt elt) Bool)
;; reflexive
(assert-rewrite ((x elt)) () (R x x) true ())
;; transitive
(assert-propagation ((x elt) (y elt) (z elt)) () ((R x y) (R y z)) (R x z) ())
;; anti-symmetric
(assert-propagation ((x elt) (y elt)) () ((R x y) (R y x)) (= x y) ())
(declare-fun f (elt) elt)
(assert-propagation ((x elt)(y elt)) () ((R (f x) (f y))) (R x y) ())
(declare-fun e1 () elt)
(declare-fun e2 () elt)
(declare-fun e3 () elt)
(declare-fun e4 () elt)
(declare-fun e5 () elt)
(assert (not (=> (and (R e1 e2) (R e3 (f e4)) (R e4 e5)
(or (and (= e3 (f e2)) (= e4 e1))
(and (= e4 e2) (= e5 e1)) )
) (= e1 e2))))
(check-sat)
(exit)
|
