<!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"/>
<title>CVC3: CVC3::Translator Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<link href="doxygen.css" rel="stylesheet" type="text/css"/>
</head>
<body>
<!-- Generated by Doxygen 1.7.4 -->
<div id="top">
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3 <span id="projectnumber">2.4.1</span></div>
</td>
</tr>
</tbody>
</table>
</div>
<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="hierarchy.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_1Translator.html">Translator</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#nested-classes">Classes</a> |
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> </div>
<div class="headertitle">
<div class="title">CVC3::Translator Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::Translator" -->
<p><code>#include <<a class="el" href="translator_8h_source.html">translator.h</a>></code></p>
<p><a href="classCVC3_1_1Translator-members.html">List of all members.</a></p>
<h2><a name="nested-classes"></a>
Classes</h2>
<ul>
<li>class <a class="el" href="classCVC3_1_1Translator_1_1HashString.html">HashString</a>
</ul>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classCVC3_1_1Translator.html#a23f150cc9a6b041d95b801bcdb5c9b5b">Translator</a> (<a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> *em, const bool &translate, const bool &real2int, const bool &convertArith, const std::string &convertToDiff, bool iteLiftArith, const std::string &expResult, const std::string &category, bool convertArray, bool combineAssump, int convertToBV)
<li><a class="el" href="classCVC3_1_1Translator.html#a9c262ba866126a6a35e979a64d7e3518">~Translator</a> ()
<li>bool <a class="el" href="classCVC3_1_1Translator.html#ad0209b8b429fc08f7cd500aae0f35792">start</a> (const std::string &dumpFile)
<li>void <a class="el" href="classCVC3_1_1Translator.html#a2085a4f56a069befeaf2de05d78312a0">dump</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, bool dumpOnly=false)
<li>bool <a class="el" href="classCVC3_1_1Translator.html#ad7100f7c31841078e4d298aa415694e0">dumpAssertion</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li>bool <a class="el" href="classCVC3_1_1Translator.html#a0642e4129e907824a8ac54d4cb89462f">dumpQuery</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li>void <a class="el" href="classCVC3_1_1Translator.html#abafa3e4622d8ef21e29d79c7efb20053">dumpQueryResult</a> (<a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> qres)
<li>void <a class="el" href="classCVC3_1_1Translator.html#a444765aa6bbf793c1ddbc66e9fb829fe">finish</a> ()
<li>void <a class="el" href="classCVC3_1_1Translator.html#ae54e65770cca9121bd7edb3066db0cca">setTheoryCore</a> (<a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> *theoryCore)
<li>void <a class="el" href="classCVC3_1_1Translator.html#ac90246c6882f3afb6dfa2c1cd28bee77">setTheoryUF</a> (<a class="el" href="classCVC3_1_1TheoryUF.html">TheoryUF</a> *theoryUF)
<li>void <a class="el" href="classCVC3_1_1Translator.html#a56398996b69a8ae5f2d483cac21c06b4">setTheoryArith</a> (<a class="el" href="classCVC3_1_1TheoryArith.html">TheoryArith</a> *theoryArith)
<li>void <a class="el" href="classCVC3_1_1Translator.html#ae98b6dcd49033de9e7af75bf832ed907">setTheoryArray</a> (<a class="el" href="classCVC3_1_1TheoryArray.html">TheoryArray</a> *theoryArray)
<li>void <a class="el" href="classCVC3_1_1Translator.html#afa7244fb9f0b749548fe1702238a1d29">setTheoryQuant</a> (<a class="el" href="classCVC3_1_1TheoryQuant.html">TheoryQuant</a> *theoryQuant)
<li>void <a class="el" href="classCVC3_1_1Translator.html#a072d9f51dc77cf2e1d1c4b7ebafd4d1d">setTheoryRecords</a> (<a class="el" href="classCVC3_1_1TheoryRecords.html">TheoryRecords</a> *theoryRecords)
<li>void <a class="el" href="classCVC3_1_1Translator.html#a8c47c28bbcfb39b3dc8244eda47a5dc9">setTheorySimulate</a> (<a class="el" href="classCVC3_1_1TheorySimulate.html">TheorySimulate</a> *theorySimulate)
<li>void <a class="el" href="classCVC3_1_1Translator.html#a87f9011a441dd3c772c0efc8d73e8548">setTheoryBitvector</a> (<a class="el" href="classCVC3_1_1TheoryBitvector.html">TheoryBitvector</a> *theoryBitvector)
<li>void <a class="el" href="classCVC3_1_1Translator.html#a9fdb4320a2310af16ef6caacdff8ab5c">setTheoryDatatype</a> (<a class="el" href="classCVC3_1_1TheoryDatatype.html">TheoryDatatype</a> *theoryDatatype)
<li>void <a class="el" href="classCVC3_1_1Translator.html#a9db51995d5dc21b254bfeb5381b4ce5a">setBenchName</a> (std::string name)
<li>std::string <a class="el" href="classCVC3_1_1Translator.html#ad5c28f74006f791727b15d17a3a20650">benchName</a> ()
<li>void <a class="el" href="classCVC3_1_1Translator.html#a4c9d948f111bd360e937b170a2c95120">setStatus</a> (std::string status)
<li>std::string <a class="el" href="classCVC3_1_1Translator.html#aee4bdef7291181744580934a93849b64">status</a> ()
<li>void <a class="el" href="classCVC3_1_1Translator.html#ac9c933a8ce7265f0463c8556c8eb624c">setSource</a> (std::string source)
<li>std::string <a class="el" href="classCVC3_1_1Translator.html#ad57a63292d37aa81d56c3102edd99f2b">source</a> ()
<li>void <a class="el" href="classCVC3_1_1Translator.html#aed753d381e5cec7619b8324a7588b874">setCategory</a> (std::string category)
<li>std::string <a class="el" href="classCVC3_1_1Translator.html#af1a89762818192869c5d2161dab0a167">category</a> ()
<li>const std::string <a class="el" href="classCVC3_1_1Translator.html#a0ee4f6a5cf7bb40bfe341e4b99f06810">fixConstName</a> (const std::string &s)
<li>const std::string <a class="el" href="classCVC3_1_1Translator.html#a6821f774dda2d0964fde109b29de20a8">escapeSymbol</a> (const std::string &s)
<li>const std::string <a class="el" href="classCVC3_1_1Translator.html#a90238a14586a6582a741bebebce13010">quoteAnnotation</a> (const std::string &s)
<li>bool <a class="el" href="classCVC3_1_1Translator.html#ab562bf78b184a0039093ce0dba0770d0">printArrayExpr</a> (<a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> &os, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Returns true if expression has been printed. <a href="#ab562bf78b184a0039093ce0dba0770d0"></a><br/></dl><li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1Translator.html#a89f83c6d0dcc3416b7b5facd68753e80">zeroVar</a> ()
</ul>
<h2><a name="pri-methods"></a>
Private Member Functions</h2>
<ul>
<li>std::string <a class="el" href="classCVC3_1_1Translator.html#aa1ff667f344c04df1ff5a6b50cd96e0a">fileToSMTLIBIdentifier</a> (const std::string &filename)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1Translator.html#aed0fe44184d5d994a340d7006136a6dc">preprocessRec</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &cache)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1Translator.html#a6cad6b15357c5baf43a287be1a762a26">preprocess</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &cache)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1Translator.html#a8643ae389927052297fef525045211ac">preprocess2Rec</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &cache, <a class="el" href="classCVC3_1_1Type.html">Type</a> desiredType)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1Translator.html#ab0934eb91855a58064402f48bf4b4ad5">preprocess2</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &cache)
<li>bool <a class="el" href="classCVC3_1_1Translator.html#aa41988d7a85be9e3b68a053ef1db50b6">containsArray</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1Translator.html#a5e42669a5a6f0a69ae33fde3ccedb8bb">processType</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
</ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> * <a class="el" href="classCVC3_1_1Translator.html#a913d9fbcdfbb4d17e3864a74480b0611">d_em</a>
<li>const bool & <a class="el" href="classCVC3_1_1Translator.html#a62b1d8ae4ec79cfb22725dd4635d59de">d_translate</a>
<li>const bool & <a class="el" href="classCVC3_1_1Translator.html#a54add6521f2f005b84cdd129d64764f2">d_real2int</a>
<li>const bool & <a class="el" href="classCVC3_1_1Translator.html#a4f578f10a492640eec9ff8de157cc521">d_convertArith</a>
<li>const std::string & <a class="el" href="classCVC3_1_1Translator.html#ac20944f0dfa8772fd1e4c1ad757bf9da">d_convertToDiff</a>
<li>bool <a class="el" href="classCVC3_1_1Translator.html#afd9c853a8d17a1c7905bb007f1494ce0">d_iteLiftArith</a>
<li>const std::string & <a class="el" href="classCVC3_1_1Translator.html#a755c43c5f5be61e8c3c034dccaef33ba">d_expResult</a>
<li>std::string <a class="el" href="classCVC3_1_1Translator.html#a4a4f7719dd2741c94c88111015846099">d_category</a>
<li>bool <a class="el" href="classCVC3_1_1Translator.html#ab09c1e81131dfc2d3a4da1f859a8108e">d_convertArray</a>
<li>bool <a class="el" href="classCVC3_1_1Translator.html#a72b7aff947a816fbf26f7a97ce0f5fdd">d_combineAssump</a>
<li><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a>< std::string, <br class="typebreak"/>
std::string, <a class="el" href="classCVC3_1_1Translator_1_1HashString.html">HashString</a> > <a class="el" href="classCVC3_1_1Translator.html#ad81beb93ee2668558c897398ce68fa44">d_replaceSymbols</a>
<li>std::ostream * <a class="el" href="classCVC3_1_1Translator.html#a61574c04bd74489b4438ca890f3ec7b4">d_osdump</a>
<dl class="el"><dd class="mdescRight">The log file for top-level API calls in the <a class="el" href="namespaceCVC3.html">CVC3</a> input language. <a href="#a61574c04bd74489b4438ca890f3ec7b4"></a><br/></dl><li>std::ofstream <a class="el" href="classCVC3_1_1Translator.html#a78a511690ef1f3421862b39dad9d02f7">d_osdumpFile</a>
<li>std::ifstream <a class="el" href="classCVC3_1_1Translator.html#ac55f4fdc4bbb29ccd09dfda38a6eeb91">d_tmpFile</a>
<li>bool <a class="el" href="classCVC3_1_1Translator.html#ac5e47db270e1b8d4ee40fe2654382413">d_dump</a>
<li>bool <a class="el" href="classCVC3_1_1Translator.html#a86e279b67edf39d32056d279a4f9de3b">d_dumpFileOpen</a>
<li>bool <a class="el" href="classCVC3_1_1Translator.html#aa4dc3a71a03482ba8bb6ff8579e09781">d_intIntArray</a>
<li>bool <a class="el" href="classCVC3_1_1Translator.html#aca1de6c7f5ab780b57d10c66f58a2890">d_intRealArray</a>
<li>bool <a class="el" href="classCVC3_1_1Translator.html#a69c89f774ba1fe6c13ca3559748776af">d_intIntRealArray</a>
<li>bool <a class="el" href="classCVC3_1_1Translator.html#a0793dec1240036cde06df95a14241438">d_ax</a>
<li>bool <a class="el" href="classCVC3_1_1Translator.html#a290235a7047226a6564add8ef5ad1f10">d_unknown</a>
<li>bool <a class="el" href="classCVC3_1_1Translator.html#a706c02509ddc23d60d43f38af6497139">d_realUsed</a>
<li>bool <a class="el" href="classCVC3_1_1Translator.html#a18db4e99db8f78e67992cb3cf68dee28">d_intUsed</a>
<li>bool <a class="el" href="classCVC3_1_1Translator.html#a2e326c83175674acde79b1e33fe391b7">d_intConstUsed</a>
<li><a class="el" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7c">ArithLang</a> <a class="el" href="classCVC3_1_1Translator.html#aa6d9fb46298801972cb082ec6eb9918d">d_langUsed</a>
<li>bool <a class="el" href="classCVC3_1_1Translator.html#a939bf8530ea41cd0e0c9f8621e17569d">d_UFIDL_ok</a>
<li>bool <a class="el" href="classCVC3_1_1Translator.html#a2adf399cb0475894d8b4ea870aaf4547">d_arithUsed</a>
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> * <a class="el" href="classCVC3_1_1Translator.html#abff660525da18bbe419aed68df4d8564">d_zeroVar</a>
<li>int <a class="el" href="classCVC3_1_1Translator.html#a53fdab56fe2f1e821b3f36c2641ae462">d_convertToBV</a>
<li><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> * <a class="el" href="classCVC3_1_1Translator.html#a1379b7c9235c804f32ab5ce19d86a907">d_theoryCore</a>
<li><a class="el" href="classCVC3_1_1TheoryUF.html">TheoryUF</a> * <a class="el" href="classCVC3_1_1Translator.html#a67f2340f940914d63aea99462eced2ad">d_theoryUF</a>
<li><a class="el" href="classCVC3_1_1TheoryArith.html">TheoryArith</a> * <a class="el" href="classCVC3_1_1Translator.html#a0d360419c4e9e9ee9ac8e8af126534d2">d_theoryArith</a>
<li><a class="el" href="classCVC3_1_1TheoryArray.html">TheoryArray</a> * <a class="el" href="classCVC3_1_1Translator.html#a9b8dc03475b2e90380f82bac9f71e39d">d_theoryArray</a>
<li><a class="el" href="classCVC3_1_1TheoryQuant.html">TheoryQuant</a> * <a class="el" href="classCVC3_1_1Translator.html#a5e85f73e319fbd8745c66852cfc1cad5">d_theoryQuant</a>
<li><a class="el" href="classCVC3_1_1TheoryRecords.html">TheoryRecords</a> * <a class="el" href="classCVC3_1_1Translator.html#a0ce73787e0363fc66f6e653cbec219f6">d_theoryRecords</a>
<li><a class="el" href="classCVC3_1_1TheorySimulate.html">TheorySimulate</a> * <a class="el" href="classCVC3_1_1Translator.html#a3fbe66e1fdb7b24735146f6e15d6c9da">d_theorySimulate</a>
<li><a class="el" href="classCVC3_1_1TheoryBitvector.html">TheoryBitvector</a> * <a class="el" href="classCVC3_1_1Translator.html#aef70b07a6df14699d8f5bc24c6e93ae9">d_theoryBitvector</a>
<li><a class="el" href="classCVC3_1_1TheoryDatatype.html">TheoryDatatype</a> * <a class="el" href="classCVC3_1_1Translator.html#ad4a063f628068060febbdff159af1eb3">d_theoryDatatype</a>
<li>std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > <a class="el" href="classCVC3_1_1Translator.html#a703373c20b6092dd4ca97566921c2583">d_dumpExprs</a>
<li>std::map< std::string, <a class="el" href="classCVC3_1_1Type.html">Type</a> > * <a class="el" href="classCVC3_1_1Translator.html#a607f817315c4f3140610420f97172c41">d_arrayConvertMap</a>
<li><a class="el" href="classCVC3_1_1Type.html">Type</a> * <a class="el" href="classCVC3_1_1Translator.html#a3fc40e37980968ff8859c1634c006749">d_indexType</a>
<li><a class="el" href="classCVC3_1_1Type.html">Type</a> * <a class="el" href="classCVC3_1_1Translator.html#ac142228e58539d53376555542fa357fc">d_elementType</a>
<li><a class="el" href="classCVC3_1_1Type.html">Type</a> * <a class="el" href="classCVC3_1_1Translator.html#a77ec037bfce2d8e0d98ed1f7c4fef2c0">d_arrayType</a>
<li>std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > <a class="el" href="classCVC3_1_1Translator.html#a0dc704ddbd08fdeddd838280539e31bd">d_equalities</a>
<li>std::string <a class="el" href="classCVC3_1_1Translator.html#a7e45d1878196924bef7ab146613975a1">d_benchName</a>
<li>std::string <a class="el" href="classCVC3_1_1Translator.html#a270ac8683f5505f82e207f3238aef007">d_status</a>
<li>std::string <a class="el" href="classCVC3_1_1Translator.html#a2181217309457039aab4b190e523f390">d_source</a>
</ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00060">60</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
</div><hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a23f150cc9a6b041d95b801bcdb5c9b5b"></a><!-- doxytag: member="CVC3::Translator::Translator" ref="a23f150cc9a6b041d95b801bcdb5c9b5b" args="(ExprManager *em, const bool &translate, const bool &real2int, const bool &convertArith, const std::string &convertToDiff, bool iteLiftArith, const std::string &expResult, const std::string &category, bool convertArray, bool combineAssump, int convertToBV)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">Translator::Translator </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a> * </td>
<td class="paramname"><em>em</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const bool & </td>
<td class="paramname"><em>translate</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const bool & </td>
<td class="paramname"><em>real2int</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const bool & </td>
<td class="paramname"><em>convertArith</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>convertToDiff</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>iteLiftArith</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>expResult</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>category</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>convertArray</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>combineAssump</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>convertToBV</em> </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="translator_8cpp_source.html#l00808">808</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00111">d_arrayConvertMap</a>.</p>
</div>
</div>
<a class="anchor" id="a9c262ba866126a6a35e979a64d7e3518"></a><!-- doxytag: member="CVC3::Translator::~Translator" ref="a9c262ba866126a6a35e979a64d7e3518" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">Translator::~Translator </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="translator_8cpp_source.html#l00839">839</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00111">d_arrayConvertMap</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="aa1ff667f344c04df1ff5a6b50cd96e0a"></a><!-- doxytag: member="CVC3::Translator::fileToSMTLIBIdentifier" ref="aa1ff667f344c04df1ff5a6b50cd96e0a" args="(const std::string &filename)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">string Translator::fileToSMTLIBIdentifier </td>
<td>(</td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>filename</em></td><td>)</td>
<td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8cpp_source.html#l00045">45</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l00845">start()</a>.</p>
</div>
</div>
<a class="anchor" id="aed0fe44184d5d994a340d7006136a6dc"></a><!-- doxytag: member="CVC3::Translator::preprocessRec" ref="aed0fe44184d5d994a340d7006136a6dc" args="(const Expr &e, ExprMap< Expr > &cache)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> Translator::preprocessRec </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>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>cache</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8cpp_source.html#l00072">72</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00090">APPLY</a>, <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="theory__bitvector_8h_source.html#l00066">CVC3::BVMULT</a>, <a class="el" href="theory__bitvector_8h_source.html#l00064">CVC3::BVPLUS</a>, <a class="el" href="theory__bitvector_8h_source.html#l00078">CVC3::BVSLE</a>, <a class="el" href="theory__bitvector_8h_source.html#l00077">CVC3::BVSLT</a>, <a class="el" href="theory__bitvector_8h_source.html#l00065">CVC3::BVSUB</a>, <a class="el" href="theory__bitvector_8h_source.html#l00063">CVC3::BVUMINUS</a>, <a class="el" href="expr_8cpp_source.html#l00525">CVC3::Expr::containsTermITE()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="translator_8h_source.html#l00054">CVC3::DIFF_ONLY</a>, <a class="el" href="theory__arith_8h_source.html#l00045">CVC3::DIVIDE</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="kinds_8h_source.html#l00061">EQ</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="theory__arith_8h_source.html#l00052">CVC3::GE</a>, <a class="el" href="expr_8h_source.html#l01069">CVC3::Expr::getBody()</a>, <a class="el" href="expr_8h_source.html#l01162">CVC3::Expr::getKids()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01050">CVC3::Expr::getName()</a>, <a class="el" href="classCVC3_1_1Rational.html#a953f2eb850fc3612097b5320dcda6047">CVC3::Rational::getNumerator()</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="expr_8h_source.html#l01191">CVC3::Expr::getOpExpr()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01135">CVC3::Expr::getRational()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="expr_8h_source.html#l01062">CVC3::Expr::getVars()</a>, <a class="el" href="theory__arith_8h_source.html#l00051">CVC3::GT</a>, <a class="el" href="theory__arith_8h_source.html#l00047">CVC3::INTDIV</a>, <a class="el" href="theory__arith_8h_source.html#l00053">CVC3::IS_INTEGER</a>, <a class="el" href="expr_8h_source.html#l01007">CVC3::Expr::isClosure()</a>, <a class="el" href="theory__arith_8h_source.html#l00174">CVC3::isInt()</a>, <a class="el" href="classCVC3_1_1Rational.html#a1366320f4de558bb964c67f8aecedb36">CVC3::Rational::isInteger()</a>, <a class="el" href="expr_8h_source.html#l00411">CVC3::Expr::isPropAtom()</a>, <a class="el" href="expr_8h_source.html#l00431">CVC3::Expr::isRational()</a>, <a class="el" href="theory__arith_8h_source.html#l00177">CVC3::isRational()</a>, <a class="el" href="expr_8h_source.html#l01005">CVC3::Expr::isVar()</a>, <a class="el" href="kinds_8h_source.html#l00081">ITE</a>, <a class="el" href="expr_8h_source.html#l00961">CVC3::Expr::iteExpr()</a>, <a class="el" href="kinds_8h_source.html#l00229">LAMBDA</a>, <a class="el" href="theory__arith_8h_source.html#l00050">CVC3::LE</a>, <a class="el" href="translator_8h_source.html#l00055">CVC3::LINEAR</a>, <a class="el" href="theory__arith_8h_source.html#l00049">CVC3::LT</a>, <a class="el" href="theory__arith_8h_source.html#l00043">CVC3::MINUS</a>, <a class="el" href="theory__arith_8h_source.html#l00048">CVC3::MOD</a>, <a class="el" href="theory__arith_8h_source.html#l00044">CVC3::MULT</a>, <a class="el" href="translator_8h_source.html#l00056">CVC3::NONLINEAR</a>, <a class="el" href="kinds_8h_source.html#l00066">NOT</a>, <a class="el" href="translator_8h_source.html#l00052">CVC3::NOT_USED</a>, <a class="el" href="theory__arith_8h_source.html#l00042">CVC3::PLUS</a>, <a class="el" href="theory__arith_8h_source.html#l00046">CVC3::POW</a>, <a class="el" href="rational_8h_source.html#l00159">CVC3::pow()</a>, <a class="el" href="kinds_8h_source.html#l00037">RATIONAL_EXPR</a>, <a class="el" href="theory__array_8h_source.html#l00032">CVC3::READ</a>, <a class="el" href="translator_8h_source.html#l00053">CVC3::TERMS_ONLY</a>, <a class="el" href="kinds_8h_source.html#l00242">UCONST</a>, <a class="el" href="theory__arith_8h_source.html#l00041">CVC3::UMINUS</a>, and <a class="el" href="theory__array_8h_source.html#l00033">CVC3::WRITE</a>.</p>
</div>
</div>
<a class="anchor" id="a6cad6b15357c5baf43a287be1a762a26"></a><!-- doxytag: member="CVC3::Translator::preprocess" ref="a6cad6b15357c5baf43a287be1a762a26" args="(const Expr &e, ExprMap< Expr > &cache)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> Translator::preprocess </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>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>cache</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8cpp_source.html#l00549">549</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>.</p>
</div>
</div>
<a class="anchor" id="a8643ae389927052297fef525045211ac"></a><!-- doxytag: member="CVC3::Translator::preprocess2Rec" ref="a8643ae389927052297fef525045211ac" args="(const Expr &e, ExprMap< Expr > &cache, Type desiredType)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> Translator::preprocess2Rec </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>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>cache</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Type.html">Type</a> </td>
<td class="paramname"><em>desiredType</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8cpp_source.html#l00563">563</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00050">ANY_TYPE</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theory__arith_8h_source.html#l00045">CVC3::DIVIDE</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="kinds_8h_source.html#l00061">EQ</a>, <a class="el" href="debug_8h_source.html#l00037">FatalAssert</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="theory__arith_8h_source.html#l00052">CVC3::GE</a>, <a class="el" href="expr_8h_source.html#l01069">CVC3::Expr::getBody()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="expr_8h_source.html#l01191">CVC3::Expr::getOpExpr()</a>, <a class="el" href="expr_8h_source.html#l01135">CVC3::Expr::getRational()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="expr_8h_source.html#l01062">CVC3::Expr::getVars()</a>, <a class="el" href="theory__arith_8h_source.html#l00051">CVC3::GT</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, <a class="el" href="expr_8h_source.html#l01007">CVC3::Expr::isClosure()</a>, <a class="el" href="theory__arith_8h_source.html#l00174">CVC3::isInt()</a>, <a class="el" href="type_8h_source.html#l00059">CVC3::Type::isNull()</a>, <a class="el" href="expr_8h_source.html#l00431">CVC3::Expr::isRational()</a>, <a class="el" href="theory__arith_8h_source.html#l00173">CVC3::isReal()</a>, <a class="el" href="kinds_8h_source.html#l00081">ITE</a>, <a class="el" href="theory__arith_8h_source.html#l00050">CVC3::LE</a>, <a class="el" href="translator_8h_source.html#l00055">CVC3::LINEAR</a>, <a class="el" href="theory__arith_8h_source.html#l00049">CVC3::LT</a>, <a class="el" href="theory__arith_8h_source.html#l00043">CVC3::MINUS</a>, <a class="el" href="theory__arith_8h_source.html#l00044">CVC3::MULT</a>, <a class="el" href="translator_8h_source.html#l00052">CVC3::NOT_USED</a>, <a class="el" href="theory__arith_8h_source.html#l00042">CVC3::PLUS</a>, <a class="el" href="kinds_8h_source.html#l00037">RATIONAL_EXPR</a>, <a class="el" href="theory__array_8h_source.html#l00032">CVC3::READ</a>, <a class="el" href="theory__arith_8h_source.html#l00033">CVC3::REAL_CONST</a>, <a class="el" href="lang_8h_source.html#l00052">CVC3::SMTLIB_V2_LANG</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="theory__arith_8h_source.html#l00041">CVC3::UMINUS</a>, and <a class="el" href="theory__array_8h_source.html#l00033">CVC3::WRITE</a>.</p>
</div>
</div>
<a class="anchor" id="ab0934eb91855a58064402f48bf4b4ad5"></a><!-- doxytag: member="CVC3::Translator::preprocess2" ref="ab0934eb91855a58064402f48bf4b4ad5" args="(const Expr &e, ExprMap< Expr > &cache)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> Translator::preprocess2 </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>< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>cache</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8cpp_source.html#l00783">783</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, and <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>.</p>
</div>
</div>
<a class="anchor" id="aa41988d7a85be9e3b68a053ef1db50b6"></a><!-- doxytag: member="CVC3::Translator::containsArray" ref="aa41988d7a85be9e3b68a053ef1db50b6" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Translator::containsArray </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><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8cpp_source.html#l00799">799</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="theory__array_8h_source.html#l00031">CVC3::ARRAY</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, and <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l00939">dump()</a>.</p>
</div>
</div>
<a class="anchor" id="a5e42669a5a6f0a69ae33fde3ccedb8bb"></a><!-- doxytag: member="CVC3::Translator::processType" ref="a5e42669a5a6f0a69ae33fde3ccedb8bb" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> Translator::processType </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><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8cpp_source.html#l01063">1063</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theory__array_8h_source.html#l00031">CVC3::ARRAY</a>, <a class="el" href="theory__bitvector_8h_source.html#l00036">CVC3::BITVECTOR</a>, <a class="el" href="translator_8h_source.html#l00114">d_arrayType</a>, <a class="el" href="translator_8h_source.html#l00088">d_ax</a>, <a class="el" href="translator_8h_source.html#l00097">d_convertToBV</a>, <a class="el" href="translator_8h_source.html#l00113">d_elementType</a>, <a class="el" href="translator_8h_source.html#l00088">d_intIntArray</a>, <a class="el" href="translator_8h_source.html#l00088">d_intIntRealArray</a>, <a class="el" href="translator_8h_source.html#l00088">d_intRealArray</a>, <a class="el" href="translator_8h_source.html#l00090">d_intUsed</a>, <a class="el" href="translator_8h_source.html#l00063">d_real2int</a>, <a class="el" href="translator_8h_source.html#l00089">d_realUsed</a>, <a class="el" href="translator_8h_source.html#l00101">d_theoryArith</a>, <a class="el" href="translator_8h_source.html#l00106">d_theoryBitvector</a>, <a class="el" href="translator_8h_source.html#l00099">d_theoryCore</a>, <a class="el" href="translator_8h_source.html#l00088">d_unknown</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="theory__core_8h_source.html#l00350">CVC3::TheoryCore::getFlags()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="theory__arith_8h_source.html#l00038">CVC3::INT</a>, <a class="el" href="theory__arith_8h_source.html#l00153">CVC3::TheoryArith::intType()</a>, <a class="el" href="theory__array_8h_source.html#l00109">CVC3::isArray()</a>, <a class="el" href="theory__arith_8h_source.html#l00174">CVC3::isInt()</a>, <a class="el" href="theory__arith_8h_source.html#l00173">CVC3::isReal()</a>, <a class="el" href="theory__bitvector_8h_source.html#l00307">CVC3::TheoryBitvector::newBitvectorType()</a>, <a class="el" href="theory__arith_8h_source.html#l00037">CVC3::REAL</a>, <a class="el" href="theory_8h_source.html#l00102">CVC3::Theory::setUsed()</a>, <a class="el" href="theory__arith_8h_source.html#l00039">CVC3::SUBRANGE</a>, <a class="el" href="theory_8cpp_source.html#l00252">CVC3::Theory::theoryOf()</a>, and <a class="el" href="kinds_8h_source.html#l00056">TYPEDECL</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>.</p>
</div>
</div>
<a class="anchor" id="ad0209b8b429fc08f7cd500aae0f35792"></a><!-- doxytag: member="CVC3::Translator::start" ref="ad0209b8b429fc08f7cd500aae0f35792" args="(const std::string &dumpFile)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Translator::start </td>
<td>(</td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>dumpFile</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8cpp_source.html#l00845">845</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00086">d_dump</a>, <a class="el" href="translator_8h_source.html#l00086">d_dumpFileOpen</a>, <a class="el" href="translator_8h_source.html#l00061">d_em</a>, <a class="el" href="translator_8h_source.html#l00083">d_osdump</a>, <a class="el" href="translator_8h_source.html#l00084">d_osdumpFile</a>, <a class="el" href="translator_8h_source.html#l00085">d_tmpFile</a>, <a class="el" href="translator_8h_source.html#l00062">d_translate</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="translator_8cpp_source.html#l00045">fileToSMTLIBIdentifier()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00360">CVC3::ExprManager::getOutputLang()</a>, <a class="el" href="lang_8h_source.html#l00034">CVC3::SMTLIB_LANG</a>, and <a class="el" href="lang_8h_source.html#l00049">CVC3::SPASS_LANG</a>.</p>
</div>
</div>
<a class="anchor" id="a2085a4f56a069befeaf2de05d78312a0"></a><!-- doxytag: member="CVC3::Translator::dump" ref="a2085a4f56a069befeaf2de05d78312a0" args="(const Expr &e, bool dumpOnly=false)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Translator::dump </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">bool </td>
<td class="paramname"><em>dumpOnly</em> = <code>false</code> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Dump the expression in the current output language </p>
<dl><dt><b>Parameters:</b></dt><dd>
<table class="params">
<tr><td class="paramname">dumpOnly</td><td>When false, the expression is output both when translating and when producing a trace of commands. When true, the expression is only output when producing a trace of commands (i.e. ignored during translation). </td></tr>
</table>
</dd>
</dl>
<p>Definition at line <a class="el" href="translator_8cpp_source.html#l00939">939</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theory__array_8h_source.html#l00031">CVC3::ARRAY</a>, <a class="el" href="kinds_8h_source.html#l00051">ARROW</a>, <a class="el" href="kinds_8h_source.html#l00240">CONST</a>, <a class="el" href="translator_8cpp_source.html#l00799">containsArray()</a>, <a class="el" href="translator_8h_source.html#l00069">d_convertArray</a>, <a class="el" href="translator_8h_source.html#l00086">d_dump</a>, <a class="el" href="translator_8h_source.html#l00109">d_dumpExprs</a>, <a class="el" href="translator_8h_source.html#l00062">d_translate</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>.</p>
</div>
</div>
<a class="anchor" id="ad7100f7c31841078e4d298aa415694e0"></a><!-- doxytag: member="CVC3::Translator::dumpAssertion" ref="ad7100f7c31841078e4d298aa415694e0" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Translator::dumpAssertion </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>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8cpp_source.html#l00970">970</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00093">ASSERT</a>, <a class="el" href="translator_8h_source.html#l00109">d_dumpExprs</a>, and <a class="el" href="translator_8h_source.html#l00062">d_translate</a>.</p>
</div>
</div>
<a class="anchor" id="a0642e4129e907824a8ac54d4cb89462f"></a><!-- doxytag: member="CVC3::Translator::dumpQuery" ref="a0642e4129e907824a8ac54d4cb89462f" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Translator::dumpQuery </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>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8cpp_source.html#l00978">978</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00109">d_dumpExprs</a>, <a class="el" href="translator_8h_source.html#l00062">d_translate</a>, and <a class="el" href="kinds_8h_source.html#l00094">QUERY</a>.</p>
</div>
</div>
<a class="anchor" id="abafa3e4622d8ef21e29d79c7efb20053"></a><!-- doxytag: member="CVC3::Translator::dumpQueryResult" ref="abafa3e4622d8ef21e29d79c7efb20053" args="(QueryResult qres)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Translator::dumpQueryResult </td>
<td>(</td>
<td class="paramtype"><a class="el" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> </td>
<td class="paramname"><em>qres</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8cpp_source.html#l00986">986</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00061">d_em</a>, <a class="el" href="translator_8h_source.html#l00083">d_osdump</a>, <a class="el" href="translator_8h_source.html#l00062">d_translate</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00360">CVC3::ExprManager::getOutputLang()</a>, <a class="el" href="queryresult_8h_source.html#l00033">CVC3::SATISFIABLE</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="lang_8h_source.html#l00049">CVC3::SPASS_LANG</a>, and <a class="el" href="queryresult_8h_source.html#l00036">CVC3::UNSATISFIABLE</a>.</p>
</div>
</div>
<a class="anchor" id="a444765aa6bbf793c1ddbc66e9fb829fe"></a><!-- doxytag: member="CVC3::Translator::finish" ref="a444765aa6bbf793c1ddbc66e9fb829fe" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Translator::finish </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="translator_8cpp_source.html#l01145">1145</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00067">AND</a>, <a class="el" href="kinds_8h_source.html#l00138">ANNOTATION</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theory__array_8h_source.html#l00116">CVC3::arrayType()</a>, <a class="el" href="kinds_8h_source.html#l00051">ARROW</a>, <a class="el" href="kinds_8h_source.html#l00093">ASSERT</a>, <a class="el" href="kinds_8h_source.html#l00048">BOOLEAN</a>, <a class="el" href="translator_8h_source.html#l00183">category()</a>, <a class="el" href="kinds_8h_source.html#l00240">CONST</a>, <a class="el" href="translator_8h_source.html#l00094">d_arithUsed</a>, <a class="el" href="translator_8h_source.html#l00111">d_arrayConvertMap</a>, <a class="el" href="translator_8h_source.html#l00114">d_arrayType</a>, <a class="el" href="translator_8h_source.html#l00088">d_ax</a>, <a class="el" href="translator_8h_source.html#l00070">d_combineAssump</a>, <a class="el" href="translator_8h_source.html#l00069">d_convertArray</a>, <a class="el" href="translator_8h_source.html#l00097">d_convertToBV</a>, <a class="el" href="translator_8h_source.html#l00086">d_dump</a>, <a class="el" href="translator_8h_source.html#l00109">d_dumpExprs</a>, <a class="el" href="translator_8h_source.html#l00086">d_dumpFileOpen</a>, <a class="el" href="translator_8h_source.html#l00113">d_elementType</a>, <a class="el" href="translator_8h_source.html#l00061">d_em</a>, <a class="el" href="translator_8h_source.html#l00115">d_equalities</a>, <a class="el" href="translator_8h_source.html#l00067">d_expResult</a>, <a class="el" href="translator_8h_source.html#l00112">d_indexType</a>, <a class="el" href="translator_8h_source.html#l00091">d_intConstUsed</a>, <a class="el" href="translator_8h_source.html#l00088">d_intIntArray</a>, <a class="el" href="translator_8h_source.html#l00090">d_intUsed</a>, <a class="el" href="translator_8h_source.html#l00092">d_langUsed</a>, <a class="el" href="translator_8h_source.html#l00083">d_osdump</a>, <a class="el" href="translator_8h_source.html#l00084">d_osdumpFile</a>, <a class="el" href="translator_8h_source.html#l00089">d_realUsed</a>, <a class="el" href="translator_8h_source.html#l00080">d_replaceSymbols</a>, <a class="el" href="translator_8h_source.html#l00102">d_theoryArray</a>, <a class="el" href="translator_8h_source.html#l00106">d_theoryBitvector</a>, <a class="el" href="translator_8h_source.html#l00099">d_theoryCore</a>, <a class="el" href="translator_8h_source.html#l00107">d_theoryDatatype</a>, <a class="el" href="translator_8h_source.html#l00103">d_theoryQuant</a>, <a class="el" href="translator_8h_source.html#l00104">d_theoryRecords</a>, <a class="el" href="translator_8h_source.html#l00105">d_theorySimulate</a>, <a class="el" href="translator_8h_source.html#l00100">d_theoryUF</a>, <a class="el" href="translator_8h_source.html#l00062">d_translate</a>, <a class="el" href="translator_8h_source.html#l00093">d_UFIDL_ok</a>, <a class="el" href="translator_8h_source.html#l00088">d_unknown</a>, <a class="el" href="translator_8h_source.html#l00096">d_zeroVar</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="translator_8h_source.html#l00054">CVC3::DIFF_ONLY</a>, <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>, <a class="el" href="theory_8cpp_source.html#l00383">CVC3::Theory::getBaseType()</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="theory__core_8h_source.html#l00350">CVC3::TheoryCore::getFlags()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00360">CVC3::ExprManager::getOutputLang()</a>, <a class="el" href="expr_8h_source.html#l01055">CVC3::Expr::getString()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="kinds_8h_source.html#l00046">ID</a>, <a class="el" href="theory__arith_8h_source.html#l00173">CVC3::isReal()</a>, <a class="el" href="translator_8h_source.html#l00055">CVC3::LINEAR</a>, <a class="el" href="expr_8h_source.html#l00937">CVC3::Expr::negate()</a>, <a class="el" href="expr__manager_8h_source.html#l00468">CVC3::ExprManager::newStringExpr()</a>, <a class="el" href="theory_8cpp_source.html#l00790">CVC3::Theory::newTypeExpr()</a>, <a class="el" href="translator_8h_source.html#l00056">CVC3::NONLINEAR</a>, <a class="el" href="kinds_8h_source.html#l00066">NOT</a>, <a class="el" href="translator_8h_source.html#l00052">CVC3::NOT_USED</a>, <a class="el" href="translator_8cpp_source.html#l00549">preprocess()</a>, <a class="el" href="translator_8cpp_source.html#l00783">preprocess2()</a>, <a class="el" href="lang_8h_source.html#l00032">CVC3::PRESENTATION_LANG</a>, <a class="el" href="translator_8cpp_source.html#l01063">processType()</a>, <a class="el" href="kinds_8h_source.html#l00094">QUERY</a>, <a class="el" href="translator_8cpp_source.html#l01830">quoteAnnotation()</a>, <a class="el" href="kinds_8h_source.html#l00044">RAW_LIST</a>, <a class="el" href="theory__array_8h_source.html#l00032">CVC3::READ</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="translator_8h_source.html#l00181">source()</a>, <a class="el" href="lang_8h_source.html#l00049">CVC3::SPASS_LANG</a>, <a class="el" href="translator_8h_source.html#l00179">status()</a>, <a class="el" href="kinds_8h_source.html#l00038">STRING_EXPR</a>, <a class="el" href="theory_8h_source.html#l00104">CVC3::Theory::theoryUsed()</a>, <a class="el" href="kinds_8h_source.html#l00053">TYPE</a>, and <a class="el" href="kinds_8h_source.html#l00242">UCONST</a>.</p>
</div>
</div>
<a class="anchor" id="ae54e65770cca9121bd7edb3066db0cca"></a><!-- doxytag: member="CVC3::Translator::setTheoryCore" ref="ae54e65770cca9121bd7edb3066db0cca" args="(TheoryCore *theoryCore)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Translator::setTheoryCore </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> * </td>
<td class="paramname"><em>theoryCore</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00166">166</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00099">d_theoryCore</a>.</p>
</div>
</div>
<a class="anchor" id="ac90246c6882f3afb6dfa2c1cd28bee77"></a><!-- doxytag: member="CVC3::Translator::setTheoryUF" ref="ac90246c6882f3afb6dfa2c1cd28bee77" args="(TheoryUF *theoryUF)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Translator::setTheoryUF </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryUF.html">TheoryUF</a> * </td>
<td class="paramname"><em>theoryUF</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00167">167</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00100">d_theoryUF</a>.</p>
</div>
</div>
<a class="anchor" id="a56398996b69a8ae5f2d483cac21c06b4"></a><!-- doxytag: member="CVC3::Translator::setTheoryArith" ref="a56398996b69a8ae5f2d483cac21c06b4" args="(TheoryArith *theoryArith)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Translator::setTheoryArith </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryArith.html">TheoryArith</a> * </td>
<td class="paramname"><em>theoryArith</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00168">168</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00101">d_theoryArith</a>.</p>
</div>
</div>
<a class="anchor" id="ae98b6dcd49033de9e7af75bf832ed907"></a><!-- doxytag: member="CVC3::Translator::setTheoryArray" ref="ae98b6dcd49033de9e7af75bf832ed907" args="(TheoryArray *theoryArray)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Translator::setTheoryArray </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryArray.html">TheoryArray</a> * </td>
<td class="paramname"><em>theoryArray</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00169">169</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00102">d_theoryArray</a>.</p>
</div>
</div>
<a class="anchor" id="afa7244fb9f0b749548fe1702238a1d29"></a><!-- doxytag: member="CVC3::Translator::setTheoryQuant" ref="afa7244fb9f0b749548fe1702238a1d29" args="(TheoryQuant *theoryQuant)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Translator::setTheoryQuant </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryQuant.html">TheoryQuant</a> * </td>
<td class="paramname"><em>theoryQuant</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00170">170</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00103">d_theoryQuant</a>.</p>
</div>
</div>
<a class="anchor" id="a072d9f51dc77cf2e1d1c4b7ebafd4d1d"></a><!-- doxytag: member="CVC3::Translator::setTheoryRecords" ref="a072d9f51dc77cf2e1d1c4b7ebafd4d1d" args="(TheoryRecords *theoryRecords)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Translator::setTheoryRecords </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryRecords.html">TheoryRecords</a> * </td>
<td class="paramname"><em>theoryRecords</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00171">171</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00104">d_theoryRecords</a>.</p>
</div>
</div>
<a class="anchor" id="a8c47c28bbcfb39b3dc8244eda47a5dc9"></a><!-- doxytag: member="CVC3::Translator::setTheorySimulate" ref="a8c47c28bbcfb39b3dc8244eda47a5dc9" args="(TheorySimulate *theorySimulate)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Translator::setTheorySimulate </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheorySimulate.html">TheorySimulate</a> * </td>
<td class="paramname"><em>theorySimulate</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00172">172</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00105">d_theorySimulate</a>.</p>
</div>
</div>
<a class="anchor" id="a87f9011a441dd3c772c0efc8d73e8548"></a><!-- doxytag: member="CVC3::Translator::setTheoryBitvector" ref="a87f9011a441dd3c772c0efc8d73e8548" args="(TheoryBitvector *theoryBitvector)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Translator::setTheoryBitvector </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryBitvector.html">TheoryBitvector</a> * </td>
<td class="paramname"><em>theoryBitvector</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00173">173</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00106">d_theoryBitvector</a>.</p>
</div>
</div>
<a class="anchor" id="a9fdb4320a2310af16ef6caacdff8ab5c"></a><!-- doxytag: member="CVC3::Translator::setTheoryDatatype" ref="a9fdb4320a2310af16ef6caacdff8ab5c" args="(TheoryDatatype *theoryDatatype)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Translator::setTheoryDatatype </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryDatatype.html">TheoryDatatype</a> * </td>
<td class="paramname"><em>theoryDatatype</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00174">174</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00107">d_theoryDatatype</a>.</p>
</div>
</div>
<a class="anchor" id="a9db51995d5dc21b254bfeb5381b4ce5a"></a><!-- doxytag: member="CVC3::Translator::setBenchName" ref="a9db51995d5dc21b254bfeb5381b4ce5a" args="(std::string name)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Translator::setBenchName </td>
<td>(</td>
<td class="paramtype">std::string </td>
<td class="paramname"><em>name</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00176">176</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00118">d_benchName</a>.</p>
</div>
</div>
<a class="anchor" id="ad5c28f74006f791727b15d17a3a20650"></a><!-- doxytag: member="CVC3::Translator::benchName" ref="ad5c28f74006f791727b15d17a3a20650" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string CVC3::Translator::benchName </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00177">177</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00118">d_benchName</a>.</p>
</div>
</div>
<a class="anchor" id="a4c9d948f111bd360e937b170a2c95120"></a><!-- doxytag: member="CVC3::Translator::setStatus" ref="a4c9d948f111bd360e937b170a2c95120" args="(std::string status)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Translator::setStatus </td>
<td>(</td>
<td class="paramtype">std::string </td>
<td class="paramname"><em>status</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00178">178</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00120">d_status</a>, and <a class="el" href="translator_8h_source.html#l00179">status()</a>.</p>
</div>
</div>
<a class="anchor" id="aee4bdef7291181744580934a93849b64"></a><!-- doxytag: member="CVC3::Translator::status" ref="aee4bdef7291181744580934a93849b64" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string CVC3::Translator::status </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00179">179</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00120">d_status</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8h_source.html#l00178">setStatus()</a>.</p>
</div>
</div>
<a class="anchor" id="ac9c933a8ce7265f0463c8556c8eb624c"></a><!-- doxytag: member="CVC3::Translator::setSource" ref="ac9c933a8ce7265f0463c8556c8eb624c" args="(std::string source)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Translator::setSource </td>
<td>(</td>
<td class="paramtype">std::string </td>
<td class="paramname"><em>source</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00180">180</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00122">d_source</a>, and <a class="el" href="translator_8h_source.html#l00181">source()</a>.</p>
</div>
</div>
<a class="anchor" id="ad57a63292d37aa81d56c3102edd99f2b"></a><!-- doxytag: member="CVC3::Translator::source" ref="ad57a63292d37aa81d56c3102edd99f2b" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string CVC3::Translator::source </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00181">181</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00122">d_source</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8h_source.html#l00180">setSource()</a>.</p>
</div>
</div>
<a class="anchor" id="aed753d381e5cec7619b8324a7588b874"></a><!-- doxytag: member="CVC3::Translator::setCategory" ref="aed753d381e5cec7619b8324a7588b874" args="(std::string category)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::Translator::setCategory </td>
<td>(</td>
<td class="paramtype">std::string </td>
<td class="paramname"><em>category</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00182">182</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00183">category()</a>, and <a class="el" href="translator_8h_source.html#l00068">d_category</a>.</p>
</div>
</div>
<a class="anchor" id="af1a89762818192869c5d2161dab0a167"></a><!-- doxytag: member="CVC3::Translator::category" ref="af1a89762818192869c5d2161dab0a167" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string CVC3::Translator::category </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00183">183</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00068">d_category</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8h_source.html#l00182">setCategory()</a>.</p>
</div>
</div>
<a class="anchor" id="a0ee4f6a5cf7bb40bfe341e4b99f06810"></a><!-- doxytag: member="CVC3::Translator::fixConstName" ref="a0ee4f6a5cf7bb40bfe341e4b99f06810" args="(const std::string &s)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const string Translator::fixConstName </td>
<td>(</td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>s</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8cpp_source.html#l01804">1804</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00061">d_em</a>, <a class="el" href="translator_8h_source.html#l00080">d_replaceSymbols</a>, <a class="el" href="hash__map_8h_source.html#l00257">Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::end()</a>, <a class="el" href="hash__map_8h_source.html#l00171">Hash::hash_map< _Key, _Data, _HashFcn, _EqualKey >::find()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00360">CVC3::ExprManager::getOutputLang()</a>, and <a class="el" href="lang_8h_source.html#l00034">CVC3::SMTLIB_LANG</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>, <a class="el" href="theory__uf_8cpp_source.html#l00657">CVC3::TheoryUF::printSmtLibShared()</a>, and <a class="el" href="theory__core_8cpp_source.html#l01915">CVC3::TheoryCore::printSmtLibShared()</a>.</p>
</div>
</div>
<a class="anchor" id="a6821f774dda2d0964fde109b29de20a8"></a><!-- doxytag: member="CVC3::Translator::escapeSymbol" ref="a6821f774dda2d0964fde109b29de20a8" args="(const std::string &s)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const string Translator::escapeSymbol </td>
<td>(</td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>s</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8cpp_source.html#l01816">1816</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00061">d_em</a>, <a class="el" href="expr__manager_8cpp_source.html#l00360">CVC3::ExprManager::getOutputLang()</a>, and <a class="el" href="lang_8h_source.html#l00052">CVC3::SMTLIB_V2_LANG</a>.</p>
<p>Referenced by <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>, and <a class="el" href="theory__core_8cpp_source.html#l01915">CVC3::TheoryCore::printSmtLibShared()</a>.</p>
</div>
</div>
<a class="anchor" id="a90238a14586a6582a741bebebce13010"></a><!-- doxytag: member="CVC3::Translator::quoteAnnotation" ref="a90238a14586a6582a741bebebce13010" args="(const std::string &s)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const string Translator::quoteAnnotation </td>
<td>(</td>
<td class="paramtype">const std::string & </td>
<td class="paramname"><em>s</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8cpp_source.html#l01830">1830</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="theory__core_8cpp_source.html#l02055">CVC3::TheoryCore::print()</a>.</p>
</div>
</div>
<a class="anchor" id="ab562bf78b184a0039093ce0dba0770d0"></a><!-- doxytag: member="CVC3::Translator::printArrayExpr" ref="ab562bf78b184a0039093ce0dba0770d0" args="(ExprStream &os, const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool Translator::printArrayExpr </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprStream.html">ExprStream</a> & </td>
<td class="paramname"><em>os</em>, </td>
</tr>
<tr>
<td class="paramkey"></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></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Returns true if expression has been printed. </p>
<p>If false is returned, array theory should print expression as usual </p>
<p>Definition at line <a class="el" href="translator_8cpp_source.html#l01850">1850</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="theory__array_8h_source.html#l00031">CVC3::ARRAY</a>, <a class="el" href="theory__array_8h_source.html#l00036">CVC3::ARRAY_LITERAL</a>, <a class="el" href="kinds_8h_source.html#l00051">ARROW</a>, <a class="el" href="theory__bitvector_8h_source.html#l00036">CVC3::BITVECTOR</a>, <a class="el" href="translator_8h_source.html#l00069">d_convertArray</a>, <a class="el" href="translator_8h_source.html#l00061">d_em</a>, <a class="el" href="translator_8h_source.html#l00088">d_intIntArray</a>, <a class="el" href="translator_8h_source.html#l00088">d_intIntRealArray</a>, <a class="el" href="translator_8h_source.html#l00088">d_intRealArray</a>, <a class="el" href="translator_8h_source.html#l00106">d_theoryBitvector</a>, <a class="el" href="translator_8h_source.html#l00088">d_unknown</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theory__bitvector_8cpp_source.html#l05331">CVC3::TheoryBitvector::getBitvectorTypeParam()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01050">CVC3::Expr::getName()</a>, <a class="el" href="expr__manager_8cpp_source.html#l00360">CVC3::ExprManager::getOutputLang()</a>, <a class="el" href="theory__array_8h_source.html#l00109">CVC3::isArray()</a>, <a class="el" href="theory__arith_8h_source.html#l00174">CVC3::isInt()</a>, <a class="el" href="theory__arith_8h_source.html#l00173">CVC3::isReal()</a>, <a class="el" href="expr__manager_8h_source.html#l00481">CVC3::ExprManager::newSymbolExpr()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00332">CVC3::nodag()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00301">CVC3::pop()</a>, <a class="el" href="expr__stream_8cpp_source.html#l00298">CVC3::push()</a>, <a class="el" href="theory__array_8h_source.html#l00032">CVC3::READ</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="expr__stream_8cpp_source.html#l00326">CVC3::space()</a>, <a class="el" href="kinds_8h_source.html#l00056">TYPEDECL</a>, <a class="el" href="kinds_8h_source.html#l00242">UCONST</a>, <a class="el" href="kinds_8h_source.html#l00088">UFUNC</a>, and <a class="el" href="theory__array_8h_source.html#l00033">CVC3::WRITE</a>.</p>
</div>
</div>
<a class="anchor" id="a89f83c6d0dcc3416b7b5facd68753e80"></a><!-- doxytag: member="CVC3::Translator::zeroVar" ref="a89f83c6d0dcc3416b7b5facd68753e80" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> Translator::zeroVar </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="translator_8cpp_source.html#l01943">1943</a> of file <a class="el" href="translator_8cpp_source.html">translator.cpp</a>.</p>
<p>References <a class="el" href="translator_8h_source.html#l00065">d_convertToDiff</a>, <a class="el" href="translator_8h_source.html#l00101">d_theoryArith</a>, <a class="el" href="translator_8h_source.html#l00099">d_theoryCore</a>, <a class="el" href="translator_8h_source.html#l00096">d_zeroVar</a>, <a class="el" href="type_8h_source.html#l00052">CVC3::Type::getExpr()</a>, <a class="el" href="theory__arith_8h_source.html#l00153">CVC3::TheoryArith::intType()</a>, <a class="el" href="theory_8cpp_source.html#l00569">CVC3::Theory::newVar()</a>, and <a class="el" href="theory__arith_8h_source.html#l00152">CVC3::TheoryArith::realType()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="a913d9fbcdfbb4d17e3864a74480b0611"></a><!-- doxytag: member="CVC3::Translator::d_em" ref="a913d9fbcdfbb4d17e3864a74480b0611" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprManager.html">ExprManager</a>* <a class="el" href="classCVC3_1_1Translator.html#a913d9fbcdfbb4d17e3864a74480b0611">CVC3::Translator::d_em</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00061">61</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l00986">dumpQueryResult()</a>, <a class="el" href="translator_8cpp_source.html#l01816">escapeSymbol()</a>, <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, <a class="el" href="translator_8cpp_source.html#l01804">fixConstName()</a>, <a class="el" href="translator_8cpp_source.html#l01850">printArrayExpr()</a>, and <a class="el" href="translator_8cpp_source.html#l00845">start()</a>.</p>
</div>
</div>
<a class="anchor" id="a62b1d8ae4ec79cfb22725dd4635d59de"></a><!-- doxytag: member="CVC3::Translator::d_translate" ref="a62b1d8ae4ec79cfb22725dd4635d59de" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const bool& <a class="el" href="classCVC3_1_1Translator.html#a62b1d8ae4ec79cfb22725dd4635d59de">CVC3::Translator::d_translate</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00062">62</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l00939">dump()</a>, <a class="el" href="translator_8cpp_source.html#l00970">dumpAssertion()</a>, <a class="el" href="translator_8cpp_source.html#l00978">dumpQuery()</a>, <a class="el" href="translator_8cpp_source.html#l00986">dumpQueryResult()</a>, <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8cpp_source.html#l00845">start()</a>.</p>
</div>
</div>
<a class="anchor" id="a54add6521f2f005b84cdd129d64764f2"></a><!-- doxytag: member="CVC3::Translator::d_real2int" ref="a54add6521f2f005b84cdd129d64764f2" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const bool& <a class="el" href="classCVC3_1_1Translator.html#a54add6521f2f005b84cdd129d64764f2">CVC3::Translator::d_real2int</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00063">63</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01063">processType()</a>.</p>
</div>
</div>
<a class="anchor" id="a4f578f10a492640eec9ff8de157cc521"></a><!-- doxytag: member="CVC3::Translator::d_convertArith" ref="a4f578f10a492640eec9ff8de157cc521" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const bool& <a class="el" href="classCVC3_1_1Translator.html#a4f578f10a492640eec9ff8de157cc521">CVC3::Translator::d_convertArith</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00064">64</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
</div>
</div>
<a class="anchor" id="ac20944f0dfa8772fd1e4c1ad757bf9da"></a><!-- doxytag: member="CVC3::Translator::d_convertToDiff" ref="ac20944f0dfa8772fd1e4c1ad757bf9da" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const std::string& <a class="el" href="classCVC3_1_1Translator.html#ac20944f0dfa8772fd1e4c1ad757bf9da">CVC3::Translator::d_convertToDiff</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00065">65</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01943">zeroVar()</a>.</p>
</div>
</div>
<a class="anchor" id="afd9c853a8d17a1c7905bb007f1494ce0"></a><!-- doxytag: member="CVC3::Translator::d_iteLiftArith" ref="afd9c853a8d17a1c7905bb007f1494ce0" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1Translator.html#afd9c853a8d17a1c7905bb007f1494ce0">CVC3::Translator::d_iteLiftArith</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00066">66</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
</div>
</div>
<a class="anchor" id="a755c43c5f5be61e8c3c034dccaef33ba"></a><!-- doxytag: member="CVC3::Translator::d_expResult" ref="a755c43c5f5be61e8c3c034dccaef33ba" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const std::string& <a class="el" href="classCVC3_1_1Translator.html#a755c43c5f5be61e8c3c034dccaef33ba">CVC3::Translator::d_expResult</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00067">67</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>.</p>
</div>
</div>
<a class="anchor" id="a4a4f7719dd2741c94c88111015846099"></a><!-- doxytag: member="CVC3::Translator::d_category" ref="a4a4f7719dd2741c94c88111015846099" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string <a class="el" href="classCVC3_1_1Translator.html#a4a4f7719dd2741c94c88111015846099">CVC3::Translator::d_category</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00068">68</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8h_source.html#l00183">category()</a>, and <a class="el" href="translator_8h_source.html#l00182">setCategory()</a>.</p>
</div>
</div>
<a class="anchor" id="ab09c1e81131dfc2d3a4da1f859a8108e"></a><!-- doxytag: member="CVC3::Translator::d_convertArray" ref="ab09c1e81131dfc2d3a4da1f859a8108e" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1Translator.html#ab09c1e81131dfc2d3a4da1f859a8108e">CVC3::Translator::d_convertArray</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00069">69</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l00939">dump()</a>, <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8cpp_source.html#l01850">printArrayExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="a72b7aff947a816fbf26f7a97ce0f5fdd"></a><!-- doxytag: member="CVC3::Translator::d_combineAssump" ref="a72b7aff947a816fbf26f7a97ce0f5fdd" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1Translator.html#a72b7aff947a816fbf26f7a97ce0f5fdd">CVC3::Translator::d_combineAssump</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00070">70</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>.</p>
</div>
</div>
<a class="anchor" id="ad81beb93ee2668558c897398ce68fa44"></a><!-- doxytag: member="CVC3::Translator::d_replaceSymbols" ref="ad81beb93ee2668558c897398ce68fa44" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classHash_1_1hash__map.html">std::hash_map</a><std::string, std::string, <a class="el" href="classCVC3_1_1Translator_1_1HashString.html">HashString</a>> <a class="el" href="classCVC3_1_1Translator.html#ad81beb93ee2668558c897398ce68fa44">CVC3::Translator::d_replaceSymbols</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00080">80</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8cpp_source.html#l01804">fixConstName()</a>.</p>
</div>
</div>
<a class="anchor" id="a61574c04bd74489b4438ca890f3ec7b4"></a><!-- doxytag: member="CVC3::Translator::d_osdump" ref="a61574c04bd74489b4438ca890f3ec7b4" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::ostream* <a class="el" href="classCVC3_1_1Translator.html#a61574c04bd74489b4438ca890f3ec7b4">CVC3::Translator::d_osdump</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>The log file for top-level API calls in the <a class="el" href="namespaceCVC3.html">CVC3</a> input language. </p>
<p>Definition at line <a class="el" href="translator_8h_source.html#l00083">83</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l00986">dumpQueryResult()</a>, <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8cpp_source.html#l00845">start()</a>.</p>
</div>
</div>
<a class="anchor" id="a78a511690ef1f3421862b39dad9d02f7"></a><!-- doxytag: member="CVC3::Translator::d_osdumpFile" ref="a78a511690ef1f3421862b39dad9d02f7" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::ofstream <a class="el" href="classCVC3_1_1Translator.html#a78a511690ef1f3421862b39dad9d02f7">CVC3::Translator::d_osdumpFile</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00084">84</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8cpp_source.html#l00845">start()</a>.</p>
</div>
</div>
<a class="anchor" id="ac55f4fdc4bbb29ccd09dfda38a6eeb91"></a><!-- doxytag: member="CVC3::Translator::d_tmpFile" ref="ac55f4fdc4bbb29ccd09dfda38a6eeb91" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::ifstream <a class="el" href="classCVC3_1_1Translator.html#ac55f4fdc4bbb29ccd09dfda38a6eeb91">CVC3::Translator::d_tmpFile</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00085">85</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l00845">start()</a>.</p>
</div>
</div>
<a class="anchor" id="ac5e47db270e1b8d4ee40fe2654382413"></a><!-- doxytag: member="CVC3::Translator::d_dump" ref="ac5e47db270e1b8d4ee40fe2654382413" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1Translator.html#ac5e47db270e1b8d4ee40fe2654382413">CVC3::Translator::d_dump</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00086">86</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l00939">dump()</a>, <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8cpp_source.html#l00845">start()</a>.</p>
</div>
</div>
<a class="anchor" id="a86e279b67edf39d32056d279a4f9de3b"></a><!-- doxytag: member="CVC3::Translator::d_dumpFileOpen" ref="a86e279b67edf39d32056d279a4f9de3b" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1Translator.html#a86e279b67edf39d32056d279a4f9de3b">CVC3::Translator::d_dumpFileOpen</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00086">86</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8cpp_source.html#l00845">start()</a>.</p>
</div>
</div>
<a class="anchor" id="aa4dc3a71a03482ba8bb6ff8579e09781"></a><!-- doxytag: member="CVC3::Translator::d_intIntArray" ref="aa4dc3a71a03482ba8bb6ff8579e09781" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1Translator.html#aa4dc3a71a03482ba8bb6ff8579e09781">CVC3::Translator::d_intIntArray</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00088">88</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, <a class="el" href="translator_8cpp_source.html#l01850">printArrayExpr()</a>, and <a class="el" href="translator_8cpp_source.html#l01063">processType()</a>.</p>
</div>
</div>
<a class="anchor" id="aca1de6c7f5ab780b57d10c66f58a2890"></a><!-- doxytag: member="CVC3::Translator::d_intRealArray" ref="aca1de6c7f5ab780b57d10c66f58a2890" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1Translator.html#aca1de6c7f5ab780b57d10c66f58a2890">CVC3::Translator::d_intRealArray</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00088">88</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01850">printArrayExpr()</a>, and <a class="el" href="translator_8cpp_source.html#l01063">processType()</a>.</p>
</div>
</div>
<a class="anchor" id="a69c89f774ba1fe6c13ca3559748776af"></a><!-- doxytag: member="CVC3::Translator::d_intIntRealArray" ref="a69c89f774ba1fe6c13ca3559748776af" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1Translator.html#a69c89f774ba1fe6c13ca3559748776af">CVC3::Translator::d_intIntRealArray</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00088">88</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01850">printArrayExpr()</a>, and <a class="el" href="translator_8cpp_source.html#l01063">processType()</a>.</p>
</div>
</div>
<a class="anchor" id="a0793dec1240036cde06df95a14241438"></a><!-- doxytag: member="CVC3::Translator::d_ax" ref="a0793dec1240036cde06df95a14241438" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1Translator.html#a0793dec1240036cde06df95a14241438">CVC3::Translator::d_ax</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00088">88</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8cpp_source.html#l01063">processType()</a>.</p>
</div>
</div>
<a class="anchor" id="a290235a7047226a6564add8ef5ad1f10"></a><!-- doxytag: member="CVC3::Translator::d_unknown" ref="a290235a7047226a6564add8ef5ad1f10" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1Translator.html#a290235a7047226a6564add8ef5ad1f10">CVC3::Translator::d_unknown</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00088">88</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, <a class="el" href="translator_8cpp_source.html#l01850">printArrayExpr()</a>, and <a class="el" href="translator_8cpp_source.html#l01063">processType()</a>.</p>
</div>
</div>
<a class="anchor" id="a706c02509ddc23d60d43f38af6497139"></a><!-- doxytag: member="CVC3::Translator::d_realUsed" ref="a706c02509ddc23d60d43f38af6497139" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1Translator.html#a706c02509ddc23d60d43f38af6497139">CVC3::Translator::d_realUsed</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00089">89</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8cpp_source.html#l01063">processType()</a>.</p>
</div>
</div>
<a class="anchor" id="a18db4e99db8f78e67992cb3cf68dee28"></a><!-- doxytag: member="CVC3::Translator::d_intUsed" ref="a18db4e99db8f78e67992cb3cf68dee28" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1Translator.html#a18db4e99db8f78e67992cb3cf68dee28">CVC3::Translator::d_intUsed</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00090">90</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8cpp_source.html#l01063">processType()</a>.</p>
</div>
</div>
<a class="anchor" id="a2e326c83175674acde79b1e33fe391b7"></a><!-- doxytag: member="CVC3::Translator::d_intConstUsed" ref="a2e326c83175674acde79b1e33fe391b7" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1Translator.html#a2e326c83175674acde79b1e33fe391b7">CVC3::Translator::d_intConstUsed</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00091">91</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>.</p>
</div>
</div>
<a class="anchor" id="aa6d9fb46298801972cb082ec6eb9918d"></a><!-- doxytag: member="CVC3::Translator::d_langUsed" ref="aa6d9fb46298801972cb082ec6eb9918d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7c">ArithLang</a> <a class="el" href="classCVC3_1_1Translator.html#aa6d9fb46298801972cb082ec6eb9918d">CVC3::Translator::d_langUsed</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00092">92</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>.</p>
</div>
</div>
<a class="anchor" id="a939bf8530ea41cd0e0c9f8621e17569d"></a><!-- doxytag: member="CVC3::Translator::d_UFIDL_ok" ref="a939bf8530ea41cd0e0c9f8621e17569d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1Translator.html#a939bf8530ea41cd0e0c9f8621e17569d">CVC3::Translator::d_UFIDL_ok</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00093">93</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>.</p>
</div>
</div>
<a class="anchor" id="a2adf399cb0475894d8b4ea870aaf4547"></a><!-- doxytag: member="CVC3::Translator::d_arithUsed" ref="a2adf399cb0475894d8b4ea870aaf4547" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="classCVC3_1_1Translator.html#a2adf399cb0475894d8b4ea870aaf4547">CVC3::Translator::d_arithUsed</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00094">94</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>.</p>
</div>
</div>
<a class="anchor" id="abff660525da18bbe419aed68df4d8564"></a><!-- doxytag: member="CVC3::Translator::d_zeroVar" ref="abff660525da18bbe419aed68df4d8564" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a>* <a class="el" href="classCVC3_1_1Translator.html#abff660525da18bbe419aed68df4d8564">CVC3::Translator::d_zeroVar</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00096">96</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8cpp_source.html#l01943">zeroVar()</a>.</p>
</div>
</div>
<a class="anchor" id="a53fdab56fe2f1e821b3f36c2641ae462"></a><!-- doxytag: member="CVC3::Translator::d_convertToBV" ref="a53fdab56fe2f1e821b3f36c2641ae462" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classCVC3_1_1Translator.html#a53fdab56fe2f1e821b3f36c2641ae462">CVC3::Translator::d_convertToBV</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00097">97</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8cpp_source.html#l01063">processType()</a>.</p>
</div>
</div>
<a class="anchor" id="a1379b7c9235c804f32ab5ce19d86a907"></a><!-- doxytag: member="CVC3::Translator::d_theoryCore" ref="a1379b7c9235c804f32ab5ce19d86a907" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a>* <a class="el" href="classCVC3_1_1Translator.html#a1379b7c9235c804f32ab5ce19d86a907">CVC3::Translator::d_theoryCore</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00099">99</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, <a class="el" href="translator_8cpp_source.html#l01063">processType()</a>, <a class="el" href="translator_8h_source.html#l00166">setTheoryCore()</a>, and <a class="el" href="translator_8cpp_source.html#l01943">zeroVar()</a>.</p>
</div>
</div>
<a class="anchor" id="a67f2340f940914d63aea99462eced2ad"></a><!-- doxytag: member="CVC3::Translator::d_theoryUF" ref="a67f2340f940914d63aea99462eced2ad" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoryUF.html">TheoryUF</a>* <a class="el" href="classCVC3_1_1Translator.html#a67f2340f940914d63aea99462eced2ad">CVC3::Translator::d_theoryUF</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00100">100</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8h_source.html#l00167">setTheoryUF()</a>.</p>
</div>
</div>
<a class="anchor" id="a0d360419c4e9e9ee9ac8e8af126534d2"></a><!-- doxytag: member="CVC3::Translator::d_theoryArith" ref="a0d360419c4e9e9ee9ac8e8af126534d2" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoryArith.html">TheoryArith</a>* <a class="el" href="classCVC3_1_1Translator.html#a0d360419c4e9e9ee9ac8e8af126534d2">CVC3::Translator::d_theoryArith</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00101">101</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01063">processType()</a>, <a class="el" href="translator_8h_source.html#l00168">setTheoryArith()</a>, and <a class="el" href="translator_8cpp_source.html#l01943">zeroVar()</a>.</p>
</div>
</div>
<a class="anchor" id="a9b8dc03475b2e90380f82bac9f71e39d"></a><!-- doxytag: member="CVC3::Translator::d_theoryArray" ref="a9b8dc03475b2e90380f82bac9f71e39d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoryArray.html">TheoryArray</a>* <a class="el" href="classCVC3_1_1Translator.html#a9b8dc03475b2e90380f82bac9f71e39d">CVC3::Translator::d_theoryArray</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00102">102</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8h_source.html#l00169">setTheoryArray()</a>.</p>
</div>
</div>
<a class="anchor" id="a5e85f73e319fbd8745c66852cfc1cad5"></a><!-- doxytag: member="CVC3::Translator::d_theoryQuant" ref="a5e85f73e319fbd8745c66852cfc1cad5" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoryQuant.html">TheoryQuant</a>* <a class="el" href="classCVC3_1_1Translator.html#a5e85f73e319fbd8745c66852cfc1cad5">CVC3::Translator::d_theoryQuant</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00103">103</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8h_source.html#l00170">setTheoryQuant()</a>.</p>
</div>
</div>
<a class="anchor" id="a0ce73787e0363fc66f6e653cbec219f6"></a><!-- doxytag: member="CVC3::Translator::d_theoryRecords" ref="a0ce73787e0363fc66f6e653cbec219f6" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoryRecords.html">TheoryRecords</a>* <a class="el" href="classCVC3_1_1Translator.html#a0ce73787e0363fc66f6e653cbec219f6">CVC3::Translator::d_theoryRecords</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00104">104</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8h_source.html#l00171">setTheoryRecords()</a>.</p>
</div>
</div>
<a class="anchor" id="a3fbe66e1fdb7b24735146f6e15d6c9da"></a><!-- doxytag: member="CVC3::Translator::d_theorySimulate" ref="a3fbe66e1fdb7b24735146f6e15d6c9da" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheorySimulate.html">TheorySimulate</a>* <a class="el" href="classCVC3_1_1Translator.html#a3fbe66e1fdb7b24735146f6e15d6c9da">CVC3::Translator::d_theorySimulate</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00105">105</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8h_source.html#l00172">setTheorySimulate()</a>.</p>
</div>
</div>
<a class="anchor" id="aef70b07a6df14699d8f5bc24c6e93ae9"></a><!-- doxytag: member="CVC3::Translator::d_theoryBitvector" ref="aef70b07a6df14699d8f5bc24c6e93ae9" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoryBitvector.html">TheoryBitvector</a>* <a class="el" href="classCVC3_1_1Translator.html#aef70b07a6df14699d8f5bc24c6e93ae9">CVC3::Translator::d_theoryBitvector</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00106">106</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, <a class="el" href="translator_8cpp_source.html#l01850">printArrayExpr()</a>, <a class="el" href="translator_8cpp_source.html#l01063">processType()</a>, and <a class="el" href="translator_8h_source.html#l00173">setTheoryBitvector()</a>.</p>
</div>
</div>
<a class="anchor" id="ad4a063f628068060febbdff159af1eb3"></a><!-- doxytag: member="CVC3::Translator::d_theoryDatatype" ref="ad4a063f628068060febbdff159af1eb3" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoryDatatype.html">TheoryDatatype</a>* <a class="el" href="classCVC3_1_1Translator.html#ad4a063f628068060febbdff159af1eb3">CVC3::Translator::d_theoryDatatype</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00107">107</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8h_source.html#l00174">setTheoryDatatype()</a>.</p>
</div>
</div>
<a class="anchor" id="a703373c20b6092dd4ca97566921c2583"></a><!-- doxytag: member="CVC3::Translator::d_dumpExprs" ref="a703373c20b6092dd4ca97566921c2583" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classCVC3_1_1Expr.html">Expr</a>> <a class="el" href="classCVC3_1_1Translator.html#a703373c20b6092dd4ca97566921c2583">CVC3::Translator::d_dumpExprs</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00109">109</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l00939">dump()</a>, <a class="el" href="translator_8cpp_source.html#l00970">dumpAssertion()</a>, <a class="el" href="translator_8cpp_source.html#l00978">dumpQuery()</a>, and <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>.</p>
</div>
</div>
<a class="anchor" id="a607f817315c4f3140610420f97172c41"></a><!-- doxytag: member="CVC3::Translator::d_arrayConvertMap" ref="a607f817315c4f3140610420f97172c41" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::map<std::string, <a class="el" href="classCVC3_1_1Type.html">Type</a>>* <a class="el" href="classCVC3_1_1Translator.html#a607f817315c4f3140610420f97172c41">CVC3::Translator::d_arrayConvertMap</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00111">111</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, <a class="el" href="translator_8cpp_source.html#l00808">Translator()</a>, and <a class="el" href="translator_8cpp_source.html#l00839">~Translator()</a>.</p>
</div>
</div>
<a class="anchor" id="a3fc40e37980968ff8859c1634c006749"></a><!-- doxytag: member="CVC3::Translator::d_indexType" ref="a3fc40e37980968ff8859c1634c006749" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Type.html">Type</a>* <a class="el" href="classCVC3_1_1Translator.html#a3fc40e37980968ff8859c1634c006749">CVC3::Translator::d_indexType</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00112">112</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>.</p>
</div>
</div>
<a class="anchor" id="ac142228e58539d53376555542fa357fc"></a><!-- doxytag: member="CVC3::Translator::d_elementType" ref="ac142228e58539d53376555542fa357fc" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Type.html">Type</a>* <a class="el" href="classCVC3_1_1Translator.html#ac142228e58539d53376555542fa357fc">CVC3::Translator::d_elementType</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00113">113</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8cpp_source.html#l01063">processType()</a>.</p>
</div>
</div>
<a class="anchor" id="a77ec037bfce2d8e0d98ed1f7c4fef2c0"></a><!-- doxytag: member="CVC3::Translator::d_arrayType" ref="a77ec037bfce2d8e0d98ed1f7c4fef2c0" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Type.html">Type</a>* <a class="el" href="classCVC3_1_1Translator.html#a77ec037bfce2d8e0d98ed1f7c4fef2c0">CVC3::Translator::d_arrayType</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00114">114</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>, and <a class="el" href="translator_8cpp_source.html#l01063">processType()</a>.</p>
</div>
</div>
<a class="anchor" id="a0dc704ddbd08fdeddd838280539e31bd"></a><!-- doxytag: member="CVC3::Translator::d_equalities" ref="a0dc704ddbd08fdeddd838280539e31bd" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classCVC3_1_1Expr.html">Expr</a>> <a class="el" href="classCVC3_1_1Translator.html#a0dc704ddbd08fdeddd838280539e31bd">CVC3::Translator::d_equalities</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00115">115</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8cpp_source.html#l01145">finish()</a>.</p>
</div>
</div>
<a class="anchor" id="a7e45d1878196924bef7ab146613975a1"></a><!-- doxytag: member="CVC3::Translator::d_benchName" ref="a7e45d1878196924bef7ab146613975a1" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string <a class="el" href="classCVC3_1_1Translator.html#a7e45d1878196924bef7ab146613975a1">CVC3::Translator::d_benchName</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00118">118</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8h_source.html#l00177">benchName()</a>, and <a class="el" href="translator_8h_source.html#l00176">setBenchName()</a>.</p>
</div>
</div>
<a class="anchor" id="a270ac8683f5505f82e207f3238aef007"></a><!-- doxytag: member="CVC3::Translator::d_status" ref="a270ac8683f5505f82e207f3238aef007" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string <a class="el" href="classCVC3_1_1Translator.html#a270ac8683f5505f82e207f3238aef007">CVC3::Translator::d_status</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00120">120</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8h_source.html#l00178">setStatus()</a>, and <a class="el" href="translator_8h_source.html#l00179">status()</a>.</p>
</div>
</div>
<a class="anchor" id="a2181217309457039aab4b190e523f390"></a><!-- doxytag: member="CVC3::Translator::d_source" ref="a2181217309457039aab4b190e523f390" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string <a class="el" href="classCVC3_1_1Translator.html#a2181217309457039aab4b190e523f390">CVC3::Translator::d_source</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="translator_8h_source.html#l00122">122</a> of file <a class="el" href="translator_8h_source.html">translator.h</a>.</p>
<p>Referenced by <a class="el" href="translator_8h_source.html#l00180">setSource()</a>, and <a class="el" href="translator_8h_source.html#l00181">source()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="translator_8h_source.html">translator.h</a></li>
<li><a class="el" href="translator_8cpp_source.html">translator.cpp</a></li>
</ul>
</div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by 
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>
