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:
FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>