CVC3
kinds.h
Go to the documentation of this file.
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,
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
49 // TUPLE_TYPE,
52  // The "type" of any expression type (as in BOOLEAN : TYPE).
54  // Declaration of new (uninterpreted) types: T1, T2, ... : TYPE
55  // (TYPEDECL T1 T2 ...)
57  // Declaration of a defined type T : TYPE = type === (TYPEDEF T type)
59 
60  // Equality
61  EQ,
62  NEQ,
64 
65  // Propositional connectives
66  NOT,
67  AND,
68  OR,
69  XOR,
70  IFF,
72  // BOOL_VAR, //!< Boolean variables are treated as 0-ary predicates
73 
74  // Propositional relations (for circuit propagation)
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
86 
87  // Uninterpreted function
89  // Application of a function
91 
92  // Top-level Commands
98  DBG,
139 
140  // Kinds used mostly in the parser
141 
143  // Variable declaration (VARDECL v1 v2 ... v_n type). A variable
144  // can be an ID or a BOUNDVAR.
146  // A list of variable declarations (VARDECLS (VARDECL ...) (VARDECL ...) ...)
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.
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)
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,
215  // Lisp version of multi-branch IF:
216  // (COND (c1 e1) (c2 e2) ... (ELSE en))
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.
228  // Lambda-abstraction LAMBDA (<vars>) : e === (LAMBDA <vars> e)
230  // Symbolic simulation operator
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.
243 
244  // User function definition f(args) : type = e === (DEFUN args type e)
245  // Here 'args' are bound var declarations
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
277 
278 
279 // // Mlss
280 // EMPTY, // {}
281 // UNION, // +
282 // INTER, // *
283 // DIFF,
284 // SINGLETON,
285 // IN,
286 // INCS,
287 // INCIN,
288 
289  //Skolem variable
291  // Expr that holds a theorem
293  //! Must always be the last kind
295 } Kind;
296 
297 #ifdef __cplusplus
298 } // end of namespace CVC3
299 #endif /* __cplusplus */
300 
301 #endif