Annotation of OpenXM_contrib2/asir2018/builtin/al.c, Revision 1.1
1.1 ! noro 1: /* $OpenXM$ */
! 2: /* ----------------------------------------------------------------------
! 3: $Id: al.c,v 1.6 2001/03/08 18:51:10 sturm Exp $
! 4: ----------------------------------------------------------------------
! 5: File al.c: Real quantifier elimination code for RISA/ASIR
! 6:
! 7: Copyright (c) 1996-2001 by
! 8: Andreas Dolzmann and Thomas Sturm, University of Passau, Germany
! 9: dolzmann@uni-passau.de, sturm@uni-passau.de
! 10: ----------------------------------------------------------------------
! 11: */
! 12:
! 13: #include <ca.h>
! 14: #include <parse.h>
! 15: #include <al.h>
! 16:
! 17: void Preverse();
! 18: void Phugo();
! 19: void Pex();
! 20: void Pall();
! 21: void constrq();
! 22: void Pfop();
! 23: void Pfargs();
! 24: void Pfopargs();
! 25: void Pcompf();
! 26: void Patnum();
! 27: int gauss_abc();
! 28: int compf();
! 29: void Patl();
! 30: void Pqevar();
! 31: void Pqe();
! 32: void Psimpl();
! 33: void Psubf();
! 34: void Pnnf();
! 35: void smkjf();
! 36: void simpl();
! 37: void simpl1();
! 38: void simpl_gand();
! 39: void simpl_th2atl();
! 40: int simpl_gand_udnargls();
! 41: int simpl_gand_thupd();
! 42: int simpl_gand_thprsism();
! 43: int simpl_gand_smtbdlhs();
! 44: int simpl_gand_smtbelhs();
! 45: void lbc();
! 46: void replaceq();
! 47: void deleteq();
! 48: void simpl_gand_insert_a();
! 49: void simpl_gand_insert_c();
! 50: int compaf();
! 51: int comprel();
! 52: int synequalf();
! 53: void simpl_impl();
! 54: void simpl_equiv();
! 55: void simpl_a();
! 56: void simpl_a_o();
! 57: void simpl_a_no();
! 58: void qe();
! 59: void blocksplit();
! 60: void qeblock();
! 61: int qeblock_verbose1a();
! 62: void qeblock_verbose1b();
! 63: void qeblock_verbose2();
! 64: void qeblock_verbose0();
! 65: int getmodulus();
! 66: int qevar();
! 67: int gausselim();
! 68: int delv();
! 69: int translate();
! 70: int translate_a();
! 71: void translate_a1();
! 72: void mklgp();
! 73: void translate_a2();
! 74: void mkqgp();
! 75: void getqcoeffs();
! 76: void mkdiscr();
! 77: int al_reorder();
! 78: void indices();
! 79: void mkeset();
! 80: int selectside();
! 81: int cmp2n();
! 82: void add2eset();
! 83: void seproots();
! 84: void sp_add2eset();
! 85: void subgpf();
! 86: void subref();
! 87: void subref_a();
! 88: void substd_a();
! 89: void substd_a1();
! 90: void substd_a2();
! 91: void substd_a21();
! 92: void substd_a21_equal();
! 93: void substd_a21_leq();
! 94: void substd_a21_lessp();
! 95: void getrecoeffs();
! 96: void subinf_a();
! 97: void subinf_a_o();
! 98: void subinf_a_o1();
! 99: void subtrans_a_no();
! 100: void subpme_a();
! 101: void subpme_a_o();
! 102: void subpme_a_o1();
! 103: int comember();
! 104: void coadd();
! 105: int coget();
! 106: int colen();
! 107: void apply2ats();
! 108: void atl();
! 109: void atl1();
! 110: void atnum();
! 111: void atnum1();
! 112: void pnegate();
! 113: void subf();
! 114: void subf_a();
! 115: void nnf();
! 116: void nnf1();
! 117: void ap();
! 118: void freevars();
! 119: void freevars1();
! 120: void freevars1_a();
! 121: void rep();
! 122: void gpp();
! 123: void esetp();
! 124: void nodep();
! 125: void gauss_mkeset1();
! 126: void gauss_mkeset2();
! 127:
! 128: extern int Verbose;
! 129:
! 130: struct oRE {
! 131: P p;
! 132: P discr;
! 133: int rootno;
! 134: int itype;
! 135: };
! 136:
! 137: typedef struct oRE *RE;
! 138:
! 139: struct oGP {
! 140: F g;
! 141: RE p;
! 142: };
! 143:
! 144: typedef struct oGP *GP;
! 145:
! 146: struct oCEL {
! 147: VL vl;
! 148: F mat;
! 149: };
! 150:
! 151: typedef struct oCEL *CEL;
! 152:
! 153: struct oCONT {
! 154: NODE first;
! 155: NODE last;
! 156: };
! 157:
! 158: typedef struct oCONT *CONT;
! 159:
! 160: struct oQVL {
! 161: oFOP q;
! 162: VL vl;
! 163: };
! 164:
! 165: typedef struct oQVL *QVL;
! 166:
! 167: #define GUARD(x) ((x)->g)
! 168: #define POINT(x) ((x)->p)
! 169: #define NEWGP(x) ((x)=(GP)MALLOC(sizeof(struct oGP)))
! 170: #define MKGP(x,g,p) (NEWGP(x),GUARD(x)=g,POINT(x)=p)
! 171:
! 172: #define NEWRE(x) ((x)=(RE)MALLOC(sizeof(struct oRE)))
! 173: #define MKRE(x,pp,d,rn,i) \
! 174: (NEWRE(x),(x)->p=pp,(x)->discr=d,(x)->rootno=rn,(x)->itype=i)
! 175: #define DISC(re) ((re)->discr)
! 176: #define ROOTNO(re) ((re)->rootno)
! 177: #define ITYPE(re) ((re)->itype)
! 178:
! 179: #define STD 0
! 180: #define EPS 1
! 181: #define PEPS 2
! 182: #define MEPS -2
! 183: #define PINF 3
! 184: #define MINF -3
! 185:
! 186: #define NEWQVL(x) ((x)=(QVL)MALLOC(sizeof(struct oQVL)))
! 187: #define MKQVL(x,qq,vvl) (NEWQVL(x),(x)->q=qq,(x)->vl=vvl)
! 188: #define VARL(x) (x)->vl
! 189: #define QUANT(x) (x)->q
! 190:
! 191: #define NUMBER(p) (p==0 || NUM(p))
! 192: #define NZNUMBER(p) (p && NUM(p))
! 193:
! 194: #define MKVL(a,b,c) \
! 195: (NEWVL(a),(a)->v=(V)b,NEXT(a)=(VL)(c))
! 196: #define NEXTVL(r,c) \
! 197: if(!(r)){NEWVL(r);(c)=(r);}else{NEWVL(NEXT(c));(c)=NEXT(c);}
! 198:
! 199: #define NEWCEL(x) ((x)=(CEL)MALLOC(sizeof(struct oCEL)))
! 200: #define MKCEL(x,vvl,mmat) (NEWCEL(x),(x)->vl=vvl,(x)->mat=mmat)
! 201: #define VRL(x) ((x)->vl)
! 202:
! 203: #define FIRST(x) ((x)->first)
! 204: #define LAST(x) ((x)->last)
! 205: #define MKCONT(x) ((x)=(CONT)MALLOC(sizeof(struct oCONT)),FIRST(x)=LAST(x)=NULL)
! 206:
! 207: struct ftab al_tab[] = {
! 208: {"simpl",Psimpl,-2},
! 209: {"ex",Pex,-2},
! 210: {"all",Pall,-2},
! 211: {"fop",Pfop,1},
! 212: {"fargs",Pfargs,1},
! 213: {"fopargs",Pfopargs,1},
! 214: {"compf",Pcompf,2},
! 215: {"atl",Patl,1},
! 216: {"qevar",Pqevar,2},
! 217: {"qe",Pqe,1},
! 218: {"atnum",Patnum,1},
! 219: {"subf",Psubf,3},
! 220: {"nnf",Pnnf,1},
! 221: {"hugo",Phugo,4},
! 222: {0,0,0}
! 223: };
! 224:
! 225: void Phugo(arg,rp)
! 226: NODE arg;
! 227: F *rp;
! 228: {
! 229: substd_a21_equal(BDY(arg),BDY(NEXT(arg)),BDY(NEXT(NEXT(arg))),BDY(NEXT(NEXT(NEXT(arg)))),rp);
! 230: ap(*rp);
! 231: substd_a21_leq(BDY(arg),BDY(NEXT(arg)),BDY(NEXT(NEXT(arg))),BDY(NEXT(NEXT(NEXT(arg)))),rp);
! 232: ap(*rp);
! 233: substd_a21_lessp(BDY(arg),BDY(NEXT(arg)),BDY(NEXT(NEXT(arg))),BDY(NEXT(NEXT(NEXT(arg)))),rp);
! 234: ap(*rp);
! 235: }
! 236:
! 237: void Pex(arg,rp)
! 238: NODE arg;
! 239: F *rp;
! 240: {
! 241: if (argc(arg) == 1)
! 242: constrq(AL_EX,0,(F)BDY(arg),rp);
! 243: else
! 244: constrq(AL_EX,BDY(arg),(F)BDY(NEXT(arg)),rp);
! 245: }
! 246:
! 247: void Pall(arg,rp)
! 248: NODE arg;
! 249: F *rp;
! 250: {
! 251: if (argc(arg) == 1)
! 252: constrq(AL_ALL,0,(F)BDY(arg),rp);
! 253: else
! 254: constrq(AL_ALL,BDY(arg),(F)BDY(NEXT(arg)),rp);
! 255: }
! 256:
! 257: void constrq(q,vars,m,rp)
! 258: oFOP q;
! 259: Obj vars;
! 260: F m,*rp;
! 261: {
! 262: VL sc;
! 263: NODE varl=NULL,varlc,arg;
! 264: P p;
! 265:
! 266: if (!vars) {
! 267: for (freevars(m,&sc); sc; sc=NEXT(sc)) {
! 268: NEXTNODE(varl,varlc);
! 269: MKV(VR(sc),p);
! 270: BDY(varlc) = (pointer)p;
! 271: }
! 272: } else if (OID(vars) == O_LIST) {
! 273: MKNODE(arg,vars,NULL);
! 274: Preverse(arg,&vars);
! 275: varl = BDY((LIST)vars);
! 276: } else
! 277: MKNODE(varl,vars,NULL);
! 278: for (; varl; varl=NEXT(varl)) {
! 279: MKQF(*rp,q,VR((P)BDY(varl)),m);
! 280: m = *rp;
! 281: }
! 282: }
! 283:
! 284: void Pfop(arg,rp)
! 285: NODE arg;
! 286: Z *rp;
! 287: {
! 288: oFOP op;
! 289:
! 290: op = FOP((F)ARG0(arg));
! 291: STOQ((int)op,*rp);
! 292: }
! 293:
! 294: void Pfargs(arg,rp)
! 295: NODE arg;
! 296: LIST *rp;
! 297: {
! 298: oFOP op;
! 299: LIST l;
! 300: NODE n1,n2;
! 301: F f;
! 302: P x;
! 303:
! 304: f = (F)ARG0(arg);
! 305: op = FOP(f);
! 306: if ( AL_TVAL(op) )
! 307: n1 = 0;
! 308: else if ( AL_JUNCT(op) )
! 309: n1 = FJARG(f);
! 310: else if ( AL_QUANT(op) ) {
! 311: MKV(FQVR(f),x);
! 312: MKNODE(n2,FQMAT(f),0); MKNODE(n1,x,n2);
! 313: } else if (AL_ATOMIC(op) )
! 314: MKNODE(n1,FPL(f),0);
! 315: else if ( AL_UNI(op) )
! 316: MKNODE(n1,FARG(f),0);
! 317: else if ( AL_EXT(op) ) {
! 318: MKNODE(n2,FRHS(f),0); MKNODE(n1,FLHS(f),n2);
! 319: }
! 320: MKLIST(l,n1);
! 321: *rp = l;
! 322: }
! 323:
! 324: void Pfopargs(arg,rp)
! 325: NODE arg;
! 326: LIST *rp;
! 327: {
! 328: oFOP op;
! 329: LIST l;
! 330: NODE n0,n1,n2;
! 331: F f;
! 332: P x;
! 333: Z op1;
! 334:
! 335: f = (F)ARG0(arg);
! 336: op = FOP(f);
! 337: STOQ((int)op,op1);
! 338: if ( AL_TVAL(op) )
! 339: n1 = 0;
! 340: else if ( AL_JUNCT(op) )
! 341: n1 = FJARG(f);
! 342: else if ( AL_QUANT(op) ) {
! 343: MKV(FQVR(f),x);
! 344: MKNODE(n2,FQMAT(f),0); MKNODE(n1,x,n2);
! 345: } else if (AL_ATOMIC(op) )
! 346: MKNODE(n1,FPL(f),0);
! 347: else if ( AL_UNI(op) )
! 348: MKNODE(n1,FARG(f),0);
! 349: else if ( AL_EXT(op) ) {
! 350: MKNODE(n2,FRHS(f),0); MKNODE(n1,FLHS(f),n2);
! 351: }
! 352: MKNODE(n0,op1,n1);
! 353: MKLIST(l,n0);
! 354: *rp = l;
! 355: }
! 356:
! 357: void Pcompf(arg,rp)
! 358: NODE arg;
! 359: Z *rp;
! 360: {
! 361: STOQ(compf(CO,BDY(arg),BDY(NEXT(arg))),*rp);
! 362: }
! 363:
! 364: void Patnum(arg,rp)
! 365: NODE arg;
! 366: Q *rp;
! 367: {
! 368: atnum(BDY(arg),rp);
! 369: }
! 370:
! 371: void Patl(arg,rp)
! 372: NODE arg;
! 373: LIST *rp;
! 374: {
! 375: NODE h;
! 376:
! 377: atl(BDY(arg),&h);
! 378: MKLIST(*rp,h);
! 379: }
! 380:
! 381: void Pqevar(arg,rp)
! 382: NODE arg;
! 383: F *rp;
! 384: {
! 385: qevar(BDY(arg),VR((P)BDY(NEXT(arg))),rp);
! 386: }
! 387:
! 388: void Pqe(arg,rp)
! 389: NODE arg;
! 390: F *rp;
! 391: {
! 392: qe(BDY(arg),rp);
! 393: }
! 394:
! 395: void Psubf(arg,rp)
! 396: NODE arg;
! 397: F *rp;
! 398: {
! 399: subf(CO,(F)BDY(arg),VR((P)BDY(NEXT(arg))),(P)BDY(NEXT(NEXT(arg))),rp);
! 400: }
! 401:
! 402: void Pnnf(arg,rp)
! 403: NODE arg;
! 404: F *rp;
! 405: {
! 406: nnf((F)BDY(arg),rp);
! 407: }
! 408:
! 409: /* Simplification */
! 410:
! 411: /* Return values of simpl_gand_udnargls() */
! 412: #define GINCONSISTENT 0
! 413: #define OK 1
! 414: #define NEWAT 2
! 415:
! 416: /* Return values of THPRSISM() */
! 417: #define CONTINUE 10
! 418: #define DROP 11
! 419: #define REPLACE 12
! 420: #define KILL 13
! 421:
! 422: void Psimpl(argl,rp)
! 423: NODE argl;
! 424: F *rp;
! 425: {
! 426: if (argc(argl) == 1)
! 427: simpl(BDY(argl),(NODE)NULL,rp);
! 428: else
! 429: simpl(BDY(argl),BDY((LIST)BDY(NEXT(argl))),rp);
! 430: }
! 431:
! 432: void smkjf(pf,j,argl)
! 433: F *pf;
! 434: oFOP j;
! 435: NODE argl;
! 436: {
! 437: if (!argl)
! 438: MKTV(*pf,AL_NEUTRAL(j));
! 439: else if (!NEXT(argl))
! 440: *pf = (F)BDY(argl);
! 441: else
! 442: MKJF(*pf,j,argl);
! 443: }
! 444:
! 445: void simpl(f,th,pnf)
! 446: F f,*pnf;
! 447: NODE th;
! 448: {
! 449: simpl1(f,th,0,pnf);
! 450: }
! 451:
! 452: void simpl1(f,th,n,pnf)
! 453: F f,*pnf;
! 454: NODE th;
! 455: int n;
! 456: {
! 457: F h;
! 458: oFOP op=FOP(f);
! 459:
! 460: if (AL_ATOMIC(op)) {
! 461: simpl_a(f,pnf);
! 462: return;
! 463: }
! 464: if (AL_JUNCT(op)) {
! 465: simpl_gand(op,AL_NEUTRAL(op),AL_OMNIPOT(op),FJARG(f),th,n,pnf);
! 466: return;
! 467: }
! 468: if (AL_TVAL(op)) {
! 469: *pnf = f;
! 470: return;
! 471: }
! 472: if (AL_QUANT(op)) {
! 473: simpl1(FQMAT(f),(NODE)NULL,n+1,&h);
! 474: MKQF(*pnf,op,FQVR(f),h);
! 475: return;
! 476: }
! 477: if (op == AL_NOT) {
! 478: simpl1(FARG(f),th,n+1,&h);
! 479: switch (FOP(h)) {
! 480: case AL_TRUE:
! 481: *pnf = F_FALSE;
! 482: break;
! 483: case AL_FALSE:
! 484: *pnf = F_TRUE;
! 485: break;
! 486: default:
! 487: MKUF(*pnf,AL_NOT,h);
! 488: }
! 489: return;
! 490: }
! 491: if (op == AL_IMPL) {
! 492: simpl_impl(AL_IMPL,FLHS(f),FRHS(f),th,n,pnf);
! 493: return;
! 494: }
! 495: if (op == AL_REPL) {
! 496: simpl_impl(AL_REPL,FRHS(f),FLHS(f),th,n,pnf);
! 497: return;
! 498: }
! 499: if (op == AL_EQUIV) {
! 500: simpl_equiv(FLHS(f),FRHS(f),th,n,pnf);
! 501: return;
! 502: }
! 503: else
! 504: error("unknown operator in simpl1");
! 505: }
! 506:
! 507: void simpl_gand(gand,gtrue,gfalse,argl,oth,n,pnf)
! 508: oFOP gand,gtrue,gfalse;
! 509: NODE argl,oth;
! 510: int n;
! 511: F *pnf;
! 512: {
! 513: NODE cnargl=NULL,cc=NULL,cnargl2=NULL,cc2=NULL,th=NULL,thc=NULL,nargl,narglc;
! 514: F fgfalse,h;
! 515: int st;
! 516:
! 517: for (; oth; oth = NEXT(oth)) {
! 518: NEXTNODE(th,thc);
! 519: BDY(thc) = BDY(oth);
! 520: }
! 521: for (; argl; argl = NEXT(argl)) {
! 522: if (FOP((F)BDY(argl)) == gfalse) {
! 523: *pnf = (F)BDY(argl);
! 524: return;
! 525: }
! 526: if (AL_ATOMIC(FOP((F)BDY(argl)))) {
! 527: simpl_a((F)BDY(argl),&h);
! 528: if (FOP(h) == gfalse) {
! 529: *pnf = h;
! 530: return;
! 531: }
! 532: st = simpl_gand_udnargls(gand,gtrue,h,n,&th,&thc,&cnargl,&cc);
! 533: if (st == GINCONSISTENT) {
! 534: MKTV(fgfalse,gfalse);
! 535: *pnf = fgfalse;
! 536: return;
! 537: }
! 538: } else
! 539: simpl_gand_insert_c((F)BDY(argl),&cnargl,&cc);
! 540: }
! 541: for (; cnargl != NULL; cnargl = NEXT(cnargl)) {
! 542: simpl1((F)BDY(cnargl),th,n+1,&h);
! 543: if (FOP(h) == gfalse) {
! 544: *pnf = h;
! 545: return;
! 546: }
! 547: st = simpl_gand_udnargls(gand,gtrue,h,n,&th,&thc,&cnargl2,&cc2);
! 548: switch (st) {
! 549: case GINCONSISTENT:
! 550: MKTV(fgfalse,gfalse);
! 551: *pnf = fgfalse;
! 552: return;
! 553: case NEWAT:
! 554: if (cnargl2 != NULL) {
! 555: if (cnargl != NULL)
! 556: NEXT(cc) = cnargl2;
! 557: else
! 558: cnargl = cnargl2;
! 559: cc = cc2;
! 560: cnargl2 = cc2 = NULL;
! 561: }
! 562: break;
! 563: }
! 564: }
! 565: simpl_th2atl(gand,th,n,&nargl,&narglc);
! 566: if (nargl == NULL)
! 567: nargl = cnargl2;
! 568: else
! 569: NEXT(narglc) = cnargl2;
! 570: smkjf(pnf,gand,nargl);
! 571: }
! 572:
! 573: void simpl_th2atl(gand,th,n,patl,patlc)
! 574: oFOP gand;
! 575: NODE th,*patl,*patlc;
! 576: int n;
! 577: {
! 578: NODE atl=NULL,atlc=NULL;
! 579: F at,negat;
! 580:
! 581: switch (gand) {
! 582: case AL_AND:
! 583: for (; th; th = NEXT(th)) {
! 584: if (LBFLB((LBF)BDY(th)) == n) {
! 585: NEXTNODE(atl,atlc);
! 586: BDY(atlc) = (pointer)LBFF((LBF)BDY(th));
! 587: }
! 588: }
! 589: break;
! 590: case AL_OR:
! 591: for (; th; th = NEXT(th)) {
! 592: if (LBFLB((LBF)BDY(th)) == n) {
! 593: at = LBFF((LBF)BDY(th));
! 594: MKAF(negat,AL_LNEGOP(FOP(at)),FPL(at));
! 595: NEXTNODE(atl,atlc);
! 596: BDY(atlc) = (pointer)negat;
! 597: }
! 598: }
! 599: break;
! 600: }
! 601: *patl = atl;
! 602: *patlc = atlc;
! 603: }
! 604:
! 605: int simpl_gand_udnargls(gand,gtrue,narg,n,pth,pthc,pcnargl,pcc)
! 606: oFOP gand,gtrue;
! 607: F narg;
! 608: int n;
! 609: NODE *pth,*pthc,*pcnargl,*pcc;
! 610: {
! 611: NODE sargl;
! 612: F h;
! 613: oFOP op;
! 614: int st,found=OK;
! 615:
! 616: op = FOP(narg);
! 617: if (op == gtrue)
! 618: return(OK);
! 619: if (AL_ATOMIC(op))
! 620: return(simpl_gand_thupd(gand,narg,n,pth,pthc));
! 621: if (op == gand) {
! 622: sargl = FJARG(narg);
! 623: for (; sargl; sargl = NEXT(sargl)) {
! 624: h = (F)BDY(sargl);
! 625: if (AL_ATOMIC(FOP(h))) {
! 626: st = simpl_gand_thupd(gand,h,n,pth,pthc);
! 627: switch (st) {
! 628: case NEWAT:
! 629: found = NEWAT;
! 630: break;
! 631: case GINCONSISTENT:
! 632: return(GINCONSISTENT);
! 633: }
! 634: } else
! 635: simpl_gand_insert_c(h,pcnargl,pcc);
! 636: }
! 637: return(found);
! 638: }
! 639: simpl_gand_insert_c(narg,pcnargl,pcc);
! 640: return(OK);
! 641: }
! 642:
! 643: int simpl_gand_thupd(top,at,n,pth,pthc)
! 644: oFOP top;
! 645: F at;
! 646: int n;
! 647: NODE *pth,*pthc;
! 648: {
! 649: LBF atpr,thpr;
! 650: NODE scth;
! 651: int st;
! 652: F h;
! 653:
! 654: if (top == AL_OR) {
! 655: MKAF(h,AL_LNEGOP(FOP(at)),FPL(at));
! 656: at = h;
! 657: }
! 658: MKLBF(atpr,at,n);
! 659: for (scth = *pth; scth; scth = NEXT(scth)) {
! 660: thpr = (LBF)BDY(scth);
! 661: st = simpl_gand_thprsism(thpr,&atpr);
! 662: switch (st) {
! 663: case GINCONSISTENT:
! 664: return(GINCONSISTENT);
! 665: case DROP:
! 666: return(OK);
! 667: case REPLACE:
! 668: /* replaceq(*pth,(pointer)thpr,(pointer)atpr,pth,pthc); */
! 669: /* return(NEWAT); */
! 670: case KILL:
! 671: deleteq(*pth,(pointer)thpr,(pointer)pth,pthc);
! 672: }
! 673: }
! 674: NEXTNODE(*pth,*pthc);
! 675: BDY(*pthc) = (pointer)atpr;
! 676: return(NEWAT);
! 677: }
! 678:
! 679: int simpl_gand_thprsism(thpr,patpr)
! 680: LBF thpr,*patpr;
! 681: {
! 682: P thlbc,atlbc,thlhs1,atlhs1,difference;
! 683: oFOP natfop;
! 684: F nat;
! 685: LBF natpr;
! 686: int st;
! 687:
! 688: lbc(FPL(LBFF(*patpr)),&atlbc);
! 689: mulp(CO,FPL(LBFF(thpr)),atlbc,&thlhs1);
! 690: lbc(FPL(LBFF(thpr)),&thlbc);
! 691: mulp(CO,FPL(LBFF(*patpr)),thlbc,&atlhs1);
! 692: subp(CO,thlhs1,atlhs1,&difference);
! 693: if (!NUMBER(difference))
! 694: return(CONTINUE);
! 695: if (difference == NULL) {
! 696: st = simpl_gand_smtbelhs(FOP(LBFF(thpr)),FOP(LBFF(*patpr)),&natfop);
! 697: if (st == REPLACE) {
! 698: MKAF(nat,natfop,FPL(LBFF(*patpr)));
! 699: MKLBF(natpr,nat,LBFLB(*patpr));
! 700: *patpr = natpr;
! 701: };
! 702: return(st);
! 703: }
! 704: return(simpl_gand_smtbdlhs(FOP(LBFF(thpr)),FOP(LBFF(*patpr)),difference));
! 705: }
! 706:
! 707: int simpl_gand_smtbelhs(thop,atop,pnatop)
! 708: oFOP thop,atop,*pnatop;
! 709: {
! 710: if (atop == thop)
! 711: return(DROP);
! 712:
! 713: switch (thop) {
! 714: case AL_EQUAL:
! 715: switch (atop) {
! 716: case AL_NEQ:
! 717: case AL_LESSP:
! 718: case AL_GREATERP:
! 719: return(GINCONSISTENT);
! 720: case AL_LEQ:
! 721: case AL_GEQ:
! 722: return(DROP);
! 723: }
! 724: case AL_NEQ:
! 725: switch (atop) {
! 726: case AL_EQUAL:
! 727: return(GINCONSISTENT);
! 728: case AL_LEQ:
! 729: *pnatop = AL_LESSP;
! 730: return(REPLACE);
! 731: case AL_GEQ:
! 732: *pnatop = AL_GREATERP;
! 733: return(REPLACE);
! 734: case AL_LESSP:
! 735: case AL_GREATERP:
! 736: *pnatop = atop;
! 737: return(REPLACE);
! 738: }
! 739: case AL_LEQ:
! 740: switch (atop) {
! 741: case AL_EQUAL:
! 742: case AL_GEQ:
! 743: *pnatop = AL_EQUAL;
! 744: return(REPLACE);
! 745: case AL_NEQ:
! 746: case AL_LESSP:
! 747: *pnatop = AL_LESSP;
! 748: return(REPLACE);
! 749: case AL_GREATERP:
! 750: return(GINCONSISTENT);
! 751: }
! 752: case AL_GEQ:
! 753: switch (atop) {
! 754: case AL_EQUAL:
! 755: case AL_LEQ:
! 756: *pnatop = AL_EQUAL;
! 757: return(REPLACE);
! 758: case AL_NEQ:
! 759: case AL_GREATERP:
! 760: *pnatop = AL_GREATERP;
! 761: return(REPLACE);
! 762: case AL_LESSP:
! 763: return(GINCONSISTENT);
! 764: }
! 765: case AL_LESSP:
! 766: switch (atop) {
! 767: case AL_EQUAL:
! 768: case AL_GEQ:
! 769: case AL_GREATERP:
! 770: return(GINCONSISTENT);
! 771: case AL_NEQ:
! 772: case AL_LEQ:
! 773: return(DROP);
! 774: }
! 775: case AL_GREATERP:
! 776: switch (atop) {
! 777: case AL_EQUAL:
! 778: case AL_LEQ:
! 779: case AL_LESSP:
! 780: return(GINCONSISTENT);
! 781: case AL_NEQ:
! 782: case AL_GEQ:
! 783: return(DROP);
! 784: }
! 785: }
! 786: }
! 787:
! 788: int simpl_gand_smtbdlhs(thop,atop,difference)
! 789: oFOP thop,atop;
! 790: P difference;
! 791: {
! 792: oFOP op1,op2;
! 793: int drop1,drop2;
! 794:
! 795: if (cmpz((Z)difference,0) == 1) { /* good luck with the next compiler */
! 796: op1 = atop;
! 797: op2 = thop;
! 798: drop1 = DROP;
! 799: drop2 = KILL;
! 800: } else {
! 801: op1 = thop;
! 802: op2 = atop;
! 803: drop1 = KILL;
! 804: drop2 = DROP;
! 805: }
! 806: switch (op1) {
! 807: case AL_EQUAL:
! 808: switch (op2) {
! 809: case AL_EQUAL:
! 810: case AL_LEQ:
! 811: case AL_LESSP:
! 812: return(GINCONSISTENT);
! 813: default:
! 814: return(drop2);
! 815: }
! 816: case AL_NEQ:
! 817: case AL_LEQ:
! 818: case AL_LESSP:
! 819: switch (op2) {
! 820: case AL_EQUAL:
! 821: case AL_LEQ:
! 822: case AL_LESSP:
! 823: return(drop1);
! 824: default:
! 825: return(CONTINUE);
! 826: }
! 827: case AL_GEQ:
! 828: switch(op2) {
! 829: case AL_EQUAL:
! 830: case AL_LEQ:
! 831: case AL_LESSP:
! 832: return(GINCONSISTENT);
! 833: default:
! 834: return(drop2);
! 835: }
! 836: case AL_GREATERP:
! 837: switch (op2) {
! 838: case AL_EQUAL:
! 839: case AL_LEQ:
! 840: case AL_LESSP:
! 841: return(GINCONSISTENT);
! 842: default:
! 843: return(drop2);
! 844: }
! 845: }
! 846: }
! 847:
! 848: void lbc(f,pc)
! 849: P f,*pc;
! 850: {
! 851: for (*pc = f; !NUM(*pc); *pc = COEF(DC(*pc)))
! 852: ;
! 853: }
! 854:
! 855: void replaceq(l,old,new,pnl,pnlc)
! 856: NODE l,*pnl,*pnlc;
! 857: pointer old,new;
! 858: {
! 859: *pnl = NULL;
! 860: for (; l; l = NEXT(l)) {
! 861: NEXTNODE(*pnl,*pnlc);
! 862: if(BDY(l) == old)
! 863: BDY(*pnlc) = new;
! 864: else
! 865: BDY(*pnlc) = BDY(l);
! 866: }
! 867: }
! 868:
! 869: void deleteq(l,obj,pnl,pnlc)
! 870: NODE l,*pnl,*pnlc;
! 871: pointer obj;
! 872: {
! 873: *pnl = NULL;
! 874: for (; l; l = NEXT(l))
! 875: if(BDY(l) != obj) {
! 876: NEXTNODE(*pnl,*pnlc);
! 877: BDY(*pnlc) = BDY(l);
! 878: }
! 879: }
! 880:
! 881: void simpl_gand_insert_a(f,paargl,pac)
! 882: F f;
! 883: NODE *paargl,*pac;
! 884: {
! 885: int w;
! 886: NODE n,sc,prev;
! 887:
! 888: if (*paargl == 0) {
! 889: NEXTNODE(*paargl,*pac);
! 890: BDY(*pac) = (pointer)f;
! 891: return;
! 892: }
! 893: w = compaf(CO,BDY(*pac),f);
! 894: if (w == 1) {
! 895: NEXTNODE(*paargl,*pac);
! 896: BDY(*pac) = (pointer)f;
! 897: return;
! 898: }
! 899: if (w == 0)
! 900: return;
! 901: w = compaf(CO,f,BDY(*paargl));
! 902: if (w == 1) {
! 903: MKNODE(n,f,*paargl);
! 904: *paargl = n;
! 905: return;
! 906: }
! 907: if (w == 0)
! 908: return;
! 909: /* f belongs strictly inside the existing list */
! 910: for (sc=*paargl; (w=compaf(CO,BDY(sc),f))==1; sc=NEXT(sc))
! 911: prev = sc;
! 912: if (w == 0)
! 913: return;
! 914: MKNODE(n,f,sc);
! 915: NEXT(prev) = n;
! 916: }
! 917:
! 918: void simpl_gand_insert_c(f,pcargl,pcc)
! 919: F f;
! 920: NODE *pcargl,*pcc;
! 921: {
! 922: NODE sc;
! 923:
! 924: for (sc=*pcargl; sc; sc=NEXT(sc))
! 925: if (synequalf(f,(F)BDY(sc)))
! 926: return;
! 927: NEXTNODE(*pcargl,*pcc);
! 928: BDY(*pcc) = (pointer)f;
! 929: }
! 930:
! 931: int compaf(vl,f1,f2)
! 932: VL vl;
! 933: F f1,f2;
! 934: {
! 935: int w;
! 936:
! 937: w = compp(vl,FPL(f1),FPL(f2));
! 938: if (w)
! 939: return w;
! 940: return comprel(FOP(f1),FOP(f2));
! 941: }
! 942:
! 943: int comprel(op1,op2)
! 944: oFOP op1,op2;
! 945: /* implement order: =, <>, <=, <, >=, > */
! 946: {
! 947: if (op1 == op2)
! 948: return 0;
! 949: switch (op1) {
! 950: case AL_EQUAL:
! 951: return 1;
! 952: case AL_NEQ:
! 953: switch (op2) {
! 954: case AL_EQUAL:
! 955: return -1;
! 956: default:
! 957: return 1;
! 958: }
! 959: case AL_LEQ:
! 960: switch (op2) {
! 961: case AL_EQUAL:
! 962: return -1;
! 963: case AL_NEQ:
! 964: return -1;
! 965: default:
! 966: return 1;
! 967: }
! 968: case AL_LESSP:
! 969: switch (op2) {
! 970: case AL_GEQ:
! 971: return 1;
! 972: case AL_GREATERP:
! 973: return 1;
! 974: default:
! 975: return -1;
! 976: }
! 977: case AL_GEQ:
! 978: switch (op2) {
! 979: case AL_GREATERP:
! 980: return 1;
! 981: default:
! 982: return -1;
! 983: }
! 984: case AL_GREATERP:
! 985: return -1;
! 986: }
! 987: error("unknown relation in comprel");
! 988: }
! 989:
! 990: int synequalf(f1,f2)
! 991: F f1,f2;
! 992: {
! 993: oFOP op=FOP(f1);
! 994:
! 995: if (op != FOP(f2))
! 996: return 0;
! 997: if (AL_ATOMIC(op))
! 998: return (compp(CO,FPL(f1),FPL(f2)) == 0);
! 999: if (AL_JUNCT(op)) {
! 1000: NODE sc1,sc2;
! 1001: for (sc1=FJARG(f1),sc2=FJARG(f2); sc1 && sc2; sc1=NEXT(sc1),sc2=NEXT(sc2))
! 1002: if (! synequalf(BDY(sc1),BDY(sc2)))
! 1003: return 0;
! 1004: if (sc1 || sc2)
! 1005: return 0;
! 1006: return 1;
! 1007: }
! 1008: }
! 1009:
! 1010: void simpl_impl(op,prem,concl,th,n,pf)
! 1011: oFOP op;
! 1012: F prem,concl,*pf;
! 1013: NODE th;
! 1014: int n;
! 1015: {
! 1016: F h,hh;
! 1017:
! 1018: simpl1(prem,th,n+1,&h);
! 1019: if (FOP(h) == AL_FALSE) {
! 1020: *pf = F_TRUE;
! 1021: return;
! 1022: }
! 1023: simpl1(concl,th,n+1,&hh);
! 1024: if (FOP(hh) == AL_TRUE) {
! 1025: *pf = F_TRUE;
! 1026: return;
! 1027: }
! 1028: if (FOP(h) == AL_TRUE) {
! 1029: *pf = hh;
! 1030: return;
! 1031: }
! 1032: if (FOP(hh) == AL_FALSE) {
! 1033: pnegate(h,pf);
! 1034: return;
! 1035: }
! 1036: if (op == AL_IMPL) {
! 1037: MKBF(*pf,AL_IMPL,h,hh);
! 1038: return;
! 1039: }
! 1040: MKBF(*pf,AL_REPL,hh,h);
! 1041: }
! 1042:
! 1043: void simpl_equiv(lhs,rhs,th,n,pf)
! 1044: F lhs,rhs,*pf;
! 1045: NODE th;
! 1046: int n;
! 1047: {
! 1048: F h,hh;
! 1049:
! 1050: simpl1(lhs,th,n+1,&h);
! 1051: simpl1(rhs,th,n+1,&hh);
! 1052: if (FOP(h) == AL_TRUE) {
! 1053: *pf = hh;
! 1054: return;
! 1055: }
! 1056: if (FOP(hh) == AL_TRUE) {
! 1057: *pf = h;
! 1058: return;
! 1059: }
! 1060: if (FOP(h) == AL_FALSE) {
! 1061: pnegate(hh,pf);
! 1062: return;
! 1063: }
! 1064: if (FOP(hh) == AL_FALSE) {
! 1065: pnegate(h,pf);
! 1066: return;
! 1067: }
! 1068: MKBF(*pf,AL_EQUIV,h,hh);
! 1069: }
! 1070:
! 1071: void simpl_a(f,pnf)
! 1072: F f,*pnf;
! 1073: {
! 1074: oFOP r=FOP(f);
! 1075: P lhs=(P)FPL(f);
! 1076:
! 1077: if (NUMBER(lhs)) {
! 1078: #if 0
! 1079: lhs = (Q)lhs; /* good luck with the next compiler */
! 1080: #endif
! 1081: switch (r) {
! 1082: case AL_EQUAL:
! 1083: *pnf = (lhs == 0) ? F_TRUE : F_FALSE;
! 1084: return;
! 1085: case AL_NEQ:
! 1086: *pnf = (lhs != 0) ? F_TRUE : F_FALSE;
! 1087: return;
! 1088: case AL_LESSP:
! 1089: *pnf = (cmpq((Q)lhs,0) == -1) ? F_TRUE : F_FALSE;
! 1090: return;
! 1091: case AL_GREATERP:
! 1092: *pnf = (cmpq((Q)lhs,0) == 1) ? F_TRUE : F_FALSE;
! 1093: return;
! 1094: case AL_LEQ:
! 1095: *pnf = (cmpq((Q)lhs,0) != 1) ? F_TRUE : F_FALSE;
! 1096: return;
! 1097: case AL_GEQ:
! 1098: *pnf = (cmpq((Q)lhs,0) != -1) ? F_TRUE : F_FALSE;
! 1099: return;
! 1100: default:
! 1101: error("unknown operator in simpl_a");
! 1102: }
! 1103: }
! 1104: if (AL_ORDER(r))
! 1105: simpl_a_o(&r,&lhs);
! 1106: else
! 1107: simpl_a_no(&lhs);
! 1108: MKAF(*pnf,r,lhs);
! 1109: }
! 1110:
! 1111: void simpl_a_o(ar,alhs)
! 1112: oFOP *ar;
! 1113: P *alhs;
! 1114: {
! 1115: DCP dec;
! 1116:
! 1117: sqfrp(CO,*alhs,&dec);
! 1118: if (sgnq((Q)COEF(dec)) == -1)
! 1119: *ar = AL_ANEGREL(*ar);
! 1120: *alhs=(P)ONE;
! 1121: for (dec = NEXT(dec); dec; dec = NEXT(dec)) {
! 1122: mulp(CO,*alhs,COEF(dec),alhs);
! 1123: if (evenz(DEG(dec)))
! 1124: mulp(CO,*alhs,COEF(dec),alhs);
! 1125: }
! 1126: }
! 1127:
! 1128: void simpl_a_no(alhs)
! 1129: P *alhs;
! 1130: {
! 1131: DCP dec;
! 1132:
! 1133: sqfrp(CO,*alhs,&dec);
! 1134: *alhs=(P)ONE;
! 1135: for (dec = NEXT(dec); dec; dec = NEXT(dec))
! 1136: mulp(CO,*alhs,COEF(dec),alhs);
! 1137: }
! 1138:
! 1139: /* QE */
! 1140:
! 1141: #define BTMIN 0
! 1142: #define BTEQUAL 0
! 1143: #define BTWO 1
! 1144: #define BTLEQ 2
! 1145: #define BTGEQ 3
! 1146: #define BTSO 4
! 1147: #define BTLESSP 5
! 1148: #define BTGREATERP 6
! 1149: #define BTNEQ 7
! 1150: #define BTMAX 7
! 1151:
! 1152: #define IPURE 0
! 1153: #define IPE 1
! 1154: #define IME 2
! 1155: #define II 3
! 1156:
! 1157: void qe(f,pnf)
! 1158: F f,*pnf;
! 1159: {
! 1160: NODE bl,sc;
! 1161: F h;
! 1162:
! 1163: simpl(f,(NODE)NULL,&h);
! 1164: nnf(h,&h);
! 1165: blocksplit(h,&bl,&h);
! 1166: for (sc=bl; sc; sc=NEXT(sc)) {
! 1167: if (QUANT(((QVL)BDY(sc))) == AL_EX)
! 1168: qeblock(VARL(((QVL)BDY(sc))),h,&h);
! 1169: else {
! 1170: pnegate(h,&h);
! 1171: qeblock(VARL(((QVL)BDY(sc))),h,&h);
! 1172: pnegate(h,&h);
! 1173: }
! 1174: }
! 1175: *pnf = h;
! 1176: }
! 1177:
! 1178: void blocksplit(f,pbl,pmat)
! 1179: F f,*pmat;
! 1180: NODE *pbl;
! 1181: {
! 1182: oFOP cq;
! 1183: NODE bl=NULL,blh;
! 1184: VL vl,vlh;
! 1185: QVL qvl;
! 1186:
! 1187: while (AL_QUANT(cq=FOP(f))) {
! 1188: NEWNODE(blh);
! 1189: vl = NULL;
! 1190: while (FOP(f) == cq) {
! 1191: NEWVL(vlh);
! 1192: VR(vlh) = FQVR(f);
! 1193: NEXT(vlh) = vl;
! 1194: vl = vlh;
! 1195: f = FQMAT(f);
! 1196: }
! 1197: MKQVL(qvl,cq,vl);
! 1198: BDY(blh) = (pointer)qvl;
! 1199: NEXT(blh) = bl;
! 1200: bl = blh;
! 1201: }
! 1202: *pbl = bl;
! 1203: *pmat = f;
! 1204: }
! 1205:
! 1206: void qeblock(vl,f,pnf)
! 1207: VL vl;
! 1208: F f,*pnf;
! 1209: {
! 1210: CONT co;
! 1211: CEL cel;
! 1212: VL cvl;
! 1213: NODE n,sc;
! 1214: NODE nargl=NULL,narglc;
! 1215: int w,pr;
! 1216: int left=0,modulus;
! 1217:
! 1218: qeblock_verbose0(vl);
! 1219: simpl(f,(NODE)NULL,&f);
! 1220: MKCONT(co);
! 1221: MKCEL(cel,vl,f);
! 1222: coadd(co,cel);
! 1223: while (coget(co,&cel)) {
! 1224: cvl = VRL(cel);
! 1225: pr = qeblock_verbose1a(co,cvl,&left,&modulus);
! 1226: w = qevar(MAT(cel),&cvl,&n);
! 1227: qeblock_verbose1b(w,pr);
! 1228: for (sc=n; sc; sc=NEXT(sc))
! 1229: if ((F)BDY(sc) != F_FALSE)
! 1230: if (cvl) {
! 1231: MKCEL(cel,cvl,(F)BDY(sc));
! 1232: if (!comember(co,cel))
! 1233: coadd(co,cel);
! 1234: } else {
! 1235: NEXTNODE(nargl,narglc);
! 1236: BDY(narglc) = BDY(sc);
! 1237: }
! 1238: }
! 1239: qeblock_verbose2();
! 1240: smkjf(pnf,AL_OR,nargl);
! 1241: simpl(*pnf,(NODE)NULL,pnf);
! 1242: }
! 1243:
! 1244: void qeblock_verbose0(vl)
! 1245: VL vl;
! 1246: {
! 1247: if (!Verbose)
! 1248: return;
! 1249: printf("eliminating");
! 1250: for (; vl; vl=NEXT(vl))
! 1251: printf(" %s",NAME(VR(vl)));
! 1252: }
! 1253:
! 1254: int qeblock_verbose1a(co,cvl,pleft,pmodulus)
! 1255: CONT co;
! 1256: VL cvl;
! 1257: int *pleft,*pmodulus;
! 1258: {
! 1259: int i=0;
! 1260:
! 1261: if (!Verbose)
! 1262: /* added by noro */
! 1263: return 0;
! 1264: if (*pleft == 0) {
! 1265: for (; cvl; cvl=NEXT(cvl))
! 1266: i++;
! 1267: printf("\nleft %d\n",i);
! 1268: *pleft = colen(co) + 1;
! 1269: *pmodulus = getmodulus(*pleft);
! 1270: printf("(%d",(*pleft)--);
! 1271: fflush(asir_out);
! 1272: return 1;
! 1273: } else if (*pleft % *pmodulus == 0) {
! 1274: printf("(%d",(*pleft)--);
! 1275: fflush(asir_out);
! 1276: return 1;
! 1277: }
! 1278: (*pleft)--;
! 1279: return 0;
! 1280: }
! 1281:
! 1282: void qeblock_verbose1b(g,print)
! 1283: int g,print;
! 1284: {
! 1285: if (!(Verbose && print))
! 1286: return;
! 1287: printf("%s) ",g ? (g==2) ? "qg" : "lg" : "e");
! 1288: fflush(asir_out);
! 1289: }
! 1290:
! 1291: void qeblock_verbose2()
! 1292: {
! 1293: if (!Verbose)
! 1294: return;
! 1295: printf("\n");
! 1296: }
! 1297:
! 1298: int getmodulus(n)
! 1299: int n;
! 1300: {
! 1301: int pow=1;
! 1302:
! 1303: while (n >= pow*100) {
! 1304: pow *= 10;
! 1305: }
! 1306: return pow;
! 1307: }
! 1308:
! 1309:
! 1310: int qevar(f,pcvl,pfl)
! 1311: F f;
! 1312: VL *pcvl;
! 1313: NODE *pfl;
! 1314: {
! 1315: int w;
! 1316: V x;
! 1317: F h;
! 1318: NODE trans[8],eset,sc,r=NULL,rc;
! 1319:
! 1320: w = gausselim(f,pcvl,&x,&eset);
! 1321: if (!w) {
! 1322: x = VR(*pcvl);
! 1323: *pcvl = NEXT(*pcvl);
! 1324: translate(f,x,trans);
! 1325: mkeset(trans,x,&eset);
! 1326: }
! 1327: for (sc=eset; sc; sc=NEXT(sc)) {
! 1328: NEXTNODE(r,rc);
! 1329: subgpf(f,x,BDY(sc),&h);
! 1330: simpl(h,(NODE)NULL,&BDY(rc));
! 1331: }
! 1332: *pfl = r;
! 1333: return w;
! 1334: }
! 1335:
! 1336: int gausselim(f,pvl,px,peset)
! 1337: F f;
! 1338: VL *pvl;
! 1339: V *px;
! 1340: NODE *peset;
! 1341: {
! 1342: Z deg,two;
! 1343: P rlhs,a,b,c;
! 1344: V v;
! 1345: VL scvl;
! 1346: NODE sc;
! 1347: int w;
! 1348:
! 1349: if (FOP(f) != AL_AND)
! 1350: return 0;
! 1351: STOQ(2,two);
! 1352: for (deg=ONE; cmpz(two,deg) >= 0; addz(deg,ONE,°))
! 1353: for (scvl=*pvl; scvl; scvl=NEXT(scvl)) {
! 1354: v = VR(scvl);
! 1355: for (sc=FJARG(f); sc; sc=NEXT(sc)) {
! 1356: if (FOP((F)BDY(sc)) != AL_EQUAL)
! 1357: continue;
! 1358: al_reorder(FPL((F)BDY(sc)),v,&rlhs);
! 1359: if (VR(rlhs) != v)
! 1360: continue;
! 1361: w = gauss_abc(rlhs,v,deg,&a,&b,&c);
! 1362: if (!w)
! 1363: continue;
! 1364: *px = v;
! 1365: delv(v,*pvl,pvl);
! 1366: if (a) {
! 1367: gauss_mkeset2(rlhs,a,b,c,peset);
! 1368: return 2;
! 1369: }
! 1370: gauss_mkeset1(rlhs,b,peset);
! 1371: return 1;
! 1372: }
! 1373: }
! 1374: return 0;
! 1375: }
! 1376:
! 1377: int gauss_abc(rlhs,v,deg,pa,pb,pc)
! 1378: P rlhs,*pa,*pb,*pc;
! 1379: V v;
! 1380: Z deg;
! 1381: {
! 1382: Z two;
! 1383: DCP rld;
! 1384:
! 1385: rld = DC(rlhs);
! 1386: if (cmpz(DEG(rld),deg) != 0)
! 1387: return 0;
! 1388: STOQ(2,two);
! 1389: if (cmpz(deg,two) == 0) {
! 1390: *pa = COEF(rld);
! 1391: rld = NEXT(rld);
! 1392: } else
! 1393: *pa = 0;
! 1394: if (rld && cmpz(DEG(rld),ONE) == 0) {
! 1395: *pb = COEF(rld);
! 1396: rld = NEXT(rld);
! 1397: } else
! 1398: *pb = 0;
! 1399: if (rld)
! 1400: *pc = COEF(rld);
! 1401: else
! 1402: *pc = 0;
! 1403: return (NZNUMBER(*pa) || NZNUMBER(*pb) || NZNUMBER(*pc));
! 1404: }
! 1405:
! 1406: void gauss_mkeset1(rlhs,b,peset)
! 1407: P rlhs,b;
! 1408: NODE *peset;
! 1409: {
! 1410: GP hgp;
! 1411:
! 1412: mklgp(rlhs,b,STD,&hgp);
! 1413: MKNODE(*peset,hgp,NULL);
! 1414: }
! 1415:
! 1416: void gauss_mkeset2(rlhs,a,b,c,peset)
! 1417: P rlhs,a,b,c;
! 1418: NODE *peset;
! 1419: {
! 1420: GP hgp;
! 1421: NODE esetc=NULL;
! 1422:
! 1423: *peset = NULL;
! 1424: if (!NUM(a)) {
! 1425: NEXTNODE(*peset,esetc);
! 1426: mklgp(rlhs,b,STD,&hgp);
! 1427: BDY(esetc) = (pointer)hgp;
! 1428: }
! 1429: NEXTNODE(*peset,esetc);
! 1430: mkqgp(rlhs,a,b,c,1,STD,&hgp);
! 1431: BDY(esetc) = (pointer)hgp;
! 1432: NEXTNODE(*peset,esetc);
! 1433: mkqgp(rlhs,a,b,c,2,STD,&hgp);
! 1434: BDY(esetc) = (pointer)hgp;
! 1435: }
! 1436:
! 1437: int delv(v,vl,pnvl)
! 1438: V v;
! 1439: VL vl,*pnvl;
! 1440: {
! 1441: VL nvl=NULL,nvlc;
! 1442:
! 1443: if (v == VR(vl)) {
! 1444: *pnvl = NEXT(vl);
! 1445: return 1;
! 1446: }
! 1447: for (; vl && (VR(vl) != v); vl=NEXT(vl)) {
! 1448: NEXTVL(nvl,nvlc);
! 1449: VR(nvlc) = VR(vl);
! 1450: }
! 1451: if (vl) {
! 1452: NEXT(nvlc) = NEXT(vl);
! 1453: *pnvl = nvl;
! 1454: return 1;
! 1455: }
! 1456: *pnvl = nvl;
! 1457: return 0;
! 1458: }
! 1459:
! 1460: int translate(f,x,trans)
! 1461: F f;
! 1462: V x;
! 1463: NODE trans[];
! 1464: {
! 1465: NODE sc,transc[8];
! 1466: int bt,w=0;
! 1467:
! 1468: for (bt=BTMIN; bt<=BTMAX; bt++)
! 1469: trans[bt] = NULL;
! 1470: for (atl(f,&sc); sc; sc=NEXT(sc))
! 1471: w = (translate_a(BDY(sc),x,trans,transc) || w);
! 1472: return w;
! 1473: }
! 1474:
! 1475: int translate_a(at,v,trans,transc)
! 1476: F at;
! 1477: V v;
! 1478: NODE trans[],transc[];
! 1479: {
! 1480: P mp;
! 1481: Z two;
! 1482: int w;
! 1483:
! 1484: w = al_reorder(FPL(at),v,&mp);
! 1485: if (w == 0)
! 1486: return 0;
! 1487: if (cmpz(ONE,DEG(DC(mp))) == 0) {
! 1488: translate_a1(FOP(at),mp,trans,transc);
! 1489: return 1;
! 1490: };
! 1491: STOQ(2,two);
! 1492: if (cmpz(two,DEG(DC(mp))) == 0) {
! 1493: translate_a2(FOP(at),mp,trans,transc);
! 1494: return 1;
! 1495: };
! 1496: error("degree violation in translate_a");
! 1497: /* XXX : NOTREACHED */
! 1498: return -1;
! 1499: }
! 1500:
! 1501: void translate_a1(op,mp,trans,transc)
! 1502: oFOP op;
! 1503: P mp;
! 1504: NODE trans[],transc[];
! 1505: {
! 1506: P b;
! 1507: int itype,btype;
! 1508: GP hgp;
! 1509:
! 1510: b = COEF(DC(mp));
! 1511: indices(op,NUM(b) ? sgnq((Q)b) : 0,&itype,&btype);
! 1512: NEXTNODE(trans[btype],transc[btype]);
! 1513: mklgp(mp,b,itype,&hgp);
! 1514: BDY(transc[btype]) = (pointer)hgp;
! 1515: }
! 1516:
! 1517: void mklgp(mp,b,itype,pgp)
! 1518: P mp,b;
! 1519: int itype;
! 1520: GP *pgp;
! 1521: {
! 1522: RE hre;
! 1523: F hf;
! 1524:
! 1525: MKRE(hre,mp,(P)ONE,1,itype);
! 1526: MKAF(hf,AL_NEQ,b);
! 1527: MKGP(*pgp,hf,hre);
! 1528: }
! 1529:
! 1530: void translate_a2(op,mp,trans,transc)
! 1531: oFOP op;
! 1532: P mp;
! 1533: NODE trans[],transc[];
! 1534: {
! 1535: P a,b,c,linred;
! 1536: int itype,btype;
! 1537: GP hgp;
! 1538:
! 1539: getqcoeffs(mp,&a,&b,&c);
! 1540: if (!NUM(a) && b) {
! 1541: MKP(VR(mp),NEXT(DC(mp)),linred);
! 1542: translate_a1(op,linred,trans,transc);
! 1543: }
! 1544: indices(op,0,&itype,&btype);
! 1545: NEXTNODE(trans[btype],transc[btype]);
! 1546: mkqgp(mp,a,b,c,-1,itype,&hgp);
! 1547: BDY(transc[btype]) = (pointer)hgp;
! 1548: }
! 1549:
! 1550: void mkqgp(mp,a,b,c,rootno,itype,pgp)
! 1551: P mp,a,b,c;
! 1552: int rootno;
! 1553: int itype;
! 1554: GP *pgp;
! 1555: {
! 1556: P discr;
! 1557: RE hre;
! 1558: F hf;
! 1559: NODE n=NULL,nc=NULL;
! 1560:
! 1561: mkdiscr(a,b,c,&discr);
! 1562: MKRE(hre,mp,discr,rootno,itype);
! 1563: NEXTNODE(n,nc);
! 1564: MKAF(hf,AL_NEQ,a);
! 1565: BDY(nc) = (pointer)hf;
! 1566: NEXTNODE(n,nc);
! 1567: MKAF(hf,AL_GEQ,discr);
! 1568: BDY(nc) = (pointer)hf;
! 1569: MKJF(hf,AL_AND,n);
! 1570: MKGP(*pgp,hf,hre);
! 1571: }
! 1572:
! 1573: void getqcoeffs(mp,pa,pb,pc)
! 1574: P mp,*pa,*pb,*pc;
! 1575: {
! 1576: DCP hdcp;
! 1577:
! 1578: *pa = COEF(DC(mp));
! 1579: hdcp = NEXT(DC(mp));
! 1580: if (hdcp && cmpz(DEG(hdcp),ONE) == 0) {
! 1581: *pb = COEF(hdcp);
! 1582: hdcp = NEXT(hdcp);
! 1583: } else
! 1584: *pb = 0;
! 1585: if (hdcp && DEG(hdcp) == 0) {
! 1586: *pc = COEF(hdcp);
! 1587: } else
! 1588: *pc = 0;
! 1589: }
! 1590:
! 1591: void mkdiscr(a,b,c,pd)
! 1592: P a,b,c,*pd;
! 1593: {
! 1594: P h1,h2;
! 1595: Z four;
! 1596:
! 1597: mulp(CO,a,c,&h1);
! 1598: STOQ(4,four);
! 1599: mulp(CO,(P)four,h1,&h2);
! 1600: mulp(CO,b,b,&h1);
! 1601: subp(CO,h1,h2,pd);
! 1602: }
! 1603:
! 1604: int al_reorder(p,v,pnp)
! 1605: P p,*pnp;
! 1606: V v;
! 1607: {
! 1608: VL tvl;
! 1609:
! 1610: reordvar(CO,v,&tvl);
! 1611: reorderp(tvl,CO,p,pnp);
! 1612: if (*pnp && !NUM(*pnp) && strcmp(NAME(VR(*pnp)),NAME(v)) == 0)
! 1613: return 1;
! 1614: else
! 1615: return 0;
! 1616: }
! 1617:
! 1618: void indices(op,s,pit,pbt)
! 1619: oFOP op;
! 1620: int s,*pit,*pbt;
! 1621: {
! 1622: switch (op) {
! 1623: case AL_EQUAL:
! 1624: *pit = STD; *pbt = BTEQUAL; return;
! 1625: case AL_NEQ:
! 1626: *pit = EPS; *pbt = BTNEQ; return;
! 1627: case AL_LEQ:
! 1628: *pit = STD;
! 1629: switch (s) {
! 1630: case 1:
! 1631: *pbt = BTLEQ; return;
! 1632: case -1:
! 1633: *pbt = BTGEQ; return;
! 1634: case 0:
! 1635: *pbt = BTWO; return;
! 1636: }
! 1637: case AL_GEQ:
! 1638: *pit = STD;
! 1639: switch (s) {
! 1640: case 1:
! 1641: *pbt = BTGEQ; return;
! 1642: case -1:
! 1643: *pbt = BTLEQ; return;
! 1644: case 0:
! 1645: *pbt = BTWO; return;
! 1646: }
! 1647: case AL_LESSP:
! 1648: switch (s) {
! 1649: case 1:
! 1650: *pit = MEPS; *pbt = BTLESSP; return;
! 1651: case -1:
! 1652: *pit = PEPS; *pbt = BTGREATERP; return;
! 1653: case 0:
! 1654: *pit = EPS; *pbt = BTSO; return;
! 1655: }
! 1656: case AL_GREATERP:
! 1657: switch (s) {
! 1658: case 1:
! 1659: *pit = PEPS; *pbt = BTGREATERP; return;
! 1660: case -1:
! 1661: *pit = MEPS; *pbt = BTLESSP; return;
! 1662: case 0:
! 1663: *pit = EPS; *pbt = BTSO; return;
! 1664: }
! 1665: default:
! 1666: error("unknown relation or sign in indices");
! 1667: }
! 1668: }
! 1669:
! 1670: void mkeset(trans,x,peset)
! 1671: NODE trans[],*peset;
! 1672: V x;
! 1673: {
! 1674: NODE esetc=NULL;
! 1675: P h;
! 1676: RE hre;
! 1677: GP hgp;
! 1678: int cw,cs,deps,dinf,ord;
! 1679:
! 1680: *peset = NULL;
! 1681: ord = selectside(trans,&cw,&cs,&deps,&dinf);
! 1682: if (ord) {
! 1683: add2eset(trans[cw],peset,&esetc);
! 1684: add2eset(trans[BTWO],peset,&esetc);
! 1685: add2eset(trans[cs],peset,&esetc);
! 1686: sp_add2eset(trans[BTSO],deps,peset,&esetc);
! 1687: NEXTNODE(*peset,esetc);
! 1688: MKRE(hre,0,0,0,dinf);
! 1689: MKGP(hgp,F_TRUE,hre);
! 1690: BDY(esetc) = (pointer)hgp;
! 1691: } else {
! 1692: NEXTNODE(*peset,esetc);
! 1693: MKV(x,h);
! 1694: MKRE(hre,h,(P)ONE,1,STD);
! 1695: MKGP(hgp,F_TRUE,hre);
! 1696: BDY(esetc) = (pointer)hgp;
! 1697: }
! 1698: add2eset(trans[BTEQUAL],peset,&esetc);
! 1699: sp_add2eset(trans[BTNEQ],deps,peset,&esetc);
! 1700: }
! 1701:
! 1702: int selectside(trans,pcw,pcs,pdeps,pdinf)
! 1703: NODE trans[];
! 1704: int *pcw,*pcs,*pdeps,*pdinf;
! 1705: {
! 1706: if (cmp2n(trans[BTLEQ],trans[BTLESSP],trans[BTGEQ],trans[BTGREATERP])==1) {
! 1707: *pcw = BTGEQ;
! 1708: *pcs = BTGREATERP;
! 1709: *pdeps = PEPS;
! 1710: *pdinf = MINF;
! 1711: } else {
! 1712: *pcw = BTLEQ;
! 1713: *pcs = BTLESSP;
! 1714: *pdeps = MEPS;
! 1715: *pdinf = PINF;
! 1716: }
! 1717: if (!(trans[BTLEQ] || trans[BTLESSP] || trans[BTGEQ] ||
! 1718: trans[BTGREATERP] || trans[BTWO] || trans[BTSO]))
! 1719: return 0;
! 1720: return 1;
! 1721: }
! 1722:
! 1723: int cmp2n(n1a,n1b,n2a,n2b)
! 1724: NODE n1a,n1b,n2a,n2b;
! 1725: {
! 1726: NODE n1,n2;
! 1727: int n1bleft=1,n2bleft=1;
! 1728:
! 1729: n1 = n1a;
! 1730: n2 = n2a;
! 1731: while (n1 && n2) {
! 1732: n1 = NEXT(n1);
! 1733: if (n1 == NULL && n1bleft) {
! 1734: n1 = n1b;
! 1735: n1bleft = 0;
! 1736: }
! 1737: n2 = NEXT(n2);
! 1738: if (n2 == NULL && n2bleft) {
! 1739: n2 = n2b;
! 1740: n2bleft = 0;
! 1741: }
! 1742: }
! 1743: if (n1 || n2)
! 1744: return n1 ? 1 : -1;
! 1745: return 0;
! 1746: }
! 1747:
! 1748: void add2eset(trfield,peset,pesetc)
! 1749: NODE trfield,*peset,*pesetc;
! 1750: {
! 1751: NODE ntrfield,ntrfieldc;
! 1752:
! 1753: if (trfield == NULL)
! 1754: return;
! 1755: seproots(trfield,&ntrfield,&ntrfieldc);
! 1756: if (*peset == NULL) {
! 1757: *peset = ntrfield;
! 1758: *pesetc = ntrfieldc;
! 1759: } else {
! 1760: NEXT(*pesetc) = ntrfield;
! 1761: *pesetc = ntrfieldc;
! 1762: }
! 1763: }
! 1764:
! 1765: void seproots(trfield,pntrfield,pntrfieldc)
! 1766: NODE trfield,*pntrfield,*pntrfieldc;
! 1767: {
! 1768: NODE sc;
! 1769: NODE ntrf=NULL,ntrfc;
! 1770: RE hre,hre2;
! 1771: GP hgp,hgp2;
! 1772:
! 1773: for (sc=trfield; sc; sc=NEXT(sc)) {
! 1774: hgp = (GP)BDY(sc);
! 1775: hre = POINT(hgp);
! 1776: if (ROOTNO(hre) == -1) {
! 1777: NEXTNODE(ntrf,ntrfc);
! 1778: MKRE(hre2,hre->p,DISC(hre),1,ITYPE(hre));
! 1779: MKGP(hgp2,GUARD(hgp),hre2);
! 1780: BDY(ntrfc) = (pointer)hgp2;
! 1781: NEXTNODE(ntrf,ntrfc);
! 1782: ROOTNO(hre) = 2;
! 1783: BDY(ntrfc) = (pointer)hgp;
! 1784: } else {
! 1785: NEXTNODE(ntrf,ntrfc);
! 1786: BDY(ntrfc) = (pointer)hgp;
! 1787: }
! 1788: }
! 1789: *pntrfield = ntrf;
! 1790: *pntrfieldc = ntrfc;
! 1791: }
! 1792:
! 1793: void sp_add2eset(trfield,itype,peset,pesetc)
! 1794: NODE trfield,*peset,*pesetc;
! 1795: int itype;
! 1796: {
! 1797: NODE sc;
! 1798: GP hgp;
! 1799:
! 1800: for (sc=trfield; sc; sc=NEXT(sc)) {
! 1801: hgp = (GP)BDY(sc);
! 1802: ITYPE(POINT(hgp)) = itype;
! 1803: }
! 1804: add2eset(trfield,peset,pesetc);
! 1805: }
! 1806:
! 1807: void subgpf(f,v,gp,pnf)
! 1808: F f,*pnf;
! 1809: V v;
! 1810: GP gp;
! 1811: {
! 1812: NODE argl=NULL,arglc=NULL;
! 1813:
! 1814: NEXTNODE(argl,arglc);
! 1815: BDY(arglc) = (pointer)GUARD(gp);
! 1816: NEXTNODE(argl,arglc);
! 1817: subref(f,v,POINT(gp),&BDY(arglc));
! 1818: MKJF(*pnf,AL_AND,argl);
! 1819: }
! 1820:
! 1821: void subref(f,v,r,pnf)
! 1822: F f,*pnf;
! 1823: V v;
! 1824: RE r;
! 1825: {
! 1826: pointer argv[2];
! 1827:
! 1828: argv[0] = (pointer)v;
! 1829: argv[1] = (pointer)r;
! 1830: apply2ats(f,subref_a,argv,pnf);
! 1831: }
! 1832:
! 1833: void subref_a(at,argv,pnat)
! 1834: F at,*pnat;
! 1835: pointer argv[];
! 1836: {
! 1837: switch (ITYPE((RE)argv[1])) {
! 1838: case STD:
! 1839: substd_a(at,argv[0],argv[1],pnat);
! 1840: return;
! 1841: case EPS:
! 1842: error("unspecified RE in subref_a()");
! 1843: case PEPS:
! 1844: case MEPS:
! 1845: subpme_a(at,argv[0],argv[1],pnat);
! 1846: return;
! 1847: case PINF:
! 1848: case MINF:
! 1849: subinf_a(at,argv[0],argv[1],pnat);
! 1850: return;
! 1851: default:
! 1852: error("unknown itype in subref_a()");
! 1853: }
! 1854: }
! 1855:
! 1856: void substd_a(at,v,re,pnf)
! 1857: F at,*pnf;
! 1858: V v;
! 1859: RE re;
! 1860: {
! 1861: VL no;
! 1862: P rlhs,prem,nlhs;
! 1863: Z dd,dndeg;
! 1864:
! 1865: reordvar(CO,v,&no);
! 1866: reorderp(no,CO,FPL(at),&rlhs);
! 1867: if (!rlhs || NUM(rlhs) || VR(rlhs) != v) {
! 1868: *pnf = at;
! 1869: return;
! 1870: }
! 1871: premp(no,rlhs,re->p,&prem);
! 1872: if (prem && !NUM(prem) && VR(prem) == v) {
! 1873: /* quadratic case */
! 1874: substd_a2(FOP(at),prem,DEG(DC(rlhs)),re,pnf);
! 1875: return;
! 1876: }
! 1877: subz(DEG(DC(rlhs)),DEG(DC(re->p)),&dd);
! 1878: addz(dd,ONE,&dndeg);
! 1879: if (AL_ORDER(FOP(at)) && (!evenz(dndeg)))
! 1880: mulp(CO,prem,COEF(DC(re->p)),&nlhs);
! 1881: else
! 1882: nlhs = prem;
! 1883: MKAF(*pnf,FOP(at),nlhs);
! 1884: }
! 1885:
! 1886: void substd_a2(op,prem,fdeg,re,pf)
! 1887: oFOP op;
! 1888: F prem;
! 1889: Q fdeg;
! 1890: RE re;
! 1891: F *pf;
! 1892: {
! 1893: P a,b,c,ld;
! 1894:
! 1895: getrecoeffs(prem,fdeg,re,&a,&b,&c,&ld);
! 1896: if (ROOTNO(re) == 1)
! 1897: chsgnp(b,&b);
! 1898: else if (ROOTNO(re) != 2)
! 1899: error("unspecified quadratic root in substd_a2");
! 1900: substd_a21(op,a,b,c,ld,pf);
! 1901: }
! 1902:
! 1903: void substd_a21(op,a,b,c,d,pf)
! 1904: oFOP op;
! 1905: P a,b,c,d;
! 1906: F *pf;
! 1907: {
! 1908: switch (op) {
! 1909: case AL_EQUAL:
! 1910: substd_a21_equal(a,b,c,d,pf);
! 1911: return;
! 1912: case AL_NEQ:
! 1913: substd_a21_equal(a,b,c,d,pf);
! 1914: pnegate(*pf,pf);
! 1915: return;
! 1916: case AL_LEQ:
! 1917: substd_a21_leq(a,b,c,d,pf);
! 1918: return;
! 1919: case AL_LESSP:
! 1920: substd_a21_lessp(a,b,c,d,pf);
! 1921: return;
! 1922: case AL_GEQ:
! 1923: substd_a21_lessp(a,b,c,d,pf);
! 1924: pnegate(*pf,pf);
! 1925: return;
! 1926: case AL_GREATERP:
! 1927: substd_a21_leq(a,b,c,d,pf);
! 1928: pnegate(*pf,pf);
! 1929: return;
! 1930: default:
! 1931: error("unknown operator in substd_a21");
! 1932: }
! 1933: }
! 1934:
! 1935: void substd_a21_equal(a,b,c,d,pf)
! 1936: P a,b,c,d;
! 1937: F *pf;
! 1938: {
! 1939: F hf;
! 1940: NODE cj=NULL,cjc=NULL;
! 1941: P hp1,hp2;
! 1942:
! 1943: NEXTNODE(cj,cjc);
! 1944: mulp(CO,a,a,&hp1);
! 1945: mulp(CO,b,b,&hp2);
! 1946: mulp(CO,hp2,c,&hp2);
! 1947: subp(CO,hp1,hp2,&hp1);
! 1948: MKAF(hf,AL_EQUAL,hp1);
! 1949: BDY(cjc) = (pointer)hf;
! 1950: NEXTNODE(cj,cjc);
! 1951: mulp(CO,a,b,&hp1);
! 1952: MKAF(hf,AL_LEQ,hp1);
! 1953: BDY(cjc) = (pointer)hf;
! 1954: MKJF(*pf,AL_AND,cj);
! 1955: }
! 1956:
! 1957: void substd_a21_leq(a,b,c,d,pf)
! 1958: P a,b,c,d;
! 1959: F *pf;
! 1960: {
! 1961: F hf;
! 1962: NODE cj=NULL,cjc=NULL,dj=NULL,djc=NULL;
! 1963: P hp1,hp2;
! 1964:
! 1965: NEXTNODE(dj,djc);
! 1966: NEXTNODE(cj,cjc);
! 1967: mulp(CO,a,d,&hp1);
! 1968: MKAF(hf,AL_LEQ,hp1);
! 1969: BDY(cjc) = (pointer)hf;
! 1970: NEXTNODE(cj,cjc);
! 1971: mulp(CO,a,a,&hp1);
! 1972: mulp(CO,b,b,&hp2);
! 1973: mulp(CO,hp2,c,&hp2);
! 1974: subp(CO,hp1,hp2,&hp1);
! 1975: MKAF(hf,AL_GEQ,hp1);
! 1976: BDY(cjc) = (pointer)hf;
! 1977: MKJF(hf,AL_AND,cj);
! 1978: BDY(djc) = (pointer)hf;
! 1979: NEXTNODE(dj,djc);
! 1980: cj = NULL;
! 1981: NEXTNODE(cj,cjc);
! 1982: MKAF(hf,AL_LEQ,hp1);
! 1983: BDY(cjc) = (pointer)hf;
! 1984: NEXTNODE(cj,cjc);
! 1985: mulp(CO,b,d,&hp1);
! 1986: MKAF(hf,AL_LEQ,hp1);
! 1987: BDY(cjc) = (pointer)hf;
! 1988: MKJF(hf,AL_AND,cj);
! 1989: BDY(djc) = (pointer)hf;
! 1990: MKJF(*pf,AL_OR,dj);
! 1991: }
! 1992:
! 1993: void substd_a21_lessp(a,b,c,d,pf)
! 1994: P a,b,c,d;
! 1995: F *pf;
! 1996: {
! 1997: F hf,hf0;
! 1998: NODE cj=NULL,cjc=NULL,d1=NULL,d1c=NULL,d2=NULL,d2c=NULL;
! 1999: P hp1,hp2;
! 2000:
! 2001: NEXTNODE(d1,d1c);
! 2002: NEXTNODE(cj,cjc);
! 2003: mulp(CO,a,d,&hp1);
! 2004: MKAF(hf0,AL_LESSP,hp1);
! 2005: BDY(cjc) = (pointer)hf0;
! 2006: NEXTNODE(cj,cjc);
! 2007: mulp(CO,a,a,&hp1);
! 2008: mulp(CO,b,b,&hp2);
! 2009: mulp(CO,hp2,c,&hp2);
! 2010: subp(CO,hp1,hp2,&hp1);
! 2011: MKAF(hf,AL_GREATERP,hp1);
! 2012: BDY(cjc) = (pointer)hf;
! 2013: MKJF(hf,AL_AND,cj);
! 2014: BDY(d1c) = (pointer)hf;
! 2015: NEXTNODE(d1,d1c);
! 2016: cj = NULL;
! 2017: NEXTNODE(cj,cjc);
! 2018: NEXTNODE(d2,d2c);
! 2019: MKAF(hf,AL_LESSP,hp1);
! 2020: BDY(d2c) = (pointer)hf;
! 2021: NEXTNODE(d2,d2c);
! 2022: BDY(d2c) = (pointer)hf0;
! 2023: MKJF(hf,AL_OR,d2);
! 2024: BDY(cjc) = (pointer)hf;
! 2025: NEXTNODE(cj,cjc);
! 2026: mulp(CO,b,d,&hp1);
! 2027: MKAF(hf,AL_LEQ,hp1);
! 2028: BDY(cjc) = (pointer)hf;
! 2029: MKJF(hf,AL_AND,cj);
! 2030: BDY(d1c) = (pointer)hf;
! 2031: MKJF(*pf,AL_OR,d1);
! 2032: }
! 2033:
! 2034: void getrecoeffs(prem,fdeg,re,pa,pb,pc,pld)
! 2035: P prem,*pa,*pb,*pc,*pld;
! 2036: Z fdeg;
! 2037: RE re;
! 2038: {
! 2039: P a,b,c,alpha,beta,h1,h2;
! 2040: Z two;
! 2041:
! 2042: alpha = COEF(DC(prem));
! 2043: beta = (NEXT(DC(prem))) ? COEF(NEXT(DC(prem))) : 0;
! 2044: getqcoeffs(re->p,&a,&b,&c);
! 2045: STOQ(2,two);
! 2046: mulp(CO,(P)two,a,&h1);
! 2047: mulp(CO,h1,beta,&h2);
! 2048: mulp(CO,b,alpha,&h1);
! 2049: subp(CO,h2,h1,pa);
! 2050: *pb = alpha;
! 2051: *pc = DISC(re);
! 2052: *pld = (evenz(fdeg)) ? (P)ONE : a;
! 2053: }
! 2054:
! 2055: void subinf_a(f,v,re,pnf)
! 2056: F f,*pnf;
! 2057: V v;
! 2058: RE re;
! 2059: {
! 2060: if (AL_ORDER(FOP(f)))
! 2061: subinf_a_o(f,v,re,pnf);
! 2062: else
! 2063: subtrans_a_no(f,v,pnf);
! 2064: }
! 2065:
! 2066: void subinf_a_o(f,v,ire,pnf)
! 2067: F f,*pnf;
! 2068: V v;
! 2069: RE ire;
! 2070: {
! 2071: P rlhs;
! 2072:
! 2073: if (!al_reorder(FPL(f),v,&rlhs))
! 2074: *pnf = f;
! 2075: else
! 2076: subinf_a_o1(FOP(f),DC(rlhs),ire,pnf);
! 2077: }
! 2078:
! 2079: void subinf_a_o1(op,lhsdcp,ire,pnf)
! 2080: oFOP op;
! 2081: DCP lhsdcp;
! 2082: RE ire;
! 2083: F *pnf;
! 2084: {
! 2085: P an;
! 2086: F h;
! 2087: NODE c=NULL,cc=NULL,d=NULL,dc=NULL;
! 2088:
! 2089: if (lhsdcp == 0) {
! 2090: MKAF(*pnf,op,0);
! 2091: return;
! 2092: }
! 2093: if (DEG(lhsdcp) == 0) {
! 2094: MKAF(*pnf,op,COEF(lhsdcp));
! 2095: return;
! 2096: }
! 2097: if (ITYPE(ire) == MINF && !evenz(DEG(lhsdcp)))
! 2098: chsgnp(COEF(lhsdcp),&an);
! 2099: else
! 2100: an = COEF(lhsdcp);
! 2101: NEXTNODE(d,dc);
! 2102: MKAF(h,AL_MKSTRICT(op),an);
! 2103: BDY(dc) = (pointer)h;
! 2104: NEXTNODE(d,dc);
! 2105: NEXTNODE(c,cc);
! 2106: MKAF(h,AL_EQUAL,an);
! 2107: BDY(cc) = (pointer)h;
! 2108: NEXTNODE(c,cc);
! 2109: subinf_a_o1(op,NEXT(lhsdcp),ire,&h);
! 2110: BDY(cc) = (pointer)h;
! 2111: MKJF(h,AL_AND,c);
! 2112: BDY(dc) = (pointer)h;
! 2113: MKJF(*pnf,AL_OR,d);
! 2114: }
! 2115:
! 2116: void subtrans_a_no(f,v,pnf)
! 2117: F f,*pnf;
! 2118: V v;
! 2119: {
! 2120: P rlhs;
! 2121: DCP sc;
! 2122: F h;
! 2123: NODE nargl=NULL,narglc;
! 2124: oFOP op=FOP(f);
! 2125:
! 2126: if (!al_reorder(FPL(f),v,&rlhs)) {
! 2127: *pnf = f;
! 2128: return;
! 2129: }
! 2130: for (sc=DC(rlhs); sc; sc=NEXT(sc)) {
! 2131: NEXTNODE(nargl,narglc);
! 2132: MKAF(h,op,COEF(sc));
! 2133: BDY(narglc) = (pointer)h;
! 2134: }
! 2135: smkjf(pnf,AL_TRSUBEXP(op),nargl);
! 2136: }
! 2137:
! 2138: void subpme_a(af,v,re,pnf)
! 2139: F af,*pnf;
! 2140: V v;
! 2141: RE re;
! 2142: {
! 2143: if (AL_ORDER(FOP(af)))
! 2144: subpme_a_o(af,v,re,pnf);
! 2145: else
! 2146: subtrans_a_no(af,v,pnf);
! 2147: }
! 2148:
! 2149: void subpme_a_o(af,v,r,pnf)
! 2150: F af,*pnf;
! 2151: V v;
! 2152: RE r;
! 2153: {
! 2154: F h;
! 2155: RE stdre;
! 2156:
! 2157: subpme_a_o1(FOP(af),FPL(af),v,ITYPE(r)==MEPS,&h);
! 2158: MKRE(stdre,r->p,DISC(r),ROOTNO(r),STD);
! 2159: subref(h,v,stdre,pnf);
! 2160: }
! 2161:
! 2162: void subpme_a_o1(op,lhs,v,minus,pnf)
! 2163: oFOP op;
! 2164: P lhs;
! 2165: V v;
! 2166: int minus;
! 2167: F *pnf;
! 2168: {
! 2169: Z deg;
! 2170: F h;
! 2171: NODE c=NULL,cc=NULL,d=NULL,dc=NULL;
! 2172: P df;
! 2173:
! 2174: degp(v,lhs,°);
! 2175: if (deg == 0) {
! 2176: MKAF(*pnf,op,lhs);
! 2177: return;
! 2178: };
! 2179: NEXTNODE(d,dc);
! 2180: MKAF(h,AL_MKSTRICT(op),lhs);
! 2181: BDY(dc) = (pointer)h;
! 2182: NEXTNODE(d,dc);
! 2183: NEXTNODE(c,cc);
! 2184: MKAF(h,AL_EQUAL,lhs);
! 2185: BDY(cc) = (pointer)h;
! 2186: NEXTNODE(c,cc);
! 2187: diffp(CO,lhs,v,&df);
! 2188: if (minus)
! 2189: chsgnp(df,&df);
! 2190: subpme_a_o1(op,df,v,minus,&h);
! 2191: BDY(cc) = (pointer)h;
! 2192: MKJF(h,AL_AND,c);
! 2193: BDY(dc) = (pointer)h;
! 2194: MKJF(*pnf,AL_OR,d);
! 2195: }
! 2196:
! 2197: int comember(co,x)
! 2198: CONT co;
! 2199: CEL x;
! 2200: {
! 2201: NODE sc;
! 2202:
! 2203: for (sc=FIRST(co); sc; sc=NEXT(sc))
! 2204: if (synequalf(MAT(x),MAT((CEL)BDY(sc))))
! 2205: return 1;
! 2206: return 0;
! 2207: }
! 2208:
! 2209: void coadd(co,x)
! 2210: CONT co;
! 2211: CEL x;
! 2212: {
! 2213: NEXTNODE(FIRST(co),LAST(co));
! 2214: BDY(LAST(co)) = (pointer)x;
! 2215: }
! 2216:
! 2217: int coget(co,px)
! 2218: CONT co;
! 2219: CEL *px;
! 2220: {
! 2221: if (FIRST(co) == 0)
! 2222: return 0;
! 2223: *px = (CEL)BDY(FIRST(co));
! 2224: FIRST(co) = NEXT(FIRST(co));
! 2225: return 1;
! 2226: }
! 2227:
! 2228: int colen(co)
! 2229: CONT co;
! 2230: {
! 2231: NODE sc;
! 2232: int n=0;
! 2233:
! 2234: for (sc=FIRST(co); sc; sc=NEXT(sc))
! 2235: n++;
! 2236: return n;
! 2237: }
! 2238:
! 2239: /* Misc */
! 2240:
! 2241: void apply2ats(f,client,argv,pnf)
! 2242: F f,*pnf;
! 2243: void (*client)();
! 2244: pointer argv[];
! 2245: {
! 2246: if (AL_ATOMIC(FOP(f)))
! 2247: (*client)(f,argv,pnf);
! 2248: else if (AL_JUNCT(FOP(f))) {
! 2249: NODE sc,n=NULL,c;
! 2250: for (sc=FJARG(f); sc; sc=NEXT(sc)) {
! 2251: NEXTNODE(n,c);
! 2252: apply2ats(BDY(sc),client,argv,&BDY(c));
! 2253: }
! 2254: MKJF(*pnf,FOP(f),n);
! 2255: }
! 2256: else if (AL_TVAL(FOP(f)))
! 2257: *pnf = f;
! 2258: else if (AL_QUANT(FOP(f))) {
! 2259: F h;
! 2260: apply2ats(FQMAT(f),client,argv,&h);
! 2261: MKQF(*pnf,FOP(f),FQVR(f),h);
! 2262: } else
! 2263: error("unknown operator in apply2ats");
! 2264: }
! 2265:
! 2266: void atl(f,pn)
! 2267: F f;
! 2268: NODE *pn;
! 2269: {
! 2270: NODE c;
! 2271:
! 2272: *pn = NULL;
! 2273: atl1(f,pn,&c);
! 2274: }
! 2275:
! 2276: void atl1(f,pn,pc)
! 2277: F f;
! 2278: NODE *pn,*pc;
! 2279: {
! 2280: NODE sc;
! 2281:
! 2282: if (AL_ATOMIC(FOP(f))) {
! 2283: simpl_gand_insert_a(f,pn,pc);
! 2284: return;
! 2285: }
! 2286: if (AL_JUNCT(FOP(f)))
! 2287: for (sc=FJARG(f); sc; sc=NEXT(sc))
! 2288: atl1(BDY(sc),pn,pc);
! 2289: }
! 2290:
! 2291: void atnum(f,pn)
! 2292: F f;
! 2293: Q *pn;
! 2294: {
! 2295: *pn = 0;
! 2296: atnum1(f,pn);
! 2297: }
! 2298:
! 2299: void atnum1(f,pn)
! 2300: F f;
! 2301: Q *pn;
! 2302: {
! 2303: NODE sc;
! 2304:
! 2305: if (AL_ATOMIC(FOP(f)))
! 2306: addq(*pn,(Q)ONE,pn);
! 2307: else if (AL_JUNCT(FOP(f)))
! 2308: for (sc=FJARG(f); sc; sc=NEXT(sc))
! 2309: atnum1(BDY(sc),pn);
! 2310: }
! 2311:
! 2312: void pnegate(f,pnf)
! 2313: F f,*pnf;
! 2314: {
! 2315: F h;
! 2316: NODE sc,n=NULL,c;
! 2317: oFOP op=FOP(f);
! 2318:
! 2319: if (AL_QUANT(op)) {
! 2320: pnegate(FQMAT(f),&h);
! 2321: MKQF(*pnf,AL_LNEGOP(op),FQVR(f),h);
! 2322: return;
! 2323: }
! 2324: if (AL_JUNCT(op)) {
! 2325: for (sc=FJARG(f); sc; sc=NEXT(sc)) {
! 2326: NEXTNODE(n,c);
! 2327: pnegate((F)BDY(sc),(F*)&BDY(c));
! 2328: }
! 2329: MKJF(*pnf,AL_LNEGOP(op),n);
! 2330: return;
! 2331: }
! 2332: if (AL_ATOMIC(op)) {
! 2333: MKAF(*pnf,AL_LNEGOP(op),FPL(f));
! 2334: return;
! 2335: }
! 2336: if (op == AL_TRUE) {
! 2337: *pnf = F_FALSE;
! 2338: return;
! 2339: }
! 2340: if (op == AL_FALSE) {
! 2341: *pnf = F_TRUE;
! 2342: return;
! 2343: }
! 2344: error("unknown operator in pnegate()");
! 2345: }
! 2346:
! 2347: void subf(o,f,v,p,pf)
! 2348: VL o;
! 2349: F f,*pf;
! 2350: V v;
! 2351: P p;
! 2352: {
! 2353: pointer argv[3];
! 2354:
! 2355: argv[0] = (pointer)o;
! 2356: argv[1] = (pointer)v;
! 2357: argv[2] = (pointer)p;
! 2358: apply2ats(f,subf_a,argv,pf);
! 2359: }
! 2360:
! 2361: void subf_a(at,argv,pat)
! 2362: F at,*pat;
! 2363: pointer argv[];
! 2364: {
! 2365: P nlhs;
! 2366:
! 2367: substp((VL)argv[0],FPL(at),(V)argv[1],(P)argv[2],&nlhs);
! 2368: MKAF(*pat,FOP(at),nlhs);
! 2369: }
! 2370:
! 2371: void nnf(f,pf)
! 2372: F f,*pf;
! 2373: {
! 2374: nnf1(f,0,0,pf);
! 2375: }
! 2376:
! 2377: void nnf1(f,neg,disj,pf)
! 2378: F f,*pf;
! 2379: int neg,disj;
! 2380: {
! 2381: F h;
! 2382: NODE sc,nargl=NULL,narglc=NULL;
! 2383: oFOP op=FOP(f);
! 2384:
! 2385: if (AL_ATOMIC(op) || AL_TVAL(op)) {
! 2386: if (neg)
! 2387: pnegate(f,pf);
! 2388: else
! 2389: *pf = f;
! 2390: return;
! 2391: }
! 2392: if (AL_JUNCT(op)) {
! 2393: if (neg)
! 2394: op = AL_LNEGOP(op);
! 2395: for (sc=FJARG(f); sc; sc=NEXT(sc)) {
! 2396: NEXTNODE(nargl,narglc);
! 2397: nnf1((F)BDY(sc),neg,op==AL_OR,(F*)&BDY(narglc));
! 2398: }
! 2399: MKJF(*pf,op,nargl);
! 2400: return;
! 2401: }
! 2402: if (op == AL_IMPL) {
! 2403: op = neg ? AL_AND : AL_OR;
! 2404: NEXTNODE(nargl,narglc);
! 2405: nnf1(FLHS(f),!neg,op==AL_OR,(F*)&BDY(narglc));
! 2406: NEXTNODE(nargl,narglc);
! 2407: nnf1(FRHS(f),neg,op==AL_OR,(F*)&BDY(narglc));
! 2408: MKJF(*pf,op,nargl);
! 2409: return;
! 2410: }
! 2411: if (op == AL_REPL) {
! 2412: op = neg ? AL_AND : AL_OR;
! 2413: NEXTNODE(nargl,narglc);
! 2414: nnf1(FLHS(f),neg,op==AL_OR,(F*)&BDY(narglc));
! 2415: NEXTNODE(nargl,narglc);
! 2416: nnf1(FRHS(f),!neg,op==AL_OR,(F*)&BDY(narglc));
! 2417: MKJF(*pf,op,nargl);
! 2418: return;
! 2419: }
! 2420: if (op == AL_EQUIV) {
! 2421: /* should consider disj and its arguments ops */
! 2422: NEXTNODE(nargl,narglc);
! 2423: MKBF(h,AL_IMPL,FLHS(f),FRHS(f));
! 2424: BDY(narglc) = (pointer)h;
! 2425: NEXTNODE(nargl,narglc);
! 2426: MKBF(h,AL_REPL,FLHS(f),FRHS(f));
! 2427: BDY(narglc) = (pointer)h;
! 2428: MKJF(h,AL_AND,nargl);
! 2429: nnf1(h,neg,disj,pf);
! 2430: return;
! 2431: }
! 2432: if (AL_QUANT(op)) {
! 2433: nnf1(FQMAT(f),neg,0,&h);
! 2434: MKQF(*pf,neg ? AL_LNEGOP(op) : op,FQVR(f),h);
! 2435: return;
! 2436: }
! 2437: if (op == AL_NOT) {
! 2438: nnf1(FARG(f),!neg,disj,pf);
! 2439: return;
! 2440: }
! 2441: error("unknown operator in nnf1()");
! 2442: }
! 2443:
! 2444: void freevars(f,pvl)
! 2445: F f;
! 2446: VL *pvl;
! 2447: {
! 2448: *pvl = NULL;
! 2449: freevars1(f,pvl,NULL);
! 2450: }
! 2451:
! 2452: void freevars1(f,pvl,cbvl)
! 2453: F f;
! 2454: VL *pvl,cbvl;
! 2455: {
! 2456: VL hvl;
! 2457: NODE sc;
! 2458: oFOP op=FOP(f);
! 2459:
! 2460: if (AL_ATOMIC(op)) {
! 2461: freevars1_a(f,pvl,cbvl);
! 2462: return;
! 2463: }
! 2464: if (AL_JUNCT(op)) {
! 2465: for (sc=FJARG(f); sc; sc=NEXT(sc))
! 2466: freevars1((F)BDY(sc),pvl,cbvl);
! 2467: return;
! 2468: }
! 2469: if (AL_QUANT(op)) {
! 2470: MKVL(hvl,FQVR(f),cbvl);
! 2471: freevars1(FQMAT(f),pvl,hvl);
! 2472: return;
! 2473: }
! 2474: if (AL_UNI(op)) {
! 2475: freevars1(FARG(f),pvl,cbvl);
! 2476: return;
! 2477: }
! 2478: if (AL_EXT(op)) {
! 2479: freevars1(FLHS(f),pvl,cbvl);
! 2480: freevars1(FRHS(f),pvl,cbvl);
! 2481: return;
! 2482: }
! 2483: if (AL_TVAL(op))
! 2484: return;
! 2485: error("unknown operator in freevars1()");
! 2486: }
! 2487:
! 2488: void freevars1_a(f,pvl,cbvl)
! 2489: F f;
! 2490: VL *pvl,cbvl;
! 2491: {
! 2492: VL sc,sc2,last;
! 2493:
! 2494: for (get_vars((Obj)FPL(f),&sc); sc; sc=NEXT(sc)) {
! 2495: for(sc2=cbvl; sc2; sc2=NEXT(sc2))
! 2496: if (VR(sc) == VR(sc2))
! 2497: break;
! 2498: if (sc2)
! 2499: continue;
! 2500: if (!*pvl) {
! 2501: MKVL(*pvl,VR(sc),NULL);
! 2502: continue;
! 2503: }
! 2504: for (sc2=*pvl; sc2; sc2=NEXT(sc2)) {
! 2505: if (VR(sc) == VR(sc2))
! 2506: break;
! 2507: last = sc2;
! 2508: }
! 2509: if (sc2)
! 2510: continue;
! 2511: MKVL(NEXT(last),VR(sc),NULL);
! 2512: }
! 2513: }
! 2514:
! 2515: int compf(vl,f1,f2)
! 2516: VL vl;
! 2517: F f1,f2;
! 2518: {
! 2519: if (AL_ATOMIC(FOP(f1)) && AL_ATOMIC(FOP(f2)))
! 2520: return compaf(vl,f1,f2);
! 2521: if (AL_ATOMIC(FOP(f1)))
! 2522: return 1;
! 2523: if (AL_ATOMIC(FOP(f2)))
! 2524: return -1;
! 2525: if (synequalf(f1,f2))
! 2526: return 0;
! 2527: return 2;
! 2528: }
! 2529:
! 2530: /* Debug */
! 2531:
! 2532: void ap(x)
! 2533: pointer *x;
! 2534: {
! 2535: printexpr(CO,(Obj)x);
! 2536: printf("\n");
! 2537: }
! 2538:
! 2539: void rep(re)
! 2540: RE re;
! 2541: {
! 2542: printf("(");
! 2543: printexpr(CO,(Obj)re->p);
! 2544: printf(",");
! 2545: printexpr(CO,(Obj)DISC(re));
! 2546: printf(",");
! 2547: printf("%d)\n",re->itype);
! 2548: }
! 2549:
! 2550: void gpp(gp)
! 2551: GP gp;
! 2552: {
! 2553: ap(gp->g);
! 2554: rep(gp->p);
! 2555: }
! 2556:
! 2557: void esetp(eset)
! 2558: NODE eset;
! 2559: {
! 2560: NODE sc;
! 2561:
! 2562: for (sc=eset; sc; sc=NEXT(sc))
! 2563: gpp(BDY(sc));
! 2564: }
! 2565:
! 2566: void nodep(n)
! 2567: NODE n;
! 2568: {
! 2569: NODE sc;
! 2570:
! 2571: for (sc=n; sc; sc=NEXT(sc))
! 2572: ap(BDY(sc));
! 2573: }
! 2574:
! 2575: void lbfp(x)
! 2576: LBF x;
! 2577: {
! 2578: printf("(%d,",LBFLB(x));
! 2579: printexpr(CO,(Obj)LBFF(x));
! 2580: printf(")");
! 2581: }
! 2582:
! 2583: void thp(x)
! 2584: NODE x;
! 2585: {
! 2586: if (x == NULL) {
! 2587: printf("[]\n");
! 2588: return;
! 2589: }
! 2590: printf("[");
! 2591: lbfp((LBF)BDY(x));
! 2592: x = NEXT(x);
! 2593: for (; x != NULL; x = NEXT(x)) {
! 2594: printf(",");
! 2595: lbfp((LBF)BDY(x));
! 2596: }
! 2597: printf("]\n");
! 2598: }
FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>
![[BACK]](/icons/cvsweb/back.gif){kind=icon}
Return to al.c CVS log ![[TXT]](/icons/cvsweb/text.gif){kind=icon}
![[DIR]](/icons/cvsweb/dir.gif){kind=icon}
Up to [local] / OpenXM_contrib2 / asir2018 / builtin