document INTEGERPV
[screamer.git] / equations.lisp
blobfbf495649f68af2dbe2103885703ac26ba8d94b0
1 ;;; -*- Mode: LISP; Package: (SCREAMS :USE CL :COLON-MODE :EXTERNAL); Base: 10; Syntax: Ansi-common-lisp -*-
3 ;;; LaHaShem HaAretz U'Mloah
5 #||#(in-package :screamer-user)
7 #-(or poplog akcl)
8 (screamer:define-screamer-package :screams (:use :iterate))
10 #-(or poplog akcl)
11 (in-package :screams)
13 #+(or poplog akcl)
14 (use-package :iterate)
16 (defvar *infinity* 1e38)
18 (defvar *fuzz* 1e-6)
20 (defun make-interval (low high) (cons low high))
22 (defun low (interval) (car interval))
24 (defun high (interval) (cdr interval))
26 (defun size (interval) (- (high interval) (low interval)))
28 (defun small? (interval) (< (size interval) *fuzz*))
30 (defun disjoint? (interval1 interval2)
31 (or (< (high interval1) (low interval2))
32 (> (low interval1) (high interval2))))
34 (defun intersects? (interval1 interval2) (not (disjoint? interval1 interval2)))
36 (defun add-interval (interval1 interval2)
37 (make-interval (+ (low interval1) (low interval2))
38 (+ (high interval1) (high interval2))))
40 (defun multiply-interval (interval1 interval2)
41 (let ((l1 (low interval1))
42 (h1 (high interval1))
43 (l2 (low interval2))
44 (h2 (high interval2)))
45 (let ((b1 (* l1 l2))
46 (b2 (* l1 h2))
47 (b3 (* h1 l2))
48 (b4 (* h1 h2)))
49 (make-interval (min b1 b2 b3 b4) (max b1 b2 b3 b4)))))
51 (defun compute-interval (expression environment)
52 (cond ((numberp expression) (make-interval expression expression))
53 ((symbolp expression) (cdr (assoc expression environment)))
54 ((eq (car expression) '+)
55 (reduce #'add-interval
56 (mapcar #'(lambda (expression)
57 (compute-interval expression environment))
58 (rest expression))))
59 ((eq (car expression) '*)
60 (reduce #'multiply-interval
61 (mapcar #'(lambda (expression)
62 (compute-interval expression environment))
63 (rest expression))))))
65 (defun impossible? (equation environment)
66 (disjoint? (compute-interval (second equation) environment)
67 (compute-interval (third equation) environment)))
69 (defun variables-of (expression)
70 (cond ((numberp expression) nil)
71 ((member expression '(+ * =)) nil)
72 ((null expression) nil)
73 ((atom expression) (list expression))
74 (t (append (variables-of (car expression))
75 (variables-of (cdr expression))))))
77 (defun make-environment (variables interval)
78 (cond ((null variables) nil)
79 ((member (first variables) (rest variables))
80 (make-environment (rest variables) interval))
81 (t (cons (cons (first variables) interval)
82 (make-environment (rest variables) interval)))))
84 (defun a-half-interval (interval)
85 (let ((midpoint (/ (+ (low interval) (high interval)) 2)))
86 (either (make-interval (low interval) midpoint)
87 (make-interval midpoint (high interval)))))
89 (defun copy-all (tree)
90 (if (atom tree) tree (cons (copy-all (car tree)) (copy-all (cdr tree)))))
92 (defun biggest-cell (environment)
93 (if (null (rest environment))
94 (first environment)
95 (let ((big-cell (biggest-cell (rest environment))))
96 (let ((interval1 (cdr (first environment)))
97 (interval2 (cdr big-cell)))
98 (if (> (size interval1) (size interval2))
99 (first environment)
100 big-cell)))))
102 (defun refine-environment (environment equations)
103 (let ((cell (biggest-cell environment)))
104 (cond ((small? (cdr cell)) (copy-all environment))
105 (t (local (setf (cdr cell) (a-half-interval (cdr cell))))
106 (if (some #'(lambda (equation) (impossible? equation environment))
107 equations)
108 (fail))
109 (refine-environment environment equations)))))
111 (defun solve (equations)
112 (refine-environment
113 (make-environment (variables-of equations)
114 (make-interval (- *infinity*) *infinity*))
115 equations))
117 (defun dam-test ()
118 (for-effects (print (solve '((= (+ (* x x) (* y y)) (* z z))
119 (= x (+ 5 y))
120 (= z (+ x y 3)))))))
122 (defun dam-testa ()
123 (for-effects
124 (print
125 (solution
126 (let ((x (a-real-betweenv (- *infinity*) *infinity*))
127 (y (a-real-betweenv (- *infinity*) *infinity*))
128 (z (a-real-betweenv (- *infinity*) *infinity*)))
129 (assert! (andv (=v (+v (*v x x) (*v y y)) (*v z z))
130 (=v x (+v 5 y))
131 (=v z (+v x y 3))))
132 (list x y z))
133 (reorder #'range-size
134 #'(lambda (x) (< x *fuzz*))
136 #'divide-and-conquer-force)))))
138 (defun eq4 () (for-effects (print (solve '((= (+ x x x x) 3))))))
140 (defun eq4a ()
141 (for-effects
142 (print
143 (solution
144 (let ((x (a-real-betweenv (- *infinity*) *infinity*)))
145 (assert! (=v (+v x x x x) 3.0))
147 (reorder #'range-size
148 #'(lambda (x) (< x *fuzz*))
150 #'divide-and-conquer-force)))))
152 (defun eq3 () (for-effects (print (solve '((= (* 4 x) 3))))))
154 (defun eq2 ()
155 (for-effects
156 (print (solve '((= (+ x x y y y) 17)
157 (= (+ x x x x x x x y y y y) 27))))))
159 (defun eq2a ()
160 (for-effects
161 (print
162 (solution
163 (let ((x (a-real-betweenv (- *infinity*) *infinity*))
164 (y (a-real-betweenv (- *infinity*) *infinity*)))
165 (assert! (andv (=v (+v x x y y y) 17.0)
166 (=v (+v x x x x x x x y y y y) 27.0)))
167 (list x y))
168 (reorder #'range-size
169 #'(lambda (x) (< x *fuzz*))
171 #'divide-and-conquer-force)))))
173 (defun eq1 ()
174 (for-effects
175 (print (solve '((= (+ (* 2 x) (* 3 y)) 17) (= (+ (* 7 x) (* 4 y)) 27))))))
177 (defun equation1 ()
178 (for-effects
179 (print
180 (solution
181 (let ((x (an-integer-betweenv -1000000 1000000))
182 (y (an-integer-betweenv -1000000 1000000)))
183 (assert! (andv (=v (+v (*v 2 x) (*v 3 y)) 17)
184 (=v (+v (*v 7 x) (*v 4 y)) 27)))
185 (list x y))
186 (reorder #'range-size
187 #'(lambda (x) (< x *fuzz*))
189 #'divide-and-conquer-force)))))
191 (defun equation1a ()
192 ;; note: This uses ratnums which eventually get turned into flonums.
193 (for-effects
194 (print
195 (solution
196 (let ((x (a-real-betweenv -1000000 1000000))
197 (y (a-real-betweenv -1000000 1000000)))
198 (assert! (andv (=v (+v (*v 2 x) (*v 3 y)) 17)
199 (=v (+v (*v 7 x) (*v 4 y)) 27)))
200 (list x y))
201 (reorder #'range-size
202 #'(lambda (x) (< x *fuzz*))
204 #'divide-and-conquer-force)))))
206 (defun equation1b ()
207 (for-effects
208 (print
209 (solution
210 (let ((x (a-real-betweenv (- *infinity*) *infinity*))
211 (y (a-real-betweenv (- *infinity*) *infinity*)))
212 (assert! (andv (=v (+v (*v 2 x) (*v 3 y)) 17)
213 (=v (+v (*v 7 x) (*v 4 y)) 27)))
214 (list x y))
215 (reorder #'range-size
216 #'(lambda (x) (< x *fuzz*))
218 #'divide-and-conquer-force)))))
220 (defun equation1c ()
221 (for-effects
222 (print
223 (solution
224 (let ((x (a-real-betweenv (- *infinity*) *infinity*))
225 (y (a-real-betweenv (- *infinity*) *infinity*)))
226 (assert! (andv (=v (+v (*v 2.0 x) (*v 3.0 y)) 17.0)
227 (=v (+v (*v 7.0 x) (*v 4.0 y)) 27.0)))
228 (list x y))
229 (reorder #'range-size
230 #'(lambda (x) (< x *fuzz*))
232 #'divide-and-conquer-force)))))
234 (defun equation2 ()
235 (for-effects
236 (print
237 (solution
238 (let ((x (a-real-betweenv (- *infinity*) *infinity*)))
239 (assert! (=v (*v x x) 4.0))
241 (reorder #'range-size
242 #'(lambda (x) (< x *fuzz*))
244 #'divide-and-conquer-force)))))
246 (defun equation3 ()
247 (for-effects
248 (print
249 (solution
250 (let ((x (a-real-betweenv (- *infinity*) *infinity*))
251 (y (a-real-betweenv (- *infinity*) *infinity*)))
252 (assert! (andv (=v (+v x x y y y) 17.0)
253 (=v (+v x x x x x x x y y y y) 27.0)))
254 (list x y))
255 (reorder #'range-size
256 #'(lambda (x) (< x *fuzz*))
258 #'divide-and-conquer-force)))))
260 (defun equation3a ()
261 ;; note: This uses ratnums which eventually get turned into flonums.
262 (for-effects
263 (print
264 (solution
265 (let ((x (a-real-betweenv -1000000 1000000))
266 (y (a-real-betweenv -1000000 1000000)))
267 (assert! (andv (=v (+v x x y y y) 17)
268 (=v (+v x x x x x x x y y y y) 27)))
269 (list x y))
270 (reorder #'range-size
271 #'(lambda (x) (< x *fuzz*))
273 #'divide-and-conquer-force)))))
275 (defun equation3b ()
276 (for-effects
277 (print
278 (solution
279 (let ((x (an-integer-betweenv (- *infinity*) *infinity*))
280 (y (an-integer-betweenv (- *infinity*) *infinity*)))
281 (assert! (andv (=v (+v x x y y y) 17)
282 (=v (+v x x x x x x x y y y y) 27)))
283 (list x y))
284 (reorder #'range-size
285 #'(lambda (x) (< x *fuzz*))
287 #'divide-and-conquer-force)))))
289 (defun equation3c ()
290 (for-effects
291 (print
292 (solution
293 (let ((x (an-integer-betweenv -1000000 1000000))
294 (y (an-integer-betweenv -1000000 1000000)))
295 (assert! (andv (=v (+v x x y y y) 17)
296 (=v (+v x x x x x x x y y y y) 27)))
297 (list x y))
298 (reorder #'range-size
299 #'(lambda (x) (< x *fuzz*))
301 #'divide-and-conquer-force)))))
303 (defun equation4 ()
304 (for-effects
305 (print
306 (solution
307 (let ((x (a-real-betweenv -1000000 1000000)))
308 (assert! (=v (+v x x x x) 8.0))
310 (reorder #'range-size
311 #'(lambda (x) (< x *fuzz*))
313 #'divide-and-conquer-force)))))
315 (defun equation4a ()
316 (for-effects
317 (print
318 (solution
319 (let ((x (a-real-betweenv (- *infinity*) *infinity*)))
320 (assert! (=v (+v x x x x) 3))
322 (reorder #'range-size
323 #'(lambda (x) (< x *fuzz*))
325 #'divide-and-conquer-force)))))
327 (defun equation4b ()
328 (for-effects
329 (print
330 (solution
331 (let ((x (a-real-betweenv (- *infinity*) *infinity*)))
332 (assert! (=v (+v x x x x) 8.0))
334 (reorder #'range-size
335 #'(lambda (x) (< x *fuzz*))
337 #'divide-and-conquer-force)))))
339 (defun equation4c ()
340 (for-effects
341 (print
342 (solution
343 (let ((x (an-integer-betweenv -1000000 1000000)))
344 (assert! (=v (+v x x x x) 8.0))
346 (reorder #'range-size
347 #'(lambda (x) (< x *fuzz*))
349 #'divide-and-conquer-force)))))
351 (defun nonlinear1 ()
352 (for-effects
353 (print
354 (solution
355 (let ((x (a-real-betweenv (- *infinity*) *infinity*))
356 (y (a-real-betweenv (- *infinity*) *infinity*))
357 (z (a-real-betweenv (- *infinity*) *infinity*)))
358 (assert!
359 (andv (orv (=v (+v (*v 4 x x y) (*v 7 y z z) (*v 6 x x z z)) 2)
360 (=v (+v (*v 3 x y) (*v 2 y y) (*v 5 x y z)) -4))
361 (>=v (*v (+v x y) (+v y z)) -5)))
362 (list x y z))
363 (reorder #'range-size
364 #'(lambda (x) (< x *fuzz*))
366 #'divide-and-conquer-force)))))
368 (defun nonlinear2 ()
369 (for-effects
370 (print
371 (solution
372 (let ((x (a-real-betweenv (- *infinity*) *infinity*))
373 (y (a-real-betweenv (- *infinity*) *infinity*))
374 (z (a-real-betweenv (- *infinity*) *infinity*)))
375 (assert!
376 (andv (=v (+v (*v 4 x x y) (*v 7 y z z) (*v 6 x x z z)) 2)
377 (=v (+v (*v 3 x y) (*v 2 y y) (*v 5 x y z)) -4)
378 (>=v (*v (+v x y) (+v y z)) -5)))
379 (list x y z))
380 (reorder #'range-size
381 #'(lambda (x) (< x *fuzz*))
383 #'divide-and-conquer-force)))))
385 ;;; Tam V'Nishlam Shevah L'El Borei Olam