[BACK]Return to al.c CVS log [TXT][DIR] Up to [local] / OpenXM_contrib2 / asir2000 / builtin

Diff for /OpenXM_contrib2/asir2000/builtin/al.c between version 1.1 and 1.6

version 1.1, 1999/12/03 07:39:07 version 1.6, 2018/03/29 01:32:50
Line 1 
Line 1 
 /* $OpenXM: OpenXM/src/asir99/builtin/al.c,v 1.2 1999/11/18 05:42:01 noro Exp $ */  /* $OpenXM: OpenXM_contrib2/asir2000/builtin/al.c,v 1.5 2001/10/09 01:36:04 noro Exp $ */
 /* ----------------------------------------------------------------------  /* ----------------------------------------------------------------------
    $Id$     $Id$
    ----------------------------------------------------------------------     ----------------------------------------------------------------------
    File al.c: Real quantifier elimination code for RISA/ASIR     File al.c: Real quantifier elimination code for RISA/ASIR
   
    Copyright (c) 1996, 1997, 1998 by     Copyright (c) 1996-2001 by
    Andreas Dolzmann and Thomas Sturm, University of Passau, Germany     Andreas Dolzmann and Thomas Sturm, University of Passau, Germany
    dolzmann@uni-passau.de, sturm@uni-passau.de     dolzmann@uni-passau.de, sturm@uni-passau.de
    ----------------------------------------------------------------------     ----------------------------------------------------------------------
Line 14 
Line 14 
 #include <parse.h>  #include <parse.h>
 #include <al.h>  #include <al.h>
   
   void Preverse();
 void Phugo();  void Phugo();
 void Pex();  void Pex();
 void Pall();  void Pall();
Line 23  void Pfargs();
Line 24  void Pfargs();
 void Pfopargs();  void Pfopargs();
 void Pcompf();  void Pcompf();
 void Patnum();  void Patnum();
   int gauss_abc();
 int compf();  int compf();
 void Patl();  void Patl();
 void Pqevar();  void Pqevar();
Line 38  void simpl_th2atl();
Line 40  void simpl_th2atl();
 int simpl_gand_udnargls();  int simpl_gand_udnargls();
 int simpl_gand_thupd();  int simpl_gand_thupd();
 int simpl_gand_thprsism();  int simpl_gand_thprsism();
   int simpl_gand_smtbdlhs();
   int simpl_gand_smtbelhs();
 void lbc();  void lbc();
 void replaceq();  void replaceq();
 void deleteq();  void deleteq();
Line 61  void qeblock_verbose0();
Line 65  void qeblock_verbose0();
 int getmodulus();  int getmodulus();
 int qevar();  int qevar();
 int gausselim();  int gausselim();
   int delv();
 int translate();  int translate();
 int translate_a();  int translate_a();
 void translate_a1();  void translate_a1();
Line 70  void mkqgp();
Line 75  void mkqgp();
 void getqcoeffs();  void getqcoeffs();
 void mkdiscr();  void mkdiscr();
 int al_reorder();  int al_reorder();
 int indices();  void indices();
 void mkeset();  void mkeset();
 int selectside();  int selectside();
 int cmp2n();  int cmp2n();
 void add2eset();  void add2eset();
   void seproots();
 void sp_add2eset();  void sp_add2eset();
 void subgpf();  void subgpf();
 void subref();  void subref();
Line 116  void rep();
Line 122  void rep();
 void gpp();  void gpp();
 void esetp();  void esetp();
 void nodep();  void nodep();
   void gauss_mkeset1();
   void gauss_mkeset2();
   
 extern Verbose;  extern Verbose;
   
 struct oRE {  struct oRE {
         P p;    P p;
         P discr;    P discr;
         int itype;          int rootno;
     int itype;
 };  };
   
 typedef struct oRE *RE;  typedef struct oRE *RE;
   
 struct oGP {  struct oGP {
         F g;    F g;
         RE p;    RE p;
 };  };
   
 typedef struct oGP *GP;  typedef struct oGP *GP;
   
 struct oCEL {  struct oCEL {
         VL vl;    VL vl;
         F mat;    F mat;
 };  };
   
 typedef struct oCEL *CEL;  typedef struct oCEL *CEL;
   
 struct oCONT {  struct oCONT {
         NODE first;    NODE first;
         NODE last;    NODE last;
 };  };
   
 typedef struct oCONT *CONT;  typedef struct oCONT *CONT;
   
 struct oQVL {  struct oQVL {
         oFOP q;    oFOP q;
         VL vl;    VL vl;
 };  };
   
 typedef struct oQVL *QVL;  typedef struct oQVL *QVL;
Line 161  typedef struct oQVL *QVL;
Line 170  typedef struct oQVL *QVL;
 #define MKGP(x,g,p) (NEWGP(x),GUARD(x)=g,POINT(x)=p)  #define MKGP(x,g,p) (NEWGP(x),GUARD(x)=g,POINT(x)=p)
   
 #define NEWRE(x) ((x)=(RE)MALLOC(sizeof(struct oRE)))  #define NEWRE(x) ((x)=(RE)MALLOC(sizeof(struct oRE)))
 #define MKRE(x,pp,d,i) \  #define MKRE(x,pp,d,rn,i) \
 (NEWRE(x),(x)->p=pp,(x)->discr=d,(x)->itype=i)  (NEWRE(x),(x)->p=pp,(x)->discr=d,(x)->rootno=rn,(x)->itype=i)
 #define DISC(re) ((re)->discr)  #define DISC(re) ((re)->discr)
   #define ROOTNO(re) ((re)->rootno)
 #define ITYPE(re) ((re)->itype)  #define ITYPE(re) ((re)->itype)
   
 #define STD 0  #define STD 0
Line 195  if(!(r)){NEWVL(r);(c)=(r);}else{NEWVL(NEXT(c));(c)=NEX
Line 205  if(!(r)){NEWVL(r);(c)=(r);}else{NEWVL(NEXT(c));(c)=NEX
 #define MKCONT(x) ((x)=(CONT)MALLOC(sizeof(struct oCONT)),FIRST(x)=LAST(x)=NULL)  #define MKCONT(x) ((x)=(CONT)MALLOC(sizeof(struct oCONT)),FIRST(x)=LAST(x)=NULL)
   
 struct ftab al_tab[] = {  struct ftab al_tab[] = {
         {"simpl",Psimpl,-2},    {"simpl",Psimpl,-2},
         {"ex",Pex,-2},    {"ex",Pex,-2},
         {"all",Pall,-2},    {"all",Pall,-2},
         {"fop",Pfop,1},    {"fop",Pfop,1},
         {"fargs",Pfargs,1},    {"fargs",Pfargs,1},
         {"fopargs",Pfopargs,1},    {"fopargs",Pfopargs,1},
         {"compf",Pcompf,2},    {"compf",Pcompf,2},
         {"atl",Patl,1},    {"atl",Patl,1},
         {"qevar",Pqevar,2},    {"qevar",Pqevar,2},
         {"qe",Pqe,1},    {"qe",Pqe,1},
         {"atnum",Patnum,1},    {"atnum",Patnum,1},
         {"subf",Psubf,3},    {"subf",Psubf,3},
         {"nnf",Pnnf,1},    {"nnf",Pnnf,1},
         {"hugo",Phugo,4},    {"hugo",Phugo,4},
         {0,0,0}    {0,0,0}
 };  };
   
 void Phugo(arg,rp)  void Phugo(arg,rp)
 NODE arg;  NODE arg;
 F *rp;  F *rp;
 {  {
         substd_a21_equal(BDY(arg),BDY(NEXT(arg)),BDY(NEXT(NEXT(arg))),BDY(NEXT(NEXT(NEXT(arg)))),rp);    substd_a21_equal(BDY(arg),BDY(NEXT(arg)),BDY(NEXT(NEXT(arg))),BDY(NEXT(NEXT(NEXT(arg)))),rp);
         ap(*rp);    ap(*rp);
         substd_a21_leq(BDY(arg),BDY(NEXT(arg)),BDY(NEXT(NEXT(arg))),BDY(NEXT(NEXT(NEXT(arg)))),rp);    substd_a21_leq(BDY(arg),BDY(NEXT(arg)),BDY(NEXT(NEXT(arg))),BDY(NEXT(NEXT(NEXT(arg)))),rp);
         ap(*rp);    ap(*rp);
         substd_a21_lessp(BDY(arg),BDY(NEXT(arg)),BDY(NEXT(NEXT(arg))),BDY(NEXT(NEXT(NEXT(arg)))),rp);    substd_a21_lessp(BDY(arg),BDY(NEXT(arg)),BDY(NEXT(NEXT(arg))),BDY(NEXT(NEXT(NEXT(arg)))),rp);
         ap(*rp);    ap(*rp);
 }  }
   
 void Pex(arg,rp)  void Pex(arg,rp)
 NODE arg;  NODE arg;
 F *rp;  F *rp;
 {  {
         if (argc(arg) == 1)    if (argc(arg) == 1)
                 constrq(AL_EX,0,(F)BDY(arg),rp);      constrq(AL_EX,0,(F)BDY(arg),rp);
         else    else
                 constrq(AL_EX,BDY(arg),(F)BDY(NEXT(arg)),rp);      constrq(AL_EX,BDY(arg),(F)BDY(NEXT(arg)),rp);
 }  }
   
 void Pall(arg,rp)  void Pall(arg,rp)
 NODE arg;  NODE arg;
 F *rp;  F *rp;
 {  {
         if (argc(arg) == 1)    if (argc(arg) == 1)
                 constrq(AL_ALL,0,(F)BDY(arg),rp);      constrq(AL_ALL,0,(F)BDY(arg),rp);
         else    else
                 constrq(AL_ALL,BDY(arg),(F)BDY(NEXT(arg)),rp);      constrq(AL_ALL,BDY(arg),(F)BDY(NEXT(arg)),rp);
 }  }
   
 void constrq(q,vars,m,rp)  void constrq(q,vars,m,rp)
Line 249  oFOP q;
Line 259  oFOP q;
 Obj vars;  Obj vars;
 F m,*rp;  F m,*rp;
 {  {
         VL sc;    VL sc;
         NODE varl=NULL,varlc,arg;    NODE varl=NULL,varlc,arg;
         P p;    P p;
   
         if (!vars) {    if (!vars) {
                 for (freevars(m,&sc); sc; sc=NEXT(sc)) {      for (freevars(m,&sc); sc; sc=NEXT(sc)) {
                         NEXTNODE(varl,varlc);        NEXTNODE(varl,varlc);
                         MKV(VR(sc),p);        MKV(VR(sc),p);
                         BDY(varlc) = (pointer)p;        BDY(varlc) = (pointer)p;
                 }      }
         } else if (OID(vars) == O_LIST) {    } else if (OID(vars) == O_LIST) {
                 MKNODE(arg,vars,NULL);      MKNODE(arg,vars,NULL);
                 Preverse(arg,&vars);      Preverse(arg,&vars);
                 varl = BDY((LIST)vars);      varl = BDY((LIST)vars);
         } else    } else
                 MKNODE(varl,vars,NULL);      MKNODE(varl,vars,NULL);
         for (; varl; varl=NEXT(varl)) {    for (; varl; varl=NEXT(varl)) {
                 MKQF(*rp,q,VR((P)BDY(varl)),m);      MKQF(*rp,q,VR((P)BDY(varl)),m);
                 m = *rp;      m = *rp;
         }    }
 }  }
   
 void Pfop(arg,rp)  void Pfop(arg,rp)
 NODE arg;  NODE arg;
 Q *rp;  Q *rp;
 {  {
         oFOP op;    oFOP op;
   
         op = FOP((F)ARG0(arg));    op = FOP((F)ARG0(arg));
         STOQ((int)op,*rp);    STOQ((int)op,*rp);
 }  }
   
 void Pfargs(arg,rp)  void Pfargs(arg,rp)
 NODE arg;  NODE arg;
 LIST *rp;  LIST *rp;
 {  {
         oFOP op;    oFOP op;
         LIST l;    LIST l;
         NODE n1,n2;    NODE n1,n2;
         F f;    F f;
         P x;    P x;
   
         f = (F)ARG0(arg);    f = (F)ARG0(arg);
         op = FOP(f);    op = FOP(f);
         if ( AL_TVAL(op) )    if ( AL_TVAL(op) )
                 n1 = 0;      n1 = 0;
         else if ( AL_JUNCT(op) )    else if ( AL_JUNCT(op) )
                 n1 = FJARG(f);      n1 = FJARG(f);
         else if ( AL_QUANT(op) ) {    else if ( AL_QUANT(op) ) {
                 MKV(FQVR(f),x);      MKV(FQVR(f),x);
                 MKNODE(n2,FQMAT(f),0); MKNODE(n1,x,n2);      MKNODE(n2,FQMAT(f),0); MKNODE(n1,x,n2);
         } else if (AL_ATOMIC(op) )    } else if (AL_ATOMIC(op) )
                 MKNODE(n1,FPL(f),0);      MKNODE(n1,FPL(f),0);
         else if ( AL_UNI(op) )    else if ( AL_UNI(op) )
                 MKNODE(n1,FARG(f),0);      MKNODE(n1,FARG(f),0);
         else if ( AL_EXT(op) ) {    else if ( AL_EXT(op) ) {
                 MKNODE(n2,FRHS(f),0); MKNODE(n1,FLHS(f),n2);      MKNODE(n2,FRHS(f),0); MKNODE(n1,FLHS(f),n2);
         }    }
         MKLIST(l,n1);    MKLIST(l,n1);
         *rp = l;    *rp = l;
 }  }
   
 void Pfopargs(arg,rp)  void Pfopargs(arg,rp)
 NODE arg;  NODE arg;
 LIST *rp;  LIST *rp;
 {  {
         oFOP op;    oFOP op;
         LIST l;    LIST l;
         NODE n0,n1,n2;    NODE n0,n1,n2;
         F f;    F f;
         P x;    P x;
         Q op1;    Q op1;
   
         f = (F)ARG0(arg);    f = (F)ARG0(arg);
         op = FOP(f);    op = FOP(f);
         STOQ((int)op,op1);    STOQ((int)op,op1);
         if ( AL_TVAL(op) )    if ( AL_TVAL(op) )
                 n1 = 0;      n1 = 0;
         else if ( AL_JUNCT(op) )    else if ( AL_JUNCT(op) )
                 n1 = FJARG(f);      n1 = FJARG(f);
         else if ( AL_QUANT(op) ) {    else if ( AL_QUANT(op) ) {
                 MKV(FQVR(f),x);      MKV(FQVR(f),x);
                 MKNODE(n2,FQMAT(f),0); MKNODE(n1,x,n2);      MKNODE(n2,FQMAT(f),0); MKNODE(n1,x,n2);
         } else if (AL_ATOMIC(op) )    } else if (AL_ATOMIC(op) )
                 MKNODE(n1,FPL(f),0);      MKNODE(n1,FPL(f),0);
         else if ( AL_UNI(op) )    else if ( AL_UNI(op) )
                 MKNODE(n1,FARG(f),0);      MKNODE(n1,FARG(f),0);
         else if ( AL_EXT(op) ) {    else if ( AL_EXT(op) ) {
                 MKNODE(n2,FRHS(f),0); MKNODE(n1,FLHS(f),n2);      MKNODE(n2,FRHS(f),0); MKNODE(n1,FLHS(f),n2);
         }    }
         MKNODE(n0,op1,n1);    MKNODE(n0,op1,n1);
         MKLIST(l,n0);    MKLIST(l,n0);
         *rp = l;    *rp = l;
 }  }
   
 void Pcompf(arg,rp)  void Pcompf(arg,rp)
 NODE arg;  NODE arg;
 Q *rp;  Q *rp;
 {  {
         STOQ(compf(CO,BDY(arg),BDY(NEXT(arg))),*rp);    STOQ(compf(CO,BDY(arg),BDY(NEXT(arg))),*rp);
 }  }
   
 void Patnum(arg,rp)  void Patnum(arg,rp)
 NODE arg;  NODE arg;
 Q *rp;  Q *rp;
 {  {
         atnum(BDY(arg),rp);    atnum(BDY(arg),rp);
 }  }
   
 void Patl(arg,rp)  void Patl(arg,rp)
 NODE arg;  NODE arg;
 LIST *rp;  LIST *rp;
 {  {
         NODE h;    NODE h;
   
         atl(BDY(arg),&h);    atl(BDY(arg),&h);
         MKLIST(*rp,h);    MKLIST(*rp,h);
 }  }
   
 void Pqevar(arg,rp)  void Pqevar(arg,rp)
 NODE arg;  NODE arg;
 F *rp;  F *rp;
 {  {
         qevar(BDY(arg),VR((P)BDY(NEXT(arg))),rp);    qevar(BDY(arg),VR((P)BDY(NEXT(arg))),rp);
 }  }
   
 void Pqe(arg,rp)  void Pqe(arg,rp)
 NODE arg;  NODE arg;
 F *rp;  F *rp;
 {  {
         qe(BDY(arg),rp);    qe(BDY(arg),rp);
 }  }
   
 void Psubf(arg,rp)  void Psubf(arg,rp)
 NODE arg;  NODE arg;
 F *rp;  F *rp;
 {  {
         subf(CO,(F)BDY(arg),VR((P)BDY(NEXT(arg))),(P)BDY(NEXT(NEXT(arg))),rp);    subf(CO,(F)BDY(arg),VR((P)BDY(NEXT(arg))),(P)BDY(NEXT(NEXT(arg))),rp);
 }  }
   
 void Pnnf(arg,rp)  void Pnnf(arg,rp)
 NODE arg;  NODE arg;
 F *rp;  F *rp;
 {  {
         nnf((F)BDY(arg),rp);    nnf((F)BDY(arg),rp);
 }  }
   
 /* Simplification */  /* Simplification */
