Annotation of OpenXM_contrib2/asir2018/include/al.h, Revision 1.1
1.1 ! 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
! 26: * e-mail at risa-admin@sec.flab.fujitsu.co.jp of the detailed specification
! 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: *
! 48: * $OpenXM$
! 49: */
! 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>