1 ;; Author Barton Willis
2 ;; University of Nebraska at Kearney
3 ;; Copyright (C) 2008 Barton Willis
5 ;; This program is free software; you can redistribute it and/or modify
6 ;; it under the terms of the GNU General Public License as published by
7 ;; the Free Software Foundation; either version 2 of the License, or
8 ;; (at your option) any later version.
10 ;; This program is distributed in the hope that it will be useful,
11 ;; but WITHOUT ANY WARRANTY; without even the implied warranty of
12 ;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 ;; GNU General Public License for more details.
15 ($load
"fourier_elim")
17 (defun $simp_inequality
(e)
18 (let ((ee (standardize-inequality e
)))
19 (if (or (eq ee t
) (eq ee nil
)) ee e
)))
21 ;; non-short-circuited boolean operators and or.
23 (mfuncall '$nary
"%and")
24 (defprop %and wxxml-nary wxxml
)
25 (defprop %and
"<mspace/><fnm> %and </fnm><mspace/>" wxxmlsym
)
26 (defprop %and
"<fnm> %and </fnm>" wxxmlword
)
27 (defprop %and
120. wxxml-lbp
)
28 (defprop %and
120. wxxml-rbp
)
29 (displa-def %and dimension-nary
" %and ")
30 (setf (get '%and
'grind
) 'msize-nary
)
31 (defprop %and tex-nary tex
)
32 (defprop %and
(" \\land ") texsym
)
33 (setf (get '$%and
'operators
) 'simp-%and
)
34 (setf (get '%and
'operators
) 'simp-%and
)
36 ;; make op(a %and b) --> "%and" This allows things like if op(e) = "%and" to work. With this disjunction_p and conjuction_p aren't needed.
37 (putprop '%and
"%and" 'op
)
38 (putprop '%or
"%or" 'op
)
40 ;; Efficiency hack (see nset.lisp) -- this tells xreduce that %and is nary.
41 (def-nary '$%and
(s) (simplify (cons '(%and
) s
)) t
)
43 (defun simp-%and
(e yy z
)
45 (let ((not-e) (acc) (b))
47 ;; flatten and simplify each argument
50 (setq ek
(simplifya (specrepcheck ek
) z
))
51 (setq b
(standardize-inequality ek
))
52 (setq ek
(if (or (eq b t
) (eq b nil
)) b ek
))
53 (if (op-equalp ek
'%and
) (setq acc
(append acc
(margs ek
))) (push ek acc
)))
55 ;; setify and remove true
56 (setq e
($disjoin t
(opapply '$set acc
)))
58 ;; logically negate each member of e
59 (setq not-e
(opapply '$set
(mapcar #'(lambda (s) (take '(mnot) s
)) (margs e
))))
62 ;; (1) if intersect(e, not(e)) # empty, return false,
63 ;; (2) if false in e, return false,
64 ;; (3) if e is empty, return true,
65 ;; (4) if e is a singleton set, return x.
67 (cond ((not ($emptyp
($intersection e not-e
))) nil
)
68 (($elementp nil e
) nil
)
70 ((not (cddr e
)) (cadr e
))
71 (t `((%and simp
) ,@(margs e
))))))
73 (mfuncall '$nary
"%or")
74 (defprop %or wxxml-nary wxxml
)
75 (defprop %or
"<mspace/><fnm> %or </fnm><mspace/>" wxxmlsym
)
76 (defprop %or
"<fnm> %or </fnm>" wxxmlword
)
77 (defprop %or
120. wxxml-lbp
)
78 (defprop %or
120. wxxml-rbp
)
80 (defprop %or tex-nary tex
)
81 (defprop %or
(" \\lor ") texsym
)
83 (displa-def %or dimension-nary
" %or ")
84 (setf (get '%or
'grind
) 'msize-nary
)
85 (setf (get '$%or
'operators
) 'simp-%or
)
86 (setf (get '%or
'operators
) 'simp-%or
)
88 (defun $disjunction_p
(e)
91 (defun $conjunction_p
(e)
95 ;; Efficiency hack (see nset.lisp) -- this tells xreduce that %or is nary.
96 (def-nary '$%or
(s) (simplify (cons '(%or
) s
)) nil
)
98 (defun simp-%or
(e yy z
)
100 (let ((not-e) (acc) (b))
102 ;; flatten and simplify each argument
105 (setq ek
(simplifya (specrepcheck ek
) z
))
106 (setq b
(standardize-inequality ek
))
107 (setq ek
(if (or (eq b t
) (eq b nil
)) b ek
))
108 (if (op-equalp ek
'%or
) (setq acc
(append acc
(margs ek
))) (push ek acc
)))
110 ;; setify and remove false
111 (setq e
($disjoin nil
(opapply '$set acc
)))
113 ;; logically negate each member of e
114 (setq not-e
(opapply '$set
(mapcar #'(lambda (s) (take '(mnot) s
)) (margs e
))))
117 ;; (1) if intersect(e, not(e)) # empty, return true
118 ;; (2) if true e in e, return true,
119 ;; (3) if e is empty, return false,
120 ;; (4) if is a singleton set, return x.
122 (cond ((not ($emptyp
($intersection e not-e
))) t
)
125 ((not (cddr e
)) (cadr e
))
126 (t `((%or simp
) ,@(margs e
))))))
128 (setf (get '$%union
'operators
) 'simp-%union
)
130 (defun simp-%union
(e yy z
)
131 (declare (ignore yy
))
133 ;; flatten and simplify each argument
136 (setq ek
(simplifya (specrepcheck ek
) z
))
137 (if (op-equalp ek
'$%union
) (setq acc
(append acc
(margs ek
))) (push ek acc
)))
138 ;; setify and remove $emptyset.
139 (setq e
(margs ($disjoin
(take '($set
)) (opapply '$set acc
))))
140 `(($%union simp
) ,@e
)))
143 (defprop $%union tex-nary tex
)
144 (defprop $%union
(" \\cup ") texsym
)
146 (setf (get '$%if
'operators
) 'simp-%if
)
148 (defun simp-%if
(e yy z
)
149 (declare (ignore yy
))
150 (pop e
) ;; remove ($%if simp)
151 (let (($domain
'$complex
)
152 (cnd (if e
(simpcheck (pop e
) z
) (wna-err '$%if
)))
153 (a (if e
(pop e
) (wna-err '$%if
)))
154 (b (if e
(pop e
) (wna-err '$%if
))))
155 (if e
(wna-err '$%if
))
156 (setq cnd
(standardize-inequality ($substitute
'%or
'mor
($substitute
'%and
'mand cnd
))))
157 (setq cnd
($substitute
'%or
'mor
($substitute
'%and
'mand cnd
)))
158 (cond ((eq cnd t
) (simpcheck a z
))
159 ((eq cnd nil
) (simpcheck b z
))
161 (setq a
(simpcheck a z
))
162 (setq b
(simpcheck b z
))
163 (if (like a b
) a
`(($%if simp
) ,cnd
,a
,b
))))))
165 (setf (get '$%integerp
'operators
) 'simp-%integerp
)
167 (defun simp-%integerp
(e yy z
)
168 (declare (ignore yy
))
171 (setq e
(simplifya (second e
) z
))
172 (setq sgn
($compare e
(take '($floor
) e
)))
173 (cond ((equal sgn
"=") t
)
174 ((member sgn
'("<" ">" "#") :test
#'equal
) nil
)
175 ((and (symbolp e
) ($featurep e
'$noninteger
)) nil
)
176 (t `(($%integerp simp
) ,e
)))))
178 (setf (get '$isnonnegative_p
'operators
) 'simp-isnonnegative-p
)
180 (defun simp-isnonnegative-p (e yy z
)
181 (declare (ignore yy
))
183 (let (($domain
'$complex
) (is-real) (sgn))
184 (setq e
(simplifya (specrepcheck (cadr e
)) z
))
185 (setq is-real
(take '($isreal_p
) e
))
186 (cond ((eq t is-real
)
188 (cond ((memq sgn
'($zero $pz $pos
)) t
)
190 (t `(($isnonnegative_p simp
) ,e
))))
191 ((eq nil is-real
) nil
)
192 (t `(($isnonnegative_p simp
) ,e
)))))
194 ;; Similar to sublis, but allow for substitutions of nonatoms.
196 (defun $subst_parallel
(l e
)
197 (let ((alist nil
) (is-a-rat ($ratp e
)) (old) (new))
198 (setq l
(if ($listp l
) (margs l
) (list l
)))
200 ;; Build an association list for the Common Lisp sublis function.
205 (setq new
(caddr lk
))
206 (setq old
(if (stringp old
) (amperchk old
) old
))
207 (push (cons old new
) alist
))
208 (merror "Each substitution must be an equation; found" lk
)))
209 (setq e
(resimplify (sublis alist
($ratdisrep e
) :test
#'alike
))) ;;or like?
210 (if is-a-rat
($rat e
) e
)))
