00001 /*****************************************************************************/ 00002 /*! 00003 * \file kinds.h 00004 * 00005 * Author: Clark Barrett 00006 * 00007 * Created: Mon Jan 20 13:38:52 2003 00008 * 00009 * <hr> 00010 * 00011 * License to use, copy, modify, sell and/or distribute this software 00012 * and its documentation for any purpose is hereby granted without 00013 * royalty, subject to the terms and conditions defined in the \ref 00014 * LICENSE file provided with this distribution. 00015 * 00016 * <hr> 00017 * 00018 */ 00019 /*****************************************************************************/ 00020 00021 #ifndef _cvc3__include__kinds_h_ 00022 #define _cvc3__include__kinds_h_ 00023 00024 namespace CVC3 { 00025 00026 // The commonly used kinds and the kinds needed by the parser. All 00027 // these kinds are registered by the ExprManager and are readily 00028 // available for everyone else. 00029 typedef enum { 00030 NULL_KIND = 0, 00031 // Generic LISP kinds for representing raw parsed expressions 00032 RAW_LIST, //!< May have any number of children >= 0 00033 //! Identifier is (ID (STRING_EXPR "name")) 00034 ID, 00035 // Leaf exprs 00036 STRING_EXPR, 00037 RATIONAL_EXPR, 00038 TRUE_EXPR, 00039 FALSE_EXPR, 00040 // Types 00041 BOOLEAN, 00042 // TUPLE_TYPE, 00043 ANY_TYPE, 00044 ARROW, 00045 // The "type" of any expression type (as in BOOLEAN : TYPE). 00046 TYPE, 00047 // Declaration of new (uninterpreted) types: T1, T2, ... : TYPE 00048 // (TYPEDECL T1 T2 ...) 00049 TYPEDECL, 00050 // Declaration of a defined type T : TYPE = type === (TYPEDEF T type) 00051 TYPEDEF, 00052 00053 // Equality 00054 EQ, 00055 NEQ, 00056 DISTINCT, 00057 00058 // Propositional connectives 00059 NOT, 00060 AND, 00061 OR, 00062 XOR, 00063 IFF, 00064 IMPLIES, 00065 // BOOL_VAR, //!< Boolean variables are treated as 0-ary predicates 00066 00067 // Propositional relations (for circuit propagation) 00068 AND_R, 00069 IFF_R, 00070 ITE_R, 00071 00072 // (ITE c e1 e2) == IF c THEN e1 ELSE e2 ENDIF, the internal 00073 // representation of the conditional. Parser produces (IF ...). 00074 ITE, 00075 00076 // Quantifiers 00077 FORALL, 00078 EXISTS, 00079 00080 // Uninterpreted function 00081 UFUNC, 00082 // Application of a function 00083 APPLY, 00084 00085 // Top-level Commands 00086 ASSERT, 00087 QUERY, 00088 CHECKSAT, 00089 CONTINUE, 00090 RESTART, 00091 DBG, 00092 TRACE, 00093 UNTRACE, 00094 OPTION, 00095 HELP, 00096 TRANSFORM, 00097 PRINT, 00098 CALL, 00099 ECHO, 00100 INCLUDE, 00101 DUMP_PROOF, 00102 DUMP_ASSUMPTIONS, 00103 DUMP_SIG, 00104 DUMP_TCC, 00105 DUMP_TCC_ASSUMPTIONS, 00106 DUMP_TCC_PROOF, 00107 DUMP_CLOSURE, 00108 DUMP_CLOSURE_PROOF, 00109 WHERE, 00110 ASSERTIONS, 00111 ASSUMPTIONS, 00112 COUNTEREXAMPLE, 00113 COUNTERMODEL, 00114 PUSH, 00115 POP, 00116 POPTO, 00117 PUSH_SCOPE, 00118 POP_SCOPE, 00119 POPTO_SCOPE, 00120 CONTEXT, 00121 FORGET, 00122 GET_TYPE, 00123 CHECK_TYPE, 00124 GET_CHILD, 00125 SUBSTITUTE, 00126 SEQ, 00127 00128 // Kinds used mostly in the parser 00129 00130 TCC, 00131 // Variable declaration (VARDECL v1 v2 ... v_n type). A variable 00132 // can be an ID or a BOUNDVAR. 00133 VARDECL, 00134 // A list of variable declarations (VARDECLS (VARDECL ...) (VARDECL ...) ...) 00135 VARDECLS, 00136 00137 // Bound variables have a "printable name", the one the user typed 00138 // in, and a uniqueID used to distinguish it from other bound 00139 // variables, which is effectively the alpha-renaming: 00140 00141 // Op(BOUND_VAR (BOUND_ID "user_name" "uniqueID")). Note that 00142 // BOUND_VAR is an operator (Expr without children), just as UFUNC 00143 // and UCONST. 00144 00145 // The uniqueID normally is just a number, so one can print a bound 00146 // variable X as X_17. 00147 00148 // NOTE that in the parsed expressions like LET x: T = e IN foo(x), 00149 // the second instance of 'x' will be an ID, and *not* a BOUNDVAR. 00150 // The parser does not know how to resolve bound variables, and it 00151 // has to be resolved later. 00152 BOUND_VAR, 00153 BOUND_ID, 00154 00155 // Updator "e1 WITH <bunch of stuff> := e2" is represented as 00156 // (UPDATE e1 (UPDATE_SELECT <bunch of stuff>) e2), where <bunch 00157 // of stuff> is the list of accessors: 00158 // (READ idx) 00159 // ID (what's that for?) 00160 // (REC_SELECT ID) 00161 // and (TUPLE_SELECT num). 00162 // UPDATE, 00163 // UPDATE_SELECT, 00164 // Record type [# f1 : t1, f2 : t2 ... #] is represented as 00165 // (RECORD_TYPE (f1 t1) (f2 t2) ... ) 00166 // RECORD_TYPE, 00167 // // (# f1=e1, f2=e2, ...#) == (RECORD (f1 e1) ...) 00168 // RECORD, 00169 // RECORD_SELECT, 00170 // RECORD_UPDATE, 00171 00172 // // (e1, e2, ...) == (TUPLE e1 e2 ...) 00173 // TUPLE, 00174 // TUPLE_SELECT, 00175 // TUPLE_UPDATE, 00176 00177 // SUBRANGE, 00178 // Enumerated type (SCALARTYPE v1 v2 ...) 00179 // SCALARTYPE, 00180 // Predicate subtype: the argument is the predicate (lambda-expression) 00181 SUBTYPE, 00182 // Datatype is Expr(DATATYPE, Constructors), where Constructors is a 00183 // vector of Expr(CONSTRUCTOR, id [ , arg ]), where 'id' is an ID, 00184 // and 'arg' a VARDECL node (list of variable declarations with 00185 // types). If 'arg' is present, the constructor has arguments 00186 // corresponding to the declared variables. 00187 // DATATYPE, 00188 // THISTYPE, // Used to indicate recursion in recursive datatypes 00189 // CONSTRUCTOR, 00190 // SELECTOR, 00191 // TESTER, 00192 // Expression e WITH accessor := e2 is transformed by the command 00193 // processor into (DATATYPE_UPDATE e accessor e2), where e is the 00194 // original datatype value C(a1, ..., an) (here C is the 00195 // constructor), and "accessor" is the name of one of the arguments 00196 // a_i of C. 00197 // DATATYPE_UPDATE, 00198 // Statement IF c1 THEN e1 ELSIF c2 THEN e2 ... ELSE e_n ENDIF is 00199 // represented as (IF (IFTHEN c1 e1) (IFTHEN c2 e2) ... (ELSE e_n)) 00200 IF, 00201 IFTHEN, 00202 ELSE, 00203 // Lisp version of multi-branch IF: 00204 // (COND (c1 e1) (c2 e2) ... (ELSE en)) 00205 COND, 00206 00207 // LET x1: t1 = e1, x2: t2 = e2, ... IN e 00208 // Parser builds: 00209 // (LET (LETDECLS (LETDECL x1 t1 e1) (LETDECL x2 t2 e2) ... ) e) 00210 // where each x_i is a BOUNDVAR. 00211 // After processing, it is rebuilt to have (LETDECL var def); the 00212 // type is set as the attribute to var. 00213 LET, 00214 LETDECLS, 00215 LETDECL, 00216 // Lambda-abstraction LAMBDA (<vars>) : e === (LAMBDA <vars> e) 00217 LAMBDA, 00218 // Symbolic simulation operator 00219 SIMULATE, 00220 00221 // Uninterpreted constants (variables) x1, x2, ... , x_n : type 00222 // (CONST (VARLIST x1 x2 ... x_n) type) 00223 // Uninterpreted functions are declared as constants of functional type. 00224 00225 // After processing, uninterpreted functions and constants 00226 // (a.k.a. variables) are represented as Op(UFUNC, (ID "name")) and 00227 // Op(UCONST, (ID "name")) with the appropriate type attribute. 00228 CONST, 00229 VARLIST, 00230 UCONST, 00231 00232 // User function definition f(args) : type = e === (DEFUN args type e) 00233 // Here 'args' are bound var declarations 00234 DEFUN, 00235 00236 // Arithmetic types and operators 00237 // REAL, 00238 // INT, 00239 00240 // UMINUS, 00241 // PLUS, 00242 // MINUS, 00243 // MULT, 00244 // DIVIDE, 00245 // INTDIV, 00246 // MOD, 00247 // LT, 00248 // LE, 00249 // GT, 00250 // GE, 00251 // IS_INTEGER, 00252 // NEGINF, 00253 // POSINF, 00254 // DARK_SHADOW, 00255 // GRAY_SHADOW, 00256 00257 // //Floor theory operators 00258 // FLOOR, 00259 // Kind for Extension to Non-linear Arithmetic 00260 // POW, 00261 00262 // Kinds for proof terms 00263 PF_APPLY, 00264 PF_HOLE, 00265 00266 00267 // // Mlss 00268 // EMPTY, // {} 00269 // UNION, // + 00270 // INTER, // * 00271 // DIFF, 00272 // SINGLETON, 00273 // IN, 00274 // INCS, 00275 // INCIN, 00276 00277 //Skolem variable 00278 SKOLEM_VAR, 00279 // Expr that holds a theorem 00280 THEOREM_KIND, 00281 //! Must always be the last kind 00282 LAST_KIND 00283 } Kind; 00284 00285 } // end of namespace CVC3 00286 00287 #endif