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