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