1module ofsfsiat;  % Ordered field standard form simplification
2
3revision('ofsfsiat, "$Id: ofsfsiat.red 3975 2017-03-24 19:12:30Z thomas-sturm $");
4
5copyright('ofsfsiat, "(c) 1995-2009 A. Dolzmann, T. Sturm, 2017 T. Sturm");
6
7% Redistribution and use in source and binary forms, with or without
8% modification, are permitted provided that the following conditions
9% are met:
10%
11%    * Redistributions of source code must retain the relevant
12%      copyright notice, this list of conditions and the following
13%      disclaimer.
14%    * Redistributions in binary form must reproduce the above
15%      copyright notice, this list of conditions and the following
16%      disclaimer in the documentation and/or other materials provided
17%      with the distribution.
18%
19% THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
20% "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
21% LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
22% A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
23% OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
24% SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
25% LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
26% DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
27% THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
28% (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
29% OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
30%
31
32procedure ofsf_simplat1(f,sop);
33   % Ordered field standard form simplify atomic formula. [f] is an
34   % atomic formula; [sop] is the boolean operator [f] occurs with or
35   % [nil]. Accesses switches [rlsiatadv], [rlsipd], [rlsiexpl], and
36   % [rlsiexpla]. Returns a quantifier-free formula that is a
37   % simplified equivalent of [f].
38   begin scalar rel,lhs;
39      rel := ofsf_op f;
40      if not (rel memq '(equal neq leq geq lessp greaterp)) then
41 	 return nil;
42      lhs := ofsf_arg2l f;
43      if domainp lhs then
44 	 return if ofsf_evalatp(rel,lhs) then 'true else 'false;
45      lhs := quotf(lhs,sfto_dcontentf lhs);
46      if minusf lhs then <<
47    	 lhs := negf lhs;
48    	 rel := ofsf_anegrel rel
49      >>;
50      if null !*rlsiatadv then return ofsf_0mk2(rel,lhs);
51      if rel eq 'equal then return ofsf_simplequal(lhs,sop);
52      if rel eq 'neq then return ofsf_simplneq(lhs,sop);
53      if rel eq 'leq then return ofsf_simplleq(lhs,sop);
54      if rel eq 'geq then return ofsf_simplgeq(lhs,sop);
55      if rel eq 'lessp then return ofsf_simpllessp(lhs,sop);
56      if rel eq 'greaterp then return ofsf_simplgreaterp(lhs,sop)
57   end;
58
59procedure ofsf_simplequal(lhs,sop);
60   % Ordered field standard form simplify [equal]-atomic formula.
61   % [lhs] is a term. Returns a quantifier-free formula.
62   begin scalar w,ff,ww;
63      w := ofsf_posdefp lhs;
64      if w eq 'stsq then return 'false;
65      ff := sfto_sqfpartf lhs;
66      ww := ofsf_posdefp ff;
67      if ww eq 'stsq then return 'false;
68      if !*rlsitsqspl and (!*rlsiexpla or !*rlsiexpl and sop = 'and) then <<
69	 if ww eq 'tsq then return ofsf_tsqsplequal ff;
70	 if w eq 'tsq then return ofsf_tsqsplequal lhs
71      >>;
72      return ofsf_facequal!*(ff,sop)
73   end;
74
75procedure ofsf_tsqsplequal(f);
76   % Trivial square sum split [equal] case.
77   begin scalar w;
78      w := ofsf_getsqsummons(f);
79      if !*rlsifac and (!*rlsiexpla or !*rlsiexpl and null cdr w) then
80	 return rl_smkn('and,for each m in w collect
81	    rl_smkn('or,for each v in m collect ofsf_0mk2('equal,v)));
82      return rl_smkn('and,for each m in w collect
83 	 ofsf_0mk2('equal,sfto_lmultf m))
84   end;
85
86procedure ofsf_facequal!*(f,sop);
87   if !*rlsifac and (!*rlsiexpla or !*rlsiexpl and sop = 'or) then
88      ofsf_facequal f
89   else
90      ofsf_0mk2('equal,f);
91
92procedure ofsf_facequal(f);
93   % Left hand side factorization [equal] case.
94   rl_smkn('or,for each x in cdr sfto_fctrf f collect ofsf_0mk2('equal,car x));
95
96procedure ofsf_simplneq(lhs,sop);
97   % Ordered field standard form simplify [neq]-atomic formula.
98   % [lhs] is a term. Returns a quantifier-free formula.
99   begin scalar w,ff,ww;
100      w := ofsf_posdefp lhs;
101      if w eq 'stsq then return 'true;
102      ff := sfto_sqfpartf lhs;
103      ww := ofsf_posdefp ff;
104      if ww eq 'stsq then return 'true;
105      if !*rlsitsqspl and (!*rlsiexpla or !*rlsiexpl and sop = 'or) then <<
106	 if ww eq 'tsq then return ofsf_tsqsplneq ff;
107	 if w eq 'tsq then return ofsf_tsqsplneq lhs
108      >>;
109      return ofsf_facneq!*(ff,sop)
110   end;
111
112procedure ofsf_tsqsplneq(f);
113   % Trivial square sum split [neq] case.
114   begin scalar w;
115      w := ofsf_getsqsummons(f);
116      if !*rlsifac and (!*rlsiexpla or !*rlsiexpl and null cdr w) then
117	 return rl_smkn('or,for each m in w collect
118	    rl_smkn('and,for each v in m collect ofsf_0mk2('neq,v)));
119      return rl_smkn('or,for each m in w collect
120 	 ofsf_0mk2('neq,sfto_lmultf m))
121   end;
122
123procedure ofsf_facneq!*(f,sop);
124   if !*rlsifac and (!*rlsiexpla or !*rlsiexpl and sop = 'and) then
125      ofsf_facneq f
126   else
127      ofsf_0mk2('neq,f);
128
129procedure ofsf_facneq(f);
130   % Left hand side factorization [neq] case.
131   rl_smkn('and,for each x in cdr sfto_fctrf f collect ofsf_0mk2('neq,car x));
132
133procedure ofsf_getsqsummons(f);
134   % Ordered field standard form get squaresum monomials. [f] is an
135   % SF. Returns a list of SFs.
136   begin scalar v,w;
137      if null f then return nil;
138      if domainp f then return {nil};  % i.e. {1}
139      w := ofsf_getsqsummons(red f);
140      v := !*k2f mvar f;
141      for each x in ofsf_getsqsummons lc f do
142	 w := (v . x) . w;
143      return w
144   end;
145
146procedure ofsf_simplleq(lhs,sop);
147   % Ordered field standard form simplify [leq]-atomic formula. [lhs]
148   % is a term, [sop] is a boolean operator or [nil]. Accesses
149   % switches [rlsipd], [rlexpl], and [rlexpla]. Returns a
150   % quantifier-free formula.
151   begin scalar s1,s2,w,x;
152      if (s1 := ofsf_posdefp lhs) eq 'stsq then
153 	 return 'false;
154      w := sfto_sqfpartf lhs;
155      if (s2 := ofsf_posdefp w) eq 'stsq then
156 	 return 'false;
157      if !*rlsitsqspl and (!*rlsiexpla or !*rlsiexpl and sop = 'and) then <<
158	 if s2 then return ofsf_tsqsplequal w;
159	 if s1 then return ofsf_tsqsplequal lhs
160      >>;
161      if s1 or s2 then
162 	 return ofsf_facequal!*(w,sop);
163      if null !*rlsipd and null !*rlsifaco then
164 	 return ofsf_0mk2('leq,lhs);
165      x := sfto_pdecf lhs;
166      s1 := ofsf_posdefp car x;
167      if s1 eq 'stsq then
168	 return ofsf_facequal!*(cdr x,sop);
169      if s1 then
170	 return ofsf_facequal!*(w,sop);
171      if ofsf_posdefp cdr x eq 'stsq then
172	 cdr x := 1;
173      if !*rlsifaco then <<
174	 car x := sfto_lmultf ofsf_facsimpl car x;
175	 cdr x := ofsf_facsimpl cdr x
176      >> else
177	 cdr x := if not eqn(cdr x,1) then {cdr x};
178      if ofsf_posdefp car x eq 'stsq then
179	 car x := 1;
180      w := sfto_lmultf cdr x;
181      if ofsf_posdefp w eq 'stsq then <<
182	 cdr x := nil;
183	 w := 1
184      >>;
185      if eqn(car x,1) and eqn(w,1) then
186	 return 'false;
187      if !*rlsiexpla or (!*rlsiexpl and (sop eq 'or)) then
188	 return rl_smkn('or,ofsf_0mk2('leq,car x) .
189	    for each fac in cdr x collect ofsf_0mk2('equal,fac));
190      return ofsf_0mk2('leq,multf(car x,exptf(w,2)))
191   end;
192
193procedure ofsf_facsimpl(u);
194   for each x in cdr sfto_fctrf u join
195      if not (ofsf_posdefp car x eq 'stsq) then
196      	 {car x};
197
198procedure ofsf_simplgeq(lhs,sop);
199   % Ordered field standard form simplify [geq]-atomic formula. [lhs]
200   % is a term, [sop] is a boolean operator or [nil]. Accesses
201   % switches [rlsipd], [rlexpl], and [rlexpla]. Returns a
202   % quantifier-free formula.
203   begin scalar x,w,s1,s2;
204      if ofsf_posdefp lhs or ofsf_posdefp sfto_sqfpartf lhs then
205 	 return 'true;
206      if not !*rlsipd and not !*rlsifaco then
207      	 return ofsf_0mk2('geq,lhs);
208      x := sfto_pdecf lhs;
209      if ofsf_posdefp car x then
210	 return 'true;
211      if ofsf_posdefp cdr x eq 'stsq then
212	 cdr x := 1;
213      if !*rlsifaco then <<
214	 car x := sfto_lmultf ofsf_facsimpl car x;
215	 cdr x := ofsf_facsimpl cdr x
216      >> else
217	 cdr x := if not eqn(cdr x,1) then {cdr x};
218      w := sfto_lmultf cdr x;
219      s1 := ofsf_posdefp car x;
220      s2 := ofsf_posdefp w;
221      if s1 and s2 then
222	 return 'true;
223      if s1 eq 'stsq then
224      	 car x := 1
225      else if s2 eq 'stsq then <<
226	 cdr x := nil;
227	 w := 1
228      >>;
229      if !*rlsiexpla or (!*rlsiexpl and (sop eq 'or)) then
230	 return rl_smkn('or,ofsf_0mk2('geq,car x) .
231	    for each fac in cdr x collect ofsf_0mk2('equal,fac));
232      return ofsf_0mk2('geq,multf(car x,exptf(w,2)))
233   end;
234
235procedure ofsf_simpllessp(lhs,sop);
236   % Ordered field standard form simplify [lessp]-atomic formula.
237   % [lhs] is a term, [sop] is a boolean operator or [nil]. Accesses
238   % switches [rlsipd], [rlexpl], and [rlexpla]. Returns a
239   % quantifier-free formula.
240   begin scalar x,w,s1,s2;
241      if ofsf_posdefp lhs or ofsf_posdefp sfto_sqfpartf lhs then
242 	 return 'false;
243      if not !*rlsipd and not !*rlsifaco then
244      	 return ofsf_0mk2('lessp,lhs);
245      x := sfto_pdecf lhs;
246      if ofsf_posdefp car x then
247	 return 'false;
248      if ofsf_posdefp cdr x eq 'stsq then
249	 cdr x := 1;
250      if !*rlsifaco then <<
251	 car x := sfto_lmultf ofsf_facsimpl car x;
252	 cdr x := ofsf_facsimpl cdr x
253      >> else
254	 cdr x := if not eqn(cdr x,1) then {cdr x};
255      w := sfto_lmultf cdr x;
256      s1 := ofsf_posdefp car x;
257      s2 := ofsf_posdefp w;
258      if s1 and s2 then
259	 return 'false;
260      if s1 eq 'stsq then
261      	 car x := 1
262      else if s2 eq 'stsq then <<
263	 cdr x := nil;
264	 w := 1
265      >>;
266      if !*rlsiexpla or (!*rlsiexpl and (sop eq 'and)) then
267	 return rl_smkn('and,ofsf_0mk2('lessp,car x) .
268	    for each fac in cdr x collect ofsf_0mk2('neq,fac));
269      return ofsf_0mk2('lessp,multf(car x,exptf(w,2)))
270   end;
271
272procedure ofsf_simplgreaterp(lhs,sop);
273   % Ordered field standard form simplify [greaterp]-atomic formula.
274   % [lhs] is a term, [sop] is a boolean operator or [nil]. Accesses
275   % switches [rlsipd], [rlexpl], and [rlexpla]. Returns a
276   % quantifier-free formula.
277   begin scalar s1,s2,w,x;
278      if !*rlpos and sfto_varf lhs then
279 	 return ofsf_0mk2('greaterp,lhs);
280      if (s1 := ofsf_posdefp lhs) eq 'stsq then
281 	 return 'true;
282      w := sfto_sqfpartf lhs;
283      if (s2 := ofsf_posdefp w) eq 'stsq then  % Proposition 3.3 (ii)
284 	 return 'true;
285      if !*rlsitsqspl and (!*rlsiexpla or !*rlsiexpl and sop = 'or) then <<
286	 if s2 then return ofsf_tsqsplneq w;
287	 if s1 then return ofsf_tsqsplneq lhs
288      >>;
289      if s1 or s2 then
290 	 return ofsf_facneq!*(w,sop);
291      if null !*rlsipd and null !*rlsifaco then
292 	 return ofsf_0mk2('greaterp,lhs);
293      x := sfto_pdecf lhs;
294      s1 := ofsf_posdefp car x;  % could return better fac info for free
295      if s1 eq 'stsq then  % in particular, 1 is an stsq.
296	 return ofsf_facneq!*(cdr x,sop);
297      if s1 then
298	 return ofsf_facneq!*(w,sop);
299      if ofsf_posdefp cdr x eq 'stsq then
300	 cdr x := 1;
301      if !*rlsifaco then <<
302	 car x := sfto_lmultf ofsf_facsimpl car x;
303	 cdr x := ofsf_facsimpl cdr x
304      >> else
305	 cdr x := if not eqn(cdr x,1) then {cdr x};
306      if ofsf_posdefp car x eq 'stsq then
307	 car x := 1;
308      w := sfto_lmultf cdr x;
309      if ofsf_posdefp w eq 'stsq then <<
310	 cdr x := nil;
311	 w := 1
312      >>;
313      if eqn(car x,1) and eqn(w,1) then
314	 return 'true;
315      if !*rlsiexpla or (!*rlsiexpl and (sop eq 'and)) then
316	 return rl_smkn('and,ofsf_0mk2('greaterp,car x) .
317	    for each fac in cdr x collect ofsf_0mk2('neq,fac));
318      return ofsf_0mk2('greaterp,multf(car x,exptf(w,2)))
319   end;
320
321procedure ofsf_evalatp(rel,lhs);
322   % Ordered field standard form evaluate atomic formula. [rel] is a
323   % relation; [lhs] is a domain element. Returns a truth value
324   % equivalent to $[rel]([lhs],0)$.
325   if rel eq 'equal then null lhs
326   else if rel eq 'neq then not null lhs
327   else if rel eq 'leq then minusf lhs or null lhs
328   else if rel eq 'geq then not minusf lhs
329   else if rel eq 'lessp then minusf lhs
330   else if rel eq 'greaterp then not (minusf lhs or null lhs)
331   else rederr {"ofsf_evalatp: unknown operator ",rel};
332
333procedure ofsf_posdefp(u);
334   % Ordered field standard form positive definite predicate. [u] is
335   % an SF. Returns ['stsq] if [u] is positive definite, ['tsq] if [u]
336   % is postive semidefinite, and [nil] else. The return values origin
337   % from "(strict) trivial square sum" but are also used for positive
338   % QE, where also other polynomials are classified positive.
339   if !*rlpos then ofsf_posdefp!-pos u else sfto_tsqsumf u;
340
341procedure ofsf_posdefp!-pos(u);
342   % Ordered field standard form positive definite predicate for
343   % positive QE. [u] is an SF. Returns ['stsq] if [u] is positive
344   % definite, ['tsq] if [u] is postive semidefinite, and [nil] else.
345   % Essentially like sfto_tsqsumf but parity of degrees does not
346   % matter.
347   if null u then 'tsq else ofsf_posdefp!-pos1 u;
348
349procedure ofsf_posdefp!-pos1(u);
350   % Ordered field standard form positive definite predicate for
351   % positive QE subroutine. [u] is an SF. Returns ['stsq] if [u] is
352   % positive definite and [nil] else.
353   if domainp u then
354      (if not minusf u then 'stsq)
355   else
356      ofsf_posdefp!-pos1 lc u and ofsf_posdefp!-pos1 red u;
357
358procedure ofsf_signat(at);
359   ofsf_0mk2(ofsf_op at, numr simp reval {'sign, mk!*sq !*f2q ofsf_arg2l at});
360
361endmodule;  % [ofsfsiat]
362
363end;  % of file
364