blob: d1d88a5494f8e8fc928450c35d0ca128c62c9df9 (
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
|
;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba
(set-logic AUFLIA)
(set-info :status sat)
(declare-sort elt1 0)
(declare-sort elt2 0)
(declare-fun g (elt2) Bool)
(declare-fun p (elt1 elt1) Bool)
(declare-fun f (elt2) elt1)
(declare-fun c1 () elt1)
(declare-fun c2 () elt1)
(assert (forall ((?e elt2)) (! (=> (g ?e) (= (f ?e) c2)) :rewrite-rule)))
(assert (forall ((?e elt2)) (! (=> (g ?e) (= (f ?e) c1)) :rewrite-rule)))
(declare-fun e () elt2)
(assert (not (=> (g e) (=> (p c1 c2) (p (f e) (f e)))) ))
(check-sat)
(exit)
|
