CVC3

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