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