forked from gowthamk/z3-hacks
-
Notifications
You must be signed in to change notification settings - Fork 0
/
interpolant_rmem.z3
36 lines (36 loc) · 2.12 KB
/
interpolant_rmem.z3
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
(set-option :auto-config false)
(set-option :smt.mbqi true)
(set-option :smt.macro-finder true)
(set-option :produce-interpolants true)
(declare-sort T0)
(declare-const l1 T0)
(declare-const l2 T0)
(declare-const v T0)
(declare-sort T1)
(declare-const z1 T1)
(declare-const z2 T1)
(declare-const z3 T1)
(declare-fun Rmem (T0 T1) Bool)
(declare-const phi1 Bool)
(declare-const phi2 Bool)
(declare-const assn1 Bool)
(declare-const assn2 Bool)
;; A fact: \forall x. (Rmem(l1) = {x}) => (Rmem(v) = {x} \union Rmem(l2))
(assert (! (= phi1 (forall ((x T1))
(=> (forall ((bv0 T1)) (= (Rmem l1 bv0) (= bv0 x)))
(forall ((bv0 T1)) (= (Rmem v bv0)
(or (Rmem l2 bv0) (= bv0 x))))))) :named f1))
;; An observation: When (Rmem(l1) = {z1}) and (Rmem(l2)= {z2,z3}), then
;; Rmem(v) was observed to be {z1,z2,z3}
(assert (! (= phi2 (! (=> (and (forall ((bv0 T1))
(= (Rmem l1 bv0) (= bv0 z1)))
(forall ((bv0 T1))
(= (Rmem l2 bv0) (or (= bv0 z2) (= bv0 z3)))))
(forall ((bv0 T1))
(= (Rmem v bv0) (or (= bv0 z1) (= bv0 z2)
(= bv0 z3))))))) :named f2))
(assert (= assn2 (and phi1 (not phi2))))
(assert assn2)
(check-sat)
;; Can Z3 derive the invariant in terms of Rmem(v), Rmem(l1) and Rmem(l2)?
(get-interpolant f1 f2)