Annotation of OpenXM_contrib2/asir2000/include/al.h, Revision 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:
FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>