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

 VCCmd (ValidityChecker *vc, Parser *parser, bool calledFromParser=false)
 ~VCCmd ()
void processCommands ()

Private Types

typedef std::hash_map< const
char *, Context * > 
CtxtMap

Private Member Functions

void printSymbols (Expr e, ExprMap< bool > &cache)
 Print the symbols in e, cache results.
bool evaluateCommand (const Expr &e)
 Take a parsed Expr and evaluate it.
bool evaluateNext ()
void findAxioms (const Expr &e, ExprMap< bool > &skolemAxioms, ExprMap< bool > &visited)
Expr skolemizeAx (const Expr &e)
void reportResult (QueryResult qres, bool checkingValidity=true)
void printModel ()
void printCounterExample ()

Private Attributes

ValidityCheckerd_vc
Parserd_parser
std::string d_name_of_cur_ctxt
CtxtMap d_map
bool d_calledFromParser

Detailed Description

Definition at line 39 of file vc_cmd.h.


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

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

ValidityChecker* CVC3::VCCmd::d_vc
private
Parser* CVC3::VCCmd::d_parser
private

Definition at line 41 of file vc_cmd.h.

Referenced by evaluateNext(), and processCommands().

std::string CVC3::VCCmd::d_name_of_cur_ctxt
private

Definition at line 44 of file vc_cmd.h.

Referenced by VCCmd().

CtxtMap CVC3::VCCmd::d_map
private

Definition at line 45 of file vc_cmd.h.

Referenced by VCCmd().

bool CVC3::VCCmd::d_calledFromParser
private

Definition at line 46 of file vc_cmd.h.

Referenced by processCommands().


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