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
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
|
; Depends on th_real.plf, th_int.plf, smt.plf, sat.plf
; Some axiom arguments are marked "; Omit", because they can be deduced from
; other arguments and should be replaced with a "_" when invoking the axiom.
;; ====================================== ;;
;; Arith Terms, Predicates, & Conversions ;;
;; ====================================== ;;
; Types for arithmetic variables
; Specifically a real
(declare real_var type)
; Specifically an integer
(declare int_var type)
; Functions to map them to terms
(declare term_real_var (! v real_var (term Real)))
(declare term_int_var (! v int_var (term Int)))
; A function to cast an integer term to real.
(declare term_int_to_real (! i (term Int) (term Real)))
; The recursive functions `reify_int_term` and `reify_real_term` work
; together to reify or "make real" an integer term. That is, to convert it to
; a real term. More precisely, they take an integer term and return a real
; term in which any integer variables are immediately converted to real terms,
; and all non-leaves in the term are real-sorted.
;
; They explicitly do not work on integer division, because such a conversion
; would not be correct when integer division is involved.
; This function recursively converts an integer term to a real term.
(program reify_int_term ((t (term Int))) (term Real)
(match t
((term_int_var v) (term_int_to_real (term_int_var v)))
((a_int i) (a_real (mpz_to_mpq i)))
((+_Int x y) (+_Real (reify_int_term x) (reify_int_term y)))
((-_Int x y) (-_Real (reify_int_term x) (reify_int_term y)))
((u-_Int x) (u-_Real (reify_int_term x)))
((*_Int x y) (*_Real (reify_int_term x) (reify_int_term y)))
; Reifying integer division is an error, since it changes the value!
((/_Int x y) (fail (term Real)))
))
; This function recursively converts a real term to a real term.
; It will never change the top-level node in the term (since that node is
; real), but it may change subterms...
(program reify_real_term ((t (term Real))) (term Real)
(match t
((term_real_var v) (term_real_var v))
((a_real v) (a_real v))
; We've found an integer term -- reify it!
((term_int_to_real t') (reify_int_term t'))
((+_Real x y) (+_Real (reify_real_term x) (reify_real_term y)))
((-_Real x y) (-_Real (reify_real_term x) (reify_real_term y)))
((u-_Real x) (u-_Real (reify_real_term x)))
((*_Real x y) (*_Real (reify_real_term x) (reify_real_term y)))
((/_Real x y) (/_Real (reify_real_term x) (reify_real_term y)))
))
; Predicates of the form (term Integer) >= (term Real) or negations thereof
(declare >=_IntReal (! x (term Int) (! y (term Real) formula)))
; From an arith predicate, compute the equivalent real predicate
; All arith predicates are (possibly negated) >='s with a real on the right.
; Technically it's a real literal on the right, but we don't assume that here.
(program reify_arith_pred ((p formula)) formula
(match p
((not p') (not (reify_arith_pred p')))
((>=_Real x y) (>=_Real (reify_real_term x) (reify_real_term y)))
((>=_Int x y) (>=_Real (reify_int_term x) (reify_int_term y)))
((>=_IntReal x y) (>=_Real (reify_int_term x) (reify_real_term y)))
(default (fail formula))
))
; From an arith predicate, prove the equivalent real predicate
(declare pf_reified_arith_pred
(! p formula
(! p' formula
(! pf (th_holds p)
(! reify_sc (^ (reify_arith_pred p) p')
(th_holds p'))))))
;; ========================== ;;
;; Int Bound Tightening Rules ;;
;; ========================== ;;
; Returns whether `ceil` is the ceiling of `q`.
(program is_ceil ((q mpq) (ceil mpz)) bool
(let diff (mp_add (mpz_to_mpq ceil) (mp_neg q))
(mp_ifneg diff
ff
(mp_ifneg (mp_add diff (~ 1/1))
tt
ff))))
; Returns whether `n` is the greatest integer less than `q`.
(program is_greatest_integer_below ((n mpz) (q mpq)) bool
(is_ceil q (mp_add n 1)))
; Negates terms of the form:
; (a) k OR
; (b) x OR
; (c) k * x
; where k is a constant and x is a variable.
; Otherwise fails.
; This aligns closely with the LFSCArithProof::printLinearMonomialNormalizer
; function.
(program negate_linear_monomial_int_term ((t (term Int))) (term Int)
(match t
((term_int_var v) (*_Int (a_int (~ 1)) (term_int_var v)))
((a_int k) (a_int (mp_neg k)))
((*_Int x y)
(match x
((a_int k)
(match y
((term_int_var v) (*_Int (a_int (mp_neg k)) y))
(default (fail (term Int)))))
(default (fail (term Int)))))
(default (fail (term Int)))
))
; This function negates linear interger terms---sums of terms of the form
; recognized by `negate_linear_monomial_int_term`.
(program negate_linear_int_term ((t (term Int))) (term Int)
(match t
((term_int_var v) (negate_linear_monomial_int_term t))
((a_int i) (negate_linear_monomial_int_term t))
((+_Int x y) (+_Int (negate_linear_int_term x) (negate_linear_int_term y)))
((*_Int x y) (negate_linear_monomial_int_term t))
(default (fail (term Int)))
))
; Statement that z is the negation of greatest integer less than q.
(declare holds_neg_of_greatest_integer_below
(! z mpz
(! q mpq
type)))
; For proving statements of the above form.
(declare check_neg_of_greatest_integer_below
(! z mpz
(! q mpq
(! sc_check (^ (is_greatest_integer_below (mp_neg z) q) tt)
(holds_neg_of_greatest_integer_below z q)))))
; Axiom for tightening [Int] < q into -[Int] >= -greatest_int_below(q).
; Note that [Int] < q is actually not([Int] >= q)
(declare tighten_not_>=_IntReal
(! t (term Int) ; Omit
(! neg_t (term Int) ; Omit
(! real_bound mpq ; Omit
(! neg_int_bound mpz ; Omit
(! pf_step (holds_neg_of_greatest_integer_below neg_int_bound real_bound)
(! pf_real_bound (th_holds (not (>=_IntReal t (a_real real_bound))))
(! sc_neg (^ (negate_linear_int_term t) neg_t)
(th_holds (>=_IntReal neg_t (term_int_to_real (a_int neg_int_bound))))))))))))
; Axiom for tightening [Int] >= q into [Int] >= ceil(q)
(declare tighten_>=_IntReal
(! t (term Int) ; Omit
(! real_bound mpq ; Omit
(! int_bound mpz
(! pf_real_bound (th_holds (>=_IntReal t (a_real real_bound)))
(! sc_floor (^ (is_ceil real_bound int_bound) tt)
(th_holds (>=_IntReal t (term_int_to_real (a_int int_bound))))))))))
; Statement that z is the greatest integer less than z'.
(declare holds_neg_of_greatest_integer_below_int
(! z mpz
(! z' mpz
type)))
; For proving statements of the above form.
(declare check_neg_of_greatest_integer_below_int
(! z mpz
(! z' mpz
(! sc_check (^ (is_greatest_integer_below (mp_neg z) (mpz_to_mpq z')) tt)
(holds_neg_of_greatest_integer_below_int z z')))))
; Axiom for tightening [Int] < i into -[Int] >= -(i - 1).
; Note that [Int] < i is actually not([Int] >= i)
(declare tighten_not_>=_IntInt
(! t (term Int) ; Omit
(! neg_t (term Int) ; Omit
(! old_bound mpz ; Omit
(! neg_int_bound mpz ; Omit
(! pf_step (holds_neg_of_greatest_integer_below_int neg_int_bound old_bound)
; Note that even when the RHS is an integer, we convert it to real and use >_IntReal
(! pf_real_bound (th_holds (not (>=_IntReal t (term_int_to_real (a_int old_bound)))))
(! sc_neg (^ (negate_linear_int_term t) neg_t)
(th_holds (>=_IntReal neg_t (term_int_to_real (a_int neg_int_bound))))))))))))
|