Line 424  F *pf;
Line 434  F *pf;
 oFOP j;  oFOP j;
 NODE argl;  NODE argl;
 {  {
         if (!argl)    if (!argl)
                 MKTV(*pf,AL_NEUTRAL(j));      MKTV(*pf,AL_NEUTRAL(j));
         else if (!NEXT(argl))    else if (!NEXT(argl))
                 *pf = (F)BDY(argl);      *pf = (F)BDY(argl);
         else    else
                 MKJF(*pf,j,argl);      MKJF(*pf,j,argl);
 }  }
   
 void simpl(f,th,pnf)  void simpl(f,th,pnf)
Line 444  F f,*pnf;
Line 454  F f,*pnf;
 NODE th;  NODE th;
 int n;  int n;
 {  {
         F h,hh;    F h;
         oFOP op=FOP(f);    oFOP op=FOP(f);
   
         if (AL_ATOMIC(op)) {    if (AL_ATOMIC(op)) {
                 simpl_a(f,pnf);      simpl_a(f,pnf);
                 return;      return;
         }    }
         if (AL_JUNCT(op)) {    if (AL_JUNCT(op)) {
                 simpl_gand(op,AL_NEUTRAL(op),AL_OMNIPOT(op),FJARG(f),th,n,pnf);      simpl_gand(op,AL_NEUTRAL(op),AL_OMNIPOT(op),FJARG(f),th,n,pnf);
                 return;      return;
         }    }
         if (AL_TVAL(op)) {    if (AL_TVAL(op)) {
                 *pnf = f;      *pnf = f;
                 return;      return;
         }    }
         if (AL_QUANT(op)) {    if (AL_QUANT(op)) {
                 simpl1(FQMAT(f),(NODE)NULL,n+1,&h);      simpl1(FQMAT(f),(NODE)NULL,n+1,&h);
                 MKQF(*pnf,op,FQVR(f),h);      MKQF(*pnf,op,FQVR(f),h);
                 return;      return;
         }    }
         if (op == AL_NOT) {    if (op == AL_NOT) {
                 simpl1(FARG(f),th,n+1,&h);      simpl1(FARG(f),th,n+1,&h);
                 switch (FOP(h)) {      switch (FOP(h)) {
                 case AL_TRUE:      case AL_TRUE:
                         *pnf = F_FALSE;        *pnf = F_FALSE;
                         break;        break;
                 case AL_FALSE:      case AL_FALSE:
                         *pnf = F_TRUE;        *pnf = F_TRUE;
                         break;        break;
                 default:      default:
                         MKUF(*pnf,AL_NOT,h);        MKUF(*pnf,AL_NOT,h);
                 }      }
                 return;      return;
         }    }
         if (op == AL_IMPL) {    if (op == AL_IMPL) {
                 simpl_impl(AL_IMPL,FLHS(f),FRHS(f),th,n,pnf);      simpl_impl(AL_IMPL,FLHS(f),FRHS(f),th,n,pnf);
                 return;      return;
         }    }
         if (op == AL_REPL) {    if (op == AL_REPL) {
                 simpl_impl(AL_REPL,FRHS(f),FLHS(f),th,n,pnf);      simpl_impl(AL_REPL,FRHS(f),FLHS(f),th,n,pnf);
                 return;      return;
         }    }
         if (op == AL_EQUIV) {    if (op == AL_EQUIV) {
                 simpl_equiv(FLHS(f),FRHS(f),th,n,pnf);      simpl_equiv(FLHS(f),FRHS(f),th,n,pnf);
                 return;      return;
         }    }
         else    else
           error("unknown operator in simpl1");      error("unknown operator in simpl1");
 }  }
   
 void simpl_gand(gand,gtrue,gfalse,argl,oth,n,pnf)  void simpl_gand(gand,gtrue,gfalse,argl,oth,n,pnf)
Line 505  F *pnf;
Line 515  F *pnf;
   int st;    int st;
   
   for (; oth; oth = NEXT(oth)) {    for (; oth; oth = NEXT(oth)) {
          NEXTNODE(th,thc);     NEXTNODE(th,thc);
          BDY(thc) = BDY(oth);     BDY(thc) = BDY(oth);
   }    }
   for (; argl; argl = NEXT(argl)) {    for (; argl; argl = NEXT(argl)) {
     if (FOP((F)BDY(argl)) == gfalse) {      if (FOP((F)BDY(argl)) == gfalse) {
                 *pnf = (F)BDY(argl);      *pnf = (F)BDY(argl);
       return;        return;
          }     }
     if (AL_ATOMIC(FOP((F)BDY(argl)))) {      if (AL_ATOMIC(FOP((F)BDY(argl)))) {
       simpl_a((F)BDY(argl),&h);        simpl_a((F)BDY(argl),&h);
       if (FOP(h) == gfalse) {        if (FOP(h) == gfalse) {
                   *pnf = h;        *pnf = h;
                   return;        return;
                 }      }
       st = simpl_gand_udnargls(gand,gtrue,h,n,&th,&thc,&cnargl,&cc);        st = simpl_gand_udnargls(gand,gtrue,h,n,&th,&thc,&cnargl,&cc);
       if (st == GINCONSISTENT) {        if (st == GINCONSISTENT) {
                   MKTV(fgfalse,gfalse);        MKTV(fgfalse,gfalse);
                   *pnf = fgfalse;        *pnf = fgfalse;
                   return;        return;
                 }      }
     } else      } else
                 simpl_gand_insert_c((F)BDY(argl),&cnargl,&cc);      simpl_gand_insert_c((F)BDY(argl),&cnargl,&cc);
   }    }
   for (; cnargl != NULL; cnargl = NEXT(cnargl)) {    for (; cnargl != NULL; cnargl = NEXT(cnargl)) {
     simpl1((F)BDY(cnargl),th,n+1,&h);      simpl1((F)BDY(cnargl),th,n+1,&h);
     if (FOP(h) == gfalse) {      if (FOP(h) == gfalse) {
                 *pnf = h;      *pnf = h;
       return;        return;
          }     }
     st = simpl_gand_udnargls(gand,gtrue,h,n,&th,&thc,&cnargl2,&cc2);      st = simpl_gand_udnargls(gand,gtrue,h,n,&th,&thc,&cnargl2,&cc2);
     switch (st) {      switch (st) {
     case GINCONSISTENT:      case GINCONSISTENT:
                 MKTV(fgfalse,gfalse);      MKTV(fgfalse,gfalse);
                 *pnf = fgfalse;      *pnf = fgfalse;
                 return;      return;
     case NEWAT:      case NEWAT:
       if (cnargl2 != NULL) {        if (cnargl2 != NULL) {
                   if (cnargl != NULL)        if (cnargl != NULL)
                          NEXT(cc) = cnargl2;         NEXT(cc) = cnargl2;
                   else        else
                          cnargl = cnargl2;         cnargl = cnargl2;
                   cc = cc2;        cc = cc2;
                   cnargl2 = cc2 = NULL;        cnargl2 = cc2 = NULL;
                 }      }
       break;        break;
     }      }
   }    }
   simpl_th2atl(gand,th,n,&nargl,&narglc);    simpl_th2atl(gand,th,n,&nargl,&narglc);
   if (nargl == NULL)    if (nargl == NULL)
          nargl = cnargl2;     nargl = cnargl2;
   else    else
          NEXT(narglc) = cnargl2;     NEXT(narglc) = cnargl2;
   smkjf(pnf,gand,nargl);    smkjf(pnf,gand,nargl);
 }  }
   
