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, GET_VALUE, GET_ASSIGNMENT,
    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
GET_VALUE
GET_ASSIGNMENT
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.