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