CVCL::VCCmd Class Reference

#include <vc_cmd.h>

Collaboration diagram for CVCL::VCCmd:

[legend]List of all members.

Public Member Functions

• VCCmd (ValidityChecker *vc, Parser *parser)
• ~VCCmd ()
• void processCommands ()

Private Types

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

Private Member Functions

• bool evaluateCommand (const Expr &e) throw (Exception)

  Take a parsed Expr and evaluate it.
  

• bool evaluateNext () throw (Exception)
• void findAxioms (const Expr &e, ExprMap< bool > &skolemAxioms, ExprMap< bool > &visited)
• Expr skolemizeAx (const Expr &e)
• void reportResult (bool ret, bool checkingValidity=true)

Private Attributes

• ValidityChecker * d_vc
• Parser * d_parser
• std::string d_name_of_cur_ctxt
• CtxtMap d_map

---

Detailed Description

Definition at line 46 of file vc_cmd.h.

---

Member Typedef Documentation

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

Definition at line 50 of file vc_cmd.h.

---

Constructor & Destructor Documentation

VCCmd::VCCmd (  ValidityChecker *  vc, Parser *  parser )

Definition at line 40 of file vc_cmd.cpp. References d_map, d_name_of_cur_ctxt, d_vc, and CVCL::ValidityChecker::getCurrentContext().

VCCmd::~VCCmd (   )

Definition at line 46 of file vc_cmd.cpp.

---

Member Function Documentation

bool VCCmd::evaluateCommand (  const Expr &  e  )  throw (Exception) [private]

Take a parsed Expr and evaluate it. Definition at line 134 of file vc_cmd.cpp. References CVCL::Expr::arity(), CVCL::ASSERT, CVCL::ASSERTIONS, CVCL::ASSUMPTIONS, CVCL::ExprMap< Data >::begin(), CVCL::Expr::begin(), CVCL::CHECK_TYPE, CVCL::CHECKSAT, CVCL::CLFLAG_BOOL, CVCL::CLFLAG_INT, CVCL::CLFLAG_STRING, CVCL::CONST, CVCL::CONTINUE, CVCL::COUNTEREXAMPLE, CVCL::COUNTERMODEL, CVCL::CLFlags::countFlags(), CVCL::DBG, CVCL::debugger, CVCL::DEFUN, CVCL::DUMP_ASSUMPTIONS, CVCL::DUMP_CLOSURE, CVCL::DUMP_CLOSURE_PROOF, CVCL::DUMP_PROOF, CVCL::DUMP_SIG, CVCL::DUMP_TCC, CVCL::DUMP_TCC_ASSUMPTIONS, CVCL::DUMP_TCC_PROOF, CVCL::ECHO, CVCL::ExprMap< Data >::end(), CVCL::Expr::end(), std::endl(), CVCL::Expr::eqExpr(), CVCL::GET_CHILD, CVCL::GET_TYPE, CVCL::Rational::getInt(), CVCL::Expr::getKids(), CVCL::Expr::getKind(), CVCL::Expr::getRational(), CVCL::Expr::getString(), CVCL::CLFlag::getType(), CVCL::HELP, CVCL::ID, CVCL::INCLUDE, CVCL::int2string(), CVCL::Type::isFunction(), CVCL::Rational::isInteger(), CVCL::Proof::isNull(), CVCL::Expr::isNull(), CVCL::Expr::isRational(), CVCL::Expr::isString(), CVCL::CLFlag::modified(), CVCL::NULL_KIND, CVCL::OPTION, CVCL::POP, CVCL::POP_SCOPE, CVCL::POPTO, CVCL::POPTO_SCOPE, CVCL::PRINT, CVCL::PUSH, CVCL::PUSH_SCOPE, CVCL::QUERY, CVCL::RATIONAL_EXPR, CVCL::RAW_LIST, CVCL::RESTART, CVCL::SEQ, CVCL::CLFlags::setFlag(), CVCL::SUBSTITUTE, CVCL::Expr::toString(), CVCL::TRACE, CVCL::Debug::traceFlag(), CVCL::TRANSFORM, CVCL::TYPE, CVCL::TYPEDEF, CVCL::UNTRACE, and CVCL::WHERE. Referenced by evaluateNext().

bool VCCmd::evaluateNext (   )  throw (Exception) [private]

Definition at line 80 of file vc_cmd.cpp. References CVCL::ASSERT, CVCL::CONST, CVCL::CONSTDEF, CVCL::Debug::counter(), d_parser, d_vc, CVCL::debugger, CVCL::Parser::done(), std::endl(), evaluateCommand(), CVCL::ValidityChecker::getFlags(), CVCL::Expr::getKind(), IF_DEBUG(), CVCL::Expr::isNull(), CVCL::Parser::next(), CVCL::QUERY, CVCL::TRACE, CVCL::TRANSFORM, CVCL::TYPEDECL, and CVCL::TYPEDEF. Referenced by processCommands().

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

Definition at line 48 of file vc_cmd.cpp. References CVCL::Expr::arity(), CVCL::Expr::begin(), CVCL::ExprMap< Data >::count(), CVCL::Expr::end(), CVCL::Expr::getBody(), CVCL::Expr::getExistential(), CVCL::ExprMap< Data >::insert(), CVCL::Expr::isClosure(), and CVCL::Expr::isSkolem().

Expr VCCmd::skolemizeAx (  const Expr &  e  )  [private]

Definition at line 68 of file vc_cmd.cpp. References CVCL::Expr::getBody(), CVCL::Expr::getVars(), CVCL::Expr::iffExpr(), CVCL::Expr::skolemExpr(), and CVCL::Expr::substExpr().

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

Definition at line 114 of file vc_cmd.cpp. References d_vc, std::endl(), CVCL::ValidityChecker::getFlags(), and CVCL::ValidityChecker::incomplete().

void VCCmd::processCommands (   )

Definition at line 689 of file vc_cmd.cpp. References d_parser, std::endl(), evaluateNext(), and CVCL::Parser::printLocation().

---

Member Data Documentation

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

Definition at line 47 of file vc_cmd.h. Referenced by evaluateNext(), reportResult(), and VCCmd().

Parser* CVCL::VCCmd::d_parser [private]

Definition at line 48 of file vc_cmd.h. Referenced by evaluateNext(), and processCommands().

std::string CVCL::VCCmd::d_name_of_cur_ctxt [private]

Definition at line 51 of file vc_cmd.h. Referenced by VCCmd().

CtxtMap CVCL::VCCmd::d_map [private]

Definition at line 52 of file vc_cmd.h. Referenced by VCCmd().

---

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

• vc_cmd.h
• vc_cmd.cpp

---