kinds.h File Reference

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Namespaces

• namespace CVC3

Enumerations

• enum CVC3::Kind {
    CVC3::NULL_KIND = 0, CVC3::TRUE_EXPR = 1, CVC3::FALSE_EXPR = 2, CVC3::RATIONAL_EXPR = 3,
    CVC3::STRING_EXPR = 4, CVC3::MAX_CONST = 100, CVC3::RAW_LIST, CVC3::ID,
    CVC3::BOOLEAN, CVC3::ANY_TYPE, CVC3::ARROW, CVC3::TYPE,
    CVC3::TYPEDECL, CVC3::TYPEDEF, CVC3::EQ, CVC3::NEQ,
    CVC3::DISTINCT, CVC3::NOT, CVC3::AND, CVC3::OR,
    CVC3::XOR, CVC3::IFF, CVC3::IMPLIES, CVC3::AND_R,
    CVC3::IFF_R, CVC3::ITE_R, CVC3::ITE, CVC3::FORALL,
    CVC3::EXISTS, CVC3::UFUNC, CVC3::APPLY, CVC3::ASSERT,
    CVC3::QUERY, CVC3::CHECKSAT, CVC3::CONTINUE, CVC3::RESTART,
    CVC3::DBG, CVC3::TRACE, CVC3::UNTRACE, CVC3::OPTION,
    CVC3::HELP, CVC3::TRANSFORM, CVC3::PRINT, CVC3::CALL,
    CVC3::ECHO, CVC3::INCLUDE, CVC3::DUMP_PROOF, CVC3::DUMP_ASSUMPTIONS,
    CVC3::DUMP_SIG, CVC3::DUMP_TCC, CVC3::DUMP_TCC_ASSUMPTIONS, CVC3::DUMP_TCC_PROOF,
    CVC3::DUMP_CLOSURE, CVC3::DUMP_CLOSURE_PROOF, CVC3::WHERE, CVC3::ASSERTIONS,
    CVC3::ASSUMPTIONS, CVC3::COUNTEREXAMPLE, CVC3::COUNTERMODEL, CVC3::PUSH,
    CVC3::POP, CVC3::POPTO, CVC3::PUSH_SCOPE, CVC3::POP_SCOPE,
    CVC3::POPTO_SCOPE, CVC3::RESET, CVC3::CONTEXT, CVC3::FORGET,
    CVC3::GET_TYPE, CVC3::CHECK_TYPE, CVC3::GET_CHILD, CVC3::SUBSTITUTE,
    CVC3::SEQ, CVC3::ARITH_VAR_ORDER, CVC3::TCC, CVC3::VARDECL,
    CVC3::VARDECLS, CVC3::BOUND_VAR, CVC3::BOUND_ID, CVC3::SUBTYPE,
    CVC3::IF, CVC3::IFTHEN, CVC3::ELSE, CVC3::COND,
    CVC3::LET, CVC3::LETDECLS, CVC3::LETDECL, CVC3::LAMBDA,
    CVC3::SIMULATE, CVC3::CONST, CVC3::VARLIST, CVC3::UCONST,
    CVC3::DEFUN, CVC3::PF_APPLY, CVC3::PF_HOLE, CVC3::SKOLEM_VAR,
    CVC3::THEOREM_KIND, CVC3::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.

---