CVC3
2.4.1
|
#include <vc_cmd.h>
typedef std::hash_map<const char*, Context*> CVC3::VCCmd::CtxtMap [private] |
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.
Print the symbols in e, cache results.
Definition at line 188 of file vc_cmd.cpp.
References CVC3::ExprMap::find(), CVC3::ExprMap::end(), CVC3::Expr::getKind(), SKOLEM_VAR, UCONST, d_vc, CVC3::ValidityChecker::getEM(), CVC3::ExprStream::dagFlag(), std::endl(), APPLY, CVC3::Expr::getOpExpr(), UFUNC, CVC3::Expr::begin(), and CVC3::Expr::end().
Referenced by printCounterExample().
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] |
Definition at line 73 of file vc_cmd.cpp.
References d_parser, CVC3::Parser::done(), TRACE_MSG, CVC3::Parser::next(), TRACE, std::endl(), IF_DEBUG, d_vc, CVC3::ValidityChecker::getFlags(), and evaluateCommand().
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::ExprMap::count(), CVC3::Expr::isSkolem(), CVC3::ExprMap::insert(), CVC3::Expr::getExistential(), CVC3::Expr::isClosure(), CVC3::Expr::getBody(), CVC3::Expr::arity(), CVC3::Expr::end(), and CVC3::Expr::begin().
Referenced by printCounterExample(), and evaluateCommand().
Definition at line 61 of file vc_cmd.cpp.
References CVC3::Expr::getVars(), CVC3::Expr::skolemExpr(), CVC3::Expr::getBody(), CVC3::Expr::substExpr(), and CVC3::Expr::iffExpr().
Referenced by printCounterExample(), and evaluateCommand().
void VCCmd::reportResult | ( | QueryResult | qres, |
bool | checkingValidity = true |
||
) | [private] |
Definition at line 102 of file vc_cmd.cpp.
References d_vc, CVC3::ValidityChecker::getFlags(), CVC3::ValidityChecker::getEM(), CVC3::ExprManager::getOutputLang(), CVC3::SMTLIB_LANG, CVC3::SMTLIB_V2_LANG, CVC3::VALID, std::endl(), CVC3::INVALID, CVC3::ABORT, CVC3::UNKNOWN, FatalAssert, IF_DEBUG, CVC3::ValidityChecker::incomplete(), and DebugAssert.
Referenced by evaluateCommand().
void VCCmd::printModel | ( | ) | [private] |
Definition at line 157 of file vc_cmd.cpp.
References d_vc, CVC3::ValidityChecker::getConcreteModel(), CVC3::ValidityChecker::scopeLevel(), std::endl(), CVC3::ExprMap::begin(), CVC3::ExprMap::end(), DebugAssert, and ASSERT.
Referenced by evaluateCommand().
void VCCmd::printCounterExample | ( | ) | [private] |
Definition at line 228 of file vc_cmd.cpp.
References d_vc, CVC3::ValidityChecker::getCounterExample(), printSymbols(), CVC3::ValidityChecker::scopeLevel(), std::endl(), ASSERT, findAxioms(), CVC3::ExprMap::end(), CVC3::ExprMap::begin(), and skolemizeAx().
Referenced by evaluateCommand().
void VCCmd::processCommands | ( | ) |
Definition at line 944 of file vc_cmd.cpp.
References evaluateNext(), d_calledFromParser, d_parser, CVC3::Parser::reset(), d_vc, CVC3::ValidityChecker::reset(), std::endl(), and CVC3::Parser::printLocation().
Referenced by CVC3::VCL::loadFile().
ValidityChecker* CVC3::VCCmd::d_vc [private] |
Definition at line 40 of file vc_cmd.h.
Referenced by VCCmd(), evaluateNext(), reportResult(), printModel(), printSymbols(), printCounterExample(), evaluateCommand(), and processCommands().
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] |
CtxtMap CVC3::VCCmd::d_map [private] |
bool CVC3::VCCmd::d_calledFromParser [private] |
Definition at line 46 of file vc_cmd.h.
Referenced by processCommands().