1module dvfsfsiat; 2% Discretely valued field standard form simplify atomic formulas. Submodule of 3% [dvfsf]. This submodule provides the black box [rl_simplat1] to [cl_simpl]. 4 5revision('dvfsfsiat, "$Id: dvfsfsiat.red 5405 2020-09-20 16:49:38Z thomas-sturm $"); 6 7copyright('dvfsfsiat, "(c) 1995-2009 A. Dolzmann and T. Sturm"); 8 9% Redistribution and use in source and binary forms, with or without 10% modification, are permitted provided that the following conditions 11% are met: 12% 13% * Redistributions of source code must retain the relevant 14% copyright notice, this list of conditions and the following 15% disclaimer. 16% * Redistributions in binary form must reproduce the above 17% copyright notice, this list of conditions and the following 18% disclaimer in the documentation and/or other materials provided 19% with the distribution. 20% 21% THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 22% "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 23% LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR 24% A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT 25% OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 26% SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT 27% LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, 28% DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY 29% THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT 30% (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE 31% OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 32% 33 34procedure dvfsf_simplat1(atf,sop); 35 % Discretely valued field simplify atomic formula. [atf] is an 36 % atomic formula; [sop] is the complex formula operator [atf] 37 % occurs with or [nil]. Returns a quantifier-free formula that is a 38 % simplified equivalent of [atf]. Accesses the fluid [dvfsf_p!*] 39 % and the switches [rlsifac], [rlsiexpl], [rlsiexpla]. 40 begin scalar op; 41 op := dvfsf_op atf; 42 if op eq 'equal or op eq 'neq then 43 return dvfsf_safield(op,dvfsf_arg2l atf,sop); 44 return dvfsf_saval(op,dvfsf_arg2l atf,dvfsf_arg2r atf,sop) 45 end; 46 47procedure dvfsf_saval(op,lhs,rhs,sop); 48 % Discretely valued field simplify atomic formula built with 49 % valuation relation. [op] is one of ['assoc], ['nasso], ['div], or 50 % ['sdiv]; [lhs] and [rhs] are SF's; [sop] is a boolean operator. 51 % Returns a formula equivalent to $[op]([lhs],[rhs])$. 52 begin 53 if minusf lhs then lhs := negf lhs; 54 if minusf rhs then rhs := negf rhs; 55 if lhs = rhs then 56 return if op eq 'sdiv or op eq 'nassoc then 'false else 'true; 57 % At most one of [lhs], [rhs] is zero. The following third reatment 58 % of zero sides is probably redundant. 59 if null lhs then << 60 if op eq 'sdiv then return 'false; 61 if op eq 'nassoc then return dvfsf_safield('neq,rhs,sop); 62 % We know [op] is one of ['div], ['assoc]. 63 return dvfsf_safield('equal,rhs,sop) 64 >>; 65 if null rhs then << 66 if op eq 'sdiv or op eq 'nassoc then 67 return dvfsf_safield('neq,lhs,sop); 68 if op eq 'assoc then 69 return dvfsf_safield('equal,lhs,sop); 70 % We know [op eq 'div] now. 71 return 'true 72 >>; 73 return dvfsf_saval1(op,lhs,rhs) 74 end; 75 76procedure dvfsf_saval1(op,lhs,rhs); 77 % Discretely valued field simplify atomic formula built with 78 % valuation relation subroutine. [op] is one of [div], [sdiv], 79 % [assoc], [nassoc]; [lhs] and [rhs] are nonzero SF's. Returns a 80 % formula equivalent to $[op]([lhs],[rhs])$. 81 begin scalar gcd,natf1,sff,junct; 82 junct := if op eq 'sdiv or op eq 'nassoc then 'and else 'or; 83 lhs := dvfsf_vsimpf lhs; 84 rhs := dvfsf_vsimpf rhs; 85 gcd := sfto_gcdf!*(lhs,rhs); 86 lhs := quotf(lhs,gcd); 87 rhs := quotf(rhs,gcd); 88 natf1 := dvfsf_saval2(op,lhs,rhs); 89 if junct eq 'and then << 90 if natf1 eq 'false then return 'false; 91 sff := dvfsf_safield('neq,gcd,'and); 92 return dvfsf_compose('and,natf1,sff) 93 >>; 94 % We know [junct eq 'or]. 95 if natf1 eq 'true then return natf1; 96 sff := dvfsf_safield('equal,gcd,'or); 97 return dvfsf_compose('or,natf1,sff) 98 end; 99 100procedure dvfsf_compose(op,at,f); 101 % Discretely valued field compose. [op] is either ['or] or ['and]; 102 % [at] is an atomic formula; [f] is a formula. Returns a formula 103 % equivalent to $[op](at,f)$. 104 if op eq 'or and (at eq 'true or f eq 'true) then 105 'true 106 else if op eq 'and and (at eq 'false or f eq 'false) then 107 'false 108 else if (at eq 'true) or (at eq 'false) then 109 f 110 else if (f eq 'true) or (f eq 'false) then 111 at 112 else if (op neq rl_op f) or not(cl_cxfp f) then 113 rl_mk2(op,at,f) 114 else 115 rl_mkn(op,at . rl_argn f); 116 117procedure dvfsf_saval2(op,lhs,rhs); 118 % Discretely valued field simplify atomic formula built with 119 % valuation relation subroutine. [op] is one of [div], [sdiv], 120 % [assoc], [nassoc]; [lhs] and [rhs] are nonzero SF's such that 121 % [lhs] and [rhs] are relatively prime. Returns a formula 122 % equivalent to $[op]([lhs],[rhs])$. 123 begin scalar natf1,w; 124 if dvfsf_p!* > 0 then % Concrete valuation given. 125 natf1 := dvfsf_sacval(op,lhs,rhs) 126 else << 127 w := dvfsf_saaval(op,lhs,rhs); 128 if rl_tvalp w then 129 natf1 := w 130 else if w neq 'failed then << 131 natf1 := w; % TODO: Repeat the trivial simplifications for [w]. 132 op := dvfsf_op natf1; 133 lhs := dvfsf_arg2l natf1; 134 rhs := dvfsf_arg2r natf1 135 >> else 136 natf1 := dvfsf_mk2(op,lhs,rhs) 137 >>; 138 if (op eq 'assor or op eq 'nassoc) and ordp(rhs,lhs) then 139 natf1 := dvfsf_mk2(op,rhs,lhs); 140 return natf1 141 end; 142 143procedure dvfsf_sacval(op,lhs,rhs); 144 % Discretely valued field simplify atomic formula built with 145 % valuation relation for concrete given valuation. [op] is one of 146 % [div], [sdiv], [assoc], [nassoc]; [lhs] and [rhs] are nonzero 147 % SF's. Returns a formula equivalent to $[op]([lhs],[rhs])$. 148 % Evaluate variable free atomic formulas and move the domain 149 % content to one side. 150 begin scalar lcont,rcont,lv,rv; 151 if domainp lhs and domainp rhs then << 152 if op eq 'assoc then 153 return if dvfsf_v lhs = dvfsf_v rhs then 'true else 'false; 154 if op eq 'nassoc then 155 return if dvfsf_v lhs neq dvfsf_v rhs then 'true else 'false; 156 if op eq 'sdiv then 157 return if dvfsf_v lhs < dvfsf_v rhs then 'true else 'false; 158 % We know [op eq 'div] now. 159 return if dvfsf_v lhs <= dvfsf_v rhs then 'true else 'false 160 >>; 161 % The content is non-zero. 162 lcont := sfto_dcontentf lhs; 163 lhs := quotf(lhs,lcont); 164 rcont := sfto_dcontentf rhs; 165 rhs := quotf(rhs,rcont); 166 lv := dvfsf_v lcont; 167 rv := dvfsf_v rcont; 168 if lv >= rv then 169 lhs := multf(numr simp ((dvfsf_p!*)**(lv-rv)),lhs) 170 else 171 rhs := multf(numr simp ((dvfsf_p!*)**(rv-lv)),rhs); 172 return dvfsf_mk2(op,lhs,rhs) 173 end; 174 175procedure dvfsf_safield(op,lhs,sop); 176 % Discretely valued field simplify atomic formula with field 177 % relation. [op] is either ['equal] or ['neq]; [lhs] is an SF; 178 % [sop] is a boolean operator. 179 % Returns a quantifier-free formula equivalent to $[op]([lhs],0)$. 180 begin 181 lhs := dvfsf_vsimpf lhs; 182 if domainp lhs then 183 if op eq 'equal then 184 return if null lhs then 'true else 'false 185 else % [op eq 'neq] 186 return if null lhs then 'false else 'true; 187 lhs := sfto_dprpartf lhs; 188 if dvfsf_p!*>0 then 189 return dvfsf_sapfacf(op,lhs,sop); 190 lhs := dvfsf_dppower lhs; 191 if domainp lhs then 192 return if op eq 'equal then 'false else 'true; 193 return dvfsf_sapfacf(op,lhs,sop) 194 end; 195 196procedure dvfsf_sapfacf(op,lhs,sop); 197 % Discretely valued field standard form polynomial factorization 198 % atomic formula with field relation. [op] is either ['equal] or 199 % [neq]. [lhs] is an SF. Returns a formula equivalent to 200 % $[op](lhs,0)$; [sop] is a boolean operator. This procedure 201 % possibly factorize [lhs] to explode the respective atomic 202 % formula. 203 begin scalar w,junct; 204 junct := if op eq 'equal then 'or else 'and; 205 if !*rlsifac and (!*rlsiexpla or !*rlsiexpl and sop = junct) then 206 return rl_smkn(junct, 207 for each x in cdr fctrf lhs collect dvfsf_sapeq(op,car x)); 208 return dvfsf_sapeq(op,lhs) 209 end; 210 211procedure dvfsf_dppower(f); 212 % Discretely valued field drop p power. [f] is an SF of the form 213 % $(p^n f')$. Returns $f'$ as an SF. 214 begin scalar qr,p; 215 p := numr simp 'p; 216 qr := qremf(f,p); 217 while null(cdr qr) do << 218 f := car qr; 219 qr := qremf(car qr,p); 220 >>; 221 return f 222 end; 223 224procedure dvfsf_saaval(op,lhs,rhs); 225 % Discretely valued field simplify atomic formula for abstract 226 % valuation. [op] is one of [div], [sdiv], [assoc], [nassoc]; [lhs] 227 % and [rhs] are SF's. Returns ['failed] or an atomic formula 228 % equivalent $[op]([lhs],[rhs])$. 229 begin scalar w; 230 w := dvfsf_sappow(op,lhs,rhs); 231 if w neq 'failed then 232 return w; 233 w := dvfsf_savpc(op,lhs,rhs); 234 if w neq 'failed then 235 return w; 236 w := dvfsf_sapureintc(op,lhs,rhs); 237 if w neq 'failed then 238 return w; 239 w := dvfsf_sapfactor(op,lhs,rhs); 240 if w neq 'failed then 241 return w; 242 return 'failed 243 end; 244 245procedure dvfsf_sappow(op,lhs,rhs); 246 % Discretely valued field simplify powers of p in atomic formula. 247 % [op] is one of ['div], ['sdiv], ['nassoc], ['assoc]; [lhs] and 248 % [rhs] are SF's. Returns ['failed] or a truth value. Simplifies 249 % atomic formulas which relates 1 to $z p^n$, for an integer [z] 250 % and a positive integer $n$ to a truth value. Otherwise ['failed] 251 % is returned. 252 begin scalar lp,rp; 253 lp := dvfsf_ppowerp lhs; 254 rp := dvfsf_ppowerp rhs; 255 if rp and lhs = numr simp 1 then 256 return if op = 'assoc then 'false else 'true; 257 if lp and rhs = numr simp 1 then 258 return if op = 'nassoc then 'true else 'false; 259 return 'failed 260 end; 261 262procedure dvfsf_savpc(op,lhs,rhs); 263 % Discretely valued field simplify atomic formulas build with 264 % valuation relation, p, and a constant. [op] is one of [div], 265 % [sdiv], [assoc], [nassoc]; [lhs] and [rhs] are SF's, such that 266 % [lhs] and [rhs] are relatively prime. Returns ['failed] or an 267 % atomic formula equivalent to $[op]([lhs],[rhs])$. The atomic 268 % formula is simplified, if it relates $z p^n$ to a constant; 269 % otherwise ['failed] is returned. 270 % 271 % WARNING: This simplifier is correct only for p-adic valued fields. 272 % 273 begin scalar w,op; 274 if not !*rlsifac then 275 return 'failed; 276 w := dvfsf_savpc1(op,lhs,rhs); 277 if w eq 'failed then 278 return 'failed; 279 op := dvfsf_op w; 280 if dvfsf_arg2l w = dvfsf_arg2r w then 281 return if op eq 'nassoc then 'false else 'true; 282 return w 283 end; 284 285procedure dvfsf_savpc1(op,lhs,rhs); 286 % Discretely valued field simplify atomic formulas build with 287 % valuation relation, p, and a constant subroutine. [op] is one of 288 % [div], [sdiv], [assoc], [nassoc]; [lhs] and [rhs] are SF's, such 289 % that [lhs] and [rhs] are relatively prime. Returns ['failed] or 290 % an atomic formula equivalent to $[op]([lhs],[rhs])$. The atomic 291 % formula is simplified, if it relates $z p^n$ to a constant; 292 % otherwise ['failed] is returned. 293 begin scalar n; 294 return if (domainp rhs) and (n := dvfsf_ppowerp lhs) then << 295 if op eq 'assoc then 296 dvfsf_mk2('nassoc,sfto_zdeqn(rhs,n),numr simp 1) 297 else if op eq 'nassoc then 298 dvfsf_mk2('assoc,sfto_zdeqn(rhs,n),numr simp 1) 299 else if op eq 'div then 300 dvfsf_mk2('nassoc,sfto_zdgen(rhs,n),numr simp 1) 301 else if op eq 'sdiv then 302 dvfsf_mk2('nassoc,sfto_zdgtn(rhs,n),numr simp 1) 303 else 304 rederr "Bug in dvfsf_savpc" 305 >> else if (domainp lhs) and (n := dvfsf_ppowerp rhs) then << 306 if op eq 'assoc then 307 dvfsf_mk2('nassoc,sfto_zdeqn(lhs,n),numr simp 1) 308 else if op eq 'nassoc then 309 dvfsf_mk2('assoc,sfto_zdeqn(lhs,n),numr simp 1) 310 else if op eq 'div then 311 dvfsf_mk2('assoc,sfto_zdgtn(lhs,n),numr simp 1) 312 else if op eq 'sdiv then 313 dvfsf_mk2('assoc,sfto_zdgen(lhs,n),numr simp 1) 314 else 315 rederr "Bug in dvfsf_savpc" 316 >> else 317 'failed 318 end; 319 320procedure dvfsf_ppowerp(u); 321 % Discretely valued field power of p predicate. [u] is an SF. 322 % Returns [nil] or a positive integer $n$. Tests [u] on 323 % representing a polynomial $z p^n$ for an integer $z$ and a 324 % natural number $n$. 325 begin scalar rou,w; 326 rou := sfto_reorder(u,'p); 327 w := (not domainp rou and mvar rou = 'p and 328 domainp lc rou and null red rou); 329 if w then 330 return ldeg u 331 end; 332 333procedure dvfsf_ppolyp(f); 334 % Discretely valued field p polynomial predicate. [f] is an SF. 335 % Returns [T] if [f] is a domian element or is a polynomial 336 % containing only the variable ['p] otherwise [nil] is returned. 337 begin scalar w; 338 if domainp f then 339 return t; 340 w := kernels f; 341 return null cdr w and car w eq 'p 342 end; 343 344procedure dvfsf_ppolydec(f); 345 % Discretely valued field p polynomial decomposition. [f] is an SF. 346 % Returns a list $(...,(a_i,n_i),...)$ such that $[f]=\sum_i 347 % a_ip^n_i$ and $n_i>n_{i+1}$. 348 if null f then 349 nil 350 else if domainp f then 351 {(f . 0)} 352 else 353 (lc f . ldeg f) . dvfsf_ppolydec red f; 354 355procedure dvfsf_vsimpf(f); 356 % Discretely valued field valuation simplification standard form. 357 % [f] is an SF. Returns an SF $f'$, such that for all terms $g$ we 358 % have $[f] \mathrel{\varrho} g$ if and only if $f' 359 % \mathrel{\varrho} g$. 360 begin scalar w,fdc,cep,c,n,cdc; 361 if domainp f then 362 return f; 363 if not dvfsf_ppolyp f then 364 return f; 365 fdc := reversip dvfsf_ppolydec(f); 366 w := car fdc; 367 fdc := cdr fdc; 368 if null fdc then 369 return f; 370 n := cdr w; 371 c := car w; 372 if (c = 1) or (c = -1) then 373 return numr simp {'expt,'p,n}; 374 cdc := sort(zfactor c,function greaterpcdr); 375 if n + cdr car cdc < cdr car fdc then 376 return numr simp {'times,c,{'expt,'p,n}}; 377 while cdc do << 378 cep := car cdc; 379 w := dvfsf_vsimpf1(car cep,cdr cep,n,fdc); 380 if w eq 'failed then 381 cdc := nil 382 else 383 cdc := cdr cdc; 384 >>; 385 if w eq 'failed then 386 return f; 387 return numr simp {'times,c,{'expt,'p,n}}; 388 end; 389 390procedure dvfsf_vsimpf1(q,m,n,fdc); 391 % Discretely valued field valuation simplification standard form 392 % subroutine. [f] is an SF. Returns an SF $f'$, such that for all 393 % terms $g$ we have $[f] \mathrel{\varrho} g$ if and only if $f' 394 % \mathrel{\varrho} g$. 395 begin scalar w,k,qp; 396 while fdc do << 397 w := car fdc; % a pair $(a . n)$ with $a*p^n$ is monomial of [f] 398 k := cdr w - n; 399 if m<k then << 400 w := nil; 401 fdc := nil 402 >> else << 403 qp := abs(q)^(m-k+1); 404 if gcdf!*(qp,car w) = qp then 405 fdc := cdr fdc 406 else << 407 w := 'failed; 408 fdc := nil; 409 >> 410 >> 411 >>; 412 if w eq 'failed then 413 return 'failed 414 end; 415 416procedure dvfsf_sapureintc(op,lhs,rhs); 417 % Discretely valued field simplifiy atomic formulas pure integer 418 % constraints. [op] is one of ['assoc], ['nassoc], ['div] or 419 % ['sdiv]; [lhs] and [rhs] are SF's. Returns ['failed] or an atomic 420 % formula. This procedure simplifies atomic formulas which relates 421 % integers. 422 if not !*rlsifac then 423 'failed 424 else if not(domainp lhs and domainp rhs) then 425 'failed 426 else if op eq 'assoc or op eq 'nassoc then 427 dvfsf_mk2(op,sfto_sqfpartz(lhs*rhs),numr simp 1) 428 else if op eq 'div then 429 dvfsf_mk2('assoc,sfto_sqfpartz lhs,numr simp 1) 430 else if op eq 'sdiv then 431 dvfsf_mk2('nassoc,sfto_sqfpartz rhs,numr simp 1) 432 else 433 rederr "bug dvfsf_sapureintc"; 434 435procedure dvfsf_sapeq(op,lhs); 436 % Discretely valued field simplify atomic formula p equation. [op] 437 % is either ['equal] or ['neq]. [lhs] is an SF. Returns an atomic 438 % formula equivalent to $[op]([lhs],0)$. This procedures 439 % simplifies atomic formulas of the form $[op](z1 p + z2,0)$, with 440 % $z1$ and $z2$ relatively prime. 441 if not(not(domainp lhs) and mvar lhs eq 'p and ldeg lhs = 1 442 and domainp lc lhs and domainp red lhs) 443 then 444 dvfsf_mk2(op,lhs,nil) 445 else if (lc lhs neq 1) or not(minusf red lhs) or not(primep red lhs) then 446 if op eq 'equal then 'false else 'true 447 else 448 dvfsf_mk2(if op eq 'equal then 'nassoc else 'assoc, 449 negf red lhs,numr simp 1); 450 451procedure dvfsf_sapfactor(op,lhs,rhs); 452 % Discretely valued field simplify atomic formula p factor. [op] is 453 % one of ['assoc], ['nassoc], ['div], or ['sdiv]. [lhs] and [rhs] 454 % are SF's. Returns ['failed] or atomic formula equivalent to 455 % $[op]([lhs],[rhs])$. This procedures simplifies atomic formulas 456 % of the form $f || p*g$, $p*f | g$. 457 begin scalar w; 458 if op eq 'sdiv then << 459 w := qremf(rhs,numr simp 'p); 460 if null cdr w then 461 return dvfsf_mk2('div,lhs,car w); 462 return 'failed 463 >>; 464 if op eq 'div then << 465 w := qremf(lhs,numr simp 'p); 466 if null cdr w then 467 return dvfsf_mk2('sdiv,car w,rhs); 468 return 'failed 469 >>; 470 return 'failed 471 end; 472 473endmodule; % [dvfsfsiat] 474 475end; % of file 476