kinds.h File Reference

Go to the source code of this file.

Enumerations

• enum Kind {
    NULL_KIND = 0, TRUE_EXPR = 1, FALSE_EXPR = 2, RATIONAL_EXPR = 3,
    STRING_EXPR = 4, MAX_CONST = 100, RAW_LIST, ID,
    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
  }

---

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.