![[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.2 ! noro 1: /* $OpenXM: OpenXM_contrib2/asir2018/builtin/al.c,v 1.1 2018/09/19 05:45:05 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: }
786: }
787:
788: int simpl_gand_smtbdlhs(thop,atop,difference)
789: oFOP thop,atop;
790: P difference;
791: {
792: oFOP op1,op2;
793: int drop1,drop2;
794:
795: if (cmpz((Z)difference,0) == 1) { /* good luck with the next compiler */
796: op1 = atop;
797: op2 = thop;
798: drop1 = DROP;
799: drop2 = KILL;
800: } else {
801: op1 = thop;
802: op2 = atop;
803: drop1 = KILL;
804: drop2 = DROP;
805: }
806: switch (op1) {
807: case AL_EQUAL:
808: switch (op2) {
809: case AL_EQUAL:
810: case AL_LEQ:
811: case AL_LESSP:
812: return(GINCONSISTENT);
813: default:
814: return(drop2);
815: }
816: case AL_NEQ:
817: case AL_LEQ:
818: case AL_LESSP:
819: switch (op2) {
820: case AL_EQUAL:
821: case AL_LEQ:
822: case AL_LESSP:
823: return(drop1);
824: default:
825: return(CONTINUE);
826: }
827: case AL_GEQ:
828: switch(op2) {
829: case AL_EQUAL:
830: case AL_LEQ:
831: case AL_LESSP:
832: return(GINCONSISTENT);
833: default:
834: return(drop2);
835: }
836: case AL_GREATERP:
837: switch (op2) {
838: case AL_EQUAL:
839: case AL_LEQ:
840: case AL_LESSP:
841: return(GINCONSISTENT);
842: default:
843: return(drop2);
844: }
845: }
846: }
847:
848: void lbc(f,pc)
849: P f,*pc;
850: {
851: for (*pc = f; !NUM(*pc); *pc = COEF(DC(*pc)))
852: ;
853: }
854:
855: void replaceq(l,old,new,pnl,pnlc)
856: NODE l,*pnl,*pnlc;
857: pointer old,new;
858: {
859: *pnl = NULL;
860: for (; l; l = NEXT(l)) {
861: NEXTNODE(*pnl,*pnlc);
862: if(BDY(l) == old)
863: BDY(*pnlc) = new;
864: else
865: BDY(*pnlc) = BDY(l);
866: }
867: }
868:
869: void deleteq(l,obj,pnl,pnlc)
870: NODE l,*pnl,*pnlc;
871: pointer obj;
872: {
873: *pnl = NULL;
874: for (; l; l = NEXT(l))
875: if(BDY(l) != obj) {
876: NEXTNODE(*pnl,*pnlc);
877: BDY(*pnlc) = BDY(l);
878: }
879: }
880:
881: void simpl_gand_insert_a(f,paargl,pac)
882: F f;
883: NODE *paargl,*pac;
884: {
885: int w;
886: NODE n,sc,prev;
887:
888: if (*paargl == 0) {
889: NEXTNODE(*paargl,*pac);
890: BDY(*pac) = (pointer)f;
891: return;
892: }
893: w = compaf(CO,BDY(*pac),f);
894: if (w == 1) {
895: NEXTNODE(*paargl,*pac);
896: BDY(*pac) = (pointer)f;
897: return;
898: }
899: if (w == 0)
900: return;
901: w = compaf(CO,f,BDY(*paargl));
902: if (w == 1) {
903: MKNODE(n,f,*paargl);
904: *paargl = n;
905: return;
906: }
907: if (w == 0)
908: return;
909: /* f belongs strictly inside the existing list */
910: for (sc=*paargl; (w=compaf(CO,BDY(sc),f))==1; sc=NEXT(sc))
911: prev = sc;
912: if (w == 0)
913: return;
914: MKNODE(n,f,sc);
915: NEXT(prev) = n;
916: }
917:
918: void simpl_gand_insert_c(f,pcargl,pcc)
919: F f;
920: NODE *pcargl,*pcc;
921: {
922: NODE sc;
923:
924: for (sc=*pcargl; sc; sc=NEXT(sc))
925: if (synequalf(f,(F)BDY(sc)))
926: return;
927: NEXTNODE(*pcargl,*pcc);
928: BDY(*pcc) = (pointer)f;
929: }
930:
931: int compaf(vl,f1,f2)
932: VL vl;
933: F f1,f2;
934: {
935: int w;
936:
937: w = compp(vl,FPL(f1),FPL(f2));
938: if (w)
939: return w;
940: return comprel(FOP(f1),FOP(f2));
941: }
942:
943: int comprel(op1,op2)
944: oFOP op1,op2;
945: /* implement order: =, <>, <=, <, >=, > */
946: {
947: if (op1 == op2)
948: return 0;
949: switch (op1) {
950: case AL_EQUAL:
951: return 1;
952: case AL_NEQ:
953: switch (op2) {
954: case AL_EQUAL:
955: return -1;
956: default:
957: return 1;
958: }
959: case AL_LEQ:
960: switch (op2) {
961: case AL_EQUAL:
962: return -1;
963: case AL_NEQ:
964: return -1;
965: default:
966: return 1;
967: }
968: case AL_LESSP:
969: switch (op2) {
970: case AL_GEQ:
971: return 1;
972: case AL_GREATERP:
973: return 1;
974: default:
975: return -1;
976: }
977: case AL_GEQ:
978: switch (op2) {
979: case AL_GREATERP:
980: return 1;
981: default:
982: return -1;
983: }
984: case AL_GREATERP:
985: return -1;
986: }
987: error("unknown relation in comprel");
988: }
989:
990: int synequalf(f1,f2)
991: F f1,f2;
992: {
993: oFOP op=FOP(f1);
994:
995: if (op != FOP(f2))
996: return 0;
997: if (AL_ATOMIC(op))
998: return (compp(CO,FPL(f1),FPL(f2)) == 0);
999: if (AL_JUNCT(op)) {
1000: NODE sc1,sc2;
1001: for (sc1=FJARG(f1),sc2=FJARG(f2); sc1 && sc2; sc1=NEXT(sc1),sc2=NEXT(sc2))
1002: if (! synequalf(BDY(sc1),BDY(sc2)))
1003: return 0;
1004: if (sc1 || sc2)
1005: return 0;
1006: return 1;
1007: }
1008: }
1009:
1010: void simpl_impl(op,prem,concl,th,n,pf)
1011: oFOP op;
1012: F prem,concl,*pf;
1013: NODE th;
1014: int n;
1015: {
1016: F h,hh;
1017:
1018: simpl1(prem,th,n+1,&h);
1019: if (FOP(h) == AL_FALSE) {
1020: *pf = F_TRUE;
1021: return;
1022: }
1023: simpl1(concl,th,n+1,&hh);
1024: if (FOP(hh) == AL_TRUE) {
1025: *pf = F_TRUE;
1026: return;
1027: }
1028: if (FOP(h) == AL_TRUE) {
1029: *pf = hh;
1030: return;
1031: }
1032: if (FOP(hh) == AL_FALSE) {
1033: pnegate(h,pf);
1034: return;
1035: }
1036: if (op == AL_IMPL) {
1037: MKBF(*pf,AL_IMPL,h,hh);
1038: return;
1039: }
1040: MKBF(*pf,AL_REPL,hh,h);
1041: }
1042:
1043: void simpl_equiv(lhs,rhs,th,n,pf)
1044: F lhs,rhs,*pf;
1045: NODE th;
1046: int n;
1047: {
1048: F h,hh;
1049:
1050: simpl1(lhs,th,n+1,&h);
1051: simpl1(rhs,th,n+1,&hh);
1052: if (FOP(h) == AL_TRUE) {
1053: *pf = hh;
1054: return;
1055: }
1056: if (FOP(hh) == AL_TRUE) {
1057: *pf = h;
1058: return;
1059: }
1060: if (FOP(h) == AL_FALSE) {
1061: pnegate(hh,pf);
1062: return;
1063: }
1064: if (FOP(hh) == AL_FALSE) {
1065: pnegate(h,pf);
1066: return;
1067: }
1068: MKBF(*pf,AL_EQUIV,h,hh);
1069: }
1070:
1071: void simpl_a(f,pnf)
1072: F f,*pnf;
1073: {
1074: oFOP r=FOP(f);
1075: P lhs=(P)FPL(f);
1076:
1077: if (NUMBER(lhs)) {
1078: #if 0
1079: lhs = (Q)lhs; /* good luck with the next compiler */
1080: #endif
1081: switch (r) {
1082: case AL_EQUAL:
1083: *pnf = (lhs == 0) ? F_TRUE : F_FALSE;
1084: return;
1085: case AL_NEQ:
1086: *pnf = (lhs != 0) ? F_TRUE : F_FALSE;
1087: return;
1088: case AL_LESSP:
1089: *pnf = (cmpq((Q)lhs,0) == -1) ? F_TRUE : F_FALSE;
1090: return;
1091: case AL_GREATERP:
1092: *pnf = (cmpq((Q)lhs,0) == 1) ? F_TRUE : F_FALSE;
1093: return;
1094: case AL_LEQ:
1095: *pnf = (cmpq((Q)lhs,0) != 1) ? F_TRUE : F_FALSE;
1096: return;
1097: case AL_GEQ:
1098: *pnf = (cmpq((Q)lhs,0) != -1) ? F_TRUE : F_FALSE;
1099: return;
1100: default:
1101: error("unknown operator in simpl_a");
1102: }
1103: }
1104: if (AL_ORDER(r))
1105: simpl_a_o(&r,&lhs);
1106: else
1107: simpl_a_no(&lhs);
1108: MKAF(*pnf,r,lhs);
1109: }
1110:
1111: void simpl_a_o(ar,alhs)
1112: oFOP *ar;
1113: P *alhs;
1114: {
1115: DCP dec;
1116:
1117: sqfrp(CO,*alhs,&dec);
1118: if (sgnq((Q)COEF(dec)) == -1)
1119: *ar = AL_ANEGREL(*ar);
1120: *alhs=(P)ONE;
1121: for (dec = NEXT(dec); dec; dec = NEXT(dec)) {
1122: mulp(CO,*alhs,COEF(dec),alhs);
1123: if (evenz(DEG(dec)))
1124: mulp(CO,*alhs,COEF(dec),alhs);
1125: }
1126: }
1127:
1128: void simpl_a_no(alhs)
1129: P *alhs;
1130: {
1131: DCP dec;
1132:
1133: sqfrp(CO,*alhs,&dec);
1134: *alhs=(P)ONE;
1135: for (dec = NEXT(dec); dec; dec = NEXT(dec))
1136: mulp(CO,*alhs,COEF(dec),alhs);
1137: }
1138:
1139: /* QE */
1140:
1141: #define BTMIN 0
1142: #define BTEQUAL 0
1143: #define BTWO 1
1144: #define BTLEQ 2
1145: #define BTGEQ 3
1146: #define BTSO 4
1147: #define BTLESSP 5
1148: #define BTGREATERP 6
1149: #define BTNEQ 7
1150: #define BTMAX 7
1151:
1152: #define IPURE 0
1153: #define IPE 1
1154: #define IME 2
1155: #define II 3
1156:
1157: void qe(f,pnf)
1158: F f,*pnf;
1159: {
1160: NODE bl,sc;
1161: F h;
1162:
1163: simpl(f,(NODE)NULL,&h);
1164: nnf(h,&h);
1165: blocksplit(h,&bl,&h);
1166: for (sc=bl; sc; sc=NEXT(sc)) {
1167: if (QUANT(((QVL)BDY(sc))) == AL_EX)
1168: qeblock(VARL(((QVL)BDY(sc))),h,&h);
1169: else {
1170: pnegate(h,&h);
1171: qeblock(VARL(((QVL)BDY(sc))),h,&h);
1172: pnegate(h,&h);
1173: }
1174: }
1175: *pnf = h;
1176: }
1177:
1178: void blocksplit(f,pbl,pmat)
1179: F f,*pmat;
1180: NODE *pbl;
1181: {
1182: oFOP cq;
1183: NODE bl=NULL,blh;
1184: VL vl,vlh;
1185: QVL qvl;
1186:
1187: while (AL_QUANT(cq=FOP(f))) {
1188: NEWNODE(blh);
1189: vl = NULL;
1190: while (FOP(f) == cq) {
1191: NEWVL(vlh);
1192: VR(vlh) = FQVR(f);
1193: NEXT(vlh) = vl;
1194: vl = vlh;
1195: f = FQMAT(f);
1196: }
1197: MKQVL(qvl,cq,vl);
1198: BDY(blh) = (pointer)qvl;
1199: NEXT(blh) = bl;
1200: bl = blh;
1201: }
1202: *pbl = bl;
1203: *pmat = f;
1204: }
1205:
1206: void qeblock(vl,f,pnf)
1207: VL vl;
1208: F f,*pnf;
1209: {
1210: CONT co;
1211: CEL cel;
1212: VL cvl;
1213: NODE n,sc;
1214: NODE nargl=NULL,narglc;
1215: int w,pr;
1216: int left=0,modulus;
1217:
1218: qeblock_verbose0(vl);
1219: simpl(f,(NODE)NULL,&f);
1220: MKCONT(co);
1221: MKCEL(cel,vl,f);
1222: coadd(co,cel);
1223: while (coget(co,&cel)) {
1224: cvl = VRL(cel);
1225: pr = qeblock_verbose1a(co,cvl,&left,&modulus);
1226: w = qevar(MAT(cel),&cvl,&n);
1227: qeblock_verbose1b(w,pr);
1228: for (sc=n; sc; sc=NEXT(sc))
1229: if ((F)BDY(sc) != F_FALSE)
1230: if (cvl) {
1231: MKCEL(cel,cvl,(F)BDY(sc));
1232: if (!comember(co,cel))
1233: coadd(co,cel);
1234: } else {
1235: NEXTNODE(nargl,narglc);
1236: BDY(narglc) = BDY(sc);
1237: }
1238: }
1239: qeblock_verbose2();
1240: smkjf(pnf,AL_OR,nargl);
1241: simpl(*pnf,(NODE)NULL,pnf);
1242: }
1243:
1244: void qeblock_verbose0(vl)
1245: VL vl;
1246: {
1247: if (!Verbose)
1248: return;
1249: printf("eliminating");
1250: for (; vl; vl=NEXT(vl))
1251: printf(" %s",NAME(VR(vl)));
1252: }
1253:
1254: int qeblock_verbose1a(co,cvl,pleft,pmodulus)
1255: CONT co;
1256: VL cvl;
1257: int *pleft,*pmodulus;
1258: {
1259: int i=0;
1260:
1261: if (!Verbose)
1262: /* added by noro */
1263: return 0;
1264: if (*pleft == 0) {
1265: for (; cvl; cvl=NEXT(cvl))
1266: i++;
1267: printf("\nleft %d\n",i);
1268: *pleft = colen(co) + 1;
1269: *pmodulus = getmodulus(*pleft);
1270: printf("(%d",(*pleft)--);
1271: fflush(asir_out);
1272: return 1;
1273: } else if (*pleft % *pmodulus == 0) {
1274: printf("(%d",(*pleft)--);
1275: fflush(asir_out);
1276: return 1;
1277: }
1278: (*pleft)--;
1279: return 0;
1280: }
1281:
1282: void qeblock_verbose1b(g,print)
1283: int g,print;
1284: {
1285: if (!(Verbose && print))
1286: return;
1287: printf("%s) ",g ? (g==2) ? "qg" : "lg" : "e");
1288: fflush(asir_out);
1289: }
1290:
1291: void qeblock_verbose2()
1292: {
1293: if (!Verbose)
1294: return;
1295: printf("\n");
1296: }
1297:
1298: int getmodulus(n)
1299: int n;
1300: {
1301: int pow=1;
1302:
1303: while (n >= pow*100) {
1304: pow *= 10;
1305: }
1306: return pow;
1307: }
1308:
1309:
1310: int qevar(f,pcvl,pfl)
1311: F f;
1312: VL *pcvl;
1313: NODE *pfl;
1314: {
1315: int w;
1316: V x;
1317: F h;
1318: NODE trans[8],eset,sc,r=NULL,rc;
1319:
1320: w = gausselim(f,pcvl,&x,&eset);
1321: if (!w) {
1322: x = VR(*pcvl);
1323: *pcvl = NEXT(*pcvl);
1324: translate(f,x,trans);
1325: mkeset(trans,x,&eset);
1326: }
1327: for (sc=eset; sc; sc=NEXT(sc)) {
1328: NEXTNODE(r,rc);
1329: subgpf(f,x,BDY(sc),&h);
1330: simpl(h,(NODE)NULL,&BDY(rc));
1331: }
1332: *pfl = r;
1333: return w;
1334: }
1335:
1336: int gausselim(f,pvl,px,peset)
1337: F f;
1338: VL *pvl;
1339: V *px;
1340: NODE *peset;
1341: {
1342: Z deg,two;
1343: P rlhs,a,b,c;
1344: V v;
1345: VL scvl;
1346: NODE sc;
1347: int w;
1348:
1349: if (FOP(f) != AL_AND)
1350: return 0;
1.2 ! noro 1351: STOZ(2,two);
1.1 noro 1352: for (deg=ONE; cmpz(two,deg) >= 0; addz(deg,ONE,°))
1353: for (scvl=*pvl; scvl; scvl=NEXT(scvl)) {
1354: v = VR(scvl);
1355: for (sc=FJARG(f); sc; sc=NEXT(sc)) {
1356: if (FOP((F)BDY(sc)) != AL_EQUAL)
1357: continue;
1358: al_reorder(FPL((F)BDY(sc)),v,&rlhs);
1359: if (VR(rlhs) != v)
1360: continue;
1361: w = gauss_abc(rlhs,v,deg,&a,&b,&c);
1362: if (!w)
1363: continue;
1364: *px = v;
1365: delv(v,*pvl,pvl);
1366: if (a) {
1367: gauss_mkeset2(rlhs,a,b,c,peset);
1368: return 2;
1369: }
1370: gauss_mkeset1(rlhs,b,peset);
1371: return 1;
1372: }
1373: }
1374: return 0;
1375: }
1376:
1377: int gauss_abc(rlhs,v,deg,pa,pb,pc)
1378: P rlhs,*pa,*pb,*pc;
1379: V v;
1380: Z deg;
1381: {
1382: Z two;
1383: DCP rld;
1384:
1385: rld = DC(rlhs);
1386: if (cmpz(DEG(rld),deg) != 0)
1387: return 0;
1.2 ! noro 1388: STOZ(2,two);
1.1 noro 1389: if (cmpz(deg,two) == 0) {
1390: *pa = COEF(rld);
1391: rld = NEXT(rld);
1392: } else
1393: *pa = 0;
1394: if (rld && cmpz(DEG(rld),ONE) == 0) {
1395: *pb = COEF(rld);
1396: rld = NEXT(rld);
1397: } else
1398: *pb = 0;
1399: if (rld)
1400: *pc = COEF(rld);
1401: else
1402: *pc = 0;
1403: return (NZNUMBER(*pa) || NZNUMBER(*pb) || NZNUMBER(*pc));
1404: }
1405:
1406: void gauss_mkeset1(rlhs,b,peset)
1407: P rlhs,b;
1408: NODE *peset;
1409: {
1410: GP hgp;
1411:
1412: mklgp(rlhs,b,STD,&hgp);
1413: MKNODE(*peset,hgp,NULL);
1414: }
1415:
1416: void gauss_mkeset2(rlhs,a,b,c,peset)
1417: P rlhs,a,b,c;
1418: NODE *peset;
1419: {
1420: GP hgp;
1421: NODE esetc=NULL;
1422:
1423: *peset = NULL;
1424: if (!NUM(a)) {
1425: NEXTNODE(*peset,esetc);
1426: mklgp(rlhs,b,STD,&hgp);
1427: BDY(esetc) = (pointer)hgp;
1428: }
1429: NEXTNODE(*peset,esetc);
1430: mkqgp(rlhs,a,b,c,1,STD,&hgp);
1431: BDY(esetc) = (pointer)hgp;
1432: NEXTNODE(*peset,esetc);
1433: mkqgp(rlhs,a,b,c,2,STD,&hgp);
1434: BDY(esetc) = (pointer)hgp;
1435: }
1436:
1437: int delv(v,vl,pnvl)
1438: V v;
1439: VL vl,*pnvl;
1440: {
1441: VL nvl=NULL,nvlc;
1442:
1443: if (v == VR(vl)) {
1444: *pnvl = NEXT(vl);
1445: return 1;
1446: }
1447: for (; vl && (VR(vl) != v); vl=NEXT(vl)) {
1448: NEXTVL(nvl,nvlc);
1449: VR(nvlc) = VR(vl);
1450: }
1451: if (vl) {
1452: NEXT(nvlc) = NEXT(vl);
1453: *pnvl = nvl;
1454: return 1;
1455: }
1456: *pnvl = nvl;
1457: return 0;
1458: }
1459:
1460: int translate(f,x,trans)
1461: F f;
1462: V x;
1463: NODE trans[];
1464: {
1465: NODE sc,transc[8];
1466: int bt,w=0;
1467:
1468: for (bt=BTMIN; bt<=BTMAX; bt++)
1469: trans[bt] = NULL;
1470: for (atl(f,&sc); sc; sc=NEXT(sc))
1471: w = (translate_a(BDY(sc),x,trans,transc) || w);
1472: return w;
1473: }
1474:
1475: int translate_a(at,v,trans,transc)
1476: F at;
1477: V v;
1478: NODE trans[],transc[];
1479: {
1480: P mp;
1481: Z two;
1482: int w;
1483:
1484: w = al_reorder(FPL(at),v,&mp);
1485: if (w == 0)
1486: return 0;
1487: if (cmpz(ONE,DEG(DC(mp))) == 0) {
1488: translate_a1(FOP(at),mp,trans,transc);
1489: return 1;
1490: };
1.2 ! noro 1491: STOZ(2,two);
1.1 noro 1492: if (cmpz(two,DEG(DC(mp))) == 0) {
1493: translate_a2(FOP(at),mp,trans,transc);
1494: return 1;
1495: };
1496: error("degree violation in translate_a");
1497: /* XXX : NOTREACHED */
1498: return -1;
1499: }
1500:
1501: void translate_a1(op,mp,trans,transc)
1502: oFOP op;
1503: P mp;
1504: NODE trans[],transc[];
1505: {
1506: P b;
1507: int itype,btype;
1508: GP hgp;
1509:
1510: b = COEF(DC(mp));
1511: indices(op,NUM(b) ? sgnq((Q)b) : 0,&itype,&btype);
1512: NEXTNODE(trans[btype],transc[btype]);
1513: mklgp(mp,b,itype,&hgp);
1514: BDY(transc[btype]) = (pointer)hgp;
1515: }
1516:
1517: void mklgp(mp,b,itype,pgp)
1518: P mp,b;
1519: int itype;
1520: GP *pgp;
1521: {
1522: RE hre;
1523: F hf;
1524:
1525: MKRE(hre,mp,(P)ONE,1,itype);
1526: MKAF(hf,AL_NEQ,b);
1527: MKGP(*pgp,hf,hre);
1528: }
1529:
1530: void translate_a2(op,mp,trans,transc)
1531: oFOP op;
1532: P mp;
1533: NODE trans[],transc[];
1534: {
1535: P a,b,c,linred;
1536: int itype,btype;
1537: GP hgp;
1538:
1539: getqcoeffs(mp,&a,&b,&c);
1540: if (!NUM(a) && b) {
1541: MKP(VR(mp),NEXT(DC(mp)),linred);
1542: translate_a1(op,linred,trans,transc);
1543: }
1544: indices(op,0,&itype,&btype);
1545: NEXTNODE(trans[btype],transc[btype]);
1546: mkqgp(mp,a,b,c,-1,itype,&hgp);
1547: BDY(transc[btype]) = (pointer)hgp;
1548: }
1549:
1550: void mkqgp(mp,a,b,c,rootno,itype,pgp)
1551: P mp,a,b,c;
1552: int rootno;
1553: int itype;
1554: GP *pgp;
1555: {
1556: P discr;
1557: RE hre;
1558: F hf;
1559: NODE n=NULL,nc=NULL;
1560:
1561: mkdiscr(a,b,c,&discr);
1562: MKRE(hre,mp,discr,rootno,itype);
1563: NEXTNODE(n,nc);
1564: MKAF(hf,AL_NEQ,a);
1565: BDY(nc) = (pointer)hf;
1566: NEXTNODE(n,nc);
1567: MKAF(hf,AL_GEQ,discr);
1568: BDY(nc) = (pointer)hf;
1569: MKJF(hf,AL_AND,n);
1570: MKGP(*pgp,hf,hre);
1571: }
1572:
1573: void getqcoeffs(mp,pa,pb,pc)
1574: P mp,*pa,*pb,*pc;
1575: {
1576: DCP hdcp;
1577:
1578: *pa = COEF(DC(mp));
1579: hdcp = NEXT(DC(mp));
1580: if (hdcp && cmpz(DEG(hdcp),ONE) == 0) {
1581: *pb = COEF(hdcp);
1582: hdcp = NEXT(hdcp);
1583: } else
1584: *pb = 0;
1585: if (hdcp && DEG(hdcp) == 0) {
1586: *pc = COEF(hdcp);
1587: } else
1588: *pc = 0;
1589: }
1590:
1591: void mkdiscr(a,b,c,pd)
1592: P a,b,c,*pd;
1593: {
1594: P h1,h2;
1595: Z four;
1596:
1597: mulp(CO,a,c,&h1);
1.2 ! noro 1598: STOZ(4,four);
1.1 noro 1599: mulp(CO,(P)four,h1,&h2);
1600: mulp(CO,b,b,&h1);
1601: subp(CO,h1,h2,pd);
1602: }
1603:
1604: int al_reorder(p,v,pnp)
1605: P p,*pnp;
1606: V v;
1607: {
1608: VL tvl;
1609:
1610: reordvar(CO,v,&tvl);
1611: reorderp(tvl,CO,p,pnp);
1612: if (*pnp && !NUM(*pnp) && strcmp(NAME(VR(*pnp)),NAME(v)) == 0)
1613: return 1;
1614: else
1615: return 0;
1616: }
1617:
1618: void indices(op,s,pit,pbt)
1619: oFOP op;
1620: int s,*pit,*pbt;
1621: {
1622: switch (op) {
1623: case AL_EQUAL:
1624: *pit = STD; *pbt = BTEQUAL; return;
1625: case AL_NEQ:
1626: *pit = EPS; *pbt = BTNEQ; return;
1627: case AL_LEQ:
1628: *pit = STD;
1629: switch (s) {
1630: case 1:
1631: *pbt = BTLEQ; return;
1632: case -1:
1633: *pbt = BTGEQ; return;
1634: case 0:
1635: *pbt = BTWO; return;
1636: }
1637: case AL_GEQ:
1638: *pit = STD;
1639: switch (s) {
1640: case 1:
1641: *pbt = BTGEQ; return;
1642: case -1:
1643: *pbt = BTLEQ; return;
1644: case 0:
1645: *pbt = BTWO; return;
1646: }
1647: case AL_LESSP:
1648: switch (s) {
1649: case 1:
1650: *pit = MEPS; *pbt = BTLESSP; return;
1651: case -1:
1652: *pit = PEPS; *pbt = BTGREATERP; return;
1653: case 0:
1654: *pit = EPS; *pbt = BTSO; return;
1655: }
1656: case AL_GREATERP:
1657: switch (s) {
1658: case 1:
1659: *pit = PEPS; *pbt = BTGREATERP; return;
1660: case -1:
1661: *pit = MEPS; *pbt = BTLESSP; return;
1662: case 0:
1663: *pit = EPS; *pbt = BTSO; return;
1664: }
1665: default:
1666: error("unknown relation or sign in indices");
1667: }
1668: }
1669:
1670: void mkeset(trans,x,peset)
1671: NODE trans[],*peset;
1672: V x;
1673: {
1674: NODE esetc=NULL;
1675: P h;
1676: RE hre;
1677: GP hgp;
1678: int cw,cs,deps,dinf,ord;
1679:
1680: *peset = NULL;
1681: ord = selectside(trans,&cw,&cs,&deps,&dinf);
1682: if (ord) {
1683: add2eset(trans[cw],peset,&esetc);
1684: add2eset(trans[BTWO],peset,&esetc);
1685: add2eset(trans[cs],peset,&esetc);
1686: sp_add2eset(trans[BTSO],deps,peset,&esetc);
1687: NEXTNODE(*peset,esetc);
1688: MKRE(hre,0,0,0,dinf);
1689: MKGP(hgp,F_TRUE,hre);
1690: BDY(esetc) = (pointer)hgp;
1691: } else {
1692: NEXTNODE(*peset,esetc);
1693: MKV(x,h);
1694: MKRE(hre,h,(P)ONE,1,STD);
1695: MKGP(hgp,F_TRUE,hre);
1696: BDY(esetc) = (pointer)hgp;
1697: }
1698: add2eset(trans[BTEQUAL],peset,&esetc);
1699: sp_add2eset(trans[BTNEQ],deps,peset,&esetc);
1700: }
1701:
1702: int selectside(trans,pcw,pcs,pdeps,pdinf)
1703: NODE trans[];
1704: int *pcw,*pcs,*pdeps,*pdinf;
1705: {
1706: if (cmp2n(trans[BTLEQ],trans[BTLESSP],trans[BTGEQ],trans[BTGREATERP])==1) {
1707: *pcw = BTGEQ;
1708: *pcs = BTGREATERP;
1709: *pdeps = PEPS;
1710: *pdinf = MINF;
1711: } else {
1712: *pcw = BTLEQ;
1713: *pcs = BTLESSP;
1714: *pdeps = MEPS;
1715: *pdinf = PINF;
1716: }
1717: if (!(trans[BTLEQ] || trans[BTLESSP] || trans[BTGEQ] ||
1718: trans[BTGREATERP] || trans[BTWO] || trans[BTSO]))
1719: return 0;
1720: return 1;
1721: }
1722:
1723: int cmp2n(n1a,n1b,n2a,n2b)
1724: NODE n1a,n1b,n2a,n2b;
1725: {
1726: NODE n1,n2;
1727: int n1bleft=1,n2bleft=1;
1728:
1729: n1 = n1a;
1730: n2 = n2a;
1731: while (n1 && n2) {
1732: n1 = NEXT(n1);
1733: if (n1 == NULL && n1bleft) {
1734: n1 = n1b;
1735: n1bleft = 0;
1736: }
1737: n2 = NEXT(n2);
1738: if (n2 == NULL && n2bleft) {
1739: n2 = n2b;
1740: n2bleft = 0;
1741: }
1742: }
1743: if (n1 || n2)
1744: return n1 ? 1 : -1;
1745: return 0;
1746: }
1747:
1748: void add2eset(trfield,peset,pesetc)
1749: NODE trfield,*peset,*pesetc;
1750: {
1751: NODE ntrfield,ntrfieldc;
1752:
1753: if (trfield == NULL)
1754: return;
1755: seproots(trfield,&ntrfield,&ntrfieldc);
1756: if (*peset == NULL) {
1757: *peset = ntrfield;
1758: *pesetc = ntrfieldc;
1759: } else {
1760: NEXT(*pesetc) = ntrfield;
1761: *pesetc = ntrfieldc;
1762: }
1763: }
1764:
1765: void seproots(trfield,pntrfield,pntrfieldc)
1766: NODE trfield,*pntrfield,*pntrfieldc;
1767: {
1768: NODE sc;
1769: NODE ntrf=NULL,ntrfc;
1770: RE hre,hre2;
1771: GP hgp,hgp2;
1772:
1773: for (sc=trfield; sc; sc=NEXT(sc)) {
1774: hgp = (GP)BDY(sc);
1775: hre = POINT(hgp);
1776: if (ROOTNO(hre) == -1) {
1777: NEXTNODE(ntrf,ntrfc);
1778: MKRE(hre2,hre->p,DISC(hre),1,ITYPE(hre));
1779: MKGP(hgp2,GUARD(hgp),hre2);
1780: BDY(ntrfc) = (pointer)hgp2;
1781: NEXTNODE(ntrf,ntrfc);
1782: ROOTNO(hre) = 2;
1783: BDY(ntrfc) = (pointer)hgp;
1784: } else {
1785: NEXTNODE(ntrf,ntrfc);
1786: BDY(ntrfc) = (pointer)hgp;
1787: }
1788: }
1789: *pntrfield = ntrf;
1790: *pntrfieldc = ntrfc;
1791: }
1792:
1793: void sp_add2eset(trfield,itype,peset,pesetc)
1794: NODE trfield,*peset,*pesetc;
1795: int itype;
1796: {
1797: NODE sc;
1798: GP hgp;
1799:
1800: for (sc=trfield; sc; sc=NEXT(sc)) {
1801: hgp = (GP)BDY(sc);
1802: ITYPE(POINT(hgp)) = itype;
1803: }
1804: add2eset(trfield,peset,pesetc);
1805: }
1806:
1807: void subgpf(f,v,gp,pnf)
1808: F f,*pnf;
1809: V v;
1810: GP gp;
1811: {
1812: NODE argl=NULL,arglc=NULL;
1813:
1814: NEXTNODE(argl,arglc);
1815: BDY(arglc) = (pointer)GUARD(gp);
1816: NEXTNODE(argl,arglc);
1817: subref(f,v,POINT(gp),&BDY(arglc));
1818: MKJF(*pnf,AL_AND,argl);
1819: }
1820:
1821: void subref(f,v,r,pnf)
1822: F f,*pnf;
1823: V v;
1824: RE r;
1825: {
1826: pointer argv[2];
1827:
1828: argv[0] = (pointer)v;
1829: argv[1] = (pointer)r;
1830: apply2ats(f,subref_a,argv,pnf);
1831: }
1832:
1833: void subref_a(at,argv,pnat)
1834: F at,*pnat;
1835: pointer argv[];
1836: {
1837: switch (ITYPE((RE)argv[1])) {
1838: case STD:
1839: substd_a(at,argv[0],argv[1],pnat);
1840: return;
1841: case EPS:
1842: error("unspecified RE in subref_a()");
1843: case PEPS:
1844: case MEPS:
1845: subpme_a(at,argv[0],argv[1],pnat);
1846: return;
1847: case PINF:
1848: case MINF:
1849: subinf_a(at,argv[0],argv[1],pnat);
1850: return;
1851: default:
1852: error("unknown itype in subref_a()");
1853: }
1854: }
1855:
1856: void substd_a(at,v,re,pnf)
1857: F at,*pnf;
1858: V v;
1859: RE re;
1860: {
1861: VL no;
1862: P rlhs,prem,nlhs;
1863: Z dd,dndeg;
1864:
1865: reordvar(CO,v,&no);
1866: reorderp(no,CO,FPL(at),&rlhs);
1867: if (!rlhs || NUM(rlhs) || VR(rlhs) != v) {
1868: *pnf = at;
1869: return;
1870: }
1871: premp(no,rlhs,re->p,&prem);
1872: if (prem && !NUM(prem) && VR(prem) == v) {
1873: /* quadratic case */
1874: substd_a2(FOP(at),prem,DEG(DC(rlhs)),re,pnf);
1875: return;
1876: }
1877: subz(DEG(DC(rlhs)),DEG(DC(re->p)),&dd);
1878: addz(dd,ONE,&dndeg);
1879: if (AL_ORDER(FOP(at)) && (!evenz(dndeg)))
1880: mulp(CO,prem,COEF(DC(re->p)),&nlhs);
1881: else
1882: nlhs = prem;
1883: MKAF(*pnf,FOP(at),nlhs);
1884: }
1885:
1886: void substd_a2(op,prem,fdeg,re,pf)
1887: oFOP op;
1888: F prem;
1889: Q fdeg;
1890: RE re;
1891: F *pf;
1892: {
1893: P a,b,c,ld;
1894:
1895: getrecoeffs(prem,fdeg,re,&a,&b,&c,&ld);
1896: if (ROOTNO(re) == 1)
1897: chsgnp(b,&b);
1898: else if (ROOTNO(re) != 2)
1899: error("unspecified quadratic root in substd_a2");
1900: substd_a21(op,a,b,c,ld,pf);
1901: }
1902:
1903: void substd_a21(op,a,b,c,d,pf)
1904: oFOP op;
1905: P a,b,c,d;
1906: F *pf;
1907: {
1908: switch (op) {
1909: case AL_EQUAL:
1910: substd_a21_equal(a,b,c,d,pf);
1911: return;
1912: case AL_NEQ:
1913: substd_a21_equal(a,b,c,d,pf);
1914: pnegate(*pf,pf);
1915: return;
1916: case AL_LEQ:
1917: substd_a21_leq(a,b,c,d,pf);
1918: return;
1919: case AL_LESSP:
1920: substd_a21_lessp(a,b,c,d,pf);
1921: return;
1922: case AL_GEQ:
1923: substd_a21_lessp(a,b,c,d,pf);
1924: pnegate(*pf,pf);
1925: return;
1926: case AL_GREATERP:
1927: substd_a21_leq(a,b,c,d,pf);
1928: pnegate(*pf,pf);
1929: return;
1930: default:
1931: error("unknown operator in substd_a21");
1932: }
1933: }
1934:
1935: void substd_a21_equal(a,b,c,d,pf)
1936: P a,b,c,d;
1937: F *pf;
1938: {
1939: F hf;
1940: NODE cj=NULL,cjc=NULL;
1941: P hp1,hp2;
1942:
1943: NEXTNODE(cj,cjc);
1944: mulp(CO,a,a,&hp1);
1945: mulp(CO,b,b,&hp2);
1946: mulp(CO,hp2,c,&hp2);
1947: subp(CO,hp1,hp2,&hp1);
1948: MKAF(hf,AL_EQUAL,hp1);
1949: BDY(cjc) = (pointer)hf;
1950: NEXTNODE(cj,cjc);
1951: mulp(CO,a,b,&hp1);
1952: MKAF(hf,AL_LEQ,hp1);
1953: BDY(cjc) = (pointer)hf;
1954: MKJF(*pf,AL_AND,cj);
1955: }
1956:
1957: void substd_a21_leq(a,b,c,d,pf)
1958: P a,b,c,d;
1959: F *pf;
1960: {
1961: F hf;
1962: NODE cj=NULL,cjc=NULL,dj=NULL,djc=NULL;
1963: P hp1,hp2;
1964:
1965: NEXTNODE(dj,djc);
1966: NEXTNODE(cj,cjc);
1967: mulp(CO,a,d,&hp1);
1968: MKAF(hf,AL_LEQ,hp1);
1969: BDY(cjc) = (pointer)hf;
1970: NEXTNODE(cj,cjc);
1971: mulp(CO,a,a,&hp1);
1972: mulp(CO,b,b,&hp2);
1973: mulp(CO,hp2,c,&hp2);
1974: subp(CO,hp1,hp2,&hp1);
1975: MKAF(hf,AL_GEQ,hp1);
1976: BDY(cjc) = (pointer)hf;
1977: MKJF(hf,AL_AND,cj);
1978: BDY(djc) = (pointer)hf;
1979: NEXTNODE(dj,djc);
1980: cj = NULL;
1981: NEXTNODE(cj,cjc);
1982: MKAF(hf,AL_LEQ,hp1);
1983: BDY(cjc) = (pointer)hf;
1984: NEXTNODE(cj,cjc);
1985: mulp(CO,b,d,&hp1);
1986: MKAF(hf,AL_LEQ,hp1);
1987: BDY(cjc) = (pointer)hf;
1988: MKJF(hf,AL_AND,cj);
1989: BDY(djc) = (pointer)hf;
1990: MKJF(*pf,AL_OR,dj);
1991: }
1992:
1993: void substd_a21_lessp(a,b,c,d,pf)
1994: P a,b,c,d;
1995: F *pf;
1996: {
1997: F hf,hf0;
1998: NODE cj=NULL,cjc=NULL,d1=NULL,d1c=NULL,d2=NULL,d2c=NULL;
1999: P hp1,hp2;
2000:
2001: NEXTNODE(d1,d1c);
2002: NEXTNODE(cj,cjc);
2003: mulp(CO,a,d,&hp1);
2004: MKAF(hf0,AL_LESSP,hp1);
2005: BDY(cjc) = (pointer)hf0;
2006: NEXTNODE(cj,cjc);
2007: mulp(CO,a,a,&hp1);
2008: mulp(CO,b,b,&hp2);
2009: mulp(CO,hp2,c,&hp2);
2010: subp(CO,hp1,hp2,&hp1);
2011: MKAF(hf,AL_GREATERP,hp1);
2012: BDY(cjc) = (pointer)hf;
2013: MKJF(hf,AL_AND,cj);
2014: BDY(d1c) = (pointer)hf;
2015: NEXTNODE(d1,d1c);
2016: cj = NULL;
2017: NEXTNODE(cj,cjc);
2018: NEXTNODE(d2,d2c);
2019: MKAF(hf,AL_LESSP,hp1);
2020: BDY(d2c) = (pointer)hf;
2021: NEXTNODE(d2,d2c);
2022: BDY(d2c) = (pointer)hf0;
2023: MKJF(hf,AL_OR,d2);
2024: BDY(cjc) = (pointer)hf;
2025: NEXTNODE(cj,cjc);
2026: mulp(CO,b,d,&hp1);
2027: MKAF(hf,AL_LEQ,hp1);
2028: BDY(cjc) = (pointer)hf;
2029: MKJF(hf,AL_AND,cj);
2030: BDY(d1c) = (pointer)hf;
2031: MKJF(*pf,AL_OR,d1);
2032: }
2033:
2034: void getrecoeffs(prem,fdeg,re,pa,pb,pc,pld)
2035: P prem,*pa,*pb,*pc,*pld;
2036: Z fdeg;
2037: RE re;
2038: {
2039: P a,b,c,alpha,beta,h1,h2;
2040: Z two;
2041:
2042: alpha = COEF(DC(prem));
2043: beta = (NEXT(DC(prem))) ? COEF(NEXT(DC(prem))) : 0;
2044: getqcoeffs(re->p,&a,&b,&c);
1.2 ! noro 2045: STOZ(2,two);
1.1 noro 2046: mulp(CO,(P)two,a,&h1);
2047: mulp(CO,h1,beta,&h2);
2048: mulp(CO,b,alpha,&h1);
2049: subp(CO,h2,h1,pa);
2050: *pb = alpha;
2051: *pc = DISC(re);
2052: *pld = (evenz(fdeg)) ? (P)ONE : a;
2053: }
2054:
2055: void subinf_a(f,v,re,pnf)
2056: F f,*pnf;
2057: V v;
2058: RE re;
2059: {
2060: if (AL_ORDER(FOP(f)))
2061: subinf_a_o(f,v,re,pnf);
2062: else
2063: subtrans_a_no(f,v,pnf);
2064: }
2065:
2066: void subinf_a_o(f,v,ire,pnf)
2067: F f,*pnf;
2068: V v;
2069: RE ire;
2070: {
2071: P rlhs;
2072:
2073: if (!al_reorder(FPL(f),v,&rlhs))
2074: *pnf = f;
2075: else
2076: subinf_a_o1(FOP(f),DC(rlhs),ire,pnf);
2077: }
2078:
2079: void subinf_a_o1(op,lhsdcp,ire,pnf)
2080: oFOP op;
2081: DCP lhsdcp;
2082: RE ire;
2083: F *pnf;
2084: {
2085: P an;
2086: F h;
2087: NODE c=NULL,cc=NULL,d=NULL,dc=NULL;
2088:
2089: if (lhsdcp == 0) {
2090: MKAF(*pnf,op,0);
2091: return;
2092: }
2093: if (DEG(lhsdcp) == 0) {
2094: MKAF(*pnf,op,COEF(lhsdcp));
2095: return;
2096: }
2097: if (ITYPE(ire) == MINF && !evenz(DEG(lhsdcp)))
2098: chsgnp(COEF(lhsdcp),&an);
2099: else
2100: an = COEF(lhsdcp);
2101: NEXTNODE(d,dc);
2102: MKAF(h,AL_MKSTRICT(op),an);
2103: BDY(dc) = (pointer)h;
2104: NEXTNODE(d,dc);
2105: NEXTNODE(c,cc);
2106: MKAF(h,AL_EQUAL,an);
2107: BDY(cc) = (pointer)h;
2108: NEXTNODE(c,cc);
2109: subinf_a_o1(op,NEXT(lhsdcp),ire,&h);
2110: BDY(cc) = (pointer)h;
2111: MKJF(h,AL_AND,c);
2112: BDY(dc) = (pointer)h;
2113: MKJF(*pnf,AL_OR,d);
2114: }
2115:
2116: void subtrans_a_no(f,v,pnf)
2117: F f,*pnf;
2118: V v;
2119: {
2120: P rlhs;
2121: DCP sc;
2122: F h;
2123: NODE nargl=NULL,narglc;
2124: oFOP op=FOP(f);
2125:
2126: if (!al_reorder(FPL(f),v,&rlhs)) {
2127: *pnf = f;
2128: return;
2129: }
2130: for (sc=DC(rlhs); sc; sc=NEXT(sc)) {
2131: NEXTNODE(nargl,narglc);
2132: MKAF(h,op,COEF(sc));
2133: BDY(narglc) = (pointer)h;
2134: }
2135: smkjf(pnf,AL_TRSUBEXP(op),nargl);
2136: }
2137:
2138: void subpme_a(af,v,re,pnf)
2139: F af,*pnf;
2140: V v;
2141: RE re;
2142: {
2143: if (AL_ORDER(FOP(af)))
2144: subpme_a_o(af,v,re,pnf);
2145: else
2146: subtrans_a_no(af,v,pnf);
2147: }
2148:
2149: void subpme_a_o(af,v,r,pnf)
2150: F af,*pnf;
2151: V v;
2152: RE r;
2153: {
2154: F h;
2155: RE stdre;
2156:
2157: subpme_a_o1(FOP(af),FPL(af),v,ITYPE(r)==MEPS,&h);
2158: MKRE(stdre,r->p,DISC(r),ROOTNO(r),STD);
2159: subref(h,v,stdre,pnf);
2160: }
2161:
2162: void subpme_a_o1(op,lhs,v,minus,pnf)
2163: oFOP op;
2164: P lhs;
2165: V v;
2166: int minus;
2167: F *pnf;
2168: {
2169: Z deg;
2170: F h;
2171: NODE c=NULL,cc=NULL,d=NULL,dc=NULL;
2172: P df;
2173:
2174: degp(v,lhs,°);
2175: if (deg == 0) {
2176: MKAF(*pnf,op,lhs);
2177: return;
2178: };
2179: NEXTNODE(d,dc);
2180: MKAF(h,AL_MKSTRICT(op),lhs);
2181: BDY(dc) = (pointer)h;
2182: NEXTNODE(d,dc);
2183: NEXTNODE(c,cc);
2184: MKAF(h,AL_EQUAL,lhs);
2185: BDY(cc) = (pointer)h;
2186: NEXTNODE(c,cc);
2187: diffp(CO,lhs,v,&df);
2188: if (minus)
2189: chsgnp(df,&df);
2190: subpme_a_o1(op,df,v,minus,&h);
2191: BDY(cc) = (pointer)h;
2192: MKJF(h,AL_AND,c);
2193: BDY(dc) = (pointer)h;
2194: MKJF(*pnf,AL_OR,d);
2195: }
2196:
2197: int comember(co,x)
2198: CONT co;
2199: CEL x;
2200: {
2201: NODE sc;
2202:
2203: for (sc=FIRST(co); sc; sc=NEXT(sc))
2204: if (synequalf(MAT(x),MAT((CEL)BDY(sc))))
2205: return 1;
2206: return 0;
2207: }
2208:
2209: void coadd(co,x)
2210: CONT co;
2211: CEL x;
2212: {
2213: NEXTNODE(FIRST(co),LAST(co));
2214: BDY(LAST(co)) = (pointer)x;
2215: }
2216:
2217: int coget(co,px)
2218: CONT co;
2219: CEL *px;
2220: {
2221: if (FIRST(co) == 0)
2222: return 0;
2223: *px = (CEL)BDY(FIRST(co));
2224: FIRST(co) = NEXT(FIRST(co));
2225: return 1;
2226: }
2227:
2228: int colen(co)
2229: CONT co;
2230: {
2231: NODE sc;
2232: int n=0;
2233:
2234: for (sc=FIRST(co); sc; sc=NEXT(sc))
2235: n++;
2236: return n;
2237: }
2238:
2239: /* Misc */
2240:
2241: void apply2ats(f,client,argv,pnf)
2242: F f,*pnf;
2243: void (*client)();
2244: pointer argv[];
2245: {
2246: if (AL_ATOMIC(FOP(f)))
2247: (*client)(f,argv,pnf);
2248: else if (AL_JUNCT(FOP(f))) {
2249: NODE sc,n=NULL,c;
2250: for (sc=FJARG(f); sc; sc=NEXT(sc)) {
2251: NEXTNODE(n,c);
2252: apply2ats(BDY(sc),client,argv,&BDY(c));
2253: }
2254: MKJF(*pnf,FOP(f),n);
2255: }
2256: else if (AL_TVAL(FOP(f)))
2257: *pnf = f;
2258: else if (AL_QUANT(FOP(f))) {
2259: F h;
2260: apply2ats(FQMAT(f),client,argv,&h);
2261: MKQF(*pnf,FOP(f),FQVR(f),h);
2262: } else
2263: error("unknown operator in apply2ats");
2264: }
2265:
2266: void atl(f,pn)
2267: F f;
2268: NODE *pn;
2269: {
2270: NODE c;
2271:
2272: *pn = NULL;
2273: atl1(f,pn,&c);
2274: }
2275:
2276: void atl1(f,pn,pc)
2277: F f;
2278: NODE *pn,*pc;
2279: {
2280: NODE sc;
2281:
2282: if (AL_ATOMIC(FOP(f))) {
2283: simpl_gand_insert_a(f,pn,pc);
2284: return;
2285: }
2286: if (AL_JUNCT(FOP(f)))
2287: for (sc=FJARG(f); sc; sc=NEXT(sc))
2288: atl1(BDY(sc),pn,pc);
2289: }
2290:
2291: void atnum(f,pn)
2292: F f;
2293: Q *pn;
2294: {
2295: *pn = 0;
2296: atnum1(f,pn);
2297: }
2298:
2299: void atnum1(f,pn)
2300: F f;
2301: Q *pn;
2302: {
2303: NODE sc;
2304:
2305: if (AL_ATOMIC(FOP(f)))
2306: addq(*pn,(Q)ONE,pn);
2307: else if (AL_JUNCT(FOP(f)))
2308: for (sc=FJARG(f); sc; sc=NEXT(sc))
2309: atnum1(BDY(sc),pn);
2310: }
2311:
2312: void pnegate(f,pnf)
2313: F f,*pnf;
2314: {
2315: F h;
2316: NODE sc,n=NULL,c;
2317: oFOP op=FOP(f);
2318:
2319: if (AL_QUANT(op)) {
2320: pnegate(FQMAT(f),&h);
2321: MKQF(*pnf,AL_LNEGOP(op),FQVR(f),h);
2322: return;
2323: }
2324: if (AL_JUNCT(op)) {
2325: for (sc=FJARG(f); sc; sc=NEXT(sc)) {
2326: NEXTNODE(n,c);
2327: pnegate((F)BDY(sc),(F*)&BDY(c));
2328: }
2329: MKJF(*pnf,AL_LNEGOP(op),n);
2330: return;
2331: }
2332: if (AL_ATOMIC(op)) {
2333: MKAF(*pnf,AL_LNEGOP(op),FPL(f));
2334: return;
2335: }
2336: if (op == AL_TRUE) {
2337: *pnf = F_FALSE;
2338: return;
2339: }
2340: if (op == AL_FALSE) {
2341: *pnf = F_TRUE;
2342: return;
2343: }
2344: error("unknown operator in pnegate()");
2345: }
2346:
2347: void subf(o,f,v,p,pf)
2348: VL o;
2349: F f,*pf;
2350: V v;
2351: P p;
2352: {
2353: pointer argv[3];
2354:
2355: argv[0] = (pointer)o;
2356: argv[1] = (pointer)v;
2357: argv[2] = (pointer)p;
2358: apply2ats(f,subf_a,argv,pf);
2359: }
2360:
2361: void subf_a(at,argv,pat)
2362: F at,*pat;
2363: pointer argv[];
2364: {
2365: P nlhs;
2366:
2367: substp((VL)argv[0],FPL(at),(V)argv[1],(P)argv[2],&nlhs);
2368: MKAF(*pat,FOP(at),nlhs);
2369: }
2370:
2371: void nnf(f,pf)
2372: F f,*pf;
2373: {
2374: nnf1(f,0,0,pf);
2375: }
2376:
2377: void nnf1(f,neg,disj,pf)
2378: F f,*pf;
2379: int neg,disj;
2380: {
2381: F h;
2382: NODE sc,nargl=NULL,narglc=NULL;
2383: oFOP op=FOP(f);
2384:
2385: if (AL_ATOMIC(op) || AL_TVAL(op)) {
2386: if (neg)
2387: pnegate(f,pf);
2388: else
2389: *pf = f;
2390: return;
2391: }
2392: if (AL_JUNCT(op)) {
2393: if (neg)
2394: op = AL_LNEGOP(op);
2395: for (sc=FJARG(f); sc; sc=NEXT(sc)) {
2396: NEXTNODE(nargl,narglc);
2397: nnf1((F)BDY(sc),neg,op==AL_OR,(F*)&BDY(narglc));
2398: }
2399: MKJF(*pf,op,nargl);
2400: return;
2401: }
2402: if (op == AL_IMPL) {
2403: op = neg ? AL_AND : AL_OR;
2404: NEXTNODE(nargl,narglc);
2405: nnf1(FLHS(f),!neg,op==AL_OR,(F*)&BDY(narglc));
2406: NEXTNODE(nargl,narglc);
2407: nnf1(FRHS(f),neg,op==AL_OR,(F*)&BDY(narglc));
2408: MKJF(*pf,op,nargl);
2409: return;
2410: }
2411: if (op == AL_REPL) {
2412: op = neg ? AL_AND : AL_OR;
2413: NEXTNODE(nargl,narglc);
2414: nnf1(FLHS(f),neg,op==AL_OR,(F*)&BDY(narglc));
2415: NEXTNODE(nargl,narglc);
2416: nnf1(FRHS(f),!neg,op==AL_OR,(F*)&BDY(narglc));
2417: MKJF(*pf,op,nargl);
2418: return;
2419: }
2420: if (op == AL_EQUIV) {
2421: /* should consider disj and its arguments ops */
2422: NEXTNODE(nargl,narglc);
2423: MKBF(h,AL_IMPL,FLHS(f),FRHS(f));
2424: BDY(narglc) = (pointer)h;
2425: NEXTNODE(nargl,narglc);
2426: MKBF(h,AL_REPL,FLHS(f),FRHS(f));
2427: BDY(narglc) = (pointer)h;
2428: MKJF(h,AL_AND,nargl);
2429: nnf1(h,neg,disj,pf);
2430: return;
2431: }
2432: if (AL_QUANT(op)) {
2433: nnf1(FQMAT(f),neg,0,&h);
2434: MKQF(*pf,neg ? AL_LNEGOP(op) : op,FQVR(f),h);
2435: return;
2436: }
2437: if (op == AL_NOT) {
2438: nnf1(FARG(f),!neg,disj,pf);
2439: return;
2440: }
2441: error("unknown operator in nnf1()");
2442: }
2443:
2444: void freevars(f,pvl)
2445: F f;
2446: VL *pvl;
2447: {
2448: *pvl = NULL;
2449: freevars1(f,pvl,NULL);
2450: }
2451:
2452: void freevars1(f,pvl,cbvl)
2453: F f;
2454: VL *pvl,cbvl;
2455: {
2456: VL hvl;
2457: NODE sc;
2458: oFOP op=FOP(f);
2459:
2460: if (AL_ATOMIC(op)) {
2461: freevars1_a(f,pvl,cbvl);
2462: return;
2463: }
2464: if (AL_JUNCT(op)) {
2465: for (sc=FJARG(f); sc; sc=NEXT(sc))
2466: freevars1((F)BDY(sc),pvl,cbvl);
2467: return;
2468: }
2469: if (AL_QUANT(op)) {
2470: MKVL(hvl,FQVR(f),cbvl);
2471: freevars1(FQMAT(f),pvl,hvl);
2472: return;
2473: }
2474: if (AL_UNI(op)) {
2475: freevars1(FARG(f),pvl,cbvl);
2476: return;
2477: }
2478: if (AL_EXT(op)) {
2479: freevars1(FLHS(f),pvl,cbvl);
2480: freevars1(FRHS(f),pvl,cbvl);
2481: return;
2482: }
2483: if (AL_TVAL(op))
2484: return;
2485: error("unknown operator in freevars1()");
2486: }
2487:
2488: void freevars1_a(f,pvl,cbvl)
2489: F f;
2490: VL *pvl,cbvl;
2491: {
2492: VL sc,sc2,last;
2493:
2494: for (get_vars((Obj)FPL(f),&sc); sc; sc=NEXT(sc)) {
2495: for(sc2=cbvl; sc2; sc2=NEXT(sc2))
2496: if (VR(sc) == VR(sc2))
2497: break;
2498: if (sc2)
2499: continue;
2500: if (!*pvl) {
2501: MKVL(*pvl,VR(sc),NULL);
2502: continue;
2503: }
2504: for (sc2=*pvl; sc2; sc2=NEXT(sc2)) {
2505: if (VR(sc) == VR(sc2))
2506: break;
2507: last = sc2;
2508: }
2509: if (sc2)
2510: continue;
2511: MKVL(NEXT(last),VR(sc),NULL);
2512: }
2513: }
2514:
2515: int compf(vl,f1,f2)
2516: VL vl;
2517: F f1,f2;
2518: {
2519: if (AL_ATOMIC(FOP(f1)) && AL_ATOMIC(FOP(f2)))
2520: return compaf(vl,f1,f2);
2521: if (AL_ATOMIC(FOP(f1)))
2522: return 1;
2523: if (AL_ATOMIC(FOP(f2)))
2524: return -1;
2525: if (synequalf(f1,f2))
2526: return 0;
2527: return 2;
2528: }
2529:
2530: /* Debug */
2531:
2532: void ap(x)
2533: pointer *x;
2534: {
2535: printexpr(CO,(Obj)x);
2536: printf("\n");
2537: }
2538:
2539: void rep(re)
2540: RE re;
2541: {
2542: printf("(");
2543: printexpr(CO,(Obj)re->p);
2544: printf(",");
2545: printexpr(CO,(Obj)DISC(re));
2546: printf(",");
2547: printf("%d)\n",re->itype);
2548: }
2549:
2550: void gpp(gp)
2551: GP gp;
2552: {
2553: ap(gp->g);
2554: rep(gp->p);
2555: }
2556:
2557: void esetp(eset)
2558: NODE eset;
2559: {
2560: NODE sc;
2561:
2562: for (sc=eset; sc; sc=NEXT(sc))
2563: gpp(BDY(sc));
2564: }
2565:
2566: void nodep(n)
2567: NODE n;
2568: {
2569: NODE sc;
2570:
2571: for (sc=n; sc; sc=NEXT(sc))
2572: ap(BDY(sc));
2573: }
2574:
2575: void lbfp(x)
2576: LBF x;
2577: {
2578: printf("(%d,",LBFLB(x));
2579: printexpr(CO,(Obj)LBFF(x));
2580: printf(")");
2581: }
2582:
2583: void thp(x)
2584: NODE x;
2585: {
2586: if (x == NULL) {
2587: printf("[]\n");
2588: return;
2589: }
2590: printf("[");
2591: lbfp((LBF)BDY(x));
2592: x = NEXT(x);
2593: for (; x != NULL; x = NEXT(x)) {
2594: printf(",");
2595: lbfp((LBF)BDY(x));
2596: }
2597: printf("]\n");
2598: }