CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
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,
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
Generated on Thu Jul 19 2012 08:17:22 for CVC3 by
1.8.1.1