expr_manager.cpp File Reference

#include "expr_manager.h"
#include "command_line_flags.h"
#include "expr_stream.h"
#include "pretty_printer.h"
#include "memory_manager_malloc.h"
#include "memory_manager_chunks.h"

Include dependency graph for expr_manager.cpp:

Go to the source code of this file.

Defines

• #define REG(k)   em.newKind(k, #k)
• #define REG_TYPE(k)   em.newKind(k, #k, true)

Functions

• static void registerKinds (ExprManager &em)

---

Detailed Description

Author: Sergey Berezin

Created: Wed Dec 4 14:20:56 2002

---

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 expr_manager.cpp.

---

Define Documentation

#define REG

(

k

)

em.newKind(k, #k)

Definition at line 490 of file expr_manager.cpp.

#define REG_TYPE

(

k

)

em.newKind(k, #k, true)

Definition at line 491 of file expr_manager.cpp.

---

Function Documentation

static void registerKinds

(

ExprManager &

em

)

[static]

Definition at line 493 of file expr_manager.cpp.

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

Referenced by CVC3::ExprManager::ExprManager().

---