<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: CVC3::VCCmd Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="inherits.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a></li><li class="navelem"><a class="el" href="classCVC3_1_1VCCmd.html">VCCmd</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="summary">
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-types">Private Types</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> |
<a href="classCVC3_1_1VCCmd-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">CVC3::VCCmd Class Reference</div> </div>
</div><!--header-->
<div class="contents">
<p><code>#include <<a class="el" href="vc__cmd_8h_source.html">vc_cmd.h</a>></code></p>
<div class="dynheader">
Collaboration diagram for CVC3::VCCmd:</div>
<div class="dyncontent">
<div class="center"><img src="classCVC3_1_1VCCmd__coll__graph.gif" border="0" usemap="#CVC3_1_1VCCmd_coll__map" alt="Collaboration graph"/></div>
<map name="CVC3_1_1VCCmd_coll__map" id="CVC3_1_1VCCmd_coll__map">
</map>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-methods"></a>
Public Member Functions</h2></td></tr>
<tr class="memitem:a889460a65419467468f7c5596e24171e"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#a889460a65419467468f7c5596e24171e">VCCmd</a> (<a class="el" href="classCVC3_1_1ValidityChecker.html">ValidityChecker</a> *<a class="el" href="main_8cpp.html#a88136d6dfceb0dedcb0b781a65423d54">vc</a>, <a class="el" href="classCVC3_1_1Parser.html">Parser</a> *parser, bool calledFromParser=false)</td></tr>
<tr class="separator:a889460a65419467468f7c5596e24171e"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aaba0fefb641158646bbcecd4c2b6f2fa"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#aaba0fefb641158646bbcecd4c2b6f2fa">~VCCmd</a> ()</td></tr>
<tr class="separator:aaba0fefb641158646bbcecd4c2b6f2fa"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ababcd4001adfc005ef5f2f365c61b829"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#ababcd4001adfc005ef5f2f365c61b829">processCommands</a> ()</td></tr>
<tr class="separator:ababcd4001adfc005ef5f2f365c61b829"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-types"></a>
Private Types</h2></td></tr>
<tr class="memitem:a6e02bca439dd43541e625c068a28622e"><td class="memItemLeft" align="right" valign="top">typedef <a class="el" href="classHash_1_1hash__map.html">std::hash_map</a>< const <br class="typebreak"/>
char *, <a class="el" href="classCVC3_1_1Context.html">Context</a> * > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#a6e02bca439dd43541e625c068a28622e">CtxtMap</a></td></tr>
<tr class="separator:a6e02bca439dd43541e625c068a28622e"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-methods"></a>
Private Member Functions</h2></td></tr>
<tr class="memitem:a51224d58ef1ab1978f31329033125446"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#a51224d58ef1ab1978f31329033125446">printSymbols</a> (<a class="el" href="classCVC3_1_1Expr.html">Expr</a> e, <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > &cache)</td></tr>
<tr class="memdesc:a51224d58ef1ab1978f31329033125446"><td class="mdescLeft"> </td><td class="mdescRight">Print the symbols in e, cache results. <a href="#a51224d58ef1ab1978f31329033125446"></a><br/></td></tr>
<tr class="separator:a51224d58ef1ab1978f31329033125446"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a96635f3d29f02b608309f9d7c6517ecd"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#a96635f3d29f02b608309f9d7c6517ecd">evaluateCommand</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:a96635f3d29f02b608309f9d7c6517ecd"><td class="mdescLeft"> </td><td class="mdescRight">Take a parsed <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> and evaluate it. <a href="#a96635f3d29f02b608309f9d7c6517ecd"></a><br/></td></tr>
<tr class="separator:a96635f3d29f02b608309f9d7c6517ecd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a60dcaba75f518a16dec9314df3aff161"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#a60dcaba75f518a16dec9314df3aff161">evaluateNext</a> ()</td></tr>
<tr class="separator:a60dcaba75f518a16dec9314df3aff161"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a04c3244b2ead42f4eeb22b3cf8c6d9a8"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#a04c3244b2ead42f4eeb22b3cf8c6d9a8">findAxioms</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > &skolemAxioms, <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > &visited)</td></tr>
<tr class="separator:a04c3244b2ead42f4eeb22b3cf8c6d9a8"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a165e689c23949794ce77632e15d3821d"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#a165e689c23949794ce77632e15d3821d">skolemizeAx</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="separator:a165e689c23949794ce77632e15d3821d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad61f2528e834203b51ff974f5212a26b"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#ad61f2528e834203b51ff974f5212a26b">reportResult</a> (<a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> qres, bool checkingValidity=true)</td></tr>
<tr class="separator:ad61f2528e834203b51ff974f5212a26b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1997d265d49f31e9624ab3f28a33d79f"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#a1997d265d49f31e9624ab3f28a33d79f">printModel</a> ()</td></tr>
<tr class="separator:a1997d265d49f31e9624ab3f28a33d79f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a0dbc7765ccb1aeaf5265ae5894330c8a"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#a0dbc7765ccb1aeaf5265ae5894330c8a">printCounterExample</a> ()</td></tr>
<tr class="separator:a0dbc7765ccb1aeaf5265ae5894330c8a"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-attribs"></a>
Private Attributes</h2></td></tr>
<tr class="memitem:aa43a0dbed5026bca03502570f6a491ef"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1ValidityChecker.html">ValidityChecker</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#aa43a0dbed5026bca03502570f6a491ef">d_vc</a></td></tr>
<tr class="separator:aa43a0dbed5026bca03502570f6a491ef"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:acd57eff603dc4690dee1ed25415167aa"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Parser.html">Parser</a> * </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#acd57eff603dc4690dee1ed25415167aa">d_parser</a></td></tr>
<tr class="separator:acd57eff603dc4690dee1ed25415167aa"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a83ac968536314974e45519a222d00dfa"><td class="memItemLeft" align="right" valign="top">std::string </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#a83ac968536314974e45519a222d00dfa">d_name_of_cur_ctxt</a></td></tr>
<tr class="separator:a83ac968536314974e45519a222d00dfa"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a5e2f199c7aa4aa087215828af54c5c90"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1VCCmd.html#a6e02bca439dd43541e625c068a28622e">CtxtMap</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#a5e2f199c7aa4aa087215828af54c5c90">d_map</a></td></tr>
<tr class="separator:a5e2f199c7aa4aa087215828af54c5c90"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a12a174396e81593ac1da765ef922559a"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1VCCmd.html#a12a174396e81593ac1da765ef922559a">d_calledFromParser</a></td></tr>
<tr class="separator:a12a174396e81593ac1da765ef922559a"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="vc__cmd_8h_source.html#l00039">39</a> of file <a class="el" href="vc__cmd_8h_source.html">vc_cmd.h</a>.</p>
</div><h2 class="groupheader">Member Typedef Documentation</h2>
<a class="anchor" id="a6e02bca439dd43541e625c068a28622e"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">typedef <a class="el" href="classHash_1_1hash__map.html">std::hash_map</a><const char*, <a class="el" href="classCVC3_1_1Context.html">Context</a>*> <a class="el" href="classCVC3_1_1VCCmd.html#a6e02bca439dd43541e625c068a28622e">CVC3::VCCmd::CtxtMap</a></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="vc__cmd_8h_source.html#l00043">43</a> of file <a class="el" href="vc__cmd_8h_source.html">vc_cmd.h</a>.</p>
</div>
</div>
<h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="a889460a65419467468f7c5596e24171e"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">VCCmd::VCCmd </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ValidityChecker.html">ValidityChecker</a> * </td>
<td class="paramname"><em>vc</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Parser.html">Parser</a> * </td>
<td class="paramname"><em>parser</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>calledFromParser</em> = <code>false</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="vc__cmd_8cpp_source.html#l00032">32</a> of file <a class="el" href="vc__cmd_8cpp_source.html">vc_cmd.cpp</a>.</p>
<p>References <a class="el" href="vc__cmd_8h_source.html#l00045">d_map</a>, <a class="el" href="vc__cmd_8h_source.html#l00044">d_name_of_cur_ctxt</a>, <a class="el" href="vc__cmd_8h_source.html#l00040">d_vc</a>, and <a class="el" href="classCVC3_1_1ValidityChecker.html#aebd7d6618f53f20bb08d091f624277cf">CVC3::ValidityChecker::getCurrentContext()</a>.</p>
</div>
</div>
<a class="anchor" id="aaba0fefb641158646bbcecd4c2b6f2fa"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">VCCmd::~VCCmd </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="vc__cmd_8cpp_source.html#l00039">39</a> of file <a class="el" href="vc__cmd_8cpp_source.html">vc_cmd.cpp</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="a51224d58ef1ab1978f31329033125446"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void VCCmd::printSymbols </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > & </td>
<td class="paramname"><em>cache</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Print the symbols in e, cache results. </p>
<p>Definition at line <a class="el" href="vc__cmd_8cpp_source.html#l00188">188</a> of file <a class="el" href="vc__cmd_8cpp_source.html">vc_cmd.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00090">APPLY</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="vc__cmd_8h_source.html#l00040">d_vc</a>, <a class="el" href="expr__stream_8h_source.html#l00175">CVC3::ExprStream::dagFlag()</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a448e0df25ec6d756861e7d1d217f1063">CVC3::ValidityChecker::getEM()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01191">CVC3::Expr::getOpExpr()</a>, <a class="el" href="kinds_8h_source.html#l00290">SKOLEM_VAR</a>, <a class="el" href="kinds_8h_source.html#l00242">UCONST</a>, and <a class="el" href="kinds_8h_source.html#l00088">UFUNC</a>.</p>
<p>Referenced by <a class="el" href="vc__cmd_8cpp_source.html#l00228">printCounterExample()</a>.</p>
</div>
</div>
<a class="anchor" id="a96635f3d29f02b608309f9d7c6517ecd"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool VCCmd::evaluateCommand </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Take a parsed <a class="el" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> and evaluate it. </p>
<p>Definition at line <a class="el" href="vc__cmd_8cpp_source.html#l00267">267</a> of file <a class="el" href="vc__cmd_8cpp_source.html">vc_cmd.cpp</a>.</p>
<p>References <a class="el" href="queryresult_8h_source.html#l00037">CVC3::ABORT</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a56eb352f856ddbad57c5d59386c6b707">CVC3::ValidityChecker::addPairToArithOrder()</a>, <a class="el" href="kinds_8h_source.html#l00138">ANNOTATION</a>, <a class="el" href="kinds_8h_source.html#l00137">ARITH_VAR_ORDER</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="kinds_8h_source.html#l00093">ASSERT</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#ad57f0a783141d3c7b0424102ea8724ac">CVC3::ValidityChecker::assertFormula()</a>, <a class="el" href="kinds_8h_source.html#l00119">ASSERTIONS</a>, <a class="el" href="kinds_8h_source.html#l00120">ASSUMPTIONS</a>, <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>, <a class="el" href="kinds_8h_source.html#l00105">CALL</a>, <a class="el" href="kinds_8h_source.html#l00133">CHECK_TYPE</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a7be9a77c0c8cbce185d02f5e5f40d21a">CVC3::ValidityChecker::checkContinue()</a>, <a class="el" href="kinds_8h_source.html#l00095">CHECKSAT</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a66b10d795e7ecfa0fa8ce8b69eb07c10">CVC3::ValidityChecker::checkUnsat()</a>, <a class="el" href="command__line__flags_8h_source.html#l00036">CVC3::CLFLAG_BOOL</a>, <a class="el" href="command__line__flags_8h_source.html#l00037">CVC3::CLFLAG_INT</a>, <a class="el" href="command__line__flags_8h_source.html#l00038">CVC3::CLFLAG_STRING</a>, <a class="el" href="kinds_8h_source.html#l00240">CONST</a>, <a class="el" href="kinds_8h_source.html#l00096">CONTINUE</a>, <a class="el" href="kinds_8h_source.html#l00121">COUNTEREXAMPLE</a>, <a class="el" href="kinds_8h_source.html#l00122">COUNTERMODEL</a>, <a class="el" href="command__line__flags_8h_source.html#l00267">CVC3::CLFlags::countFlags()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#af4c4ae47ec16622d9e2a9d9df8142b4f">CVC3::ValidityChecker::createOp()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#aaaef06da81d945fb5fd75cc134f80ca5">CVC3::ValidityChecker::createType()</a>, <a class="el" href="vc__cmd_8h_source.html#l00040">d_vc</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a6cc46f1745f4296f9479479a58d3db6d">CVC3::ValidityChecker::dataType()</a>, <a class="el" href="kinds_8h_source.html#l00098">DBG</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="kinds_8h_source.html#l00246">DEFUN</a>, <a class="el" href="kinds_8h_source.html#l00111">DUMP_ASSUMPTIONS</a>, <a class="el" href="kinds_8h_source.html#l00116">DUMP_CLOSURE</a>, <a class="el" href="kinds_8h_source.html#l00117">DUMP_CLOSURE_PROOF</a>, <a class="el" href="kinds_8h_source.html#l00110">DUMP_PROOF</a>, <a class="el" href="kinds_8h_source.html#l00112">DUMP_SIG</a>, <a class="el" href="kinds_8h_source.html#l00113">DUMP_TCC</a>, <a class="el" href="kinds_8h_source.html#l00114">DUMP_TCC_ASSUMPTIONS</a>, <a class="el" href="kinds_8h_source.html#l00115">DUMP_TCC_PROOF</a>, <a class="el" href="kinds_8h_source.html#l00106">ECHO</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00041">findAxioms()</a>, <a class="el" href="kinds_8h_source.html#l00131">FORGET</a>, <a class="el" href="kinds_8h_source.html#l00109">GET_ASSIGNMENT</a>, <a class="el" href="kinds_8h_source.html#l00134">GET_CHILD</a>, <a class="el" href="kinds_8h_source.html#l00132">GET_TYPE</a>, <a class="el" href="kinds_8h_source.html#l00108">GET_VALUE</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#ad9650915ed1bd526642a9c8d059e7e37">CVC3::ValidityChecker::getAssignment()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a3a38ef396cf06f30bb5bceb5249716e1">CVC3::ValidityChecker::getAssumptions()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a48cceb9c7004dc5887e4f5067b8bc77a">CVC3::ValidityChecker::getAssumptionsTCC()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a31e9c1b41d4887a377af5af9c43586da">CVC3::ValidityChecker::getClosure()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a40c96301728846e2e3cc913ca716f897">CVC3::ValidityChecker::getConcreteModel()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a448e0df25ec6d756861e7d1d217f1063">CVC3::ValidityChecker::getEM()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a9a09f71dc5a3dd47f0240abceab2fad3">CVC3::ValidityChecker::getFlags()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00354">CVC3::ExprManager::getInputLang()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00412">CVC3::ExprManager::getKind()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#ae82f9d7b8b0584323baa04d7d99a1ba4">CVC3::ValidityChecker::getProof()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a28fcabfa37fb118b722525255f0d3b98">CVC3::ValidityChecker::getProofClosure()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a92b98914e5abc57e902e2afc431615ed">CVC3::ValidityChecker::getProofTCC()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a7a46eaebfca225ea519648db19d6c904">CVC3::ValidityChecker::getTCC()</a>, <a class="el" href="command__line__flags_8h_source.html#l00197">CVC3::CLFlag::getType()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#ab946acc8d84a44eb7bfec63d42bb0b91">CVC3::ValidityChecker::getValue()</a>, <a class="el" href="kinds_8h_source.html#l00102">HELP</a>, <a class="el" href="kinds_8h_source.html#l00046">ID</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="kinds_8h_source.html#l00107">INCLUDE</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a20580108288f5df03a54076a9bd8fed5">CVC3::ValidityChecker::incomplete()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#aef6a6eb5eb79e61a2e754ddbb65504a8">CVC3::ValidityChecker::inconsistent()</a>, <a class="el" href="cvc__util_8h_source.html#l00046">CVC3::int2string()</a>, <a class="el" href="queryresult_8h_source.html#l00034">CVC3::INVALID</a>, <a class="el" href="proof_8h_source.html#l00047">CVC3::Proof::isNull()</a>, <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>, <a class="el" href="theory__arith_8h_source.html#l00177">CVC3::isRational()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a9e157d46874e099d9330437aa0c72921">CVC3::ValidityChecker::listExpr()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a68a96b7331b5a81b67c600cec05bbf8e">CVC3::ValidityChecker::loadFile()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a6f81650a2585c2698d30225c37754acf">CVC3::ValidityChecker::logAnnotation()</a>, <a class="el" href="command__line__flags_8h_source.html#l00200">CVC3::CLFlag::modified()</a>, <a class="el" href="kinds_8h_source.html#l00032">NULL_KIND</a>, <a class="el" href="kinds_8h_source.html#l00101">OPTION</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#ad1f1ac87cd8a210686d04eb82a6133c5">CVC3::ValidityChecker::parseExpr()</a>, <a class="el" href="kinds_8h_source.html#l00124">POP</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a3cee14a9c3b852b501a0594dd951f60c">CVC3::ValidityChecker::pop()</a>, <a class="el" href="kinds_8h_source.html#l00127">POP_SCOPE</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#aa619f5732634c9274efaf7a61d5de646">CVC3::ValidityChecker::popScope()</a>, <a class="el" href="kinds_8h_source.html#l00125">POPTO</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a7448ad88871ee774e6de9eae725867ab">CVC3::ValidityChecker::popto()</a>, <a class="el" href="kinds_8h_source.html#l00128">POPTO_SCOPE</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a4ce4e72785c769c641466c0477a50c24">CVC3::ValidityChecker::poptoScope()</a>, <a class="el" href="lang_8h_source.html#l00032">CVC3::PRESENTATION_LANG</a>, <a class="el" href="kinds_8h_source.html#l00104">PRINT</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00228">printCounterExample()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a6f6909a3f7da22df2bf97b21319883eb">CVC3::ValidityChecker::printExpr()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00157">printModel()</a>, <a class="el" href="kinds_8h_source.html#l00123">PUSH</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a93cbbe8c21c2404b03ccaa43636d5f59">CVC3::ValidityChecker::push()</a>, <a class="el" href="kinds_8h_source.html#l00126">PUSH_SCOPE</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#aa6abf3f929951daba04f5e7874aa471c">CVC3::ValidityChecker::pushScope()</a>, <a class="el" href="kinds_8h_source.html#l00094">QUERY</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a93b515a079fc8fdae5826dfcc343909e">CVC3::ValidityChecker::query()</a>, <a class="el" href="kinds_8h_source.html#l00037">RATIONAL_EXPR</a>, <a class="el" href="kinds_8h_source.html#l00044">RAW_LIST</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00102">reportResult()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a0acc9330bfe47d579f1fa105d2603e85">CVC3::ValidityChecker::reprocessFlags()</a>, <a class="el" href="kinds_8h_source.html#l00129">RESET</a>, <a class="el" href="kinds_8h_source.html#l00097">RESTART</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#aefdc8ccae46e254d26b574d5d3ad6fc1">CVC3::ValidityChecker::restart()</a>, <a class="el" href="queryresult_8h_source.html#l00033">CVC3::SATISFIABLE</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a8e60da88d484801579c15960f41a3f72">CVC3::ValidityChecker::scopeLevel()</a>, <a class="el" href="kinds_8h_source.html#l00136">SEQ</a>, <a class="el" href="command__line__flags_8h_source.html#l00302">CVC3::CLFlags::setFlag()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a088a718e4f0041caea02312077a586c9">CVC3::ValidityChecker::simplify()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00061">skolemizeAx()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#ac1a5a5a29d08461ec42bc904524aa550">CVC3::ValidityChecker::stackLevel()</a>, <a class="el" href="kinds_8h_source.html#l00135">SUBSTITUTE</a>, <a class="el" href="exception_8h_source.html#l00046">CVC3::Exception::toString()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>, <a class="el" href="kinds_8h_source.html#l00103">TRANSFORM</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a4e9d64bd0f01ce88b9e8494861ab527d">CVC3::ValidityChecker::trueExpr()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a2c9bb81c75da36453ffb16a804a24605">CVC3::ValidityChecker::tryModelGeneration()</a>, <a class="el" href="kinds_8h_source.html#l00053">TYPE</a>, <a class="el" href="kinds_8h_source.html#l00058">TYPEDEF</a>, <a class="el" href="queryresult_8h_source.html#l00038">CVC3::UNKNOWN</a>, <a class="el" href="kinds_8h_source.html#l00100">UNTRACE</a>, <a class="el" href="queryresult_8h_source.html#l00035">CVC3::VALID</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a4dc02c11317b0f12606e5ec264dd9ca9">CVC3::ValidityChecker::varExpr()</a>, and <a class="el" href="kinds_8h_source.html#l00118">WHERE</a>.</p>
<p>Referenced by <a class="el" href="vc__cmd_8cpp_source.html#l00073">evaluateNext()</a>.</p>
</div>
</div>
<a class="anchor" id="a60dcaba75f518a16dec9314df3aff161"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool VCCmd::evaluateNext </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="vc__cmd_8cpp_source.html#l00073">73</a> of file <a class="el" href="vc__cmd_8cpp_source.html">vc_cmd.cpp</a>.</p>
<p>References <a class="el" href="vc__cmd_8h_source.html#l00041">d_parser</a>, <a class="el" href="vc__cmd_8h_source.html#l00040">d_vc</a>, <a class="el" href="classCVC3_1_1Parser.html#a088627f9421c691414cd06161f99394a">CVC3::Parser::done()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00267">evaluateCommand()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a9a09f71dc5a3dd47f0240abceab2fad3">CVC3::ValidityChecker::getFlags()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="classCVC3_1_1Parser.html#a85eb8f5faba18ee392023d93ac6cc401">CVC3::Parser::next()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="debug_8h_source.html#l00414">TRACE_MSG</a>.</p>
<p>Referenced by <a class="el" href="vc__cmd_8cpp_source.html#l00944">processCommands()</a>.</p>
</div>
</div>
<a class="anchor" id="a04c3244b2ead42f4eeb22b3cf8c6d9a8"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void VCCmd::findAxioms </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > & </td>
<td class="paramname"><em>skolemAxioms</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > & </td>
<td class="paramname"><em>visited</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="vc__cmd_8cpp_source.html#l00041">41</a> of file <a class="el" href="vc__cmd_8cpp_source.html">vc_cmd.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="expr__map_8h_source.html#l00173">CVC3::ExprMap< Data >::count()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr_8h_source.html#l01069">CVC3::Expr::getBody()</a>, <a class="el" href="expr_8h_source.html#l01123">CVC3::Expr::getExistential()</a>, <a class="el" href="expr__map_8h_source.html#l00177">CVC3::ExprMap< Data >::insert()</a>, <a class="el" href="expr_8h_source.html#l01007">CVC3::Expr::isClosure()</a>, and <a class="el" href="expr_8h_source.html#l00432">CVC3::Expr::isSkolem()</a>.</p>
<p>Referenced by <a class="el" href="vc__cmd_8cpp_source.html#l00267">evaluateCommand()</a>, and <a class="el" href="vc__cmd_8cpp_source.html#l00228">printCounterExample()</a>.</p>
</div>
</div>
<a class="anchor" id="a165e689c23949794ce77632e15d3821d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> VCCmd::skolemizeAx </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="vc__cmd_8cpp_source.html#l00061">61</a> of file <a class="el" href="vc__cmd_8cpp_source.html">vc_cmd.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01069">CVC3::Expr::getBody()</a>, <a class="el" href="expr_8h_source.html#l01062">CVC3::Expr::getVars()</a>, <a class="el" href="expr_8h_source.html#l00965">CVC3::Expr::iffExpr()</a>, <a class="el" href="expr_8h_source.html#l00977">CVC3::Expr::skolemExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00178">CVC3::Expr::substExpr()</a>.</p>
<p>Referenced by <a class="el" href="vc__cmd_8cpp_source.html#l00267">evaluateCommand()</a>, and <a class="el" href="vc__cmd_8cpp_source.html#l00228">printCounterExample()</a>.</p>
</div>
</div>
<a class="anchor" id="ad61f2528e834203b51ff974f5212a26b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void VCCmd::reportResult </td>
<td>(</td>
<td class="paramtype"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> </td>
<td class="paramname"><em>qres</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>checkingValidity</em> = <code>true</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="vc__cmd_8cpp_source.html#l00102">102</a> of file <a class="el" href="vc__cmd_8cpp_source.html">vc_cmd.cpp</a>.</p>
<p>References <a class="el" href="queryresult_8h_source.html#l00037">CVC3::ABORT</a>, <a class="el" href="vc__cmd_8h_source.html#l00040">d_vc</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a448e0df25ec6d756861e7d1d217f1063">CVC3::ValidityChecker::getEM()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a9a09f71dc5a3dd47f0240abceab2fad3">CVC3::ValidityChecker::getFlags()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00360">CVC3::ExprManager::getOutputLang()</a>, <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a20580108288f5df03a54076a9bd8fed5">CVC3::ValidityChecker::incomplete()</a>, <a class="el" href="queryresult_8h_source.html#l00034">CVC3::INVALID</a>, <a class="el" href="lang_8h_source.html#l00034">CVC3::SMTLIB_LANG</a>, <a class="el" href="lang_8h_source.html#l00052">CVC3::SMTLIB_V2_LANG</a>, <a class="el" href="queryresult_8h_source.html#l00038">CVC3::UNKNOWN</a>, and <a class="el" href="queryresult_8h_source.html#l00035">CVC3::VALID</a>.</p>
<p>Referenced by <a class="el" href="vc__cmd_8cpp_source.html#l00267">evaluateCommand()</a>.</p>
</div>
</div>
<a class="anchor" id="a1997d265d49f31e9624ab3f28a33d79f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void VCCmd::printModel </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="vc__cmd_8cpp_source.html#l00157">157</a> of file <a class="el" href="vc__cmd_8cpp_source.html">vc_cmd.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00093">ASSERT</a>, <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>, <a class="el" href="vc__cmd_8h_source.html#l00040">d_vc</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a40c96301728846e2e3cc913ca716f897">CVC3::ValidityChecker::getConcreteModel()</a>, and <a class="el" href="classCVC3_1_1ValidityChecker.html#a8e60da88d484801579c15960f41a3f72">CVC3::ValidityChecker::scopeLevel()</a>.</p>
<p>Referenced by <a class="el" href="vc__cmd_8cpp_source.html#l00267">evaluateCommand()</a>.</p>
</div>
</div>
<a class="anchor" id="a0dbc7765ccb1aeaf5265ae5894330c8a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void VCCmd::printCounterExample </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="vc__cmd_8cpp_source.html#l00228">228</a> of file <a class="el" href="vc__cmd_8cpp_source.html">vc_cmd.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00093">ASSERT</a>, <a class="el" href="expr__map_8h_source.html#l00190">CVC3::ExprMap< Data >::begin()</a>, <a class="el" href="vc__cmd_8h_source.html#l00040">d_vc</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00041">findAxioms()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a4e3b0f9d1129f476f116ad766105ddad">CVC3::ValidityChecker::getCounterExample()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00188">printSymbols()</a>, <a class="el" href="classCVC3_1_1ValidityChecker.html#a8e60da88d484801579c15960f41a3f72">CVC3::ValidityChecker::scopeLevel()</a>, and <a class="el" href="vc__cmd_8cpp_source.html#l00061">skolemizeAx()</a>.</p>
<p>Referenced by <a class="el" href="vc__cmd_8cpp_source.html#l00267">evaluateCommand()</a>.</p>
</div>
</div>
<a class="anchor" id="ababcd4001adfc005ef5f2f365c61b829"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void VCCmd::processCommands </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="vc__cmd_8cpp_source.html#l00944">944</a> of file <a class="el" href="vc__cmd_8cpp_source.html">vc_cmd.cpp</a>.</p>
<p>References <a class="el" href="vc__cmd_8h_source.html#l00046">d_calledFromParser</a>, <a class="el" href="vc__cmd_8h_source.html#l00041">d_parser</a>, <a class="el" href="vc__cmd_8h_source.html#l00040">d_vc</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00073">evaluateNext()</a>, <a class="el" href="classCVC3_1_1Parser.html#a96620f0d491db182bbaefa186d05621b">CVC3::Parser::printLocation()</a>, <a class="el" href="classCVC3_1_1Parser.html#a84d22e302246021152e5dbc950e67758">CVC3::Parser::reset()</a>, and <a class="el" href="classCVC3_1_1ValidityChecker.html#accfa11d7cb5f45e4f73c01c09507f6b0">CVC3::ValidityChecker::reset()</a>.</p>
<p>Referenced by <a class="el" href="vcl_8cpp_source.html#l02393">CVC3::VCL::loadFile()</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Data Documentation</h2>
<a class="anchor" id="aa43a0dbed5026bca03502570f6a491ef"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ValidityChecker.html">ValidityChecker</a>* CVC3::VCCmd::d_vc</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="vc__cmd_8h_source.html#l00040">40</a> of file <a class="el" href="vc__cmd_8h_source.html">vc_cmd.h</a>.</p>
<p>Referenced by <a class="el" href="vc__cmd_8cpp_source.html#l00267">evaluateCommand()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00073">evaluateNext()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00228">printCounterExample()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00157">printModel()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00188">printSymbols()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00944">processCommands()</a>, <a class="el" href="vc__cmd_8cpp_source.html#l00102">reportResult()</a>, and <a class="el" href="vc__cmd_8cpp_source.html#l00032">VCCmd()</a>.</p>
</div>
</div>
<a class="anchor" id="acd57eff603dc4690dee1ed25415167aa"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Parser.html">Parser</a>* CVC3::VCCmd::d_parser</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="vc__cmd_8h_source.html#l00041">41</a> of file <a class="el" href="vc__cmd_8h_source.html">vc_cmd.h</a>.</p>
<p>Referenced by <a class="el" href="vc__cmd_8cpp_source.html#l00073">evaluateNext()</a>, and <a class="el" href="vc__cmd_8cpp_source.html#l00944">processCommands()</a>.</p>
</div>
</div>
<a class="anchor" id="a83ac968536314974e45519a222d00dfa"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::string CVC3::VCCmd::d_name_of_cur_ctxt</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="vc__cmd_8h_source.html#l00044">44</a> of file <a class="el" href="vc__cmd_8h_source.html">vc_cmd.h</a>.</p>
<p>Referenced by <a class="el" href="vc__cmd_8cpp_source.html#l00032">VCCmd()</a>.</p>
</div>
</div>
<a class="anchor" id="a5e2f199c7aa4aa087215828af54c5c90"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1VCCmd.html#a6e02bca439dd43541e625c068a28622e">CtxtMap</a> CVC3::VCCmd::d_map</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="vc__cmd_8h_source.html#l00045">45</a> of file <a class="el" href="vc__cmd_8h_source.html">vc_cmd.h</a>.</p>
<p>Referenced by <a class="el" href="vc__cmd_8cpp_source.html#l00032">VCCmd()</a>.</p>
</div>
</div>
<a class="anchor" id="a12a174396e81593ac1da765ef922559a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::VCCmd::d_calledFromParser</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="vc__cmd_8h_source.html#l00046">46</a> of file <a class="el" href="vc__cmd_8h_source.html">vc_cmd.h</a>.</p>
<p>Referenced by <a class="el" href="vc__cmd_8cpp_source.html#l00944">processCommands()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="vc__cmd_8h_source.html">vc_cmd.h</a></li>
<li><a class="el" href="vc__cmd_8cpp_source.html">vc_cmd.cpp</a></li>
</ul>
</div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:19 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
