CVC3  2.4.1
Public Member Functions | Private Types | Private Member Functions | Private Attributes
CVC3::VCCmd Class Reference

#include <vc_cmd.h>

List of all members.

Public Member Functions

Private Types

Private Member Functions

Private Attributes


Member Typedef Documentation

typedef std::hash_map<const char*, Context*> CVC3::VCCmd::CtxtMap [private]

Definition at line 43 of file vc_cmd.h.


Constructor & Destructor Documentation

VCCmd::VCCmd ( ValidityChecker vc,
Parser parser,
bool  calledFromParser = false 
)

Definition at line 32 of file vc_cmd.cpp.

References d_map, d_name_of_cur_ctxt, d_vc, and CVC3::ValidityChecker::getCurrentContext().

VCCmd::~VCCmd ( )

Definition at line 39 of file vc_cmd.cpp.


Member Function Documentation

void VCCmd::printSymbols ( Expr  e,
ExprMap< bool > &  cache 
) [private]
bool VCCmd::evaluateCommand ( const Expr e) [private]

Take a parsed Expr and evaluate it.

Definition at line 267 of file vc_cmd.cpp.

References TRACE, CVC3::Expr::toString(), CVC3::PRESENTATION_LANG, RAW_LIST, ID, d_vc, CVC3::ValidityChecker::getEM(), CVC3::ExprManager::getKind(), NULL_KIND, CONST, CVC3::ValidityChecker::parseExpr(), CVC3::ValidityChecker::createOp(), CVC3::ValidityChecker::varExpr(), TRACE_MSG, DebugAssert, DEFUN, CVC3::ValidityChecker::listExpr(), TYPEDEF, CVC3::Expr::arity(), CVC3::ValidityChecker::dataType(), CVC3::ValidityChecker::createType(), TYPE, CVC3::Expr::begin(), ASSERT, CVC3::int2string(), CVC3::ValidityChecker::assertFormula(), QUERY, CVC3::ValidityChecker::query(), CVC3::UNKNOWN, CVC3::ValidityChecker::getFlags(), CVC3::ValidityChecker::tryModelGeneration(), reportResult(), CVC3::INVALID, printCounterExample(), printModel(), CHECKSAT, CVC3::ValidityChecker::checkUnsat(), CVC3::ValidityChecker::trueExpr(), CVC3::SATISFIABLE, CONTINUE, CVC3::ValidityChecker::checkContinue(), CVC3::VALID, std::endl(), CVC3::ABORT, IF_DEBUG, CVC3::ValidityChecker::incomplete(), FatalAssert, RESTART, CVC3::ValidityChecker::restart(), TRANSFORM, CVC3::ValidityChecker::simplify(), CVC3::ValidityChecker::printExpr(), PRINT, PUSH, POP, PUSH_SCOPE, POP_SCOPE, RATIONAL_EXPR, CVC3::ValidityChecker::push(), CVC3::ValidityChecker::stackLevel(), CVC3::ValidityChecker::pop(), CVC3::ValidityChecker::pushScope(), CVC3::ValidityChecker::scopeLevel(), CVC3::ValidityChecker::popScope(), POPTO, POPTO_SCOPE, CVC3::ValidityChecker::popto(), CVC3::ValidityChecker::poptoScope(), RESET, WHERE, ASSERTIONS, ASSUMPTIONS, CVC3::ValidityChecker::getAssumptions(), findAxioms(), CVC3::ExprMap::begin(), CVC3::ExprMap::end(), skolemizeAx(), COUNTEREXAMPLE, COUNTERMODEL, CVC3::Exception::toString(), UNTRACE, OPTION, CVC3::CLFlags::countFlags(), CVC3::CLFlag::modified(), CVC3::CLFlag::getType(), CVC3::CLFLAG_BOOL, CVC3::isRational(), CVC3::CLFlags::setFlag(), CVC3::CLFLAG_INT, CVC3::CLFLAG_STRING, CVC3::ValidityChecker::reprocessFlags(), GET_VALUE, CVC3::ValidityChecker::getConcreteModel(), CVC3::ValidityChecker::getValue(), GET_ASSIGNMENT, CVC3::ValidityChecker::getAssignment(), DUMP_PROOF, CVC3::ValidityChecker::getProof(), DUMP_ASSUMPTIONS, CVC3::ValidityChecker::inconsistent(), DUMP_TCC, CVC3::ValidityChecker::getTCC(), CVC3::Expr::isNull(), DUMP_TCC_ASSUMPTIONS, CVC3::ValidityChecker::getAssumptionsTCC(), DUMP_TCC_PROOF, CVC3::ValidityChecker::getProofTCC(), CVC3::Proof::isNull(), DUMP_CLOSURE, CVC3::ValidityChecker::getClosure(), DUMP_CLOSURE_PROOF, CVC3::ValidityChecker::getProofClosure(), ECHO, SEQ, ARITH_VAR_ORDER, CVC3::ValidityChecker::addPairToArithOrder(), ANNOTATION, CVC3::ValidityChecker::logAnnotation(), INCLUDE, CVC3::ValidityChecker::loadFile(), CVC3::ExprManager::getInputLang(), HELP, DUMP_SIG, DBG, SUBSTITUTE, GET_CHILD, GET_TYPE, CHECK_TYPE, FORGET, and CALL.

Referenced by evaluateNext().

bool VCCmd::evaluateNext ( ) [private]
void VCCmd::findAxioms ( const Expr e,
ExprMap< bool > &  skolemAxioms,
ExprMap< bool > &  visited 
) [private]
Expr VCCmd::skolemizeAx ( const Expr e) [private]
void VCCmd::reportResult ( QueryResult  qres,
bool  checkingValidity = true 
) [private]
void VCCmd::printModel ( ) [private]
void VCCmd::printCounterExample ( ) [private]
void VCCmd::processCommands ( )

Member Data Documentation

Definition at line 41 of file vc_cmd.h.

Referenced by evaluateNext(), and processCommands().

Definition at line 44 of file vc_cmd.h.

Referenced by VCCmd().

Definition at line 45 of file vc_cmd.h.

Referenced by VCCmd().

Definition at line 46 of file vc_cmd.h.

Referenced by processCommands().


The documentation for this class was generated from the following files: