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