Annotation of OpenXM_contrib2/asir2000/builtin/al.c, Revision 1.6
1.6 ! noro 1: /* $OpenXM: OpenXM_contrib2/asir2000/builtin/al.c,v 1.5 2001/10/09 01:36:04 noro Exp $ */
1.1 noro 2: /* ----------------------------------------------------------------------
1.3 noro 3: $Id: al.c,v 1.6 2001/03/08 18:51:10 sturm Exp $
1.1 noro 4: ----------------------------------------------------------------------
5: File al.c: Real quantifier elimination code for RISA/ASIR
6:
1.2 noro 7: Copyright (c) 1996-2001 by
1.1 noro 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:
1.5 noro 17: void Preverse();
1.1 noro 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();
1.5 noro 27: int gauss_abc();
1.1 noro 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();
1.5 noro 43: int simpl_gand_smtbdlhs();
44: int simpl_gand_smtbelhs();
1.1 noro 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();
1.3 noro 68: int delv();
1.1 noro 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();
1.5 noro 78: void indices();
1.1 noro 79: void mkeset();
80: int selectside();
81: int cmp2n();
82: void add2eset();
1.2 noro 83: void seproots();
1.1 noro 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();
1.5 noro 125: void gauss_mkeset1();
126: void gauss_mkeset2();
1.1 noro 127:
128: extern Verbose;
129:
130: struct oRE {
1.6 ! noro 131: P p;
! 132: P discr;
1.2 noro 133: int rootno;
1.6 ! noro 134: int itype;
1.1 noro 135: };
136:
137: typedef struct oRE *RE;
138:
139: struct oGP {
1.6 ! noro 140: F g;
! 141: RE p;
1.1 noro 142: };
143:
144: typedef struct oGP *GP;
145:
146: struct oCEL {
1.6 ! noro 147: VL vl;
! 148: F mat;
1.1 noro 149: };
150:
151: typedef struct oCEL *CEL;
152:
153: struct oCONT {
1.6 ! noro 154: NODE first;
! 155: NODE last;
1.1 noro 156: };
157:
158: typedef struct oCONT *CONT;
159:
160: struct oQVL {
1.6 ! noro 161: oFOP q;
! 162: VL vl;
1.1 noro 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)))
1.2 noro 173: #define MKRE(x,pp,d,rn,i) \
174: (NEWRE(x),(x)->p=pp,(x)->discr=d,(x)->rootno=rn,(x)->itype=i)
1.1 noro 175: #define DISC(re) ((re)->discr)
1.2 noro 176: #define ROOTNO(re) ((re)->rootno)
1.1 noro 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[] = {
1.6 ! noro 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}
1.1 noro 223: };
224:
225: void Phugo(arg,rp)
226: NODE arg;
227: F *rp;
228: {
1.6 ! noro 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);
1.1 noro 235: }
236:
237: void Pex(arg,rp)
238: NODE arg;
239: F *rp;
240: {
1.6 ! noro 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);
1.1 noro 245: }
246:
247: void Pall(arg,rp)
248: NODE arg;
249: F *rp;
250: {
1.6 ! noro 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);
1.1 noro 255: }
256:
257: void constrq(q,vars,m,rp)
258: oFOP q;
259: Obj vars;
260: F m,*rp;
261: {
1.6 ! noro 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: }
1.1 noro 282: }
283:
284: void Pfop(arg,rp)
285: NODE arg;
286: Q *rp;
287: {
1.6 ! noro 288: oFOP op;
1.1 noro 289:
1.6 ! noro 290: op = FOP((F)ARG0(arg));
! 291: STOQ((int)op,*rp);
1.1 noro 292: }
293:
294: void Pfargs(arg,rp)
295: NODE arg;
296: LIST *rp;
297: {
1.6 ! noro 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;
1.1 noro 322: }
323:
324: void Pfopargs(arg,rp)
325: NODE arg;
326: LIST *rp;
327: {
1.6 ! noro 328: oFOP op;
! 329: LIST l;
! 330: NODE n0,n1,n2;
! 331: F f;
! 332: P x;
! 333: Q 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;
1.1 noro 355: }
356:
357: void Pcompf(arg,rp)
358: NODE arg;
359: Q *rp;
360: {
1.6 ! noro 361: STOQ(compf(CO,BDY(arg),BDY(NEXT(arg))),*rp);
1.1 noro 362: }
363:
364: void Patnum(arg,rp)
365: NODE arg;
366: Q *rp;
367: {
1.6 ! noro 368: atnum(BDY(arg),rp);
1.1 noro 369: }
370:
371: void Patl(arg,rp)
372: NODE arg;
373: LIST *rp;
374: {
1.6 ! noro 375: NODE h;
1.1 noro 376:
1.6 ! noro 377: atl(BDY(arg),&h);
! 378: MKLIST(*rp,h);
1.1 noro 379: }
380:
381: void Pqevar(arg,rp)
382: NODE arg;
383: F *rp;
384: {
1.6 ! noro 385: qevar(BDY(arg),VR((P)BDY(NEXT(arg))),rp);
1.1 noro 386: }
387:
388: void Pqe(arg,rp)
389: NODE arg;
390: F *rp;
391: {
1.6 ! noro 392: qe(BDY(arg),rp);
1.1 noro 393: }
394:
395: void Psubf(arg,rp)
396: NODE arg;
397: F *rp;
398: {
1.6 ! noro 399: subf(CO,(F)BDY(arg),VR((P)BDY(NEXT(arg))),(P)BDY(NEXT(NEXT(arg))),rp);
1.1 noro 400: }
401:
402: void Pnnf(arg,rp)
403: NODE arg;
404: F *rp;
405: {
1.6 ! noro 406: nnf((F)BDY(arg),rp);
1.1 noro 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: {
1.6 ! noro 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);
1.1 noro 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: {
1.6 ! noro 457: F h;
! 458: oFOP op=FOP(f);
1.1 noro 459:
1.6 ! noro 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");
1.1 noro 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)) {
1.6 ! noro 518: NEXTNODE(th,thc);
! 519: BDY(thc) = BDY(oth);
1.1 noro 520: }
521: for (; argl; argl = NEXT(argl)) {
522: if (FOP((F)BDY(argl)) == gfalse) {
1.6 ! noro 523: *pnf = (F)BDY(argl);
1.1 noro 524: return;
1.6 ! noro 525: }
1.1 noro 526: if (AL_ATOMIC(FOP((F)BDY(argl)))) {
527: simpl_a((F)BDY(argl),&h);
528: if (FOP(h) == gfalse) {
1.6 ! noro 529: *pnf = h;
! 530: return;
! 531: }
1.1 noro 532: st = simpl_gand_udnargls(gand,gtrue,h,n,&th,&thc,&cnargl,&cc);
533: if (st == GINCONSISTENT) {
1.6 ! noro 534: MKTV(fgfalse,gfalse);
! 535: *pnf = fgfalse;
! 536: return;
! 537: }
1.1 noro 538: } else
1.6 ! noro 539: simpl_gand_insert_c((F)BDY(argl),&cnargl,&cc);
! 540: }
1.1 noro 541: for (; cnargl != NULL; cnargl = NEXT(cnargl)) {
542: simpl1((F)BDY(cnargl),th,n+1,&h);
543: if (FOP(h) == gfalse) {
1.6 ! noro 544: *pnf = h;
1.1 noro 545: return;
1.6 ! noro 546: }
1.1 noro 547: st = simpl_gand_udnargls(gand,gtrue,h,n,&th,&thc,&cnargl2,&cc2);
548: switch (st) {
549: case GINCONSISTENT:
1.6 ! noro 550: MKTV(fgfalse,gfalse);
! 551: *pnf = fgfalse;
! 552: return;
1.1 noro 553: case NEWAT:
554: if (cnargl2 != NULL) {
1.6 ! noro 555: if (cnargl != NULL)
! 556: NEXT(cc) = cnargl2;
! 557: else
! 558: cnargl = cnargl2;
! 559: cc = cc2;
! 560: cnargl2 = cc2 = NULL;
! 561: }
1.1 noro 562: break;
563: }
564: }
565: simpl_th2atl(gand,th,n,&nargl,&narglc);
566: if (nargl == NULL)
1.6 ! noro 567: nargl = cnargl2;
1.1 noro 568: else
1.6 ! noro 569: NEXT(narglc) = cnargl2;
1.1 noro 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:
1.6 ! noro 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;
1.1 noro 590: case AL_OR:
1.6 ! noro 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;
1.1 noro 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);
1.6 ! noro 623: for (; sargl; sargl = NEXT(sargl)) {
! 624: h = (F)BDY(sargl);
1.1 noro 625: if (AL_ATOMIC(FOP(h))) {
1.6 ! noro 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: }
1.1 noro 634: } else
1.6 ! noro 635: simpl_gand_insert_c(h,pcnargl,pcc);
1.1 noro 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 (cmpq((Q)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)) {
1.6 ! noro 861: NEXTNODE(*pnl,*pnlc);
! 862: if(BDY(l) == old)
! 863: BDY(*pnlc) = new;
! 864: else
! 865: BDY(*pnlc) = BDY(l);
1.1 noro 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))
1.6 ! noro 875: if(BDY(l) != obj) {
! 876: NEXTNODE(*pnl,*pnlc);
! 877: BDY(*pnlc) = BDY(l);
! 878: }
1.1 noro 879: }
880:
881: void simpl_gand_insert_a(f,paargl,pac)
882: F f;
883: NODE *paargl,*pac;
884: {
1.6 ! noro 885: int w;
! 886: NODE n,sc,prev;
1.1 noro 887:
1.6 ! noro 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;
1.1 noro 916: }
917:
918: void simpl_gand_insert_c(f,pcargl,pcc)
919: F f;
920: NODE *pcargl,*pcc;
921: {
1.6 ! noro 922: NODE sc;
1.1 noro 923:
1.6 ! noro 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;
1.1 noro 929: }
930:
931: int compaf(vl,f1,f2)
932: VL vl;
933: F f1,f2;
934: {
1.6 ! noro 935: int w;
1.1 noro 936:
1.6 ! noro 937: w = compp(vl,FPL(f1),FPL(f2));
! 938: if (w)
! 939: return w;
! 940: return comprel(FOP(f1),FOP(f2));
1.1 noro 941: }
942:
943: int comprel(op1,op2)
944: oFOP op1,op2;
945: /* implement order: =, <>, <=, <, >=, > */
946: {
1.6 ! noro 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");
1.1 noro 988: }
989:
990: int synequalf(f1,f2)
991: F f1,f2;
992: {
1.6 ! noro 993: oFOP op=FOP(f1);
1.1 noro 994:
1.6 ! noro 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: }
1.1 noro 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: {
1.6 ! noro 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);
1.1 noro 1041: }
1042:
1043: void simpl_equiv(lhs,rhs,th,n,pf)
1044: F lhs,rhs,*pf;
1045: NODE th;
1046: int n;
1047: {
1.6 ! noro 1048: F h,hh;
1.1 noro 1049:
1.6 ! noro 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);
1.1 noro 1069: }
1070:
1071: void simpl_a(f,pnf)
1072: F f,*pnf;
1073: {
1.6 ! noro 1074: oFOP r=FOP(f);
! 1075: P lhs=(P)FPL(f);
1.1 noro 1076:
1.6 ! noro 1077: if (NUMBER(lhs)) {
1.1 noro 1078: #if 0
1.6 ! noro 1079: lhs = (Q)lhs; /* good luck with the next compiler */
1.1 noro 1080: #endif
1.6 ! noro 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);
1.1 noro 1109: }
1110:
1111: void simpl_a_o(ar,alhs)
1112: oFOP *ar;
1113: P *alhs;
1114: {
1.6 ! noro 1115: DCP dec;
1.1 noro 1116:
1.6 ! noro 1117: sqfrp(CO,*alhs,&dec);
! 1118: if (SGN((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 (EVENN(NM(DEG(dec))))
! 1124: mulp(CO,*alhs,COEF(dec),alhs);
! 1125: }
1.1 noro 1126: }
1127:
1128: void simpl_a_no(alhs)
1129: P *alhs;
1130: {
1.6 ! noro 1131: DCP dec;
1.1 noro 1132:
1.6 ! noro 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);
1.1 noro 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: {
1.6 ! noro 1160: NODE bl,sc;
! 1161: F h;
1.1 noro 1162:
1.6 ! noro 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;
1.1 noro 1176: }
1177:
1178: void blocksplit(f,pbl,pmat)
1179: F f,*pmat;
1180: NODE *pbl;
1181: {
1.6 ! noro 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;
1.1 noro 1204: }
1205:
1206: void qeblock(vl,f,pnf)
1207: VL vl;
1208: F f,*pnf;
1209: {
1.6 ! noro 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);
1.1 noro 1242: }
1243:
1244: void qeblock_verbose0(vl)
1245: VL vl;
1246: {
1.6 ! noro 1247: if (!Verbose)
! 1248: return;
! 1249: printf("eliminating");
! 1250: for (; vl; vl=NEXT(vl))
! 1251: printf(" %s",NAME(VR(vl)));
1.1 noro 1252: }
1253:
1254: int qeblock_verbose1a(co,cvl,pleft,pmodulus)
1255: CONT co;
1256: VL cvl;
1257: int *pleft,*pmodulus;
1258: {
1.6 ! noro 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;
1.1 noro 1280: }
1281:
1282: void qeblock_verbose1b(g,print)
1283: int g,print;
1284: {
1.6 ! noro 1285: if (!(Verbose && print))
! 1286: return;
! 1287: printf("%s) ",g ? (g==2) ? "qg" : "lg" : "e");
! 1288: fflush(asir_out);
1.1 noro 1289: }
1290:
1291: void qeblock_verbose2()
1292: {
1.6 ! noro 1293: if (!Verbose)
! 1294: return;
! 1295: printf("\n");
1.1 noro 1296: }
1297:
1298: int getmodulus(n)
1299: int n;
1300: {
1.6 ! noro 1301: int pow=1;
! 1302:
! 1303: while (n >= pow*100) {
! 1304: pow *= 10;
! 1305: }
! 1306: return pow;
1.1 noro 1307: }
1308:
1309:
1310: int qevar(f,pcvl,pfl)
1311: F f;
1312: VL *pcvl;
1313: NODE *pfl;
1314: {
1.6 ! noro 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;
1.1 noro 1334: }
1335:
1336: int gausselim(f,pvl,px,peset)
1337: F f;
1338: VL *pvl;
1339: V *px;
1340: NODE *peset;
1341: {
1.6 ! noro 1342: Q 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; cmpq(two,deg) >= 0; addq(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;
1.1 noro 1375: }
1376:
1377: int gauss_abc(rlhs,v,deg,pa,pb,pc)
1378: P rlhs,*pa,*pb,*pc;
1379: V v;
1380: Q deg;
1381: {
1.6 ! noro 1382: Q two;
! 1383: DCP rld;
! 1384:
! 1385: rld = DC(rlhs);
! 1386: if (cmpq(DEG(rld),deg) != 0)
! 1387: return 0;
! 1388: STOQ(2,two);
! 1389: if (cmpq(deg,two) == 0) {
! 1390: *pa = COEF(rld);
! 1391: rld = NEXT(rld);
! 1392: } else
! 1393: *pa = 0;
! 1394: if (rld && cmpq(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));
1.1 noro 1404: }
1405:
1.5 noro 1406: void gauss_mkeset1(rlhs,b,peset)
1.1 noro 1407: P rlhs,b;
1408: NODE *peset;
1409: {
1.6 ! noro 1410: GP hgp;
1.1 noro 1411:
1.6 ! noro 1412: mklgp(rlhs,b,STD,&hgp);
! 1413: MKNODE(*peset,hgp,NULL);
1.1 noro 1414: }
1415:
1.5 noro 1416: void gauss_mkeset2(rlhs,a,b,c,peset)
1.1 noro 1417: P rlhs,a,b,c;
1418: NODE *peset;
1419: {
1.6 ! noro 1420: GP hgp;
! 1421: NODE esetc=NULL;
1.1 noro 1422:
1.6 ! noro 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;
1.1 noro 1435: }
1436:
1.3 noro 1437: int delv(v,vl,pnvl)
1.1 noro 1438: V v;
1.3 noro 1439: VL vl,*pnvl;
1.1 noro 1440: {
1.3 noro 1441: VL nvl=NULL,nvlc;
1.1 noro 1442:
1.6 ! noro 1443: if (v == VR(vl)) {
! 1444: *pnvl = NEXT(vl);
! 1445: return 1;
! 1446: }
! 1447: for (; vl && (VR(vl) != v); vl=NEXT(vl)) {
1.3 noro 1448: NEXTVL(nvl,nvlc);
1.6 ! noro 1449: VR(nvlc) = VR(vl);
! 1450: }
! 1451: if (vl) {
1.3 noro 1452: NEXT(nvlc) = NEXT(vl);
1.6 ! noro 1453: *pnvl = nvl;
! 1454: return 1;
! 1455: }
! 1456: *pnvl = nvl;
! 1457: return 0;
1.1 noro 1458: }
1459:
1460: int translate(f,x,trans)
1461: F f;
1462: V x;
1463: NODE trans[];
1464: {
1.6 ! noro 1465: NODE sc,transc[8];
! 1466: int bt,w=0;
1.1 noro 1467:
1.6 ! noro 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;
1.1 noro 1473: }
1474:
1475: int translate_a(at,v,trans,transc)
1476: F at;
1477: V v;
1478: NODE trans[],transc[];
1479: {
1.6 ! noro 1480: P mp;
! 1481: Q two;
! 1482: int w;
! 1483:
! 1484: w = al_reorder(FPL(at),v,&mp);
! 1485: if (w == 0)
! 1486: return 0;
! 1487: if (cmpq(ONE,DEG(DC(mp))) == 0) {
! 1488: translate_a1(FOP(at),mp,trans,transc);
! 1489: return 1;
! 1490: };
! 1491: STOQ(2,two);
! 1492: if (cmpq(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;
1.1 noro 1499: }
1500:
1501: void translate_a1(op,mp,trans,transc)
1502: oFOP op;
1503: P mp;
1504: NODE trans[],transc[];
1505: {
1.6 ! noro 1506: P b;
! 1507: int itype,btype;
! 1508: GP hgp;
! 1509:
! 1510: b = COEF(DC(mp));
! 1511: indices(op,NUM(b) ? SGN((Q)b) : 0,&itype,&btype);
! 1512: NEXTNODE(trans[btype],transc[btype]);
! 1513: mklgp(mp,b,itype,&hgp);
! 1514: BDY(transc[btype]) = (pointer)hgp;
1.1 noro 1515: }
1516:
1517: void mklgp(mp,b,itype,pgp)
1518: P mp,b;
1519: int itype;
1520: GP *pgp;
1521: {
1.6 ! noro 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);
1.1 noro 1528: }
1529:
1530: void translate_a2(op,mp,trans,transc)
1531: oFOP op;
1532: P mp;
1533: NODE trans[],transc[];
1534: {
1.6 ! noro 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;
1.1 noro 1548: }
1549:
1.2 noro 1550: void mkqgp(mp,a,b,c,rootno,itype,pgp)
1.1 noro 1551: P mp,a,b,c;
1.2 noro 1552: int rootno;
1.1 noro 1553: int itype;
1554: GP *pgp;
1555: {
1.6 ! noro 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);
1.1 noro 1571: }
1572:
1573: void getqcoeffs(mp,pa,pb,pc)
1574: P mp,*pa,*pb,*pc;
1575: {
1.6 ! noro 1576: DCP hdcp;
! 1577:
! 1578: *pa = COEF(DC(mp));
! 1579: hdcp = NEXT(DC(mp));
! 1580: if (hdcp && cmpq(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;
1.1 noro 1589: }
1590:
1591: void mkdiscr(a,b,c,pd)
1592: P a,b,c,*pd;
1593: {
1.6 ! noro 1594: P h1,h2;
! 1595: Q 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);
1.1 noro 1602: }
1603:
1604: int al_reorder(p,v,pnp)
1605: P p,*pnp;
1606: V v;
1607: {
1.6 ! noro 1608: VL tvl;
1.1 noro 1609:
1.6 ! noro 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;
1.1 noro 1616: }
1617:
1.5 noro 1618: void indices(op,s,pit,pbt)
1.1 noro 1619: oFOP op;
1620: int s,*pit,*pbt;
1621: {
1.6 ! noro 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: }
1.1 noro 1668: }
1669:
1670: void mkeset(trans,x,peset)
1671: NODE trans[],*peset;
1672: V x;
1673: {
1.6 ! noro 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);
1.1 noro 1700: }
1701:
1702: int selectside(trans,pcw,pcs,pdeps,pdinf)
1703: NODE trans[];
1704: int *pcw,*pcs,*pdeps,*pdinf;
1705: {
1.6 ! noro 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;
1.1 noro 1721: }
1.6 ! noro 1722:
1.1 noro 1723: int cmp2n(n1a,n1b,n2a,n2b)
1724: NODE n1a,n1b,n2a,n2b;
1725: {
1.6 ! noro 1726: NODE n1,n2;
! 1727: int n1bleft=1,n2bleft=1;
1.1 noro 1728:
1.6 ! noro 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;
1.1 noro 1746: }
1747:
1748: void add2eset(trfield,peset,pesetc)
1749: NODE trfield,*peset,*pesetc;
1750: {
1.2 noro 1751: NODE ntrfield,ntrfieldc;
1752:
1.6 ! noro 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: }
1.2 noro 1763: }
1764:
1765: void seproots(trfield,pntrfield,pntrfieldc)
1766: NODE trfield,*pntrfield,*pntrfieldc;
1767: {
1.6 ! noro 1768: NODE sc;
! 1769: NODE ntrf=NULL,ntrfc;
! 1770: RE hre,hre2;
! 1771: GP hgp,hgp2;
1.2 noro 1772:
1.6 ! noro 1773: for (sc=trfield; sc; sc=NEXT(sc)) {
1.2 noro 1774: hgp = (GP)BDY(sc);
1.6 ! noro 1775: hre = POINT(hgp);
1.2 noro 1776: if (ROOTNO(hre) == -1) {
1.6 ! noro 1777: NEXTNODE(ntrf,ntrfc);
! 1778: MKRE(hre2,PL(hre),DISC(hre),1,ITYPE(hre));
1.2 noro 1779: MKGP(hgp2,GUARD(hgp),hre2);
1.6 ! noro 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;
1.1 noro 1791: }
1792:
1793: void sp_add2eset(trfield,itype,peset,pesetc)
1794: NODE trfield,*peset,*pesetc;
1795: int itype;
1796: {
1.6 ! noro 1797: NODE sc;
! 1798: GP hgp;
1.1 noro 1799:
1.6 ! noro 1800: for (sc=trfield; sc; sc=NEXT(sc)) {
! 1801: hgp = (GP)BDY(sc);
! 1802: ITYPE(POINT(hgp)) = itype;
! 1803: }
! 1804: add2eset(trfield,peset,pesetc);
1.1 noro 1805: }
1806:
1807: void subgpf(f,v,gp,pnf)
1808: F f,*pnf;
1809: V v;
1810: GP gp;
1811: {
1.6 ! noro 1812: NODE argl=NULL,arglc=NULL;
1.1 noro 1813:
1.6 ! noro 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);
1.1 noro 1819: }
1820:
1821: void subref(f,v,r,pnf)
1822: F f,*pnf;
1823: V v;
1824: RE r;
1825: {
1.6 ! noro 1826: pointer argv[2];
1.1 noro 1827:
1.6 ! noro 1828: argv[0] = (pointer)v;
! 1829: argv[1] = (pointer)r;
! 1830: apply2ats(f,subref_a,argv,pnf);
1.1 noro 1831: }
1832:
1833: void subref_a(at,argv,pnat)
1834: F at,*pnat;
1835: pointer argv[];
1836: {
1.6 ! noro 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: }
1.1 noro 1854: }
1855:
1856: void substd_a(at,v,re,pnf)
1857: F at,*pnf;
1858: V v;
1859: RE re;
1860: {
1.6 ! noro 1861: VL no;
! 1862: P rlhs,prem,nlhs;
! 1863: Q 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,PL(re),&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: subq(DEG(DC(rlhs)),DEG(DC(PL(re))),&dd);
! 1878: addq(dd,ONE,&dndeg);
! 1879: if (AL_ORDER(FOP(at)) && (!EVENN(NM(dndeg))))
! 1880: mulp(CO,prem,COEF(DC(PL(re))),&nlhs);
! 1881: else
! 1882: nlhs = prem;
! 1883: MKAF(*pnf,FOP(at),nlhs);
1.1 noro 1884: }
1.6 ! noro 1885:
1.1 noro 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: {
1.6 ! noro 1893: P a,b,c,ld;
1.2 noro 1894:
1.6 ! noro 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);
1.1 noro 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: {
1.6 ! noro 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: }
1.1 noro 1933: }
1934:
1935: void substd_a21_equal(a,b,c,d,pf)
1936: P a,b,c,d;
1937: F *pf;
1938: {
1.6 ! noro 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);
1.1 noro 1955: }
1956:
1957: void substd_a21_leq(a,b,c,d,pf)
1958: P a,b,c,d;
1959: F *pf;
1960: {
1.6 ! noro 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);
1.1 noro 1991: }
1992:
1993: void substd_a21_lessp(a,b,c,d,pf)
1994: P a,b,c,d;
1995: F *pf;
1996: {
1.6 ! noro 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);
1.1 noro 2032: }
2033:
2034: void getrecoeffs(prem,fdeg,re,pa,pb,pc,pld)
2035: P prem,*pa,*pb,*pc,*pld;
2036: Q fdeg;
2037: RE re;
2038: {
1.6 ! noro 2039: P a,b,c,alpha,beta,h1,h2;
! 2040: Q two;
1.1 noro 2041:
1.6 ! noro 2042: alpha = COEF(DC(prem));
! 2043: beta = (NEXT(DC(prem))) ? COEF(NEXT(DC(prem))) : 0;
! 2044: getqcoeffs(PL(re),&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 = (EVENN(NM(fdeg))) ? (P)ONE : a;
1.1 noro 2053: }
1.6 ! noro 2054:
1.1 noro 2055: void subinf_a(f,v,re,pnf)
2056: F f,*pnf;
2057: V v;
2058: RE re;
2059: {
1.6 ! noro 2060: if (AL_ORDER(FOP(f)))
! 2061: subinf_a_o(f,v,re,pnf);
! 2062: else
! 2063: subtrans_a_no(f,v,pnf);
1.1 noro 2064: }
2065:
2066: void subinf_a_o(f,v,ire,pnf)
2067: F f,*pnf;
2068: V v;
2069: RE ire;
2070: {
1.6 ! noro 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);
1.1 noro 2077: }
2078:
2079: void subinf_a_o1(op,lhsdcp,ire,pnf)
2080: oFOP op;
2081: DCP lhsdcp;
2082: RE ire;
2083: F *pnf;
2084: {
1.6 ! noro 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 && !EVENN(NM(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);
1.1 noro 2114: }
2115:
2116: void subtrans_a_no(f,v,pnf)
2117: F f,*pnf;
2118: V v;
2119: {
1.6 ! noro 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);
1.1 noro 2136: }
2137:
2138: void subpme_a(af,v,re,pnf)
2139: F af,*pnf;
2140: V v;
2141: RE re;
2142: {
1.6 ! noro 2143: if (AL_ORDER(FOP(af)))
! 2144: subpme_a_o(af,v,re,pnf);
! 2145: else
! 2146: subtrans_a_no(af,v,pnf);
1.1 noro 2147: }
2148:
2149: void subpme_a_o(af,v,r,pnf)
2150: F af,*pnf;
2151: V v;
2152: RE r;
2153: {
1.6 ! noro 2154: F h;
! 2155: RE stdre;
! 2156:
! 2157: subpme_a_o1(FOP(af),FPL(af),v,ITYPE(r)==MEPS,&h);
! 2158: MKRE(stdre,PL(r),DISC(r),ROOTNO(r),STD);
! 2159: subref(h,v,stdre,pnf);
1.1 noro 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: {
1.6 ! noro 2169: Q 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);
1.1 noro 2195: }
2196:
2197: int comember(co,x)
2198: CONT co;
2199: CEL x;
2200: {
1.6 ! noro 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;
1.1 noro 2207: }
2208:
2209: void coadd(co,x)
2210: CONT co;
2211: CEL x;
2212: {
1.6 ! noro 2213: NEXTNODE(FIRST(co),LAST(co));
! 2214: BDY(LAST(co)) = (pointer)x;
1.1 noro 2215: }
2216:
2217: int coget(co,px)
2218: CONT co;
2219: CEL *px;
2220: {
1.6 ! noro 2221: if (FIRST(co) == 0)
! 2222: return 0;
! 2223: *px = (CEL)BDY(FIRST(co));
! 2224: FIRST(co) = NEXT(FIRST(co));
! 2225: return 1;
1.1 noro 2226: }
2227:
2228: int colen(co)
2229: CONT co;
2230: {
1.6 ! noro 2231: NODE sc;
! 2232: int n=0;
! 2233:
! 2234: for (sc=FIRST(co); sc; sc=NEXT(sc))
! 2235: n++;
! 2236: return n;
1.1 noro 2237: }
2238:
2239: /* Misc */
2240:
2241: void apply2ats(f,client,argv,pnf)
2242: F f,*pnf;
2243: void (*client)();
2244: pointer argv[];
2245: {
1.6 ! noro 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");
1.1 noro 2264: }
2265:
2266: void atl(f,pn)
2267: F f;
2268: NODE *pn;
2269: {
1.6 ! noro 2270: NODE c;
1.1 noro 2271:
1.6 ! noro 2272: *pn = NULL;
! 2273: atl1(f,pn,&c);
1.1 noro 2274: }
2275:
2276: void atl1(f,pn,pc)
2277: F f;
2278: NODE *pn,*pc;
2279: {
1.6 ! noro 2280: NODE sc;
1.1 noro 2281:
1.6 ! noro 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);
1.1 noro 2289: }
2290:
2291: void atnum(f,pn)
2292: F f;
2293: Q *pn;
2294: {
1.6 ! noro 2295: *pn = 0;
! 2296: atnum1(f,pn);
1.1 noro 2297: }
2298:
2299: void atnum1(f,pn)
2300: F f;
2301: Q *pn;
2302: {
1.6 ! noro 2303: NODE sc;
! 2304:
! 2305: if (AL_ATOMIC(FOP(f)))
! 2306: addq(*pn,ONE,pn);
! 2307: else if (AL_JUNCT(FOP(f)))
! 2308: for (sc=FJARG(f); sc; sc=NEXT(sc))
! 2309: atnum1(BDY(sc),pn);
1.1 noro 2310: }
2311:
2312: void pnegate(f,pnf)
2313: F f,*pnf;
2314: {
1.6 ! noro 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()");
1.1 noro 2345: }
2346:
2347: void subf(o,f,v,p,pf)
2348: VL o;
2349: F f,*pf;
2350: V v;
2351: P p;
2352: {
1.6 ! noro 2353: pointer argv[3];
1.1 noro 2354:
1.6 ! noro 2355: argv[0] = (pointer)o;
! 2356: argv[1] = (pointer)v;
! 2357: argv[2] = (pointer)p;
! 2358: apply2ats(f,subf_a,argv,pf);
1.1 noro 2359: }
2360:
2361: void subf_a(at,argv,pat)
2362: F at,*pat;
2363: pointer argv[];
2364: {
1.6 ! noro 2365: P nlhs;
1.1 noro 2366:
1.6 ! noro 2367: substp((VL)argv[0],FPL(at),(V)argv[1],(P)argv[2],&nlhs);
! 2368: MKAF(*pat,FOP(at),nlhs);
1.1 noro 2369: }
2370:
2371: void nnf(f,pf)
2372: F f,*pf;
2373: {
1.6 ! noro 2374: nnf1(f,0,0,pf);
1.1 noro 2375: }
2376:
2377: void nnf1(f,neg,disj,pf)
2378: F f,*pf;
2379: int neg,disj;
2380: {
1.6 ! noro 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()");
1.1 noro 2442: }
2443:
2444: void freevars(f,pvl)
2445: F f;
2446: VL *pvl;
2447: {
1.6 ! noro 2448: *pvl = NULL;
! 2449: freevars1(f,pvl,NULL);
1.1 noro 2450: }
2451:
2452: void freevars1(f,pvl,cbvl)
2453: F f;
2454: VL *pvl,cbvl;
2455: {
1.6 ! noro 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()");
1.1 noro 2486: }
2487:
2488: void freevars1_a(f,pvl,cbvl)
2489: F f;
2490: VL *pvl,cbvl;
2491: {
1.6 ! noro 2492: VL sc,sc2,last;
1.1 noro 2493:
1.6 ! noro 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: }
1.1 noro 2513: }
2514:
2515: int compf(vl,f1,f2)
2516: VL vl;
2517: F f1,f2;
2518: {
1.6 ! noro 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;
1.1 noro 2528: }
2529:
2530: /* Debug */
2531:
2532: void ap(x)
2533: pointer *x;
2534: {
1.6 ! noro 2535: printexpr(CO,(Obj)x);
! 2536: printf("\n");
1.1 noro 2537: }
2538:
2539: void rep(re)
2540: RE re;
2541: {
1.6 ! noro 2542: printf("(");
! 2543: printexpr(CO,(Obj)PL(re));
! 2544: printf(",");
! 2545: printexpr(CO,(Obj)DISC(re));
! 2546: printf(",");
! 2547: printf("%d)\n",re->itype);
1.1 noro 2548: }
2549:
2550: void gpp(gp)
2551: GP gp;
2552: {
1.6 ! noro 2553: ap(gp->g);
! 2554: rep(gp->p);
1.1 noro 2555: }
2556:
2557: void esetp(eset)
2558: NODE eset;
2559: {
1.6 ! noro 2560: NODE sc;
1.1 noro 2561:
1.6 ! noro 2562: for (sc=eset; sc; sc=NEXT(sc))
! 2563: gpp(BDY(sc));
1.1 noro 2564: }
2565:
2566: void nodep(n)
2567: NODE n;
2568: {
1.6 ! noro 2569: NODE sc;
1.1 noro 2570:
1.6 ! noro 2571: for (sc=n; sc; sc=NEXT(sc))
! 2572: ap(BDY(sc));
1.1 noro 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) {
1.6 ! noro 2587: printf("[]\n");
! 2588: return;
1.1 noro 2589: }
2590: printf("[");
2591: lbfp((LBF)BDY(x));
2592: x = NEXT(x);
2593: for (; x != NULL; x = NEXT(x)) {
1.6 ! noro 2594: printf(",");
! 2595: lbfp((LBF)BDY(x));
1.1 noro 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 / asir2000 / builtin