CVC3
2.4.1
|
#include <vc_cmd.h>
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. More... | |
bool | evaluateCommand (const Expr &e) |
Take a parsed Expr and evaluate it. More... | |
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 |
|
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 APPLY, CVC3::Expr::begin(), d_vc, CVC3::ExprStream::dagFlag(), CVC3::ExprMap< Data >::end(), CVC3::Expr::end(), std::endl(), CVC3::ExprMap< Data >::find(), CVC3::ValidityChecker::getEM(), CVC3::Expr::getKind(), CVC3::Expr::getOpExpr(), SKOLEM_VAR, UCONST, and UFUNC.
Referenced by printCounterExample().
|
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().
|
private |
Definition at line 73 of file vc_cmd.cpp.
References d_parser, d_vc, CVC3::Parser::done(), std::endl(), evaluateCommand(), CVC3::ValidityChecker::getFlags(), IF_DEBUG, CVC3::Parser::next(), TRACE, and TRACE_MSG.
Referenced by processCommands().
|
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().
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().
|
private |
Definition at line 102 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::SMTLIB_V2_LANG, CVC3::UNKNOWN, and CVC3::VALID.
Referenced by evaluateCommand().
|
private |
Definition at line 157 of file vc_cmd.cpp.
References ASSERT, CVC3::ExprMap< Data >::begin(), d_vc, DebugAssert, CVC3::ExprMap< Data >::end(), std::endl(), CVC3::ValidityChecker::getConcreteModel(), and CVC3::ValidityChecker::scopeLevel().
Referenced by evaluateCommand().
|
private |
Definition at line 228 of file vc_cmd.cpp.
References 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 944 of file vc_cmd.cpp.
References d_calledFromParser, d_parser, d_vc, std::endl(), evaluateNext(), CVC3::Parser::printLocation(), CVC3::Parser::reset(), and CVC3::ValidityChecker::reset().
Referenced by CVC3::VCL::loadFile().
|
private |
Definition at line 40 of file vc_cmd.h.
Referenced by evaluateCommand(), evaluateNext(), printCounterExample(), printModel(), printSymbols(), processCommands(), reportResult(), and VCCmd().
|
private |
Definition at line 41 of file vc_cmd.h.
Referenced by evaluateNext(), and processCommands().
|
private |
|
private |
Definition at line 46 of file vc_cmd.h.
Referenced by processCommands().