Annotation of OpenXM_contrib2/asir2000/include/al.h, Revision 1.3
1.2 noro 1: /*
2: * Copyright (c) 1994-2000 FUJITSU LABORATORIES LIMITED
3: * All rights reserved.
4: *
5: * FUJITSU LABORATORIES LIMITED ("FLL") hereby grants you a limited,
6: * non-exclusive and royalty-free license to use, copy, modify and
7: * redistribute, solely for non-commercial and non-profit purposes, the
8: * computer program, "Risa/Asir" ("SOFTWARE"), subject to the terms and
9: * conditions of this Agreement. For the avoidance of doubt, you acquire
10: * only a limited right to use the SOFTWARE hereunder, and FLL or any
11: * third party developer retains all rights, including but not limited to
12: * copyrights, in and to the SOFTWARE.
13: *
14: * (1) FLL does not grant you a license in any way for commercial
15: * purposes. You may use the SOFTWARE only for non-commercial and
16: * non-profit purposes only, such as academic, research and internal
17: * business use.
18: * (2) The SOFTWARE is protected by the Copyright Law of Japan and
19: * international copyright treaties. If you make copies of the SOFTWARE,
20: * with or without modification, as permitted hereunder, you shall affix
21: * to all such copies of the SOFTWARE the above copyright notice.
22: * (3) An explicit reference to this SOFTWARE and its copyright owner
23: * shall be made on your publication or presentation in any form of the
24: * results obtained by use of the SOFTWARE.
25: * (4) In the event that you modify the SOFTWARE, you shall notify FLL by
1.3 ! noro 26: * e-mail at risa-admin@sec.flab.fujitsu.co.jp of the detailed specification
1.2 noro 27: * for such modification or the source code of the modified part of the
28: * SOFTWARE.
29: *
30: * THE SOFTWARE IS PROVIDED AS IS WITHOUT ANY WARRANTY OF ANY KIND. FLL
31: * MAKES ABSOLUTELY NO WARRANTIES, EXPRESSED, IMPLIED OR STATUTORY, AND
32: * EXPRESSLY DISCLAIMS ANY IMPLIED WARRANTY OF MERCHANTABILITY, FITNESS
33: * FOR A PARTICULAR PURPOSE OR NONINFRINGEMENT OF THIRD PARTIES'
34: * RIGHTS. NO FLL DEALER, AGENT, EMPLOYEES IS AUTHORIZED TO MAKE ANY
35: * MODIFICATIONS, EXTENSIONS, OR ADDITIONS TO THIS WARRANTY.
36: * UNDER NO CIRCUMSTANCES AND UNDER NO LEGAL THEORY, TORT, CONTRACT,
37: * OR OTHERWISE, SHALL FLL BE LIABLE TO YOU OR ANY OTHER PERSON FOR ANY
38: * DIRECT, INDIRECT, SPECIAL, INCIDENTAL, PUNITIVE OR CONSEQUENTIAL
39: * DAMAGES OF ANY CHARACTER, INCLUDING, WITHOUT LIMITATION, DAMAGES
40: * ARISING OUT OF OR RELATING TO THE SOFTWARE OR THIS AGREEMENT, DAMAGES
41: * FOR LOSS OF GOODWILL, WORK STOPPAGE, OR LOSS OF DATA, OR FOR ANY
42: * DAMAGES, EVEN IF FLL SHALL HAVE BEEN INFORMED OF THE POSSIBILITY OF
43: * SUCH DAMAGES, OR FOR ANY CLAIM BY ANY OTHER PARTY. EVEN IF A PART
44: * OF THE SOFTWARE HAS BEEN DEVELOPED BY A THIRD PARTY, THE THIRD PARTY
45: * DEVELOPER SHALL HAVE NO LIABILITY IN CONNECTION WITH THE USE,
46: * PERFORMANCE OR NON-PERFORMANCE OF THE SOFTWARE.
47: *
1.3 ! noro 48: * $OpenXM: OpenXM_contrib2/asir2000/include/al.h,v 1.2 2000/08/21 08:31:36 noro Exp $
1.2 noro 49: */
1.1 noro 50: /* ----------------------------------------------------------------------
51: $Id: al.h,v 1.2 1998/12/08 16:23:05 sturm Exp $
52: ----------------------------------------------------------------------
53: File al.h: Real quantifier elimination code for RISA/ASIR
54:
55: Copyright (c) 1996, 1997, 1998 by
56: Andreas Dolzmann and Thomas Sturm, University of Passau, Germany
57: dolzmann@uni-passau.de, sturm@uni-passau.de
58: ----------------------------------------------------------------------
59: */
60:
61: /* Operator bitstrings: (qua, junct, bin, uni, atomic, x1, x2, x3)
62: where x1, x3, x3 are
63: atomic: direction, strict, order
64: uni: -, -, -
65: bin: direction, -, order
66: junct: conjunctive, conjunctive, -
67: qua: conjunctive, conjunctive, - */
68:
69: #define AL_TRUE 0x00
70: #define AL_FALSE 0x06
71: #define AL_EX 0x80
72: #define AL_ALL 0x86
73: #define AL_OR 0x40
74: #define AL_AND 0x46
75: #define AL_NOT 0x10
76: #define AL_IMPL 0x25
77: #define AL_REPL 0x21
78: #define AL_EQUIV 0x20
79:
80: #define AL_EQUAL 0x08
81: #define AL_NEQ 0x0E
82: #define AL_LESSP 0x0B
83: #define AL_GREATERP 0x0F
84: #define AL_LEQ 0x09
85: #define AL_GEQ 0x0D
86:
87: #define AL_QUANT(op) ((op) & 0x80)
88: #define AL_JUNCT(op) ((op) & 0x40)
89: #define AL_TVAL(op) (!((op) & 0xF9))
90: #define AL_UNI(op) ((op) & 0x10)
91: #define AL_EXT(op) ((op) & 0x20)
92: #define AL_ATOMIC(op) ((op) & 0x08)
93: #define AL_ORDER(op) ((op) & 0x01)
94: #define AL_ANEGREL(r) ((r) ^ 0x04)
95: #define AL_ANEGJUNCT(r) ((r) ^ 0x06)
96: #define AL_NEUTRAL(j) ((j) ^ 0x46)
97: #define AL_OMNIPOT(j) ((j) & 0x06)
98:
99: #define AL_MKSTRICT(op) ((op) | 0x02)
100: #define AL_LNEGOP(op) ((op) ^ 0x06)
101:
102: /* Formal lower bound: AL_GREATERP or AL_GEQ */
103: #define AL_FLB(rel) (rel == AL_GREATERP || rel == AL_GEQ)
104:
105: /* Transcendent substitution expansion:
106: AL_EQUAL -> AL_AND, AL_NEQ -> AL_OR, used by subtrans_a_no */
107: #define AL_TRSUBEXP(no) ((no) ^ 0x4E)
108:
109:
110: /* Public Data Structures */
111:
112: /* #define O_F 14; defined in ca.h */
113:
114: #define LBFLB(x) ((x)->label)
115: #define LBFF(x) ((x)->formula)
116:
117: #define FOP(x) ((x)->op)
118:
119: #define FPL(x) ((x)->arg.faarg)
120: #define FARG(x) ((x)->arg.fuarg)
121: #define FJARG(x) ((x)->arg.fjarg)
122:
123: #define FBARG(x) ((x)->arg.fbarg)
124: #define FQARG(x) ((x)->arg.fqarg)
125:
126: #define FLHS(x) (FBARG(x)->lhs)
127: #define FRHS(x) (FBARG(x)->rhs)
128: #define FQVR(x) VR(FQARG(x))
129: #define MAT(x) ((x)->mat)
130: #define FQMAT(x) MAT(FQARG(x))
131:
132: #define NEWLBF(l) ((l)=(LBF)MALLOC(sizeof(struct oLBF)))
133: #define NEWF(f) ((f)=(F)MALLOC(sizeof(struct oF)),OID(f)=O_F)
134: #define NEWFQARG(x) ((x)=(FQARG)MALLOC(sizeof(struct oFQARG)))
135: #define NEWFBARG(x) ((x)=(FBARG)MALLOC(sizeof(struct oFBARG)))
136:
137: #define MKLBF(x,f,l) (NEWLBF(x),LBFF(x)=f,LBFLB(x)=l)
138: #define MKTV(f,tv) (NEWF(f),FOP(f)=tv,(f)->arg.dummy=0)
139: #define MKAF(f,r,p) (NEWF(f),FOP(f)=r,FPL(f)=p)
140: #define MKUF(f,op,arg) (NEWF(f),FOP(f)=op,FARG(f)=arg)
141: #define MKBF(f,op,lhs,rhs) \
142: (NEWF(f),FOP(f)=op,NEWFBARG(FBARG(f)),FLHS(f)=lhs,FRHS(f)=rhs)
143: #define MKJF(f,j,argl) (NEWF(f),FOP(f)=j,FJARG(f)=argl)
144: #define MKQF(f,q,var,m) \
145: (NEWF(f),FOP(f)=q,NEWFQARG(FQARG(f)),FQVR(f)=var,FQMAT(f)=m)
146:
147: typedef unsigned int oFOP;
148:
149: struct oF {
150: short id;
151: oFOP op;
152: union {
153: void *dummy;
154: P faarg;
155: struct oF *fuarg;
156: struct oFBARG *fbarg;
157: NODE fjarg;
158: struct oFQARG *fqarg;
159: } arg;
160: };
161:
162: typedef struct oF *F;
163:
164: struct oFBARG {
165: F lhs;
166: F rhs;
167: };
168:
169: typedef struct oFBARG *FBARG;
170:
171: struct oFQARG {
172: V v;
173: F mat;
174: };
175:
176: typedef struct oFQARG *FQARG;
177:
178: struct oLBF {
179: F formula;
180: int label;
181: };
182:
183: typedef struct oLBF *LBF;
184:
185: extern F F_TRUE;
186: extern F F_FALSE;
187:
FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>
![[BACK]](/icons/cvsweb/back.gif){kind=icon}
Return to al.h CVS log ![[TXT]](/icons/cvsweb/text.gif){kind=icon}
![[DIR]](/icons/cvsweb/dir.gif){kind=icon}
Up to [local] / OpenXM_contrib2 / asir2000 / include