blob: 7daf012e2c3a51ae4aff08d63a4a32caef5c9411 (
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
|
(set-logic QF_ALL_SUPPORTED)
(set-info :status unsat)
(declare-sort Loc 0)
(declare-const loc0 Loc)
(declare-datatypes ((Node 0)) (((node (data Int) (left Loc) (right Loc)))))
(declare-fun data0 () Node)
(declare-const dv Int)
(declare-const v Loc)
(declare-const dl Int)
(declare-const l Loc)
(declare-const dr Int)
(declare-const r Loc)
(define-fun ten-tree0 ((x Loc) (d Int)) Bool
(or (and (_ emp Loc Node) (= x (as sep.nil Loc))) (and (sep (pto x (node d l r)) (and (_ emp Loc Node) (= l (as sep.nil Loc))) (and (_ emp Loc Node) (= r (as sep.nil Loc)))) (= dl (- d 10)) (= dr (+ d 10)))))
(declare-const dy Int)
(declare-const y Loc)
(declare-const dz Int)
(declare-const z Loc)
(define-fun ord-tree0 ((x Loc) (d Int)) Bool
(or (and (_ emp Loc Node) (= x (as sep.nil Loc))) (and (sep (pto x (node d y z)) (and (_ emp Loc Node) (= y (as sep.nil Loc))) (and (_ emp Loc Node) (= z (as sep.nil Loc)))) (<= dy d) (<= d dz))))
;------- f -------
(assert (= y (as sep.nil Loc)))
(assert (= z (as sep.nil Loc)))
(assert (= dy dv))
(assert (= dz (+ dv 10)))
;-----------------
(assert (not (= v (as sep.nil Loc))))
(assert (ten-tree0 v dv))
(assert (not (ord-tree0 v dv)))
(check-sat)
|
