CVC3::VCCmd Class Reference

#include <vc_cmd.h>

Collaboration diagram for CVC3::VCCmd:

[legend]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

• ValidityChecker * d_vc
• Parser * d_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]

Print the symbols in e, cache results.

Definition at line 183 of file vc_cmd.cpp.

References CVC3::APPLY, CVC3::Expr::begin(), d_vc, CVC3::Expr::end(), CVC3::ExprMap< Data >::end(), std::endl(), CVC3::ExprMap< Data >::find(), CVC3::ValidityChecker::getEM(), CVC3::Type::getExpr(), CVC3::Expr::getKind(), CVC3::Expr::getOpExpr(), CVC3::Expr::getType(), CVC3::SKOLEM_VAR, CVC3::UCONST, and CVC3::UFUNC.

Referenced by printCounterExample().

bool VCCmd::evaluateCommand

(

const Expr &

e

)

[private]

Take a parsed Expr and evaluate it.

Definition at line 262 of file vc_cmd.cpp.

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

Referenced by evaluateNext().

bool VCCmd::evaluateNext

(

)

[private]

Definition at line 73 of file vc_cmd.cpp.

References d_parser, CVC3::Parser::done(), std::endl(), evaluateCommand(), IF_DEBUG, CVC3::Parser::next(), CVC3::TRACE, and TRACE_MSG.

Referenced by processCommands().

void VCCmd::findAxioms	(	const Expr &	e,
		ExprMap< bool > &	skolemAxioms,
		ExprMap< bool > &	visited
	)			[private]

Definition at line 41 of file vc_cmd.cpp.

References CVC3::Expr::arity(), CVC3::Expr::begin(), CVC3::ExprMap< Data >::count(), CVC3::Expr::end(), CVC3::Expr::getBody(), CVC3::Expr::getExistential(), CVC3::ExprMap< Data >::insert(), CVC3::Expr::isClosure(), and CVC3::Expr::isSkolem().

Referenced by evaluateCommand(), and printCounterExample().

Expr VCCmd::skolemizeAx

(

const Expr &

e

)

[private]

Definition at line 61 of file vc_cmd.cpp.

References CVC3::Expr::getBody(), CVC3::Expr::getVars(), CVC3::Expr::iffExpr(), CVC3::Expr::skolemExpr(), and CVC3::Expr::substExpr().

Referenced by evaluateCommand(), and printCounterExample().

void VCCmd::reportResult	(	QueryResult	qres,
		bool	checkingValidity = true
	)			[private]

Definition at line 98 of file vc_cmd.cpp.

References CVC3::ABORT, d_vc, DebugAssert, std::endl(), FatalAssert, CVC3::ValidityChecker::getEM(), CVC3::ValidityChecker::getFlags(), CVC3::ExprManager::getOutputLang(), IF_DEBUG, CVC3::ValidityChecker::incomplete(), CVC3::INVALID, CVC3::SMTLIB_LANG, CVC3::UNKNOWN, and CVC3::VALID.

Referenced by evaluateCommand().

void VCCmd::printModel

(

)

[private]

Definition at line 152 of file vc_cmd.cpp.

References CVC3::ASSERT, CVC3::ExprMap< Data >::begin(), d_vc, DebugAssert, CVC3::ExprMap< Data >::end(), std::endl(), CVC3::ValidityChecker::getConcreteModel(), and CVC3::ValidityChecker::scopeLevel().

Referenced by evaluateCommand().

void VCCmd::printCounterExample

(

)

[private]

Definition at line 223 of file vc_cmd.cpp.

References CVC3::ASSERT, CVC3::ExprMap< Data >::begin(), d_vc, CVC3::ExprMap< Data >::end(), std::endl(), findAxioms(), CVC3::ValidityChecker::getCounterExample(), printSymbols(), CVC3::ValidityChecker::scopeLevel(), and skolemizeAx().

Referenced by evaluateCommand().

void VCCmd::processCommands

(

)

Definition at line 893 of file vc_cmd.cpp.

References d_calledFromParser, d_parser, d_vc, std::endl(), evaluateNext(), CVC3::Parser::printLocation(), CVC3::ValidityChecker::reset(), and CVC3::Parser::reset().

Referenced by CVC3::VCL::loadFile().

---

Member Data Documentation

ValidityChecker* CVC3::VCCmd::d_vc [private]

Definition at line 40 of file vc_cmd.h.

Referenced by evaluateCommand(), printCounterExample(), printModel(), printSymbols(), processCommands(), reportResult(), and VCCmd().

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:

• vc_cmd.h
• vc_cmd.cpp

---