CVC3
Enumerations

kinds.h File Reference

Go to the source code of this file.

Enumerations


Detailed Description

Author: Clark Barrett

Created: Mon Jan 20 13:38:52 2003


License to use, copy, modify, sell and/or distribute this software and its documentation for any purpose is hereby granted without royalty, subject to the terms and conditions defined in the LICENSE file provided with this distribution.


Definition in file kinds.h.


Enumeration Type Documentation

enum Kind
Enumerator:
NULL_KIND 
TRUE_EXPR 
FALSE_EXPR 
RATIONAL_EXPR 
STRING_EXPR 
MAX_CONST 
RAW_LIST 

May have any number of children >= 0

ID 

Identifier is (ID (STRING_EXPR "name"))

BOOLEAN 
ANY_TYPE 
ARROW 
TYPE 
TYPEDECL 
TYPEDEF 
EQ 
NEQ 
DISTINCT 
NOT 
AND 
OR 
XOR 
IFF 
IMPLIES 
AND_R 
IFF_R 
ITE_R 
ITE 
FORALL 
EXISTS 
UFUNC 
APPLY 
ASSERT 
QUERY 
CHECKSAT 
CONTINUE 
RESTART 
DBG 
TRACE 
UNTRACE 
OPTION 
HELP 
TRANSFORM 
PRINT 
CALL 
ECHO 
INCLUDE 
DUMP_PROOF 
DUMP_ASSUMPTIONS 
DUMP_SIG 
DUMP_TCC 
DUMP_TCC_ASSUMPTIONS 
DUMP_TCC_PROOF 
DUMP_CLOSURE 
DUMP_CLOSURE_PROOF 
WHERE 
ASSERTIONS 
ASSUMPTIONS 
COUNTEREXAMPLE 
COUNTERMODEL 
PUSH 
POP 
POPTO 
PUSH_SCOPE 
POP_SCOPE 
POPTO_SCOPE 
RESET 
CONTEXT 
FORGET 
GET_TYPE 
CHECK_TYPE 
GET_CHILD 
SUBSTITUTE 
SEQ 
ARITH_VAR_ORDER 
ANNOTATION 
TCC 
VARDECL 
VARDECLS 
BOUND_VAR 
BOUND_ID 
SUBTYPE 
IF 
IFTHEN 
ELSE 
COND 
LET 
LETDECLS 
LETDECL 
LAMBDA 
SIMULATE 
CONST 
VARLIST 
UCONST 
DEFUN 
PF_APPLY 
PF_HOLE 
SKOLEM_VAR 
THEOREM_KIND 
LAST_KIND 

Must always be the last kind.

Definition at line 31 of file kinds.h.