[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.1.1 and 1.5

version 1.1.1.1, 1999/12/03 07:39:07 version 1.5, 2001/10/09 01:36:04
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.4 2001/03/09 01:14:13 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 rootno;
         int itype;          int itype;
 };  };
   
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 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)) {
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) {
Line 1250  int *pleft,*pmodulus;
Line 1259  int *pleft,*pmodulus;
         int i=0;          int i=0;
   
         if (!Verbose)          if (!Verbose)
                 return;          /* added by noro */
                   return 0;
         if (*pleft == 0) {          if (*pleft == 0) {
                 for (; cvl; cvl=NEXT(cvl))                  for (; cvl; cvl=NEXT(cvl))
                         i++;                          i++;
Line 1352  NODE *peset;
Line 1362  NODE *peset;
                                 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;
Line 1393  Q deg;
Line 1403  Q deg;
         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;
 {  {
Line 1403  NODE *peset;
Line 1413  NODE *peset;
         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;  
         F hf;  
         GP hgp;          GP hgp;
         P discr;          NODE esetc=NULL;
         NODE esetc;  
   
         *peset = NULL;          *peset = NULL;
         if (!NUM(a)) {          if (!NUM(a)) {
Line 1420  NODE *peset;
Line 1427  NODE *peset;
                 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) {
                   NEXT(nvlc) = NEXT(vl);
                   *pnvl = nvl;
                   return 1;
           }
           *pnvl = nvl;
         return 0;          return 0;
 }  }
   
Line 1448  V x;
Line 1463  V x;
 NODE trans[];  NODE trans[];
 {  {
         NODE sc,transc[8];          NODE sc,transc[8];
         RE hre;  
         GP hgp;  
         int bt,w=0;          int bt,w=0;
         P h;  
   
         for (bt=BTMIN; bt<=BTMAX; bt++)          for (bt=BTMIN; bt<=BTMAX; bt++)
                 trans[bt] = NULL;                  trans[bt] = NULL;
Line 1482  NODE trans[],transc[];
Line 1494  NODE 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 1508  GP *pgp;
Line 1522  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);
 }  }
Line 1529  NODE trans[],transc[];
Line 1543  NODE 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;
Line 1600  V v;
Line 1615  V v;
                 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;
 {  {
Line 1656  void mkeset(trans,x,peset)
Line 1671  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;
Line 1670  V x;
Line 1685  V x;
                 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;
         }          }
Line 1733  NODE n1a,n1b,n2a,n2b;
Line 1748  NODE n1a,n1b,n2a,n2b;
 void add2eset(trfield,peset,pesetc)  void add2eset(trfield,peset,pesetc)
 NODE trfield,*peset,*pesetc;  NODE trfield,*peset,*pesetc;
 {  {
           NODE ntrfield,ntrfieldc;
   
         if (trfield == NULL)          if (trfield == NULL)
                 return;                  return;
         if (*peset == NULL)          seproots(trfield,&ntrfield,&ntrfieldc);
                 *peset = *pesetc = trfield;          if (*peset == NULL) {
         else                  *peset = ntrfield;
                 NEXT(*pesetc) = trfield;                  *pesetc = ntrfieldc;
         while (NEXT(*pesetc))          } else {
                 *pesetc = NEXT(*pesetc);                  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;
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);
Line 1812  V v;
Line 1859  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);
Line 1844  RE re;
Line 1891  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);          getrecoeffs(prem,fdeg,re,&a,&b,&c,&ld);
         NEXTNODE(d,dc);          if (ROOTNO(re) == 1)
         substd_a21(op,a,b,c,ld,&hf);            chsgnp(b,&b);
         BDY(dc) = (pointer)hf;          else if (ROOTNO(re) != 2)
         NEXTNODE(d,dc);            error("unspecified quadratic root in substd_a2");
         chsgnp(b,&b);          substd_a21(op,a,b,c,ld,pf);
         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 1895  P a,b,c,d;
Line 1937  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);
Line 1917  P a,b,c,d;
Line 1959  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);
Line 1953  P a,b,c,d;
Line 1995  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);
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));
Line 2042  F *pnf;
Line 2084  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);
Line 2113  RE r;
Line 2155  RE r;
         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);
 }  }
   
Line 2126  F *pnf;
Line 2168  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);
Line 2337  F f,*pf;
Line 2379  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)) {
Legend:
Removed from v.1.1.1.1  
changed lines
  Added in v.1.5
FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>