Line 566  NODE th,*patl,*patlc;
Line 576  NODE th,*patl,*patlc;
 int n;  int n;
 {  {
   NODE atl=NULL,atlc=NULL;    NODE atl=NULL,atlc=NULL;
   LBF h;  
   F at,negat;    F at,negat;
   
   switch (gand) {    switch (gand) {
   case AL_AND:    case AL_AND:
          for (; th; th = NEXT(th)) {     for (; th; th = NEXT(th)) {
                 if (LBFLB((LBF)BDY(th)) == n) {      if (LBFLB((LBF)BDY(th)) == n) {
                   NEXTNODE(atl,atlc);        NEXTNODE(atl,atlc);
                   BDY(atlc) = (pointer)LBFF((LBF)BDY(th));        BDY(atlc) = (pointer)LBFF((LBF)BDY(th));
                 }      }
          }     }
          break;     break;
   case AL_OR:    case AL_OR:
          for (; th; th = NEXT(th)) {     for (; th; th = NEXT(th)) {
                 if (LBFLB((LBF)BDY(th)) == n) {      if (LBFLB((LBF)BDY(th)) == n) {
                   at = LBFF((LBF)BDY(th));        at = LBFF((LBF)BDY(th));
                   MKAF(negat,AL_LNEGOP(FOP(at)),FPL(at));        MKAF(negat,AL_LNEGOP(FOP(at)),FPL(at));
                   NEXTNODE(atl,atlc);        NEXTNODE(atl,atlc);
                   BDY(atlc) = (pointer)negat;        BDY(atlc) = (pointer)negat;
                 }      }
          }     }
          break;     break;
   }    }
   *patl = atl;    *patl = atl;
   *patlc = atlc;    *patlc = atlc;
Line 611  NODE *pth,*pthc,*pcnargl,*pcc;
Line 620  NODE *pth,*pthc,*pcnargl,*pcc;
     return(simpl_gand_thupd(gand,narg,n,pth,pthc));      return(simpl_gand_thupd(gand,narg,n,pth,pthc));
   if (op == gand) {    if (op == gand) {
     sargl = FJARG(narg);      sargl = FJARG(narg);
          for (; sargl; sargl = NEXT(sargl)) {     for (; sargl; sargl = NEXT(sargl)) {
                 h = (F)BDY(sargl);      h = (F)BDY(sargl);
       if (AL_ATOMIC(FOP(h))) {        if (AL_ATOMIC(FOP(h))) {
                   st = simpl_gand_thupd(gand,h,n,pth,pthc);        st = simpl_gand_thupd(gand,h,n,pth,pthc);
                   switch (st) {        switch (st) {
                   case NEWAT:        case NEWAT:
                          found = NEWAT;         found = NEWAT;
                          break;         break;
                   case GINCONSISTENT:        case GINCONSISTENT:
                          return(GINCONSISTENT);         return(GINCONSISTENT);
                   }        }
       } else        } else
                   simpl_gand_insert_c(h,pcnargl,pcc);        simpl_gand_insert_c(h,pcnargl,pcc);
     }      }
     return(found);      return(found);
   }    }
Line 849  pointer old,new;
Line 858  pointer old,new;
 {  {
   *pnl = NULL;    *pnl = NULL;
   for (; l; l = NEXT(l)) {    for (; l; l = NEXT(l)) {
          NEXTNODE(*pnl,*pnlc);     NEXTNODE(*pnl,*pnlc);
          if(BDY(l) == old)     if(BDY(l) == old)
                 BDY(*pnlc) = new;      BDY(*pnlc) = new;
          else     else
                 BDY(*pnlc) = BDY(l);      BDY(*pnlc) = BDY(l);
   }    }
 }  }
   
Line 863  pointer obj;
Line 872  pointer obj;
 {  {
   *pnl = NULL;    *pnl = NULL;
   for (; l; l = NEXT(l))    for (; l; l = NEXT(l))
          if(BDY(l) != obj) {     if(BDY(l) != obj) {
                 NEXTNODE(*pnl,*pnlc);      NEXTNODE(*pnl,*pnlc);
                 BDY(*pnlc) = BDY(l);      BDY(*pnlc) = BDY(l);
          }     }
 }  }
   
 void simpl_gand_insert_a(f,paargl,pac)  void simpl_gand_insert_a(f,paargl,pac)
 F f;  F f;
 NODE *paargl,*pac;  NODE *paargl,*pac;
 {  {
         int w;    int w;
         NODE n,sc,prev;    NODE n,sc,prev;
   
         if (*paargl == 0) {    if (*paargl == 0) {
                 NEXTNODE(*paargl,*pac);      NEXTNODE(*paargl,*pac);
                 BDY(*pac) = (pointer)f;      BDY(*pac) = (pointer)f;
                 return;      return;
         }    }
         w = compaf(CO,BDY(*pac),f);    w = compaf(CO,BDY(*pac),f);
         if (w == 1) {    if (w == 1) {
                 NEXTNODE(*paargl,*pac);      NEXTNODE(*paargl,*pac);
                 BDY(*pac) = (pointer)f;      BDY(*pac) = (pointer)f;
                 return;      return;
         }    }
         if (w == 0)    if (w == 0)
                 return;      return;
         w = compaf(CO,f,BDY(*paargl));    w = compaf(CO,f,BDY(*paargl));
         if (w == 1) {    if (w == 1) {
                 MKNODE(n,f,*paargl);      MKNODE(n,f,*paargl);
                 *paargl = n;      *paargl = n;
                 return;      return;
         }    }
         if (w == 0)    if (w == 0)
                 return;      return;
         /* f belongs strictly inside the existing list */    /* f belongs strictly inside the existing list */
         for (sc=*paargl; (w=compaf(CO,BDY(sc),f))==1; sc=NEXT(sc))    for (sc=*paargl; (w=compaf(CO,BDY(sc),f))==1; sc=NEXT(sc))
                 prev = sc;      prev = sc;
         if (w == 0)    if (w == 0)
                 return;      return;
         MKNODE(n,f,sc);    MKNODE(n,f,sc);
         NEXT(prev) = n;    NEXT(prev) = n;
 }  }
   
 void simpl_gand_insert_c(f,pcargl,pcc)  void simpl_gand_insert_c(f,pcargl,pcc)
 F f;  F f;
 NODE *pcargl,*pcc;  NODE *pcargl,*pcc;
 {  {
         NODE sc;    NODE sc;
   
         for (sc=*pcargl; sc; sc=NEXT(sc))    for (sc=*pcargl; sc; sc=NEXT(sc))
                 if (synequalf(f,(F)BDY(sc)))      if (synequalf(f,(F)BDY(sc)))
                         return;        return;
         NEXTNODE(*pcargl,*pcc);    NEXTNODE(*pcargl,*pcc);
         BDY(*pcc) = (pointer)f;    BDY(*pcc) = (pointer)f;
 }  }
   
 int compaf(vl,f1,f2)  int compaf(vl,f1,f2)
 VL vl;  VL vl;
 F f1,f2;  F f1,f2;
 {  {
         int w;    int w;
   
         w = compp(vl,FPL(f1),FPL(f2));    w = compp(vl,FPL(f1),FPL(f2));
         if (w)    if (w)
                 return w;      return w;
         return comprel(FOP(f1),FOP(f2));    return comprel(FOP(f1),FOP(f2));
 }  }
   
 int comprel(op1,op2)  int comprel(op1,op2)
 oFOP op1,op2;  oFOP op1,op2;
 /* implement order: =, <>, <=, <, >=, > */  /* implement order: =, <>, <=, <, >=, > */
 {  {
         if (op1 == op2)    if (op1 == op2)
                 return 0;      return 0;
         switch (op1) {    switch (op1) {
         case AL_EQUAL:    case AL_EQUAL:
                 return 1;      return 1;
         case AL_NEQ:    case AL_NEQ:
                 switch (op2) {      switch (op2) {
                 case AL_EQUAL:      case AL_EQUAL:
                         return -1;        return -1;
                 default:      default:
                         return 1;        return 1;
                 }      }
         case AL_LEQ:    case AL_LEQ:
                 switch (op2) {      switch (op2) {
                 case AL_EQUAL:      case AL_EQUAL:
                         return -1;        return -1;
                 case AL_NEQ:      case AL_NEQ:
                         return -1;        return -1;
                 default:      default:
                         return 1;        return 1;
                 }      }
         case AL_LESSP:    case AL_LESSP:
                 switch (op2) {      switch (op2) {
                 case AL_GEQ:      case AL_GEQ:
                         return 1;        return 1;
                 case AL_GREATERP:      case AL_GREATERP:
                         return 1;        return 1;
                 default:      default:
                         return -1;        return -1;
                 }      }
         case AL_GEQ:    case AL_GEQ:
                 switch (op2) {      switch (op2) {
                 case AL_GREATERP:      case AL_GREATERP:
                         return 1;        return 1;
                 default:      default:
                         return -1;        return -1;
                 }      }
         case AL_GREATERP:    case AL_GREATERP:
                 return -1;      return -1;
         }    }
         error("unknown relation in comprel");    error("unknown relation in comprel");
 }  }
   
 int synequalf(f1,f2)  int synequalf(f1,f2)
 F f1,f2;  F f1,f2;
 {  {
         oFOP op=FOP(f1);    oFOP op=FOP(f1);
   
         if (op != FOP(f2))    if (op != FOP(f2))
                 return 0;      return 0;
         if (AL_ATOMIC(op))    if (AL_ATOMIC(op))
                 return (compp(CO,FPL(f1),FPL(f2)) == 0);      return (compp(CO,FPL(f1),FPL(f2)) == 0);
         if (AL_JUNCT(op)) {    if (AL_JUNCT(op)) {
                 NODE sc1,sc2;      NODE sc1,sc2;
                 for (sc1=FJARG(f1),sc2=FJARG(f2); sc1 && sc2; sc1=NEXT(sc1),sc2=NEXT(sc2))      for (sc1=FJARG(f1),sc2=FJARG(f2); sc1 && sc2; sc1=NEXT(sc1),sc2=NEXT(sc2))
                         if (! synequalf(BDY(sc1),BDY(sc2)))        if (! synequalf(BDY(sc1),BDY(sc2)))
                                 return 0;          return 0;
                 if (sc1 || sc2)      if (sc1 || sc2)
                         return 0;        return 0;
                 return 1;      return 1;
         }    }
 }  }
   
 void simpl_impl(op,prem,concl,th,n,pf)  void simpl_impl(op,prem,concl,th,n,pf)
Line 1004  F prem,concl,*pf;
Line 1013  F prem,concl,*pf;
 NODE th;  NODE th;
 int n;  int n;
 {  {
         F h,hh;    F h,hh;
   
         simpl1(prem,th,n+1,&h);    simpl1(prem,th,n+1,&h);
         if (FOP(h) == AL_FALSE) {    if (FOP(h) == AL_FALSE) {
                 *pf = F_TRUE;      *pf = F_TRUE;
                 return;      return;
         }    }
         simpl1(concl,th,n+1,&hh);    simpl1(concl,th,n+1,&hh);
         if (FOP(hh) == AL_TRUE) {    if (FOP(hh) == AL_TRUE) {
                 *pf = F_TRUE;      *pf = F_TRUE;
                 return;      return;
         }    }
         if (FOP(h) == AL_TRUE) {    if (FOP(h) == AL_TRUE) {
                 *pf = hh;      *pf = hh;
                 return;      return;
         }    }
         if (FOP(hh) == AL_FALSE) {    if (FOP(hh) == AL_FALSE) {
                 pnegate(h,pf);      pnegate(h,pf);
                 return;      return;
         }    }
         if (op == AL_IMPL) {    if (op == AL_IMPL) {
                 MKBF(*pf,AL_IMPL,h,hh);      MKBF(*pf,AL_IMPL,h,hh);
                 return;      return;
         }    }
         MKBF(*pf,AL_REPL,hh,h);    MKBF(*pf,AL_REPL,hh,h);
 }  }
   
 void simpl_equiv(lhs,rhs,th,n,pf)  void simpl_equiv(lhs,rhs,th,n,pf)
Line 1036  F lhs,rhs,*pf;
Line 1045  F lhs,rhs,*pf;
 NODE th;  NODE th;
 int n;  int n;
 {  {
         F h,hh;    F h,hh;
   
         simpl1(lhs,th,n+1,&h);    simpl1(lhs,th,n+1,&h);
         simpl1(rhs,th,n+1,&hh);    simpl1(rhs,th,n+1,&hh);
         if (FOP(h) == AL_TRUE) {    if (FOP(h) == AL_TRUE) {
                 *pf = hh;      *pf = hh;
                 return;      return;
         }    }
         if (FOP(hh) == AL_TRUE) {    if (FOP(hh) == AL_TRUE) {
                 *pf = h;      *pf = h;
                 return;      return;
         }    }
         if (FOP(h) == AL_FALSE) {    if (FOP(h) == AL_FALSE) {
                 pnegate(hh,pf);      pnegate(hh,pf);
                 return;      return;
         }    }
         if (FOP(hh) == AL_FALSE) {    if (FOP(hh) == AL_FALSE) {
                 pnegate(h,pf);      pnegate(h,pf);
                 return;      return;
         }    }
         MKBF(*pf,AL_EQUIV,h,hh);    MKBF(*pf,AL_EQUIV,h,hh);
 }  }
   
 void simpl_a(f,pnf)  void simpl_a(f,pnf)
 F f,*pnf;  F f,*pnf;
 {  {
         oFOP r=FOP(f);    oFOP r=FOP(f);
         P lhs=(P)FPL(f);    P lhs=(P)FPL(f);
   
         if (NUMBER(lhs)) {    if (NUMBER(lhs)) {
 #if 0  #if 0
            lhs = (Q)lhs; /* good luck with the next compiler */       lhs = (Q)lhs; /* good luck with the next compiler */
 #endif  #endif
                 switch (r) {      switch (r) {
                 case AL_EQUAL:      case AL_EQUAL:
                         *pnf = (lhs == 0) ? F_TRUE : F_FALSE;        *pnf = (lhs == 0) ? F_TRUE : F_FALSE;
                         return;        return;
                 case AL_NEQ:      case AL_NEQ:
                         *pnf = (lhs != 0) ? F_TRUE : F_FALSE;        *pnf = (lhs != 0) ? F_TRUE : F_FALSE;
                         return;        return;
                 case AL_LESSP:      case AL_LESSP:
                         *pnf = (cmpq((Q)lhs,0) == -1) ? F_TRUE : F_FALSE;        *pnf = (cmpq((Q)lhs,0) == -1) ? F_TRUE : F_FALSE;
                         return;        return;
                 case AL_GREATERP:      case AL_GREATERP:
                         *pnf = (cmpq((Q)lhs,0) == 1) ? F_TRUE : F_FALSE;        *pnf = (cmpq((Q)lhs,0) == 1) ? F_TRUE : F_FALSE;
                         return;        return;
                 case AL_LEQ:      case AL_LEQ:
                         *pnf = (cmpq((Q)lhs,0) != 1) ? F_TRUE : F_FALSE;        *pnf = (cmpq((Q)lhs,0) != 1) ? F_TRUE : F_FALSE;
                         return;        return;
                 case AL_GEQ:      case AL_GEQ:
                         *pnf = (cmpq((Q)lhs,0) != -1) ? F_TRUE : F_FALSE;        *pnf = (cmpq((Q)lhs,0) != -1) ? F_TRUE : F_FALSE;
                         return;        return;
                 default:      default:
                         error("unknown operator in simpl_a");        error("unknown operator in simpl_a");
                 }      }
         }    }
         if (AL_ORDER(r))    if (AL_ORDER(r))
                 simpl_a_o(&r,&lhs);      simpl_a_o(&r,&lhs);
         else    else
                 simpl_a_no(&lhs);      simpl_a_no(&lhs);
         MKAF(*pnf,r,lhs);    MKAF(*pnf,r,lhs);
 }  }
   
 void simpl_a_o(ar,alhs)  void simpl_a_o(ar,alhs)
 oFOP *ar;  oFOP *ar;
 P *alhs;  P *alhs;
 {  {
         DCP dec;    DCP dec;
   
         sqfrp(CO,*alhs,&dec);    sqfrp(CO,*alhs,&dec);
         if (SGN((Q)COEF(dec)) == -1)    if (SGN((Q)COEF(dec)) == -1)
                 *ar = AL_ANEGREL(*ar);      *ar = AL_ANEGREL(*ar);
         *alhs=(P)ONE;    *alhs=(P)ONE;
         for (dec = NEXT(dec); dec; dec = NEXT(dec)) {    for (dec = NEXT(dec); dec; dec = NEXT(dec)) {
                 mulp(CO,*alhs,COEF(dec),alhs);      mulp(CO,*alhs,COEF(dec),alhs);
                 if (EVENN(NM(DEG(dec))))      if (EVENN(NM(DEG(dec))))
                         mulp(CO,*alhs,COEF(dec),alhs);        mulp(CO,*alhs,COEF(dec),alhs);
         }    }
 }  }
   
 void simpl_a_no(alhs)  void simpl_a_no(alhs)
 P *alhs;  P *alhs;
 {  {
         DCP dec;    DCP dec;
   
         sqfrp(CO,*alhs,&dec);    sqfrp(CO,*alhs,&dec);
         *alhs=(P)ONE;    *alhs=(P)ONE;
         for (dec = NEXT(dec); dec; dec = NEXT(dec))    for (dec = NEXT(dec); dec; dec = NEXT(dec))
                 mulp(CO,*alhs,COEF(dec),alhs);      mulp(CO,*alhs,COEF(dec),alhs);
 }  }
   
 /* QE */  /* QE */
Line 1148  P *alhs;
Line 1157  P *alhs;
 void qe(f,pnf)  void qe(f,pnf)
 F f,*pnf;  F f,*pnf;
 {  {
         NODE bl,sc;    NODE bl,sc;
         F h;    F h;
   
         simpl(f,(NODE)NULL,&h);    simpl(f,(NODE)NULL,&h);
         nnf(h,&h);    nnf(h,&h);
         blocksplit(h,&bl,&h);    blocksplit(h,&bl,&h);
         for (sc=bl; sc; sc=NEXT(sc)) {    for (sc=bl; sc; sc=NEXT(sc)) {
                 if (QUANT(((QVL)BDY(sc))) == AL_EX)      if (QUANT(((QVL)BDY(sc))) == AL_EX)
                         qeblock(VARL(((QVL)BDY(sc))),h,&h);        qeblock(VARL(((QVL)BDY(sc))),h,&h);
                 else {      else {
                         pnegate(h,&h);        pnegate(h,&h);
                         qeblock(VARL(((QVL)BDY(sc))),h,&h);        qeblock(VARL(((QVL)BDY(sc))),h,&h);
                         pnegate(h,&h);        pnegate(h,&h);
                 }      }
         }    }
         *pnf = h;    *pnf = h;
 }  }
   
 void blocksplit(f,pbl,pmat)  void blocksplit(f,pbl,pmat)
 F f,*pmat;  F f,*pmat;
 NODE *pbl;  NODE *pbl;
 {  {
         oFOP cq;    oFOP cq;
         NODE bl=NULL,blh;    NODE bl=NULL,blh;
         VL vl,vlh;    VL vl,vlh;
         QVL qvl;    QVL qvl;
   
         while (AL_QUANT(cq=FOP(f))) {    while (AL_QUANT(cq=FOP(f))) {
                 NEWNODE(blh);      NEWNODE(blh);
                 vl = NULL;      vl = NULL;
                 while (FOP(f) == cq) {      while (FOP(f) == cq) {
                         NEWVL(vlh);        NEWVL(vlh);
                         VR(vlh) = FQVR(f);        VR(vlh) = FQVR(f);
                         NEXT(vlh) = vl;        NEXT(vlh) = vl;
                         vl = vlh;        vl = vlh;
                         f = FQMAT(f);        f = FQMAT(f);
                 }      }
                 MKQVL(qvl,cq,vl);      MKQVL(qvl,cq,vl);
                 BDY(blh) = (pointer)qvl;      BDY(blh) = (pointer)qvl;
                 NEXT(blh) = bl;      NEXT(blh) = bl;
                 bl = blh;      bl = blh;
         }    }
         *pbl = bl;    *pbl = bl;
         *pmat = f;    *pmat = f;
 }  }
   
 void qeblock(vl,f,pnf)  void qeblock(vl,f,pnf)
 VL vl;  VL vl;
 F f,*pnf;  F f,*pnf;
 {  {
         CONT co;    CONT co;
         CEL cel;    CEL cel;
         VL cvl;    VL cvl;
         NODE n,sc;    NODE n,sc;
         NODE nargl=NULL,narglc;    NODE nargl=NULL,narglc;
         int w,pr;    int w,pr;
         int left=0,modulus;    int left=0,modulus;
   
         qeblock_verbose0(vl);    qeblock_verbose0(vl);
         simpl(f,(NODE)NULL,&f);    simpl(f,(NODE)NULL,&f);
         MKCONT(co);    MKCONT(co);
         MKCEL(cel,vl,f);    MKCEL(cel,vl,f);
         coadd(co,cel);    coadd(co,cel);
         while (coget(co,&cel)) {    while (coget(co,&cel)) {
                 cvl = VRL(cel);      cvl = VRL(cel);
                 pr = qeblock_verbose1a(co,cvl,&left,&modulus);      pr = qeblock_verbose1a(co,cvl,&left,&modulus);
                 w = qevar(MAT(cel),&cvl,&n);      w = qevar(MAT(cel),&cvl,&n);
                 qeblock_verbose1b(w,pr);      qeblock_verbose1b(w,pr);
                 for (sc=n; sc; sc=NEXT(sc))      for (sc=n; sc; sc=NEXT(sc))
                         if ((F)BDY(sc) != F_FALSE)        if ((F)BDY(sc) != F_FALSE)
                                 if (cvl) {          if (cvl) {
                                         MKCEL(cel,cvl,(F)BDY(sc));            MKCEL(cel,cvl,(F)BDY(sc));
                                         if (!comember(co,cel))            if (!comember(co,cel))
                                                 coadd(co,cel);              coadd(co,cel);
                                 } else {          } else {
                                         NEXTNODE(nargl,narglc);            NEXTNODE(nargl,narglc);
                                         BDY(narglc) = BDY(sc);            BDY(narglc) = BDY(sc);
                                 }          }
         }    }
         qeblock_verbose2();    qeblock_verbose2();
         smkjf(pnf,AL_OR,nargl);    smkjf(pnf,AL_OR,nargl);
         simpl(*pnf,(NODE)NULL,pnf);    simpl(*pnf,(NODE)NULL,pnf);
 }  }
   
 void qeblock_verbose0(vl)  void qeblock_verbose0(vl)
 VL vl;  VL vl;
 {  {
         if (!Verbose)    if (!Verbose)
                 return;      return;
         printf("eliminating");    printf("eliminating");
         for (; vl; vl=NEXT(vl))    for (; vl; vl=NEXT(vl))
                 printf(" %s",NAME(VR(vl)));      printf(" %s",NAME(VR(vl)));
 }  }
   
 int qeblock_verbose1a(co,cvl,pleft,pmodulus)  int qeblock_verbose1a(co,cvl,pleft,pmodulus)
Line 1247  CONT co;
Line 1256  CONT co;
 VL cvl;  VL cvl;
 int *pleft,*pmodulus;  int *pleft,*pmodulus;
 {  {
         int i=0;    int i=0;
   
         if (!Verbose)    if (!Verbose)
                 return;    /* added by noro */
         if (*pleft == 0) {      return 0;
                 for (; cvl; cvl=NEXT(cvl))    if (*pleft == 0) {
                         i++;      for (; cvl; cvl=NEXT(cvl))
                 printf("\nleft %d\n",i);        i++;
                 *pleft = colen(co) + 1;      printf("\nleft %d\n",i);
                 *pmodulus = getmodulus(*pleft);      *pleft = colen(co) + 1;
                 printf("(%d",(*pleft)--);      *pmodulus = getmodulus(*pleft);
                 fflush(asir_out);      printf("(%d",(*pleft)--);
                 return 1;      fflush(asir_out);
         } else if (*pleft % *pmodulus == 0) {      return 1;
                 printf("(%d",(*pleft)--);    } else if (*pleft % *pmodulus == 0) {
                 fflush(asir_out);      printf("(%d",(*pleft)--);
                 return 1;      fflush(asir_out);
         }      return 1;
         (*pleft)--;    }
         return 0;    (*pleft)--;
     return 0;
 }  }
   
 void qeblock_verbose1b(g,print)  void qeblock_verbose1b(g,print)
 int g,print;  int g,print;
 {  {
         if (!(Verbose && print))    if (!(Verbose && print))
                 return;      return;
         printf("%s) ",g ? (g==2) ? "qg" : "lg" : "e");    printf("%s) ",g ? (g==2) ? "qg" : "lg" : "e");
         fflush(asir_out);    fflush(asir_out);
 }  }
   
 void qeblock_verbose2()  void qeblock_verbose2()
 {  {
         if (!Verbose)    if (!Verbose)
                 return;      return;
         printf("\n");    printf("\n");
 }  }
   
 int getmodulus(n)  int getmodulus(n)
 int n;  int n;
 {  {
         int pow=1;    int pow=1;
   
         while (n >= pow*100) {    while (n >= pow*100) {
                 pow *= 10;      pow *= 10;
         }    }
         return pow;    return pow;
 }  }
   
   
Line 1302  F f;
Line 1312  F f;
 VL *pcvl;  VL *pcvl;
 NODE *pfl;  NODE *pfl;
 {  {
         int w;    int w;
         V x;    V x;
         F h;    F h;
         NODE trans[8],eset,sc,r=NULL,rc;    NODE trans[8],eset,sc,r=NULL,rc;
   
         w = gausselim(f,pcvl,&x,&eset);    w = gausselim(f,pcvl,&x,&eset);
         if (!w) {    if (!w) {
                 x = VR(*pcvl);      x = VR(*pcvl);
                 *pcvl = NEXT(*pcvl);      *pcvl = NEXT(*pcvl);
                 translate(f,x,trans);      translate(f,x,trans);
                 mkeset(trans,x,&eset);      mkeset(trans,x,&eset);
         }    }
         for (sc=eset; sc; sc=NEXT(sc)) {    for (sc=eset; sc; sc=NEXT(sc)) {
                 NEXTNODE(r,rc);      NEXTNODE(r,rc);
                 subgpf(f,x,BDY(sc),&h);      subgpf(f,x,BDY(sc),&h);
                 simpl(h,(NODE)NULL,&BDY(rc));      simpl(h,(NODE)NULL,&BDY(rc));
         }    }
         *pfl = r;    *pfl = r;
         return w;    return w;
 }  }
   
 int gausselim(f,pvl,px,peset)  int gausselim(f,pvl,px,peset)
Line 1329  VL *pvl;
Line 1339  VL *pvl;
 V *px;  V *px;
 NODE *peset;  NODE *peset;
 {  {
         Q deg,two;    Q deg,two;
         P rlhs,a,b,c;    P rlhs,a,b,c;
         V v;    V v;
         VL scvl;    VL scvl;
         NODE sc;    NODE sc;
         int w;    int w;
   
         if (FOP(f) != AL_AND)    if (FOP(f) != AL_AND)
                 return 0;      return 0;
         STOQ(2,two);    STOQ(2,two);
         for (deg=ONE; cmpq(two,deg) >= 0; addq(deg,ONE,&deg))    for (deg=ONE; cmpq(two,deg) >= 0; addq(deg,ONE,&deg))
                 for (scvl=*pvl; scvl; scvl=NEXT(scvl)) {      for (scvl=*pvl; scvl; scvl=NEXT(scvl)) {
                         v = VR(scvl);        v = VR(scvl);
                         for (sc=FJARG(f); sc; sc=NEXT(sc)) {        for (sc=FJARG(f); sc; sc=NEXT(sc)) {
                                 if (FOP((F)BDY(sc)) != AL_EQUAL)          if (FOP((F)BDY(sc)) != AL_EQUAL)
                                         continue;            continue;
                                 al_reorder(FPL((F)BDY(sc)),v,&rlhs);          al_reorder(FPL((F)BDY(sc)),v,&rlhs);
                                 if (VR(rlhs) != v)          if (VR(rlhs) != v)
                                         continue;            continue;
                                 w = gauss_abc(rlhs,v,deg,&a,&b,&c);          w = gauss_abc(rlhs,v,deg,&a,&b,&c);
                                 if (!w)          if (!w)
                                         continue;            continue;
                                 *px = v;          *px = v;
                                 delvip(v,pvl);          delv(v,*pvl,pvl);
                                 if (a) {          if (a) {
                                         gauss_mkeset2(rlhs,a,b,c,peset);            gauss_mkeset2(rlhs,a,b,c,peset);
                                         return 2;            return 2;
                                 }          }
                                 gauss_mkeset1(rlhs,b,peset);          gauss_mkeset1(rlhs,b,peset);
                                 return 1;          return 1;
                         }        }
                 }      }
         return 0;    return 0;
 }  }
   
 int gauss_abc(rlhs,v,deg,pa,pb,pc)  int gauss_abc(rlhs,v,deg,pa,pb,pc)
Line 1369  P rlhs,*pa,*pb,*pc;
Line 1379  P rlhs,*pa,*pb,*pc;
 V v;  V v;
 Q deg;  Q deg;
 {  {
         Q two;    Q two;
         DCP rld;    DCP rld;
   
         rld = DC(rlhs);    rld = DC(rlhs);
         if (cmpq(DEG(rld),deg) != 0)    if (cmpq(DEG(rld),deg) != 0)
                 return 0;      return 0;
         STOQ(2,two);    STOQ(2,two);
         if (cmpq(deg,two) == 0) {    if (cmpq(deg,two) == 0) {
                 *pa = COEF(rld);      *pa = COEF(rld);
                 rld = NEXT(rld);      rld = NEXT(rld);
         } else    } else
                 *pa = 0;      *pa = 0;
         if (rld && cmpq(DEG(rld),ONE) == 0) {    if (rld && cmpq(DEG(rld),ONE) == 0) {
                 *pb = COEF(rld);      *pb = COEF(rld);
                 rld = NEXT(rld);      rld = NEXT(rld);
         } else    } else
                 *pb = 0;      *pb = 0;
         if (rld)    if (rld)
                 *pc = COEF(rld);      *pc = COEF(rld);
         else    else
                 *pc = 0;      *pc = 0;
         return (NZNUMBER(*pa) || NZNUMBER(*pb) || NZNUMBER(*pc));    return (NZNUMBER(*pa) || NZNUMBER(*pb) || NZNUMBER(*pc));
 }  }
   
 gauss_mkeset1(rlhs,b,peset)  void gauss_mkeset1(rlhs,b,peset)
 P rlhs,b;  P rlhs,b;
 NODE *peset;  NODE *peset;
 {  {
         GP hgp;    GP hgp;
   
         mklgp(rlhs,b,STD,&hgp);    mklgp(rlhs,b,STD,&hgp);
         MKNODE(*peset,hgp,NULL);    MKNODE(*peset,hgp,NULL);
 }  }
   
 gauss_mkeset2(rlhs,a,b,c,peset)  void gauss_mkeset2(rlhs,a,b,c,peset)
 P rlhs,a,b,c;  P rlhs,a,b,c;
 NODE *peset;  NODE *peset;
 {  {
         RE hre;    GP hgp;
         F hf;    NODE esetc=NULL;
         GP hgp;  
         P discr;  
         NODE esetc;  
   
         *peset = NULL;    *peset = NULL;
         if (!NUM(a)) {    if (!NUM(a)) {
                 NEXTNODE(*peset,esetc);      NEXTNODE(*peset,esetc);
                 mklgp(rlhs,b,STD,&hgp);      mklgp(rlhs,b,STD,&hgp);
                 BDY(esetc) = (pointer)hgp;      BDY(esetc) = (pointer)hgp;
         }    }
         NEXTNODE(*peset,esetc);    NEXTNODE(*peset,esetc);
         mkqgp(rlhs,a,b,c,STD,&hgp);    mkqgp(rlhs,a,b,c,1,STD,&hgp);
         BDY(esetc) = (pointer)hgp;    BDY(esetc) = (pointer)hgp;
     NEXTNODE(*peset,esetc);
     mkqgp(rlhs,a,b,c,2,STD,&hgp);
     BDY(esetc) = (pointer)hgp;
 }  }
   
 int delvip(v,pvl)  int delv(v,vl,pnvl)
 V v;  V v;
 VL *pvl;  VL vl,*pnvl;
 {  {
         VL prev;          VL nvl=NULL,nvlc;
   
         if (v == VR(*pvl)) {    if (v == VR(vl)) {
                 *pvl = NEXT(*pvl);            *pnvl = NEXT(vl);
                 return 1;      return 1;
         }    }
         for (prev=*pvl; NEXT(prev); prev=NEXT(prev))    for (; vl && (VR(vl) != v); vl=NEXT(vl)) {
                 if (VR(NEXT(prev)) == v) {                  NEXTVL(nvl,nvlc);
                         NEXT(prev) = NEXT(NEXT(prev));      VR(nvlc) = VR(vl);
                         return 1;    }
                 }    if (vl) {
         return 0;                  NEXT(nvlc) = NEXT(vl);
       *pnvl = nvl;
       return 1;
     }
     *pnvl = nvl;
     return 0;
 }  }
   
 int translate(f,x,trans)  int translate(f,x,trans)
Line 1447  F f;
Line 1462  F f;
 V x;  V x;
 NODE trans[];  NODE trans[];
 {  {
         NODE sc,transc[8];    NODE sc,transc[8];
         RE hre;    int bt,w=0;
         GP hgp;  
         int bt,w=0;  
         P h;  
   
         for (bt=BTMIN; bt<=BTMAX; bt++)    for (bt=BTMIN; bt<=BTMAX; bt++)
                 trans[bt] = NULL;      trans[bt] = NULL;
         for (atl(f,&sc); sc; sc=NEXT(sc))    for (atl(f,&sc); sc; sc=NEXT(sc))
                 w = (translate_a(BDY(sc),x,trans,transc) || w);      w = (translate_a(BDY(sc),x,trans,transc) || w);
         return w;    return w;
 }  }
   
 int translate_a(at,v,trans,transc)  int translate_a(at,v,trans,transc)
Line 1465  F at;
Line 1477  F at;
 V v;  V v;
 NODE trans[],transc[];  NODE trans[],transc[];
 {  {
         P mp;    P mp;
         Q two;    Q two;
         int w;    int w;
   
         w = al_reorder(FPL(at),v,&mp);    w = al_reorder(FPL(at),v,&mp);
         if (w == 0)    if (w == 0)
                 return 0;      return 0;
         if (cmpq(ONE,DEG(DC(mp))) == 0) {    if (cmpq(ONE,DEG(DC(mp))) == 0) {
                 translate_a1(FOP(at),mp,trans,transc);      translate_a1(FOP(at),mp,trans,transc);
                 return 1;      return 1;
         };    };
         STOQ(2,two);    STOQ(2,two);
         if (cmpq(two,DEG(DC(mp))) == 0) {    if (cmpq(two,DEG(DC(mp))) == 0) {
                 translate_a2(FOP(at),mp,trans,transc);      translate_a2(FOP(at),mp,trans,transc);
                 return 1;      return 1;
         };    };
         error("degree violation in translate_a");    error("degree violation in translate_a");
     /* XXX : NOTREACHED */
     return -1;
 }  }
   
 void translate_a1(op,mp,trans,transc)  void translate_a1(op,mp,trans,transc)
Line 1489  oFOP op;
Line 1503  oFOP op;
 P mp;  P mp;
 NODE trans[],transc[];  NODE trans[],transc[];
 {  {
         P b;    P b;
         int itype,btype;    int itype,btype;
         GP hgp;    GP hgp;
   
         b = COEF(DC(mp));    b = COEF(DC(mp));
         indices(op,NUM(b) ? SGN((Q)b) : 0,&itype,&btype);    indices(op,NUM(b) ? SGN((Q)b) : 0,&itype,&btype);
         NEXTNODE(trans[btype],transc[btype]);    NEXTNODE(trans[btype],transc[btype]);
         mklgp(mp,b,itype,&hgp);    mklgp(mp,b,itype,&hgp);
         BDY(transc[btype]) = (pointer)hgp;    BDY(transc[btype]) = (pointer)hgp;
 }  }
   
 void mklgp(mp,b,itype,pgp)  void mklgp(mp,b,itype,pgp)
Line 1505  P mp,b;
Line 1519  P mp,b;
 int itype;  int itype;
 GP *pgp;  GP *pgp;
 {  {
         RE hre;    RE hre;
         F hf;    F hf;
   
         MKRE(hre,mp,(P)ONE,itype);    MKRE(hre,mp,(P)ONE,1,itype);
         MKAF(hf,AL_NEQ,b);    MKAF(hf,AL_NEQ,b);
         MKGP(*pgp,hf,hre);    MKGP(*pgp,hf,hre);
 }  }
   
 void translate_a2(op,mp,trans,transc)  void translate_a2(op,mp,trans,transc)
Line 1518  oFOP op;
Line 1532  oFOP op;
 P mp;  P mp;
 NODE trans[],transc[];  NODE trans[],transc[];
 {  {
         P a,b,c,linred;    P a,b,c,linred;
         int itype,btype;    int itype,btype;
         GP hgp;    GP hgp;
   
         getqcoeffs(mp,&a,&b,&c);    getqcoeffs(mp,&a,&b,&c);
         if (!NUM(a) && b) {    if (!NUM(a) && b) {
                 MKP(VR(mp),NEXT(DC(mp)),linred);      MKP(VR(mp),NEXT(DC(mp)),linred);
                 translate_a1(op,linred,trans,transc);      translate_a1(op,linred,trans,transc);
         }    }
         indices(op,0,&itype,&btype);    indices(op,0,&itype,&btype);
         NEXTNODE(trans[btype],transc[btype]);    NEXTNODE(trans[btype],transc[btype]);
         mkqgp(mp,a,b,c,itype,&hgp);    mkqgp(mp,a,b,c,-1,itype,&hgp);
         BDY(transc[btype]) = (pointer)hgp;    BDY(transc[btype]) = (pointer)hgp;
 }  }
   
 void mkqgp(mp,a,b,c,itype,pgp)  void mkqgp(mp,a,b,c,rootno,itype,pgp)
 P mp,a,b,c;  P mp,a,b,c;
   int rootno;
 int itype;  int itype;
 GP *pgp;  GP *pgp;
 {  {
         P discr;    P discr;
         RE hre;    RE hre;
         F hf;    F hf;
         NODE n=NULL,nc;    NODE n=NULL,nc=NULL;
   
         mkdiscr(a,b,c,&discr);    mkdiscr(a,b,c,&discr);
         MKRE(hre,mp,discr,itype);    MKRE(hre,mp,discr,rootno,itype);
         NEXTNODE(n,nc);    NEXTNODE(n,nc);
         MKAF(hf,AL_NEQ,a);    MKAF(hf,AL_NEQ,a);
         BDY(nc) = (pointer)hf;    BDY(nc) = (pointer)hf;
         NEXTNODE(n,nc);    NEXTNODE(n,nc);
         MKAF(hf,AL_GEQ,discr);    MKAF(hf,AL_GEQ,discr);
         BDY(nc) = (pointer)hf;    BDY(nc) = (pointer)hf;
         MKJF(hf,AL_AND,n);    MKJF(hf,AL_AND,n);
         MKGP(*pgp,hf,hre);    MKGP(*pgp,hf,hre);
 }  }
   
 void getqcoeffs(mp,pa,pb,pc)  void getqcoeffs(mp,pa,pb,pc)
 P mp,*pa,*pb,*pc;  P mp,*pa,*pb,*pc;
 {  {
         DCP hdcp;    DCP hdcp;
   
         *pa = COEF(DC(mp));    *pa = COEF(DC(mp));
         hdcp = NEXT(DC(mp));    hdcp = NEXT(DC(mp));
         if (hdcp && cmpq(DEG(hdcp),ONE) == 0) {    if (hdcp && cmpq(DEG(hdcp),ONE) == 0) {
                 *pb = COEF(hdcp);      *pb = COEF(hdcp);
                 hdcp = NEXT(hdcp);      hdcp = NEXT(hdcp);
         } else    } else
                 *pb = 0;      *pb = 0;
         if (hdcp && DEG(hdcp) == 0) {    if (hdcp && DEG(hdcp) == 0) {
                 *pc = COEF(hdcp);      *pc = COEF(hdcp);
         } else    } else
                 *pc = 0;      *pc = 0;
 }  }
   
 void mkdiscr(a,b,c,pd)  void mkdiscr(a,b,c,pd)
 P a,b,c,*pd;  P a,b,c,*pd;
 {  {
         P h1,h2;    P h1,h2;
         Q four;    Q four;
   
         mulp(CO,a,c,&h1);    mulp(CO,a,c,&h1);
         STOQ(4,four);    STOQ(4,four);
         mulp(CO,(P)four,h1,&h2);    mulp(CO,(P)four,h1,&h2);
         mulp(CO,b,b,&h1);    mulp(CO,b,b,&h1);
         subp(CO,h1,h2,pd);    subp(CO,h1,h2,pd);
 }  }
   
 int al_reorder(p,v,pnp)  int al_reorder(p,v,pnp)
 P p,*pnp;  P p,*pnp;
 V v;  V v;
 {  {
         VL tvl;    VL tvl;
   
         reordvar(CO,v,&tvl);    reordvar(CO,v,&tvl);
         reorderp(tvl,CO,p,pnp);    reorderp(tvl,CO,p,pnp);
         if (*pnp && !NUM(*pnp) && strcmp(NAME(VR(*pnp)),NAME(v)) == 0)    if (*pnp && !NUM(*pnp) && strcmp(NAME(VR(*pnp)),NAME(v)) == 0)
                 return 1;      return 1;
         else    else
                 return 0;      return 0;
 }  }
   
 int indices(op,s,pit,pbt)  void indices(op,s,pit,pbt)
 oFOP op;  oFOP op;
 int s,*pit,*pbt;  int s,*pit,*pbt;
 {  {
         switch (op) {    switch (op) {
         case AL_EQUAL:    case AL_EQUAL:
                 *pit = STD; *pbt = BTEQUAL; return;      *pit = STD; *pbt = BTEQUAL; return;
         case AL_NEQ:    case AL_NEQ:
                 *pit = EPS; *pbt = BTNEQ; return;      *pit = EPS; *pbt = BTNEQ; return;
         case AL_LEQ:    case AL_LEQ:
                 *pit = STD;      *pit = STD;
                 switch (s) {      switch (s) {
                 case 1:      case 1:
                         *pbt = BTLEQ; return;        *pbt = BTLEQ; return;
                 case -1:      case -1:
                         *pbt = BTGEQ; return;        *pbt = BTGEQ; return;
                 case 0:      case 0:
                         *pbt = BTWO; return;        *pbt = BTWO; return;
                 }      }
         case AL_GEQ:    case AL_GEQ:
                 *pit = STD;      *pit = STD;
                 switch (s) {      switch (s) {
                 case 1:      case 1:
                         *pbt = BTGEQ; return;        *pbt = BTGEQ; return;
                 case -1:      case -1:
                         *pbt = BTLEQ; return;        *pbt = BTLEQ; return;
                 case 0:      case 0:
                         *pbt = BTWO; return;        *pbt = BTWO; return;
                 }      }
         case AL_LESSP:    case AL_LESSP:
                 switch (s) {      switch (s) {
                 case 1:      case 1:
                         *pit = MEPS; *pbt = BTLESSP; return;        *pit = MEPS; *pbt = BTLESSP; return;
                 case -1:      case -1:
                         *pit = PEPS; *pbt = BTGREATERP; return;        *pit = PEPS; *pbt = BTGREATERP; return;
                 case 0:      case 0:
                         *pit = EPS; *pbt = BTSO; return;        *pit = EPS; *pbt = BTSO; return;
                 }      }
         case AL_GREATERP:    case AL_GREATERP:
                 switch (s) {      switch (s) {
                 case 1:      case 1:
                         *pit = PEPS; *pbt = BTGREATERP; return;        *pit = PEPS; *pbt = BTGREATERP; return;
                 case -1:      case -1:
                         *pit = MEPS; *pbt = BTLESSP; return;        *pit = MEPS; *pbt = BTLESSP; return;
                 case 0:      case 0:
                         *pit = EPS; *pbt = BTSO; return;        *pit = EPS; *pbt = BTSO; return;
                 }      }
         default:    default:
                 error("unknown relation or sign in indices");      error("unknown relation or sign in indices");
         }    }
 }  }
   
 void mkeset(trans,x,peset)  void mkeset(trans,x,peset)
 NODE trans[],*peset;  NODE trans[],*peset;
 V x;  V x;
 {  {
         NODE esetc;    NODE esetc=NULL;
         P h;    P h;
         RE hre;    RE hre;
         GP hgp;    GP hgp;
         int cw,cs,deps,dinf,ord;    int cw,cs,deps,dinf,ord;
   
         *peset = NULL;    *peset = NULL;
         ord = selectside(trans,&cw,&cs,&deps,&dinf);    ord = selectside(trans,&cw,&cs,&deps,&dinf);
         if (ord) {    if (ord) {
                 add2eset(trans[cw],peset,&esetc);      add2eset(trans[cw],peset,&esetc);
                 add2eset(trans[BTWO],peset,&esetc);      add2eset(trans[BTWO],peset,&esetc);
                 add2eset(trans[cs],peset,&esetc);      add2eset(trans[cs],peset,&esetc);
                 sp_add2eset(trans[BTSO],deps,peset,&esetc);      sp_add2eset(trans[BTSO],deps,peset,&esetc);
                 NEXTNODE(*peset,esetc);      NEXTNODE(*peset,esetc);
                 MKRE(hre,0,0,dinf);      MKRE(hre,0,0,0,dinf);
                 MKGP(hgp,F_TRUE,hre);      MKGP(hgp,F_TRUE,hre);
                 BDY(esetc) = (pointer)hgp;      BDY(esetc) = (pointer)hgp;
         } else {    } else {
                 NEXTNODE(*peset,esetc);      NEXTNODE(*peset,esetc);
                 MKV(x,h);      MKV(x,h);
                 MKRE(hre,h,(P)ONE,STD);      MKRE(hre,h,(P)ONE,1,STD);
                 MKGP(hgp,F_TRUE,hre);      MKGP(hgp,F_TRUE,hre);
                 BDY(esetc) = (pointer)hgp;      BDY(esetc) = (pointer)hgp;
         }    }
         add2eset(trans[BTEQUAL],peset,&esetc);    add2eset(trans[BTEQUAL],peset,&esetc);
         sp_add2eset(trans[BTNEQ],deps,peset,&esetc);    sp_add2eset(trans[BTNEQ],deps,peset,&esetc);
 }  }
   
 int selectside(trans,pcw,pcs,pdeps,pdinf)  int selectside(trans,pcw,pcs,pdeps,pdinf)
 NODE trans[];  NODE trans[];
 int *pcw,*pcs,*pdeps,*pdinf;  int *pcw,*pcs,*pdeps,*pdinf;
 {  {
         if (cmp2n(trans[BTLEQ],trans[BTLESSP],trans[BTGEQ],trans[BTGREATERP])==1) {    if (cmp2n(trans[BTLEQ],trans[BTLESSP],trans[BTGEQ],trans[BTGREATERP])==1) {
                 *pcw = BTGEQ;      *pcw = BTGEQ;
                 *pcs = BTGREATERP;      *pcs = BTGREATERP;
                 *pdeps = PEPS;      *pdeps = PEPS;
                 *pdinf = MINF;      *pdinf = MINF;
         } else {    } else {
                 *pcw = BTLEQ;      *pcw = BTLEQ;
                 *pcs = BTLESSP;      *pcs = BTLESSP;
                 *pdeps = MEPS;      *pdeps = MEPS;
                 *pdinf = PINF;      *pdinf = PINF;
         }    }
         if (!(trans[BTLEQ] || trans[BTLESSP] || trans[BTGEQ] ||    if (!(trans[BTLEQ] || trans[BTLESSP] || trans[BTGEQ] ||
                         trans[BTGREATERP] || trans[BTWO] || trans[BTSO]))        trans[BTGREATERP] || trans[BTWO] || trans[BTSO]))
                 return 0;      return 0;
         return 1;    return 1;
 }  }
   
 int cmp2n(n1a,n1b,n2a,n2b)  int cmp2n(n1a,n1b,n2a,n2b)
 NODE n1a,n1b,n2a,n2b;  NODE n1a,n1b,n2a,n2b;
 {  {
         NODE n1,n2;    NODE n1,n2;
         int n1bleft=1,n2bleft=1;    int n1bleft=1,n2bleft=1;
   
         n1 = n1a;    n1 = n1a;
         n2 = n2a;    n2 = n2a;
         while (n1 && n2) {    while (n1 && n2) {
                 n1 = NEXT(n1);      n1 = NEXT(n1);
                 if (n1 == NULL && n1bleft) {      if (n1 == NULL && n1bleft) {
                         n1 = n1b;        n1 = n1b;
                         n1bleft = 0;        n1bleft = 0;
                 }      }
                 n2 = NEXT(n2);      n2 = NEXT(n2);
                 if (n2 == NULL && n2bleft) {      if (n2 == NULL && n2bleft) {
                         n2 = n2b;        n2 = n2b;
                         n2bleft = 0;        n2bleft = 0;
                 }      }
         }    }
         if (n1 || n2)    if (n1 || n2)
                 return n1 ? 1 : -1;      return n1 ? 1 : -1;
         return 0;    return 0;
 }  }
   
 void add2eset(trfield,peset,pesetc)  void add2eset(trfield,peset,pesetc)
 NODE trfield,*peset,*pesetc;  NODE trfield,*peset,*pesetc;
 {  {
         if (trfield == NULL)          NODE ntrfield,ntrfieldc;
                 return;  
         if (*peset == NULL)    if (trfield == NULL)
                 *peset = *pesetc = trfield;      return;
         else    seproots(trfield,&ntrfield,&ntrfieldc);
                 NEXT(*pesetc) = trfield;    if (*peset == NULL) {
         while (NEXT(*pesetc))      *peset = ntrfield;
                 *pesetc = NEXT(*pesetc);      *pesetc = ntrfieldc;
     } else {
       NEXT(*pesetc) = ntrfield;
       *pesetc = ntrfieldc;
     }
 }  }
   
   void seproots(trfield,pntrfield,pntrfieldc)
   NODE trfield,*pntrfield,*pntrfieldc;
   {
           NODE sc;
     NODE ntrf=NULL,ntrfc;
     RE hre,hre2;
     GP hgp,hgp2;
   
     for (sc=trfield; sc; sc=NEXT(sc)) {
                   hgp = (GP)BDY(sc);
       hre = POINT(hgp);
                   if (ROOTNO(hre) == -1) {
               NEXTNODE(ntrf,ntrfc);
         MKRE(hre2,PL(hre),DISC(hre),1,ITYPE(hre));
                           MKGP(hgp2,GUARD(hgp),hre2);
         BDY(ntrfc) = (pointer)hgp2;
               NEXTNODE(ntrf,ntrfc);
         ROOTNO(hre) = 2;
         BDY(ntrfc) = (pointer)hgp;
       } else {
               NEXTNODE(ntrf,ntrfc);
         BDY(ntrfc) = (pointer)hgp;
       }
     }
     *pntrfield = ntrf;
     *pntrfieldc = ntrfc;
   }
   
 void sp_add2eset(trfield,itype,peset,pesetc)  void sp_add2eset(trfield,itype,peset,pesetc)
 NODE trfield,*peset,*pesetc;  NODE trfield,*peset,*pesetc;
 int itype;  int itype;
 {  {
         NODE sc;    NODE sc;
         GP hgp;    GP hgp;
   
         for (sc=trfield; sc; sc=NEXT(sc)) {    for (sc=trfield; sc; sc=NEXT(sc)) {
                 hgp = (GP)BDY(sc);      hgp = (GP)BDY(sc);
                 ITYPE(POINT(hgp)) = itype;      ITYPE(POINT(hgp)) = itype;
         }    }
         add2eset(trfield,peset,pesetc);    add2eset(trfield,peset,pesetc);
 }  }
   
 void subgpf(f,v,gp,pnf)  void subgpf(f,v,gp,pnf)
Line 1762  F f,*pnf;
Line 1809  F f,*pnf;
 V v;  V v;
 GP gp;  GP gp;
 {  {
         NODE argl=NULL,arglc;    NODE argl=NULL,arglc=NULL;
   
         NEXTNODE(argl,arglc);    NEXTNODE(argl,arglc);
         BDY(arglc) = (pointer)GUARD(gp);    BDY(arglc) = (pointer)GUARD(gp);
         NEXTNODE(argl,arglc);    NEXTNODE(argl,arglc);
         subref(f,v,POINT(gp),&BDY(arglc));    subref(f,v,POINT(gp),&BDY(arglc));
         MKJF(*pnf,AL_AND,argl);    MKJF(*pnf,AL_AND,argl);
 }  }
   
 void subref(f,v,r,pnf)  void subref(f,v,r,pnf)
Line 1776  F f,*pnf;
Line 1823  F f,*pnf;
 V v;  V v;
 RE r;  RE r;
 {  {
         pointer argv[2];    pointer argv[2];
   
         argv[0] = (pointer)v;    argv[0] = (pointer)v;
         argv[1] = (pointer)r;    argv[1] = (pointer)r;
         apply2ats(f,subref_a,argv,pnf);    apply2ats(f,subref_a,argv,pnf);
 }  }
   
 void subref_a(at,argv,pnat)  void subref_a(at,argv,pnat)
 F at,*pnat;  F at,*pnat;
 pointer argv[];  pointer argv[];
 {  {
         switch (ITYPE((RE)argv[1])) {    switch (ITYPE((RE)argv[1])) {
         case STD:    case STD:
                 substd_a(at,argv[0],argv[1],pnat);      substd_a(at,argv[0],argv[1],pnat);
                 return;      return;
         case EPS:    case EPS:
                 error("unspecified RE in subref_a()");      error("unspecified RE in subref_a()");
         case PEPS:    case PEPS:
         case MEPS:    case MEPS:
                 subpme_a(at,argv[0],argv[1],pnat);      subpme_a(at,argv[0],argv[1],pnat);
                 return;      return;
         case PINF:    case PINF:
         case MINF:    case MINF:
                 subinf_a(at,argv[0],argv[1],pnat);      subinf_a(at,argv[0],argv[1],pnat);
                 return;      return;
         default:    default:
                 error("unknown itype in subref_a()");      error("unknown itype in subref_a()");
         }    }
 }  }
   
 void substd_a(at,v,re,pnf)  void substd_a(at,v,re,pnf)
Line 1811  F at,*pnf;
Line 1858  F at,*pnf;
 V v;  V v;
 RE re;  RE re;
 {  {
         VL no;    VL no;
         P rlhs,prem,bdn,nlhs;    P rlhs,prem,nlhs;
         Q dd,dndeg;    Q dd,dndeg;
   
         reordvar(CO,v,&no);    reordvar(CO,v,&no);
         reorderp(no,CO,FPL(at),&rlhs);    reorderp(no,CO,FPL(at),&rlhs);
         if (!rlhs || NUM(rlhs) || VR(rlhs) != v) {    if (!rlhs || NUM(rlhs) || VR(rlhs) != v) {
                 *pnf = at;      *pnf = at;
                 return;      return;
         }    }
         premp(no,rlhs,PL(re),&prem);    premp(no,rlhs,PL(re),&prem);
         if (prem && !NUM(prem) && VR(prem) == v) {    if (prem && !NUM(prem) && VR(prem) == v) {
                 /* quadratic case */      /* quadratic case */
                 substd_a2(FOP(at),prem,DEG(DC(rlhs)),re,pnf);      substd_a2(FOP(at),prem,DEG(DC(rlhs)),re,pnf);
                 return;      return;
         }    }
         subq(DEG(DC(rlhs)),DEG(DC(PL(re))),&dd);    subq(DEG(DC(rlhs)),DEG(DC(PL(re))),&dd);
         addq(dd,ONE,&dndeg);    addq(dd,ONE,&dndeg);
         if (AL_ORDER(FOP(at)) && (!EVENN(NM(dndeg))))    if (AL_ORDER(FOP(at)) && (!EVENN(NM(dndeg))))
                 mulp(CO,prem,COEF(DC(PL(re))),&nlhs);      mulp(CO,prem,COEF(DC(PL(re))),&nlhs);
         else    else
                 nlhs = prem;      nlhs = prem;
         MKAF(*pnf,FOP(at),nlhs);    MKAF(*pnf,FOP(at),nlhs);
 }  }
   
 void substd_a2(op,prem,fdeg,re,pf)  void substd_a2(op,prem,fdeg,re,pf)
 oFOP op;  oFOP op;
 F prem;  F prem;
Line 1843  Q fdeg;
Line 1890  Q fdeg;
 RE re;  RE re;
 F *pf;  F *pf;
 {  {
         P a,b,c,ld;    P a,b,c,ld;
         F hf;  
         NODE d=NULL,dc;    getrecoeffs(prem,fdeg,re,&a,&b,&c,&ld);
     if (ROOTNO(re) == 1)
         getrecoeffs(prem,fdeg,re,&a,&b,&c,&ld);      chsgnp(b,&b);
         NEXTNODE(d,dc);    else if (ROOTNO(re) != 2)
         substd_a21(op,a,b,c,ld,&hf);      error("unspecified quadratic root in substd_a2");
         BDY(dc) = (pointer)hf;    substd_a21(op,a,b,c,ld,pf);
         NEXTNODE(d,dc);  
         chsgnp(b,&b);  
         substd_a21(op,a,b,c,ld,&hf);  
         BDY(dc) = (pointer)hf;  
         MKJF(*pf,AL_OR,d);  
 }  }
   
 void substd_a21(op,a,b,c,d,pf)  void substd_a21(op,a,b,c,d,pf)
Line 1863  oFOP op;
Line 1905  oFOP op;
 P a,b,c,d;  P a,b,c,d;
 F *pf;  F *pf;
 {  {
         switch (op) {    switch (op) {
         case AL_EQUAL:    case AL_EQUAL:
                 substd_a21_equal(a,b,c,d,pf);      substd_a21_equal(a,b,c,d,pf);
                 return;      return;
         case AL_NEQ:    case AL_NEQ:
                 substd_a21_equal(a,b,c,d,pf);      substd_a21_equal(a,b,c,d,pf);
                 pnegate(*pf,pf);      pnegate(*pf,pf);
                 return;      return;
         case AL_LEQ:    case AL_LEQ:
                 substd_a21_leq(a,b,c,d,pf);      substd_a21_leq(a,b,c,d,pf);
                 return;      return;
         case AL_LESSP:    case AL_LESSP:
                 substd_a21_lessp(a,b,c,d,pf);      substd_a21_lessp(a,b,c,d,pf);
                 return;      return;
         case AL_GEQ:    case AL_GEQ:
                 substd_a21_lessp(a,b,c,d,pf);      substd_a21_lessp(a,b,c,d,pf);
                 pnegate(*pf,pf);      pnegate(*pf,pf);
                 return;      return;
         case AL_GREATERP:    case AL_GREATERP:
                 substd_a21_leq(a,b,c,d,pf);      substd_a21_leq(a,b,c,d,pf);
                 pnegate(*pf,pf);      pnegate(*pf,pf);
                 return;      return;
         default:    default:
                 error("unknown operator in substd_a21");      error("unknown operator in substd_a21");
         }    }
 }  }
   
 void substd_a21_equal(a,b,c,d,pf)  void substd_a21_equal(a,b,c,d,pf)
 P a,b,c,d;  P a,b,c,d;
 F *pf;  F *pf;
 {  {
         F hf;    F hf;
         NODE cj=NULL,cjc;    NODE cj=NULL,cjc=NULL;
         P hp1,hp2;    P hp1,hp2;
   
         NEXTNODE(cj,cjc);    NEXTNODE(cj,cjc);
         mulp(CO,a,a,&hp1);    mulp(CO,a,a,&hp1);
         mulp(CO,b,b,&hp2);    mulp(CO,b,b,&hp2);
         mulp(CO,hp2,c,&hp2);    mulp(CO,hp2,c,&hp2);
         subp(CO,hp1,hp2,&hp1);    subp(CO,hp1,hp2,&hp1);
         MKAF(hf,AL_EQUAL,hp1);    MKAF(hf,AL_EQUAL,hp1);
         BDY(cjc) = (pointer)hf;    BDY(cjc) = (pointer)hf;
         NEXTNODE(cj,cjc);    NEXTNODE(cj,cjc);
         mulp(CO,a,b,&hp1);    mulp(CO,a,b,&hp1);
         MKAF(hf,AL_LEQ,hp1);    MKAF(hf,AL_LEQ,hp1);
         BDY(cjc) = (pointer)hf;    BDY(cjc) = (pointer)hf;
         MKJF(*pf,AL_AND,cj);    MKJF(*pf,AL_AND,cj);
 }  }
   
 void substd_a21_leq(a,b,c,d,pf)  void substd_a21_leq(a,b,c,d,pf)
 P a,b,c,d;  P a,b,c,d;
 F *pf;  F *pf;
 {  {
         F hf;    F hf;
         NODE cj=NULL,cjc,dj=NULL,djc;    NODE cj=NULL,cjc=NULL,dj=NULL,djc=NULL;
         P hp1,hp2;    P hp1,hp2;
   
         NEXTNODE(dj,djc);    NEXTNODE(dj,djc);
         NEXTNODE(cj,cjc);    NEXTNODE(cj,cjc);
         mulp(CO,a,d,&hp1);    mulp(CO,a,d,&hp1);
         MKAF(hf,AL_LEQ,hp1);    MKAF(hf,AL_LEQ,hp1);
         BDY(cjc) = (pointer)hf;    BDY(cjc) = (pointer)hf;
         NEXTNODE(cj,cjc);    NEXTNODE(cj,cjc);
         mulp(CO,a,a,&hp1);    mulp(CO,a,a,&hp1);
         mulp(CO,b,b,&hp2);    mulp(CO,b,b,&hp2);
         mulp(CO,hp2,c,&hp2);    mulp(CO,hp2,c,&hp2);
         subp(CO,hp1,hp2,&hp1);    subp(CO,hp1,hp2,&hp1);
         MKAF(hf,AL_GEQ,hp1);    MKAF(hf,AL_GEQ,hp1);
         BDY(cjc) = (pointer)hf;    BDY(cjc) = (pointer)hf;
         MKJF(hf,AL_AND,cj);    MKJF(hf,AL_AND,cj);
         BDY(djc) = (pointer)hf;    BDY(djc) = (pointer)hf;
         NEXTNODE(dj,djc);    NEXTNODE(dj,djc);
         cj = NULL;    cj = NULL;
         NEXTNODE(cj,cjc);    NEXTNODE(cj,cjc);
         MKAF(hf,AL_LEQ,hp1);    MKAF(hf,AL_LEQ,hp1);
         BDY(cjc) = (pointer)hf;    BDY(cjc) = (pointer)hf;
         NEXTNODE(cj,cjc);    NEXTNODE(cj,cjc);
         mulp(CO,b,d,&hp1);    mulp(CO,b,d,&hp1);
         MKAF(hf,AL_LEQ,hp1);    MKAF(hf,AL_LEQ,hp1);
         BDY(cjc) = (pointer)hf;    BDY(cjc) = (pointer)hf;
         MKJF(hf,AL_AND,cj);    MKJF(hf,AL_AND,cj);
         BDY(djc) = (pointer)hf;    BDY(djc) = (pointer)hf;
         MKJF(*pf,AL_OR,dj);    MKJF(*pf,AL_OR,dj);
 }  }
   
 void substd_a21_lessp(a,b,c,d,pf)  void substd_a21_lessp(a,b,c,d,pf)
 P a,b,c,d;  P a,b,c,d;
 F *pf;  F *pf;
 {  {
         F hf,hf0;    F hf,hf0;
         NODE cj=NULL,cjc,d1=NULL,d1c,d2=NULL,d2c;    NODE cj=NULL,cjc=NULL,d1=NULL,d1c=NULL,d2=NULL,d2c=NULL;
         P hp1,hp2;    P hp1,hp2;
   
         NEXTNODE(d1,d1c);    NEXTNODE(d1,d1c);
         NEXTNODE(cj,cjc);    NEXTNODE(cj,cjc);
         mulp(CO,a,d,&hp1);    mulp(CO,a,d,&hp1);
         MKAF(hf0,AL_LESSP,hp1);    MKAF(hf0,AL_LESSP,hp1);
         BDY(cjc) = (pointer)hf0;    BDY(cjc) = (pointer)hf0;
         NEXTNODE(cj,cjc);    NEXTNODE(cj,cjc);
         mulp(CO,a,a,&hp1);    mulp(CO,a,a,&hp1);
         mulp(CO,b,b,&hp2);    mulp(CO,b,b,&hp2);
         mulp(CO,hp2,c,&hp2);    mulp(CO,hp2,c,&hp2);
         subp(CO,hp1,hp2,&hp1);    subp(CO,hp1,hp2,&hp1);
         MKAF(hf,AL_GREATERP,hp1);    MKAF(hf,AL_GREATERP,hp1);
         BDY(cjc) = (pointer)hf;    BDY(cjc) = (pointer)hf;
         MKJF(hf,AL_AND,cj);    MKJF(hf,AL_AND,cj);
         BDY(d1c) = (pointer)hf;    BDY(d1c) = (pointer)hf;
         NEXTNODE(d1,d1c);    NEXTNODE(d1,d1c);
         cj = NULL;    cj = NULL;
         NEXTNODE(cj,cjc);    NEXTNODE(cj,cjc);
         NEXTNODE(d2,d2c);    NEXTNODE(d2,d2c);
         MKAF(hf,AL_LESSP,hp1);    MKAF(hf,AL_LESSP,hp1);
         BDY(d2c) = (pointer)hf;    BDY(d2c) = (pointer)hf;
         NEXTNODE(d2,d2c);    NEXTNODE(d2,d2c);
         BDY(d2c) = (pointer)hf0;    BDY(d2c) = (pointer)hf0;
         MKJF(hf,AL_OR,d2);    MKJF(hf,AL_OR,d2);
         BDY(cjc) = (pointer)hf;    BDY(cjc) = (pointer)hf;
         NEXTNODE(cj,cjc);    NEXTNODE(cj,cjc);
         mulp(CO,b,d,&hp1);    mulp(CO,b,d,&hp1);
         MKAF(hf,AL_LEQ,hp1);    MKAF(hf,AL_LEQ,hp1);
         BDY(cjc) = (pointer)hf;    BDY(cjc) = (pointer)hf;
         MKJF(hf,AL_AND,cj);    MKJF(hf,AL_AND,cj);
         BDY(d1c) = (pointer)hf;    BDY(d1c) = (pointer)hf;
         MKJF(*pf,AL_OR,d1);    MKJF(*pf,AL_OR,d1);
 }  }
   
 void getrecoeffs(prem,fdeg,re,pa,pb,pc,pld)  void getrecoeffs(prem,fdeg,re,pa,pb,pc,pld)
Line 1994  P prem,*pa,*pb,*pc,*pld;
Line 2036  P prem,*pa,*pb,*pc,*pld;
 Q fdeg;  Q fdeg;
 RE re;  RE re;
 {  {
         P a,b,c,alpha,beta,h1,h2,h3;    P a,b,c,alpha,beta,h1,h2;
         Q two;    Q two;
   
         alpha = COEF(DC(prem));    alpha = COEF(DC(prem));
         beta = (NEXT(DC(prem))) ? COEF(NEXT(DC(prem))) : 0;    beta = (NEXT(DC(prem))) ? COEF(NEXT(DC(prem))) : 0;
         getqcoeffs(PL(re),&a,&b,&c);    getqcoeffs(PL(re),&a,&b,&c);
         STOQ(2,two);    STOQ(2,two);
         mulp(CO,(P)two,a,&h1);    mulp(CO,(P)two,a,&h1);
         mulp(CO,h1,beta,&h2);    mulp(CO,h1,beta,&h2);
         mulp(CO,b,alpha,&h1);    mulp(CO,b,alpha,&h1);
         subp(CO,h2,h1,pa);    subp(CO,h2,h1,pa);
         *pb = alpha;    *pb = alpha;
         *pc = DISC(re);    *pc = DISC(re);
         *pld = (EVENN(NM(fdeg))) ? (P)ONE : a;    *pld = (EVENN(NM(fdeg))) ? (P)ONE : a;
 }  }
   
 void subinf_a(f,v,re,pnf)  void subinf_a(f,v,re,pnf)
 F f,*pnf;  F f,*pnf;
 V v;  V v;
 RE re;  RE re;
 {  {
         if (AL_ORDER(FOP(f)))    if (AL_ORDER(FOP(f)))
                 subinf_a_o(f,v,re,pnf);      subinf_a_o(f,v,re,pnf);
         else    else
                 subtrans_a_no(f,v,pnf);      subtrans_a_no(f,v,pnf);
 }  }
   
 void subinf_a_o(f,v,ire,pnf)  void subinf_a_o(f,v,ire,pnf)
Line 2026  F f,*pnf;
Line 2068  F f,*pnf;
 V v;  V v;
 RE ire;  RE ire;
 {  {
         P rlhs;    P rlhs;
   
         if (!al_reorder(FPL(f),v,&rlhs))    if (!al_reorder(FPL(f),v,&rlhs))
                 *pnf = f;      *pnf = f;
         else    else
                 subinf_a_o1(FOP(f),DC(rlhs),ire,pnf);      subinf_a_o1(FOP(f),DC(rlhs),ire,pnf);
 }  }
   
 void subinf_a_o1(op,lhsdcp,ire,pnf)  void subinf_a_o1(op,lhsdcp,ire,pnf)
Line 2040  DCP lhsdcp;
Line 2082  DCP lhsdcp;
 RE ire;  RE ire;
 F *pnf;  F *pnf;
 {  {
         P an;    P an;
         F h;    F h;
         NODE c=NULL,cc,d=NULL,dc;    NODE c=NULL,cc=NULL,d=NULL,dc=NULL;
   
         if (lhsdcp == 0) {    if (lhsdcp == 0) {
                 MKAF(*pnf,op,0);      MKAF(*pnf,op,0);
                 return;      return;
         }    }
         if (DEG(lhsdcp) == 0) {    if (DEG(lhsdcp) == 0) {
                 MKAF(*pnf,op,COEF(lhsdcp));      MKAF(*pnf,op,COEF(lhsdcp));
                 return;      return;
         }    }
         if (ITYPE(ire) == MINF && !EVENN(NM(DEG(lhsdcp))))    if (ITYPE(ire) == MINF && !EVENN(NM(DEG(lhsdcp))))
                 chsgnp(COEF(lhsdcp),&an);      chsgnp(COEF(lhsdcp),&an);
         else    else
                 an = COEF(lhsdcp);      an = COEF(lhsdcp);
         NEXTNODE(d,dc);    NEXTNODE(d,dc);
         MKAF(h,AL_MKSTRICT(op),an);    MKAF(h,AL_MKSTRICT(op),an);
         BDY(dc) = (pointer)h;    BDY(dc) = (pointer)h;
         NEXTNODE(d,dc);    NEXTNODE(d,dc);
         NEXTNODE(c,cc);    NEXTNODE(c,cc);
         MKAF(h,AL_EQUAL,an);    MKAF(h,AL_EQUAL,an);
         BDY(cc) = (pointer)h;    BDY(cc) = (pointer)h;
         NEXTNODE(c,cc);    NEXTNODE(c,cc);
         subinf_a_o1(op,NEXT(lhsdcp),ire,&h);    subinf_a_o1(op,NEXT(lhsdcp),ire,&h);
         BDY(cc) = (pointer)h;    BDY(cc) = (pointer)h;
         MKJF(h,AL_AND,c);    MKJF(h,AL_AND,c);
         BDY(dc) = (pointer)h;    BDY(dc) = (pointer)h;
         MKJF(*pnf,AL_OR,d);    MKJF(*pnf,AL_OR,d);
 }  }
   
 void subtrans_a_no(f,v,pnf)  void subtrans_a_no(f,v,pnf)
 F f,*pnf;  F f,*pnf;
 V v;  V v;
 {  {
         P rlhs;    P rlhs;
         DCP sc;    DCP sc;
         F h;    F h;
         NODE nargl=NULL,narglc;    NODE nargl=NULL,narglc;
         oFOP op=FOP(f);    oFOP op=FOP(f);
   
         if (!al_reorder(FPL(f),v,&rlhs)) {    if (!al_reorder(FPL(f),v,&rlhs)) {
                 *pnf = f;      *pnf = f;
                 return;      return;
         }    }
         for (sc=DC(rlhs); sc; sc=NEXT(sc)) {    for (sc=DC(rlhs); sc; sc=NEXT(sc)) {
                 NEXTNODE(nargl,narglc);      NEXTNODE(nargl,narglc);
                 MKAF(h,op,COEF(sc));      MKAF(h,op,COEF(sc));
                 BDY(narglc) = (pointer)h;      BDY(narglc) = (pointer)h;
         }    }
         smkjf(pnf,AL_TRSUBEXP(op),nargl);    smkjf(pnf,AL_TRSUBEXP(op),nargl);
 }  }
   
 void subpme_a(af,v,re,pnf)  void subpme_a(af,v,re,pnf)
Line 2098  F af,*pnf;
Line 2140  F af,*pnf;
 V v;  V v;
 RE re;  RE re;
 {  {
         if (AL_ORDER(FOP(af)))    if (AL_ORDER(FOP(af)))
                 subpme_a_o(af,v,re,pnf);      subpme_a_o(af,v,re,pnf);
         else    else
                 subtrans_a_no(af,v,pnf);      subtrans_a_no(af,v,pnf);
 }  }
   
 void subpme_a_o(af,v,r,pnf)  void subpme_a_o(af,v,r,pnf)
Line 2109  F af,*pnf;
Line 2151  F af,*pnf;
 V v;  V v;
 RE r;  RE r;
 {  {
         F h;    F h;
         RE stdre;    RE stdre;
   
         subpme_a_o1(FOP(af),FPL(af),v,ITYPE(r)==MEPS,&h);    subpme_a_o1(FOP(af),FPL(af),v,ITYPE(r)==MEPS,&h);
         MKRE(stdre,PL(r),DISC(r),STD);    MKRE(stdre,PL(r),DISC(r),ROOTNO(r),STD);
         subref(h,v,stdre,pnf);    subref(h,v,stdre,pnf);
 }  }
   
 void subpme_a_o1(op,lhs,v,minus,pnf)  void subpme_a_o1(op,lhs,v,minus,pnf)
Line 2124  V v;
Line 2166  V v;
 int minus;  int minus;
 F *pnf;  F *pnf;
 {  {
         Q deg;    Q deg;
         F h;    F h;
         NODE c=NULL,cc,d=NULL,dc;    NODE c=NULL,cc=NULL,d=NULL,dc=NULL;
         P df;    P df;
   
         degp(v,lhs,&deg);    degp(v,lhs,&deg);
         if (deg == 0) {    if (deg == 0) {
                 MKAF(*pnf,op,lhs);      MKAF(*pnf,op,lhs);
                 return;      return;
         };    };
         NEXTNODE(d,dc);    NEXTNODE(d,dc);
         MKAF(h,AL_MKSTRICT(op),lhs);    MKAF(h,AL_MKSTRICT(op),lhs);
         BDY(dc) = (pointer)h;    BDY(dc) = (pointer)h;
         NEXTNODE(d,dc);    NEXTNODE(d,dc);
         NEXTNODE(c,cc);    NEXTNODE(c,cc);
         MKAF(h,AL_EQUAL,lhs);    MKAF(h,AL_EQUAL,lhs);
         BDY(cc) = (pointer)h;    BDY(cc) = (pointer)h;
         NEXTNODE(c,cc);    NEXTNODE(c,cc);
         diffp(CO,lhs,v,&df);    diffp(CO,lhs,v,&df);
         if (minus)    if (minus)
                 chsgnp(df,&df);      chsgnp(df,&df);
         subpme_a_o1(op,df,v,minus,&h);    subpme_a_o1(op,df,v,minus,&h);
         BDY(cc) = (pointer)h;    BDY(cc) = (pointer)h;
         MKJF(h,AL_AND,c);    MKJF(h,AL_AND,c);
         BDY(dc) = (pointer)h;    BDY(dc) = (pointer)h;
         MKJF(*pnf,AL_OR,d);    MKJF(*pnf,AL_OR,d);
 }  }
   
 int comember(co,x)  int comember(co,x)
 CONT co;  CONT co;
 CEL x;  CEL x;
 {  {
         NODE sc;    NODE sc;
   
         for (sc=FIRST(co); sc; sc=NEXT(sc))    for (sc=FIRST(co); sc; sc=NEXT(sc))
                 if (synequalf(MAT(x),MAT((CEL)BDY(sc))))      if (synequalf(MAT(x),MAT((CEL)BDY(sc))))
                         return 1;        return 1;
         return 0;    return 0;
 }  }
   
 void coadd(co,x)  void coadd(co,x)
 CONT co;  CONT co;
 CEL x;  CEL x;
 {  {
         NEXTNODE(FIRST(co),LAST(co));    NEXTNODE(FIRST(co),LAST(co));
         BDY(LAST(co)) = (pointer)x;    BDY(LAST(co)) = (pointer)x;
 }  }
   
 int coget(co,px)  int coget(co,px)
 CONT co;  CONT co;
 CEL *px;  CEL *px;
 {  {
         if (FIRST(co) == 0)    if (FIRST(co) == 0)
                 return 0;      return 0;
         *px = (CEL)BDY(FIRST(co));    *px = (CEL)BDY(FIRST(co));
         FIRST(co) = NEXT(FIRST(co));    FIRST(co) = NEXT(FIRST(co));
         return 1;    return 1;
 }  }
   
 int colen(co)  int colen(co)
 CONT co;  CONT co;
 {  {
         NODE sc;    NODE sc;
         int n=0;    int n=0;
   
         for (sc=FIRST(co); sc; sc=NEXT(sc))    for (sc=FIRST(co); sc; sc=NEXT(sc))
                 n++;      n++;
         return n;    return n;
 }  }
   
 /* Misc */  /* Misc */
Line 2201  F f,*pnf;
Line 2243  F f,*pnf;
 void (*client)();  void (*client)();
 pointer argv[];  pointer argv[];
 {  {
         if (AL_ATOMIC(FOP(f)))    if (AL_ATOMIC(FOP(f)))
                 (*client)(f,argv,pnf);      (*client)(f,argv,pnf);
         else if (AL_JUNCT(FOP(f))) {    else if (AL_JUNCT(FOP(f))) {
                 NODE sc,n=NULL,c;      NODE sc,n=NULL,c;
                 for (sc=FJARG(f); sc; sc=NEXT(sc)) {      for (sc=FJARG(f); sc; sc=NEXT(sc)) {
                         NEXTNODE(n,c);        NEXTNODE(n,c);
                         apply2ats(BDY(sc),client,argv,&BDY(c));        apply2ats(BDY(sc),client,argv,&BDY(c));
                 }      }
                 MKJF(*pnf,FOP(f),n);      MKJF(*pnf,FOP(f),n);
         }    }
         else if (AL_TVAL(FOP(f)))    else if (AL_TVAL(FOP(f)))
                 *pnf = f;      *pnf = f;
         else if (AL_QUANT(FOP(f))) {    else if (AL_QUANT(FOP(f))) {
                 F h;      F h;
                 apply2ats(FQMAT(f),client,argv,&h);      apply2ats(FQMAT(f),client,argv,&h);
                 MKQF(*pnf,FOP(f),FQVR(f),h);      MKQF(*pnf,FOP(f),FQVR(f),h);
         } else    } else
                 error("unknown operator in apply2ats");      error("unknown operator in apply2ats");
 }  }
   
 void atl(f,pn)  void atl(f,pn)
 F f;  F f;
 NODE *pn;  NODE *pn;
 {  {
         NODE c;    NODE c;
   
         *pn = NULL;    *pn = NULL;
         atl1(f,pn,&c);    atl1(f,pn,&c);
 }  }
   
 void atl1(f,pn,pc)  void atl1(f,pn,pc)
 F f;  F f;
 NODE *pn,*pc;  NODE *pn,*pc;
 {  {
         NODE sc;    NODE sc;
   
         if (AL_ATOMIC(FOP(f))) {    if (AL_ATOMIC(FOP(f))) {
                 simpl_gand_insert_a(f,pn,pc);      simpl_gand_insert_a(f,pn,pc);
                 return;      return;
         }    }
         if (AL_JUNCT(FOP(f)))    if (AL_JUNCT(FOP(f)))
                 for (sc=FJARG(f); sc; sc=NEXT(sc))      for (sc=FJARG(f); sc; sc=NEXT(sc))
                         atl1(BDY(sc),pn,pc);        atl1(BDY(sc),pn,pc);
 }  }
   
 void atnum(f,pn)  void atnum(f,pn)
 F f;  F f;
 Q *pn;  Q *pn;
 {  {
         *pn = 0;    *pn = 0;
         atnum1(f,pn);    atnum1(f,pn);
 }  }
   
 void atnum1(f,pn)  void atnum1(f,pn)
 F f;  F f;
 Q *pn;  Q *pn;
 {  {
         NODE sc;    NODE sc;
   
         if (AL_ATOMIC(FOP(f)))    if (AL_ATOMIC(FOP(f)))
                 addq(*pn,ONE,pn);      addq(*pn,ONE,pn);
         else if (AL_JUNCT(FOP(f)))    else if (AL_JUNCT(FOP(f)))
                 for (sc=FJARG(f); sc; sc=NEXT(sc))      for (sc=FJARG(f); sc; sc=NEXT(sc))
                         atnum1(BDY(sc),pn);        atnum1(BDY(sc),pn);
 }  }
   
 void pnegate(f,pnf)  void pnegate(f,pnf)
 F f,*pnf;  F f,*pnf;
 {  {
         F h;    F h;
         NODE sc,n=NULL,c;    NODE sc,n=NULL,c;
         oFOP op=FOP(f);    oFOP op=FOP(f);
   
         if (AL_QUANT(op)) {    if (AL_QUANT(op)) {
                 pnegate(FQMAT(f),&h);      pnegate(FQMAT(f),&h);
                 MKQF(*pnf,AL_LNEGOP(op),FQVR(f),h);      MKQF(*pnf,AL_LNEGOP(op),FQVR(f),h);
                 return;      return;
         }    }
         if (AL_JUNCT(op)) {    if (AL_JUNCT(op)) {
                 for (sc=FJARG(f); sc; sc=NEXT(sc)) {      for (sc=FJARG(f); sc; sc=NEXT(sc)) {
                         NEXTNODE(n,c);        NEXTNODE(n,c);
                         pnegate((F)BDY(sc),(F*)&BDY(c));        pnegate((F)BDY(sc),(F*)&BDY(c));
                 }      }
                 MKJF(*pnf,AL_LNEGOP(op),n);      MKJF(*pnf,AL_LNEGOP(op),n);
                 return;      return;
         }    }
         if (AL_ATOMIC(op)) {    if (AL_ATOMIC(op)) {
                 MKAF(*pnf,AL_LNEGOP(op),FPL(f));      MKAF(*pnf,AL_LNEGOP(op),FPL(f));
                 return;      return;
         }    }
         if (op == AL_TRUE) {    if (op == AL_TRUE) {
                 *pnf = F_FALSE;      *pnf = F_FALSE;
                 return;      return;
         }    }
         if (op == AL_FALSE) {    if (op == AL_FALSE) {
                 *pnf = F_TRUE;      *pnf = F_TRUE;
                 return;      return;
         }    }
         error("unknown operator in pnegate()");    error("unknown operator in pnegate()");
 }  }
   
 void subf(o,f,v,p,pf)  void subf(o,f,v,p,pf)
Line 2308  F f,*pf;
Line 2350  F f,*pf;
 V v;  V v;
 P p;  P p;
 {  {
         pointer argv[3];    pointer argv[3];
   
         argv[0] = (pointer)o;    argv[0] = (pointer)o;
         argv[1] = (pointer)v;    argv[1] = (pointer)v;
         argv[2] = (pointer)p;    argv[2] = (pointer)p;
         apply2ats(f,subf_a,argv,pf);    apply2ats(f,subf_a,argv,pf);
 }  }
   
 void subf_a(at,argv,pat)  void subf_a(at,argv,pat)
 F at,*pat;  F at,*pat;
 pointer argv[];  pointer argv[];
 {  {
         P nlhs;    P nlhs;
   
         substp((VL)argv[0],FPL(at),(V)argv[1],(P)argv[2],&nlhs);    substp((VL)argv[0],FPL(at),(V)argv[1],(P)argv[2],&nlhs);
         MKAF(*pat,FOP(at),nlhs);    MKAF(*pat,FOP(at),nlhs);
 }  }
   
 void nnf(f,pf)  void nnf(f,pf)
 F f,*pf;  F f,*pf;
 {  {
         nnf1(f,0,0,pf);    nnf1(f,0,0,pf);
 }  }
   
 void nnf1(f,neg,disj,pf)  void nnf1(f,neg,disj,pf)
 F f,*pf;  F f,*pf;
 int neg,disj;  int neg,disj;
 {  {
         F h;    F h;
         NODE sc,nargl=NULL,narglc;    NODE sc,nargl=NULL,narglc=NULL;
         oFOP op=FOP(f);    oFOP op=FOP(f);
   
         if (AL_ATOMIC(op) || AL_TVAL(op)) {    if (AL_ATOMIC(op) || AL_TVAL(op)) {
                 if (neg)      if (neg)
                         pnegate(f,pf);        pnegate(f,pf);
                 else      else
                         *pf = f;        *pf = f;
                 return;      return;
         }    }
         if (AL_JUNCT(op)) {    if (AL_JUNCT(op)) {
                 if (neg)      if (neg)
                         op = AL_LNEGOP(op);        op = AL_LNEGOP(op);
                 for (sc=FJARG(f); sc; sc=NEXT(sc)) {      for (sc=FJARG(f); sc; sc=NEXT(sc)) {
                         NEXTNODE(nargl,narglc);        NEXTNODE(nargl,narglc);
                         nnf1((F)BDY(sc),neg,op==AL_OR,(F*)&BDY(narglc));        nnf1((F)BDY(sc),neg,op==AL_OR,(F*)&BDY(narglc));
                 }      }
                 MKJF(*pf,op,nargl);      MKJF(*pf,op,nargl);
                 return;      return;
         }    }
         if (op == AL_IMPL) {    if (op == AL_IMPL) {
                 op = neg ? AL_AND : AL_OR;      op = neg ? AL_AND : AL_OR;
                 NEXTNODE(nargl,narglc);      NEXTNODE(nargl,narglc);
                 nnf1(FLHS(f),!neg,op==AL_OR,(F*)&BDY(narglc));      nnf1(FLHS(f),!neg,op==AL_OR,(F*)&BDY(narglc));
                 NEXTNODE(nargl,narglc);      NEXTNODE(nargl,narglc);
                 nnf1(FRHS(f),neg,op==AL_OR,(F*)&BDY(narglc));      nnf1(FRHS(f),neg,op==AL_OR,(F*)&BDY(narglc));
                 MKJF(*pf,op,nargl);      MKJF(*pf,op,nargl);
                 return;      return;
         }    }
         if (op == AL_REPL) {    if (op == AL_REPL) {
                 op = neg ? AL_AND : AL_OR;      op = neg ? AL_AND : AL_OR;
                 NEXTNODE(nargl,narglc);      NEXTNODE(nargl,narglc);
                 nnf1(FLHS(f),neg,op==AL_OR,(F*)&BDY(narglc));      nnf1(FLHS(f),neg,op==AL_OR,(F*)&BDY(narglc));
                 NEXTNODE(nargl,narglc);      NEXTNODE(nargl,narglc);
                 nnf1(FRHS(f),!neg,op==AL_OR,(F*)&BDY(narglc));      nnf1(FRHS(f),!neg,op==AL_OR,(F*)&BDY(narglc));
                 MKJF(*pf,op,nargl);      MKJF(*pf,op,nargl);
                 return;      return;
         }    }
         if (op == AL_EQUIV) {    if (op == AL_EQUIV) {
                 /* should consider disj and its arguments ops */      /* should consider disj and its arguments ops */
                 NEXTNODE(nargl,narglc);      NEXTNODE(nargl,narglc);
                 MKBF(h,AL_IMPL,FLHS(f),FRHS(f));      MKBF(h,AL_IMPL,FLHS(f),FRHS(f));
                 BDY(narglc) = (pointer)h;      BDY(narglc) = (pointer)h;
                 NEXTNODE(nargl,narglc);      NEXTNODE(nargl,narglc);
                 MKBF(h,AL_REPL,FLHS(f),FRHS(f));      MKBF(h,AL_REPL,FLHS(f),FRHS(f));
                 BDY(narglc) = (pointer)h;      BDY(narglc) = (pointer)h;
                 MKJF(h,AL_AND,nargl);      MKJF(h,AL_AND,nargl);
                 nnf1(h,neg,disj,pf);      nnf1(h,neg,disj,pf);
                 return;      return;
         }    }
         if (AL_QUANT(op)) {    if (AL_QUANT(op)) {
                 nnf1(FQMAT(f),neg,0,&h);      nnf1(FQMAT(f),neg,0,&h);
                 MKQF(*pf,neg ? AL_LNEGOP(op) : op,FQVR(f),h);      MKQF(*pf,neg ? AL_LNEGOP(op) : op,FQVR(f),h);
                 return;      return;
         }    }
         if (op == AL_NOT) {    if (op == AL_NOT) {
                 nnf1(FARG(f),!neg,disj,pf);      nnf1(FARG(f),!neg,disj,pf);
                 return;      return;
         }    }
         error("unknown operator in nnf1()");    error("unknown operator in nnf1()");
 }  }
   
 void freevars(f,pvl)  void freevars(f,pvl)
 F f;  F f;
 VL *pvl;  VL *pvl;
 {  {
         *pvl = NULL;    *pvl = NULL;
         freevars1(f,pvl,NULL);    freevars1(f,pvl,NULL);
 }  }
   
 void freevars1(f,pvl,cbvl)  void freevars1(f,pvl,cbvl)
 F f;  F f;
 VL *pvl,cbvl;  VL *pvl,cbvl;
 {  {
         VL hvl;    VL hvl;
         NODE sc;    NODE sc;
         oFOP op=FOP(f);    oFOP op=FOP(f);
   
         if (AL_ATOMIC(op)) {    if (AL_ATOMIC(op)) {
                 freevars1_a(f,pvl,cbvl);      freevars1_a(f,pvl,cbvl);
                 return;      return;
         }    }
         if (AL_JUNCT(op)) {    if (AL_JUNCT(op)) {
                 for (sc=FJARG(f); sc; sc=NEXT(sc))      for (sc=FJARG(f); sc; sc=NEXT(sc))
                         freevars1((F)BDY(sc),pvl,cbvl);        freevars1((F)BDY(sc),pvl,cbvl);
                 return;      return;
         }    }
         if (AL_QUANT(op)) {    if (AL_QUANT(op)) {
                 MKVL(hvl,FQVR(f),cbvl);      MKVL(hvl,FQVR(f),cbvl);
                 freevars1(FQMAT(f),pvl,hvl);      freevars1(FQMAT(f),pvl,hvl);
                 return;      return;
         }    }
         if (AL_UNI(op)) {    if (AL_UNI(op)) {
                 freevars1(FARG(f),pvl,cbvl);      freevars1(FARG(f),pvl,cbvl);
                 return;      return;
         }    }
         if (AL_EXT(op)) {    if (AL_EXT(op)) {
                 freevars1(FLHS(f),pvl,cbvl);      freevars1(FLHS(f),pvl,cbvl);
                 freevars1(FRHS(f),pvl,cbvl);      freevars1(FRHS(f),pvl,cbvl);
                 return;      return;
         }    }
         if (AL_TVAL(op))    if (AL_TVAL(op))
                 return;      return;
         error("unknown operator in freevars1()");    error("unknown operator in freevars1()");
 }  }
   
 void freevars1_a(f,pvl,cbvl)  void freevars1_a(f,pvl,cbvl)
 F f;  F f;
 VL *pvl,cbvl;  VL *pvl,cbvl;
 {  {
         VL sc,sc2,last;    VL sc,sc2,last;
   
         for (get_vars((Obj)FPL(f),&sc); sc; sc=NEXT(sc)) {    for (get_vars((Obj)FPL(f),&sc); sc; sc=NEXT(sc)) {
                 for(sc2=cbvl; sc2; sc2=NEXT(sc2))      for(sc2=cbvl; sc2; sc2=NEXT(sc2))
                         if (VR(sc) == VR(sc2))        if (VR(sc) == VR(sc2))
                                 break;          break;
                 if (sc2)      if (sc2)
                         continue;        continue;
                 if (!*pvl) {      if (!*pvl) {
                         MKVL(*pvl,VR(sc),NULL);        MKVL(*pvl,VR(sc),NULL);
                         continue;        continue;
                 }      }
                 for (sc2=*pvl; sc2; sc2=NEXT(sc2)) {      for (sc2=*pvl; sc2; sc2=NEXT(sc2)) {
                         if (VR(sc) == VR(sc2))        if (VR(sc) == VR(sc2))
                                 break;          break;
                         last = sc2;        last = sc2;
                 }      }
                 if (sc2)      if (sc2)
                         continue;        continue;
                 MKVL(NEXT(last),VR(sc),NULL);      MKVL(NEXT(last),VR(sc),NULL);
         }    }
 }  }
   
 int compf(vl,f1,f2)  int compf(vl,f1,f2)
 VL vl;  VL vl;
 F f1,f2;  F f1,f2;
 {  {
         if (AL_ATOMIC(FOP(f1)) && AL_ATOMIC(FOP(f2)))    if (AL_ATOMIC(FOP(f1)) && AL_ATOMIC(FOP(f2)))
                 return compaf(vl,f1,f2);      return compaf(vl,f1,f2);
         if (AL_ATOMIC(FOP(f1)))    if (AL_ATOMIC(FOP(f1)))
                 return 1;      return 1;
         if (AL_ATOMIC(FOP(f2)))    if (AL_ATOMIC(FOP(f2)))
                 return -1;      return -1;
         if (synequalf(f1,f2))    if (synequalf(f1,f2))
                 return 0;      return 0;
         return 2;    return 2;
 }  }
   
 /* Debug */  /* Debug */
Line 2490  F f1,f2;
Line 2532  F f1,f2;
 void ap(x)  void ap(x)
 pointer *x;  pointer *x;
 {  {
         printexpr(CO,(Obj)x);    printexpr(CO,(Obj)x);
         printf("\n");    printf("\n");
 }  }
   
 void rep(re)  void rep(re)
 RE re;  RE re;
 {  {
         printf("(");    printf("(");
         printexpr(CO,(Obj)PL(re));    printexpr(CO,(Obj)PL(re));
         printf(",");    printf(",");
         printexpr(CO,(Obj)DISC(re));    printexpr(CO,(Obj)DISC(re));
         printf(",");    printf(",");
         printf("%d)\n",re->itype);    printf("%d)\n",re->itype);
 }  }
   
 void gpp(gp)  void gpp(gp)
 GP gp;  GP gp;
 {  {
         ap(gp->g);    ap(gp->g);
         rep(gp->p);    rep(gp->p);
 }  }
   
 void esetp(eset)  void esetp(eset)
 NODE eset;  NODE eset;
 {  {
         NODE sc;    NODE sc;
   
         for (sc=eset; sc; sc=NEXT(sc))    for (sc=eset; sc; sc=NEXT(sc))
                 gpp(BDY(sc));      gpp(BDY(sc));
 }  }
   
 void nodep(n)  void nodep(n)
 NODE n;  NODE n;
 {  {
         NODE sc;    NODE sc;
   
         for (sc=n; sc; sc=NEXT(sc))    for (sc=n; sc; sc=NEXT(sc))
                 ap(BDY(sc));      ap(BDY(sc));
 }  }
   
 void lbfp(x)  void lbfp(x)
Line 2542  void thp(x)
Line 2584  void thp(x)
 NODE x;  NODE x;
 {  {
   if (x == NULL) {    if (x == NULL) {
          printf("[]\n");     printf("[]\n");
          return;     return;
   }    }
   printf("[");    printf("[");
   lbfp((LBF)BDY(x));    lbfp((LBF)BDY(x));
   x = NEXT(x);    x = NEXT(x);
   for (; x != NULL; x = NEXT(x)) {    for (; x != NULL; x = NEXT(x)) {
          printf(",");     printf(",");
          lbfp((LBF)BDY(x));     lbfp((LBF)BDY(x));
   }    }
   printf("]\n");    printf("]\n");
 }  }
Legend:
Removed from v.1.1  
changed lines
  Added in v.1.6
FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>