blob: 76c77d60a53ff973705e925c5486570c1afe601a (
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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
; -------------------------------------------------------------------------
; Boogie universal background predicate
; Copyright (c) 2004-2006, Microsoft Corp.
:logic AUFLIA
:category { industrial }
:extrasorts ( boogieU )
:extrasorts ( boogieT )
:extrasorts ( TermBool )
:extrafuns (( boolTrue TermBool ))
:extrafuns (( boolFalse TermBool ))
:extrafuns (( boolIff TermBool TermBool TermBool ))
:extrafuns (( boolImplies TermBool TermBool TermBool ))
:extrafuns (( boolAnd TermBool TermBool TermBool ))
:extrafuns (( boolOr TermBool TermBool TermBool ))
:extrafuns (( boolNot TermBool TermBool ))
:extrafuns (( UEqual boogieU boogieU TermBool ))
:extrafuns (( TEqual boogieT boogieT TermBool ))
:extrafuns (( IntEqual Int Int TermBool ))
:extrafuns (( intLess Int Int TermBool ))
:extrafuns (( intAtMost Int Int TermBool ))
:extrafuns (( intGreater Int Int TermBool ))
:extrafuns (( intAtLeast Int Int TermBool ))
:extrafuns (( boogieIntMod Int Int Int ))
:extrafuns (( boogieIntDiv Int Int Int ))
; used for translation with type premisses
:extrapreds (( UOrdering2 boogieU boogieU ))
; used for translation with type arguments
:extrapreds (( UOrdering3 boogieT boogieU boogieU ))
; used for translation with type premisses
:extrafuns (( TermUOrdering2 boogieU boogieU TermBool ))
; used for translation with type arguments
:extrafuns (( TermUOrdering3 boogieT boogieU boogieU TermBool ))
; formula/term axioms
:assumption
(forall (?x TermBool) (?y TermBool)
(iff
(= (boolIff ?x ?y) boolTrue)
(iff (= ?x boolTrue) (= ?y boolTrue))))
:assumption
(forall (?x TermBool) (?y TermBool)
(iff
(= (boolImplies ?x ?y) boolTrue)
(implies (= ?x boolTrue) (= ?y boolTrue))))
:assumption
(forall (?x TermBool) (?y TermBool)
(iff
(= (boolAnd ?x ?y) boolTrue)
(and (= ?x boolTrue) (= ?y boolTrue))))
:assumption
(forall (?x TermBool) (?y TermBool)
(iff
(= (boolOr ?x ?y) boolTrue)
(or (= ?x boolTrue) (= ?y boolTrue))))
:assumption
(forall (?x TermBool)
(iff
(= (boolNot ?x) boolTrue)
(not (= ?x boolTrue)))
:pat { (boolNot ?x) }
)
:assumption
(forall (?x boogieU) (?y boogieU)
(iff
(= (UEqual ?x ?y) boolTrue)
(= ?x ?y)))
:assumption
(forall (?x boogieT) (?y boogieT)
(iff
(= (TEqual ?x ?y) boolTrue)
(= ?x ?y)))
:assumption
(forall (?x Int) (?y Int)
(iff
(= (IntEqual ?x ?y) boolTrue)
(= ?x ?y)))
:assumption
(forall (?x Int) (?y Int)
(iff
(= (intLess ?x ?y) boolTrue)
(< ?x ?y)))
:assumption
(forall (?x Int) (?y Int)
(iff
(= (intAtMost ?x ?y) boolTrue)
(<= ?x ?y)))
:assumption
(forall (?x Int) (?y Int)
(iff
(= (intAtLeast ?x ?y) boolTrue)
(>= ?x ?y)))
:assumption
(forall (?x Int) (?y Int)
(iff
(= (intGreater ?x ?y) boolTrue)
(> ?x ?y)))
; false is not true
:assumption
(distinct boolFalse boolTrue)
:assumption
(forall (?x boogieU) (?y boogieU)
(iff
(= (TermUOrdering2 ?x ?y) boolTrue)
(UOrdering2 ?x ?y)))
:assumption
(forall (?x boogieT) (?y boogieU) (?z boogieU)
(iff
(= (TermUOrdering3 ?x ?y ?z) boolTrue)
(UOrdering3 ?x ?y ?z)))
; End Boogie universal background predicate
; -------------------------------------------------------------------------
|
