1 /*****************************************************************************/ 2 /*! 3 * \file kinds.h 4 * 5 * Author: Clark Barrett 6 * 7 * Created: Mon Jan 20 13:38:52 2003 8 * 9 * <hr> 10 * 11 * License to use, copy, modify, sell and/or distribute this software 12 * and its documentation for any purpose is hereby granted without 13 * royalty, subject to the terms and conditions defined in the \ref 14 * LICENSE file provided with this distribution. 15 * 16 * <hr> 17 * 18 */ 19 /*****************************************************************************/ 20 21 #ifndef _cvc3__include__kinds_h_ 22 #define _cvc3__include__kinds_h_ 23 24 #ifdef __cplusplus 25 namespace CVC3 { 26 #endif /* __cplusplus */ 27 28 // The commonly used kinds and the kinds needed by the parser. All 29 // these kinds are registered by the ExprManager and are readily 30 // available for everyone else. 31 typedef enum { 32 NULL_KIND = 0, 33 34 // Constant (Leaf) Exprs 35 TRUE_EXPR = 1, 36 FALSE_EXPR = 2, 37 RATIONAL_EXPR = 3, 38 STRING_EXPR = 4, 39 40 // All constants should have kinds less than MAX_CONST 41 MAX_CONST = 100, 42 43 // Generic LISP kinds for representing raw parsed expressions 44 RAW_LIST, //!< May have any number of children >= 0 45 //! Identifier is (ID (STRING_EXPR "name")) 46 ID, 47 // Types 48 BOOLEAN, 49 // TUPLE_TYPE, 50 ANY_TYPE, 51 ARROW, 52 // The "type" of any expression type (as in BOOLEAN : TYPE). 53 TYPE, 54 // Declaration of new (uninterpreted) types: T1, T2, ... : TYPE 55 // (TYPEDECL T1 T2 ...) 56 TYPEDECL, 57 // Declaration of a defined type T : TYPE = type === (TYPEDEF T type) 58 TYPEDEF, 59 60 // Equality 61 EQ, 62 NEQ, 63 DISTINCT, 64 65 // Propositional connectives 66 NOT, 67 AND, 68 OR, 69 XOR, 70 IFF, 71 IMPLIES, 72 // BOOL_VAR, //!< Boolean variables are treated as 0-ary predicates 73 74 // Propositional relations (for circuit propagation) 75 AND_R, 76 IFF_R, 77 ITE_R, 78 79 // (ITE c e1 e2) == IF c THEN e1 ELSE e2 ENDIF, the internal 80 // representation of the conditional. Parser produces (IF ...). 81 ITE, 82 83 // Quantifiers 84 FORALL, 85 EXISTS, 86 87 // Uninterpreted function 88 UFUNC, 89 // Application of a function 90 APPLY, 91 92 // Top-level Commands 93 ASSERT, 94 QUERY, 95 CHECKSAT, 96 CONTINUE, 97 RESTART, 98 DBG, 99 TRACE, 100 UNTRACE, 101 OPTION, 102 HELP, 103 TRANSFORM, 104 PRINT, 105 CALL, 106 ECHO, 107 INCLUDE, 108 GET_VALUE, 109 GET_ASSIGNMENT, 110 DUMP_PROOF, 111 DUMP_ASSUMPTIONS, 112 DUMP_SIG, 113 DUMP_TCC, 114 DUMP_TCC_ASSUMPTIONS, 115 DUMP_TCC_PROOF, 116 DUMP_CLOSURE, 117 DUMP_CLOSURE_PROOF, 118 WHERE, 119 ASSERTIONS, 120 ASSUMPTIONS, 121 COUNTEREXAMPLE, 122 COUNTERMODEL, 123 PUSH, 124 POP, 125 POPTO, 126 PUSH_SCOPE, 127 POP_SCOPE, 128 POPTO_SCOPE, 129 RESET, 130 CONTEXT, 131 FORGET, 132 GET_TYPE, 133 CHECK_TYPE, 134 GET_CHILD, 135 SUBSTITUTE, 136 SEQ, 137 ARITH_VAR_ORDER, 138 ANNOTATION, 139 140 // Kinds used mostly in the parser 141 142 TCC, 143 // Variable declaration (VARDECL v1 v2 ... v_n type). A variable 144 // can be an ID or a BOUNDVAR. 145 VARDECL, 146 // A list of variable declarations (VARDECLS (VARDECL ...) (VARDECL ...) ...) 147 VARDECLS, 148 149 // Bound variables have a "printable name", the one the user typed 150 // in, and a uniqueID used to distinguish it from other bound 151 // variables, which is effectively the alpha-renaming: 152 153 // Op(BOUND_VAR (BOUND_ID "user_name" "uniqueID")). Note that 154 // BOUND_VAR is an operator (Expr without children), just as UFUNC 155 // and UCONST. 156 157 // The uniqueID normally is just a number, so one can print a bound 158 // variable X as X_17. 159 160 // NOTE that in the parsed expressions like LET x: T = e IN foo(x), 161 // the second instance of 'x' will be an ID, and *not* a BOUNDVAR. 162 // The parser does not know how to resolve bound variables, and it 163 // has to be resolved later. 164 BOUND_VAR, 165 BOUND_ID, 166 167 // Updator "e1 WITH <bunch of stuff> := e2" is represented as 168 // (UPDATE e1 (UPDATE_SELECT <bunch of stuff>) e2), where <bunch 169 // of stuff> is the list of accessors: 170 // (READ idx) 171 // ID (what's that for?) 172 // (REC_SELECT ID) 173 // and (TUPLE_SELECT num). 174 // UPDATE, 175 // UPDATE_SELECT, 176 // Record type [# f1 : t1, f2 : t2 ... #] is represented as 177 // (RECORD_TYPE (f1 t1) (f2 t2) ... ) 178 // RECORD_TYPE, 179 // // (# f1=e1, f2=e2, ...#) == (RECORD (f1 e1) ...) 180 // RECORD, 181 // RECORD_SELECT, 182 // RECORD_UPDATE, 183 184 // // (e1, e2, ...) == (TUPLE e1 e2 ...) 185 // TUPLE, 186 // TUPLE_SELECT, 187 // TUPLE_UPDATE, 188 189 // SUBRANGE, 190 // Enumerated type (SCALARTYPE v1 v2 ...) 191 // SCALARTYPE, 192 // Predicate subtype: the argument is the predicate (lambda-expression) 193 SUBTYPE, 194 // Datatype is Expr(DATATYPE, Constructors), where Constructors is a 195 // vector of Expr(CONSTRUCTOR, id [ , arg ]), where 'id' is an ID, 196 // and 'arg' a VARDECL node (list of variable declarations with 197 // types). If 'arg' is present, the constructor has arguments 198 // corresponding to the declared variables. 199 // DATATYPE, 200 // THISTYPE, // Used to indicate recursion in recursive datatypes 201 // CONSTRUCTOR, 202 // SELECTOR, 203 // TESTER, 204 // Expression e WITH accessor := e2 is transformed by the command 205 // processor into (DATATYPE_UPDATE e accessor e2), where e is the 206 // original datatype value C(a1, ..., an) (here C is the 207 // constructor), and "accessor" is the name of one of the arguments 208 // a_i of C. 209 // DATATYPE_UPDATE, 210 // Statement IF c1 THEN e1 ELSIF c2 THEN e2 ... ELSE e_n ENDIF is 211 // represented as (IF (IFTHEN c1 e1) (IFTHEN c2 e2) ... (ELSE e_n)) 212 IF, 213 IFTHEN, 214 ELSE, 215 // Lisp version of multi-branch IF: 216 // (COND (c1 e1) (c2 e2) ... (ELSE en)) 217 COND, 218 219 // LET x1: t1 = e1, x2: t2 = e2, ... IN e 220 // Parser builds: 221 // (LET (LETDECLS (LETDECL x1 t1 e1) (LETDECL x2 t2 e2) ... ) e) 222 // where each x_i is a BOUNDVAR. 223 // After processing, it is rebuilt to have (LETDECL var def); the 224 // type is set as the attribute to var. 225 LET, 226 LETDECLS, 227 LETDECL, 228 // Lambda-abstraction LAMBDA (<vars>) : e === (LAMBDA <vars> e) 229 LAMBDA, 230 // Symbolic simulation operator 231 SIMULATE, 232 233 // Uninterpreted constants (variables) x1, x2, ... , x_n : type 234 // (CONST (VARLIST x1 x2 ... x_n) type) 235 // Uninterpreted functions are declared as constants of functional type. 236 237 // After processing, uninterpreted functions and constants 238 // (a.k.a. variables) are represented as Op(UFUNC, (ID "name")) and 239 // Op(UCONST, (ID "name")) with the appropriate type attribute. 240 CONST, 241 VARLIST, 242 UCONST, 243 244 // User function definition f(args) : type = e === (DEFUN args type e) 245 // Here 'args' are bound var declarations 246 DEFUN, 247 248 // Arithmetic types and operators 249 // REAL, 250 // INT, 251 252 // UMINUS, 253 // PLUS, 254 // MINUS, 255 // MULT, 256 // DIVIDE, 257 // INTDIV, 258 // MOD, 259 // LT, 260 // LE, 261 // GT, 262 // GE, 263 // IS_INTEGER, 264 // NEGINF, 265 // POSINF, 266 // DARK_SHADOW, 267 // GRAY_SHADOW, 268 269 // //Floor theory operators 270 // FLOOR, 271 // Kind for Extension to Non-linear Arithmetic 272 // POW, 273 274 // Kinds for proof terms 275 PF_APPLY, 276 PF_HOLE, 277 278 279 // // Mlss 280 // EMPTY, // {} 281 // UNION, // + 282 // INTER, // * 283 // DIFF, 284 // SINGLETON, 285 // IN, 286 // INCS, 287 // INCIN, 288 289 //Skolem variable 290 SKOLEM_VAR, 291 // Expr that holds a theorem 292 THEOREM_KIND, 293 //! Must always be the last kind 294 LAST_KIND 295 } Kind; 296 297 #ifdef __cplusplus 298 } // end of namespace CVC3 299 #endif /* __cplusplus */ 300 301 #endif 302