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