kinds.h

Go to the documentation of this file.
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

Generated on Tue Jul 3 14:33:37 2007 for CVC3 by  doxygen 1.5.1