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