Return to al.h CVS log

Up to [local] / OpenXM_contrib2 / asir2000 / include

Annotation of OpenXM_contrib2/asir2000/include/al.h, Revision 1.1.1.1

1.1       noro        1: /* $OpenXM: OpenXM/src/asir99/include/al.h,v 1.1.1.1 1999/11/10 08:12:30 noro Exp $ */
                      2: /* ----------------------------------------------------------------------
                      3:    $Id: al.h,v 1.2 1998/12/08 16:23:05 sturm Exp $
                      4:    ----------------------------------------------------------------------
                      5:    File al.h: Real quantifier elimination code for RISA/ASIR
                      6:
                      7:    Copyright (c) 1996, 1997, 1998 by
                      8:    Andreas Dolzmann and Thomas Sturm, University of Passau, Germany
                      9:    dolzmann@uni-passau.de, sturm@uni-passau.de
                     10:    ----------------------------------------------------------------------
                     11: */
                     12:
                     13: /* Operator bitstrings: (qua, junct, bin, uni, atomic, x1, x2, x3)
                     14:    where x1, x3, x3 are
                     15:    atomic: direction, strict, order
                     16:    uni: -, -, -
                     17:    bin: direction, -, order
                     18:    junct: conjunctive, conjunctive, -
                     19:    qua: conjunctive, conjunctive, - */
                     20:
                     21: #define AL_TRUE 0x00
                     22: #define AL_FALSE 0x06
                     23: #define AL_EX 0x80
                     24: #define AL_ALL 0x86
                     25: #define AL_OR 0x40
                     26: #define AL_AND 0x46
                     27: #define AL_NOT 0x10
                     28: #define AL_IMPL 0x25
                     29: #define AL_REPL 0x21
                     30: #define AL_EQUIV 0x20
                     31:
                     32: #define AL_EQUAL 0x08
                     33: #define AL_NEQ 0x0E
                     34: #define AL_LESSP 0x0B
                     35: #define AL_GREATERP 0x0F
                     36: #define AL_LEQ 0x09
                     37: #define AL_GEQ 0x0D
                     38:
                     39: #define AL_QUANT(op) ((op) & 0x80)
                     40: #define AL_JUNCT(op) ((op) & 0x40)
                     41: #define AL_TVAL(op) (!((op) & 0xF9))
                     42: #define AL_UNI(op) ((op) & 0x10)
                     43: #define AL_EXT(op) ((op) & 0x20)
                     44: #define AL_ATOMIC(op) ((op) & 0x08)
                     45: #define AL_ORDER(op) ((op) & 0x01)
                     46: #define AL_ANEGREL(r) ((r) ^ 0x04)
                     47: #define AL_ANEGJUNCT(r) ((r) ^ 0x06)
                     48: #define AL_NEUTRAL(j) ((j) ^ 0x46)
                     49: #define AL_OMNIPOT(j) ((j) & 0x06)
                     50:
                     51: #define AL_MKSTRICT(op) ((op) | 0x02)
                     52: #define AL_LNEGOP(op) ((op) ^ 0x06)
                     53:
                     54: /* Formal lower bound: AL_GREATERP or AL_GEQ */
                     55: #define AL_FLB(rel) (rel == AL_GREATERP || rel == AL_GEQ)
                     56:
                     57: /* Transcendent substitution expansion:
                     58:    AL_EQUAL -> AL_AND, AL_NEQ -> AL_OR, used by subtrans_a_no */
                     59: #define AL_TRSUBEXP(no) ((no) ^ 0x4E)
                     60:
                     61:
                     62: /* Public Data Structures */
                     63:
                     64: /* #define O_F 14; defined in ca.h */
                     65:
                     66: #define LBFLB(x) ((x)->label)
                     67: #define LBFF(x) ((x)->formula)
                     68:
                     69: #define FOP(x) ((x)->op)
                     70:
                     71: #define FPL(x) ((x)->arg.faarg)
                     72: #define FARG(x) ((x)->arg.fuarg)
                     73: #define FJARG(x) ((x)->arg.fjarg)
                     74:
                     75: #define FBARG(x) ((x)->arg.fbarg)
                     76: #define FQARG(x) ((x)->arg.fqarg)
                     77:
                     78: #define FLHS(x) (FBARG(x)->lhs)
                     79: #define FRHS(x) (FBARG(x)->rhs)
                     80: #define FQVR(x) VR(FQARG(x))
                     81: #define MAT(x) ((x)->mat)
                     82: #define FQMAT(x) MAT(FQARG(x))
                     83:
                     84: #define NEWLBF(l) ((l)=(LBF)MALLOC(sizeof(struct oLBF)))
                     85: #define NEWF(f) ((f)=(F)MALLOC(sizeof(struct oF)),OID(f)=O_F)
                     86: #define NEWFQARG(x) ((x)=(FQARG)MALLOC(sizeof(struct oFQARG)))
                     87: #define NEWFBARG(x) ((x)=(FBARG)MALLOC(sizeof(struct oFBARG)))
                     88:
                     89: #define MKLBF(x,f,l) (NEWLBF(x),LBFF(x)=f,LBFLB(x)=l)
                     90: #define MKTV(f,tv) (NEWF(f),FOP(f)=tv,(f)->arg.dummy=0)
                     91: #define MKAF(f,r,p) (NEWF(f),FOP(f)=r,FPL(f)=p)
                     92: #define MKUF(f,op,arg) (NEWF(f),FOP(f)=op,FARG(f)=arg)
                     93: #define MKBF(f,op,lhs,rhs) \
                     94: (NEWF(f),FOP(f)=op,NEWFBARG(FBARG(f)),FLHS(f)=lhs,FRHS(f)=rhs)
                     95: #define MKJF(f,j,argl) (NEWF(f),FOP(f)=j,FJARG(f)=argl)
                     96: #define MKQF(f,q,var,m) \
                     97: (NEWF(f),FOP(f)=q,NEWFQARG(FQARG(f)),FQVR(f)=var,FQMAT(f)=m)
                     98:
                     99: typedef unsigned int oFOP;
                    100:
                    101: struct oF {
                    102:    short id;
                    103:    oFOP op;
                    104:    union {
                    105:       void *dummy;
                    106:       P faarg;
                    107:       struct oF *fuarg;
                    108:       struct oFBARG *fbarg;
                    109:       NODE fjarg;
                    110:       struct oFQARG *fqarg;
                    111:    } arg;
                    112: };
                    113:
                    114: typedef struct oF *F;
                    115:
                    116: struct oFBARG {
                    117:    F lhs;
                    118:    F rhs;
                    119: };
                    120:
                    121: typedef struct oFBARG *FBARG;
                    122:
                    123: struct oFQARG {
                    124:   V v;
                    125:   F mat;
                    126: };
                    127:
                    128: typedef struct oFQARG *FQARG;
                    129:
                    130: struct oLBF {
                    131:   F formula;
                    132:   int label;
                    133: };
                    134:
                    135: typedef struct oLBF *LBF;
                    136:
                    137: extern F F_TRUE;
                    138: extern F F_FALSE;
                    139: