silicon/src/main/resources/predicate_snap_functions_axioms.smt2 at 494401db0cdfec803c2f46c30d63b7ba203e5b26 · lfwa/silicon · GitHub

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
; This Source Code Form is subject to the terms of the Mozilla Public
; License, v. 2.0. If a copy of the MPL was not distributed with this
; file, You can obtain one at http://mozilla.org/MPL/2.0/.

; The axioms are parametric
;   - $PRD$ is a Silver predicate name
;   - $S$ is the sort corresponding to the type of the field

; ATTENTION: The triggers mention the sort wrappers introduced for PSFs.
; The axiom therefore needs to be emitted after the sort wrappers have
; been emitted.

(assert (forall ((vs $PSF<$S$>) (ws $PSF<$S$>)) (!
    (=>
      (and
        (Set_equal ($PSF.domain_$PRD$ vs) ($PSF.domain_$PRD$ ws))
        (forall ((x $Snap)) (!
          (=>
            (Set_in x ($PSF.domain_$PRD$ vs))
            (= ($PSF.lookup_$PRD$ vs x) ($PSF.lookup_$PRD$ ws x)))
          ; :pattern ((Set_in x ($PSF.domain_$PRD$ vs)))
          :pattern (($PSF.lookup_$PRD$ vs x) ($PSF.lookup_$PRD$ ws x))
          :qid |qp.$PSF<$S$>-eq-inner|
          )))
      (= vs ws))
    :pattern (($SortWrappers.$PSF<$S$>To$Snap vs)
              ($SortWrappers.$PSF<$S$>To$Snap ws)
;              ($PSF.after_$PRD$ vs ws)
              )
    :qid |qp.$PSF<$S$>-eq-outer|
    )))

(assert (forall ((s $Snap) (pm $PPM)) (!
    ($Perm.isValidVar ($PSF.perm_$PRD$ pm s))
    :pattern (($PSF.perm_$PRD$ pm s))))) ; ensure :pattern ((f x)) instead of pattern (f x) since pattern must a be a list.

(assert (forall ((s $Snap) (f $S$)) (!
    (= ($PSF.loc_$PRD$ f s) true)
    :pattern (($PSF.loc_$PRD$ f s))))) ; ensure :pattern ((f x)) instead of pattern (f x) since pattern must a be a list.