<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: translator.h Source File</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li><a href="annotated.html"><span>Classes</span></a></li>
<li class="current"><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="files.html"><span>File List</span></a></li>
<li><a href="globals.html"><span>File Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="dir_68267d1309a1af8e8297ef4c3efbcdba.html">src</a></li><li class="navelem"><a class="el" href="dir_b0856f6b0d80ccb263b2f415c91f9e17.html">include</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="headertitle">
<div class="title">translator.h</div> </div>
</div><!--header-->
<div class="contents">
<a href="translator_8h.html">Go to the documentation of this file.</a><div class="fragment"><div class="line"><a name="l00001"></a><span class="lineno"> 1</span> <span class="comment">/*****************************************************************************/</span><span class="comment"></span></div>
<div class="line"><a name="l00002"></a><span class="lineno"> 2</span> <span class="comment">/*!</span></div>
<div class="line"><a name="l00003"></a><span class="lineno"> 3</span> <span class="comment"> * \file translator.h</span></div>
<div class="line"><a name="l00004"></a><span class="lineno"> 4</span> <span class="comment"> * \brief An exception to be thrown by the smtlib translator.</span></div>
<div class="line"><a name="l00005"></a><span class="lineno"> 5</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00006"></a><span class="lineno"> 6</span> <span class="comment"> * Author: Clark Barrett</span></div>
<div class="line"><a name="l00007"></a><span class="lineno"> 7</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00008"></a><span class="lineno"> 8</span> <span class="comment"> * Created: Sat Jun 25 18:03:09 2005</span></div>
<div class="line"><a name="l00009"></a><span class="lineno"> 9</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00010"></a><span class="lineno"> 10</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00011"></a><span class="lineno"> 11</span> <span class="comment"> *</span></div>
<div class="line"><a name="l00012"></a><span class="lineno"> 12</span> <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span></div>
<div class="line"><a name="l00013"></a><span class="lineno"> 13</span> <span class="comment"> * and its documentation for any purpose is hereby granted without</span></div>
<div class="line"><a name="l00014"></a><span class="lineno"> 14</span> <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span></div>
<div class="line"><a name="l00015"></a><span class="lineno"> 15</span> <span class="comment"> * LICENSE file provided with this distribution.</span></div>
<div class="line"><a name="l00016"></a><span class="lineno"> 16</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00017"></a><span class="lineno"> 17</span> <span class="comment"> * <hr></span></div>
<div class="line"><a name="l00018"></a><span class="lineno"> 18</span> <span class="comment"> * </span></div>
<div class="line"><a name="l00019"></a><span class="lineno"> 19</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00020"></a><span class="lineno"> 20</span> <span class="comment">/*****************************************************************************/</span></div>
<div class="line"><a name="l00021"></a><span class="lineno"> 21</span> </div>
<div class="line"><a name="l00022"></a><span class="lineno"> 22</span> <span class="preprocessor">#ifndef _cvc3__translator_h_</span></div>
<div class="line"><a name="l00023"></a><span class="lineno"> 23</span> <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__translator_h_</span></div>
<div class="line"><a name="l00024"></a><span class="lineno"> 24</span> <span class="preprocessor"></span></div>
<div class="line"><a name="l00025"></a><span class="lineno"> 25</span> <span class="preprocessor">#include <string></span></div>
<div class="line"><a name="l00026"></a><span class="lineno"> 26</span> <span class="preprocessor">#include <fstream></span></div>
<div class="line"><a name="l00027"></a><span class="lineno"> 27</span> <span class="preprocessor">#include <vector></span></div>
<div class="line"><a name="l00028"></a><span class="lineno"> 28</span> <span class="preprocessor">#include <map></span></div>
<div class="line"><a name="l00029"></a><span class="lineno"> 29</span> <span class="preprocessor">#include "<a class="code" href="queryresult_8h.html" title="enumerated type for result of queries">queryresult.h</a>"</span></div>
<div class="line"><a name="l00030"></a><span class="lineno"> 30</span> <span class="preprocessor">#include "<a class="code" href="compat__hash__map_8h.html">compat_hash_map.h</a>"</span></div>
<div class="line"><a name="l00031"></a><span class="lineno"> 31</span> </div>
<div class="line"><a name="l00032"></a><span class="lineno"> 32</span> <span class="keyword">namespace </span>CVC3 {</div>
<div class="line"><a name="l00033"></a><span class="lineno"> 33</span> </div>
<div class="line"><a name="l00034"></a><span class="lineno"> 34</span> <span class="keyword">class </span>Expr;</div>
<div class="line"><a name="l00035"></a><span class="lineno"> 35</span> <span class="keyword">template</span> <<span class="keyword">class</span> Data> <span class="keyword">class </span>ExprMap;</div>
<div class="line"><a name="l00036"></a><span class="lineno"> 36</span> <span class="keyword">class </span>Type;</div>
<div class="line"><a name="l00037"></a><span class="lineno"> 37</span> <span class="keyword">class </span>ExprManager;</div>
<div class="line"><a name="l00038"></a><span class="lineno"> 38</span> <span class="keyword">class </span>ExprStream;</div>
<div class="line"><a name="l00039"></a><span class="lineno"> 39</span> <span class="keyword">class </span>TheoryCore;</div>
<div class="line"><a name="l00040"></a><span class="lineno"> 40</span> <span class="keyword">class </span>TheoryUF;</div>
<div class="line"><a name="l00041"></a><span class="lineno"> 41</span> <span class="keyword">class </span>TheoryArith;</div>
<div class="line"><a name="l00042"></a><span class="lineno"> 42</span> <span class="keyword">class </span>TheoryArray;</div>
<div class="line"><a name="l00043"></a><span class="lineno"> 43</span> <span class="keyword">class </span>TheoryQuant;</div>
<div class="line"><a name="l00044"></a><span class="lineno"> 44</span> <span class="keyword">class </span>TheoryRecords;</div>
<div class="line"><a name="l00045"></a><span class="lineno"> 45</span> <span class="keyword">class </span>TheorySimulate;</div>
<div class="line"><a name="l00046"></a><span class="lineno"> 46</span> <span class="keyword">class </span>TheoryBitvector;</div>
<div class="line"><a name="l00047"></a><span class="lineno"> 47</span> <span class="keyword">class </span>TheoryDatatype;</div>
<div class="line"><a name="l00048"></a><span class="lineno"> 48</span> <span class="keyword">template</span> <<span class="keyword">class</span> Data> <span class="keyword">class </span>ExprMap;</div>
<div class="line"><a name="l00049"></a><span class="lineno"> 49</span> <span class="comment"></span></div>
<div class="line"><a name="l00050"></a><span class="lineno"> 50</span> <span class="comment">//! Used to keep track of which subset of arith is being used</span></div>
<div class="line"><a name="l00051"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7c"> 51</a></span> <span class="comment"></span><span class="keyword">typedef</span> <span class="keyword">enum</span> {</div>
<div class="line"><a name="l00052"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7ca5b626d14a049953c62f0cb7d44c0e465"> 52</a></span>  <a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7ca5b626d14a049953c62f0cb7d44c0e465">NOT_USED</a> = 0,</div>
<div class="line"><a name="l00053"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7ca39f089c20d31c9fa12e8f7adad7f13bd"> 53</a></span>  <a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7ca39f089c20d31c9fa12e8f7adad7f13bd">TERMS_ONLY</a>,</div>
<div class="line"><a name="l00054"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7cadf2229be3becac5a1196d6b5d0b5810d"> 54</a></span>  <a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7cadf2229be3becac5a1196d6b5d0b5810d">DIFF_ONLY</a>,</div>
<div class="line"><a name="l00055"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7ca807972dafe8919cb23e79c536f1f1fc1"> 55</a></span>  <a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7ca807972dafe8919cb23e79c536f1f1fc1">LINEAR</a>,</div>
<div class="line"><a name="l00056"></a><span class="lineno"><a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7caf73c1418f111cce667132ba34c016977"> 56</a></span>  <a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7caf73c1418f111cce667132ba34c016977">NONLINEAR</a></div>
<div class="line"><a name="l00057"></a><span class="lineno"> 57</span> } <a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7c" title="Used to keep track of which subset of arith is being used.">ArithLang</a>;</div>
<div class="line"><a name="l00058"></a><span class="lineno"> 58</span> </div>
<div class="line"><a name="l00059"></a><span class="lineno"> 59</span> <span class="comment">//All the translation code should go here</span></div>
<div class="line"><a name="l00060"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html"> 60</a></span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Translator.html">Translator</a> {</div>
<div class="line"><a name="l00061"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a913d9fbcdfbb4d17e3864a74480b0611"> 61</a></span>  <a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a>* <a class="code" href="classCVC3_1_1Translator.html#a913d9fbcdfbb4d17e3864a74480b0611">d_em</a>;</div>
<div class="line"><a name="l00062"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a62b1d8ae4ec79cfb22725dd4635d59de"> 62</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>& <a class="code" href="classCVC3_1_1Translator.html#a62b1d8ae4ec79cfb22725dd4635d59de">d_translate</a>;</div>
<div class="line"><a name="l00063"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a54add6521f2f005b84cdd129d64764f2"> 63</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>& <a class="code" href="classCVC3_1_1Translator.html#a54add6521f2f005b84cdd129d64764f2">d_real2int</a>;</div>
<div class="line"><a name="l00064"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a4f578f10a492640eec9ff8de157cc521"> 64</a></span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>& <a class="code" href="classCVC3_1_1Translator.html#a4f578f10a492640eec9ff8de157cc521">d_convertArith</a>;</div>
<div class="line"><a name="l00065"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#ac20944f0dfa8772fd1e4c1ad757bf9da"> 65</a></span>  <span class="keyword">const</span> std::string& <a class="code" href="classCVC3_1_1Translator.html#ac20944f0dfa8772fd1e4c1ad757bf9da">d_convertToDiff</a>;</div>
<div class="line"><a name="l00066"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#afd9c853a8d17a1c7905bb007f1494ce0"> 66</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#afd9c853a8d17a1c7905bb007f1494ce0">d_iteLiftArith</a>;</div>
<div class="line"><a name="l00067"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a755c43c5f5be61e8c3c034dccaef33ba"> 67</a></span>  <span class="keyword">const</span> std::string& <a class="code" href="classCVC3_1_1Translator.html#a755c43c5f5be61e8c3c034dccaef33ba">d_expResult</a>;</div>
<div class="line"><a name="l00068"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a4a4f7719dd2741c94c88111015846099"> 68</a></span>  std::string <a class="code" href="classCVC3_1_1Translator.html#a4a4f7719dd2741c94c88111015846099">d_category</a>;</div>
<div class="line"><a name="l00069"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#ab09c1e81131dfc2d3a4da1f859a8108e"> 69</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#ab09c1e81131dfc2d3a4da1f859a8108e">d_convertArray</a>;</div>
<div class="line"><a name="l00070"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a72b7aff947a816fbf26f7a97ce0f5fdd"> 70</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#a72b7aff947a816fbf26f7a97ce0f5fdd">d_combineAssump</a>;</div>
<div class="line"><a name="l00071"></a><span class="lineno"> 71</span> <span class="comment"></span></div>
<div class="line"><a name="l00072"></a><span class="lineno"> 72</span> <span class="comment"> /** Private class for hashing strings; copied from ExprManager */</span></div>
<div class="line"><a name="l00073"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator_1_1HashString.html"> 73</a></span>  <span class="keyword">class </span><a class="code" href="classCVC3_1_1Translator_1_1HashString.html">HashString</a> {</div>
<div class="line"><a name="l00074"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator_1_1HashString.html#ad5f8c6bb2644a17c3ea9bd826b953b59"> 74</a></span>  <a class="code" href="structHash_1_1hash_3_01char_01_5_01_4.html">std::hash<char*></a> <a class="code" href="classCVC3_1_1Translator_1_1HashString.html#ad5f8c6bb2644a17c3ea9bd826b953b59">h</a>;</div>
<div class="line"><a name="l00075"></a><span class="lineno"> 75</span>  <span class="keyword">public</span>:</div>
<div class="line"><a name="l00076"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator_1_1HashString.html#a36e4809b34f6b9e4b8f6da780ff9e351"> 76</a></span>  <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1Translator_1_1HashString.html#a36e4809b34f6b9e4b8f6da780ff9e351">operator()</a>(<span class="keyword">const</span> std::string& s)<span class="keyword"> const </span>{</div>
<div class="line"><a name="l00077"></a><span class="lineno"> 77</span>  <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Translator_1_1HashString.html#ad5f8c6bb2644a17c3ea9bd826b953b59">h</a>(const_cast<char*>(s.c_str()));</div>
<div class="line"><a name="l00078"></a><span class="lineno"> 78</span>  }</div>
<div class="line"><a name="l00079"></a><span class="lineno"> 79</span>  };</div>
<div class="line"><a name="l00080"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#ad81beb93ee2668558c897398ce68fa44"> 80</a></span>  <a class="code" href="classHash_1_1hash__map.html">std::hash_map<std::string, std::string, HashString></a> <a class="code" href="classCVC3_1_1Translator.html#ad81beb93ee2668558c897398ce68fa44">d_replaceSymbols</a>;</div>
<div class="line"><a name="l00081"></a><span class="lineno"> 81</span> <span class="comment"></span></div>
<div class="line"><a name="l00082"></a><span class="lineno"> 82</span> <span class="comment"> //! The log file for top-level API calls in the CVC3 input language</span></div>
<div class="line"><a name="l00083"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a61574c04bd74489b4438ca890f3ec7b4"> 83</a></span> <span class="comment"></span> std::ostream* <a class="code" href="classCVC3_1_1Translator.html#a61574c04bd74489b4438ca890f3ec7b4" title="The log file for top-level API calls in the CVC3 input language.">d_osdump</a>;</div>
<div class="line"><a name="l00084"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a78a511690ef1f3421862b39dad9d02f7"> 84</a></span>  std::ofstream <a class="code" href="classCVC3_1_1Translator.html#a78a511690ef1f3421862b39dad9d02f7">d_osdumpFile</a>;</div>
<div class="line"><a name="l00085"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#ac55f4fdc4bbb29ccd09dfda38a6eeb91"> 85</a></span>  std::ifstream <a class="code" href="classCVC3_1_1Translator.html#ac55f4fdc4bbb29ccd09dfda38a6eeb91">d_tmpFile</a>;</div>
<div class="line"><a name="l00086"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a86e279b67edf39d32056d279a4f9de3b"> 86</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#ac5e47db270e1b8d4ee40fe2654382413">d_dump</a>, <a class="code" href="classCVC3_1_1Translator.html#a86e279b67edf39d32056d279a4f9de3b">d_dumpFileOpen</a>;</div>
<div class="line"><a name="l00087"></a><span class="lineno"> 87</span> </div>
<div class="line"><a name="l00088"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a290235a7047226a6564add8ef5ad1f10"> 88</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#aa4dc3a71a03482ba8bb6ff8579e09781">d_intIntArray</a>, <a class="code" href="classCVC3_1_1Translator.html#aca1de6c7f5ab780b57d10c66f58a2890">d_intRealArray</a>, <a class="code" href="classCVC3_1_1Translator.html#a69c89f774ba1fe6c13ca3559748776af">d_intIntRealArray</a>, <a class="code" href="classCVC3_1_1Translator.html#a0793dec1240036cde06df95a14241438">d_ax</a>, <a class="code" href="classCVC3_1_1Translator.html#a290235a7047226a6564add8ef5ad1f10">d_unknown</a>;</div>
<div class="line"><a name="l00089"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a706c02509ddc23d60d43f38af6497139"> 89</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#a706c02509ddc23d60d43f38af6497139">d_realUsed</a>;</div>
<div class="line"><a name="l00090"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a18db4e99db8f78e67992cb3cf68dee28"> 90</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#a18db4e99db8f78e67992cb3cf68dee28">d_intUsed</a>;</div>
<div class="line"><a name="l00091"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a2e326c83175674acde79b1e33fe391b7"> 91</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#a2e326c83175674acde79b1e33fe391b7">d_intConstUsed</a>;</div>
<div class="line"><a name="l00092"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#aa6d9fb46298801972cb082ec6eb9918d"> 92</a></span>  <a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7c" title="Used to keep track of which subset of arith is being used.">ArithLang</a> <a class="code" href="classCVC3_1_1Translator.html#aa6d9fb46298801972cb082ec6eb9918d">d_langUsed</a>;</div>
<div class="line"><a name="l00093"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a939bf8530ea41cd0e0c9f8621e17569d"> 93</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#a939bf8530ea41cd0e0c9f8621e17569d">d_UFIDL_ok</a>;</div>
<div class="line"><a name="l00094"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a2adf399cb0475894d8b4ea870aaf4547"> 94</a></span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#a2adf399cb0475894d8b4ea870aaf4547">d_arithUsed</a>;</div>
<div class="line"><a name="l00095"></a><span class="lineno"> 95</span> </div>
<div class="line"><a name="l00096"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#abff660525da18bbe419aed68df4d8564"> 96</a></span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>* <a class="code" href="classCVC3_1_1Translator.html#abff660525da18bbe419aed68df4d8564">d_zeroVar</a>;</div>
<div class="line"><a name="l00097"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a53fdab56fe2f1e821b3f36c2641ae462"> 97</a></span>  <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1Translator.html#a53fdab56fe2f1e821b3f36c2641ae462">d_convertToBV</a>;</div>
<div class="line"><a name="l00098"></a><span class="lineno"> 98</span> </div>
<div class="line"><a name="l00099"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a1379b7c9235c804f32ab5ce19d86a907"> 99</a></span>  <a class="code" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a>* <a class="code" href="classCVC3_1_1Translator.html#a1379b7c9235c804f32ab5ce19d86a907">d_theoryCore</a>;</div>
<div class="line"><a name="l00100"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a67f2340f940914d63aea99462eced2ad"> 100</a></span>  <a class="code" href="classCVC3_1_1TheoryUF.html" title="This theory handles uninterpreted functions.">TheoryUF</a>* <a class="code" href="classCVC3_1_1Translator.html#a67f2340f940914d63aea99462eced2ad">d_theoryUF</a>;</div>
<div class="line"><a name="l00101"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a0d360419c4e9e9ee9ac8e8af126534d2"> 101</a></span>  <a class="code" href="classCVC3_1_1TheoryArith.html" title="This theory handles basic linear arithmetic.">TheoryArith</a>* <a class="code" href="classCVC3_1_1Translator.html#a0d360419c4e9e9ee9ac8e8af126534d2">d_theoryArith</a>;</div>
<div class="line"><a name="l00102"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a9b8dc03475b2e90380f82bac9f71e39d"> 102</a></span>  <a class="code" href="classCVC3_1_1TheoryArray.html" title="This theory handles arrays.">TheoryArray</a>* <a class="code" href="classCVC3_1_1Translator.html#a9b8dc03475b2e90380f82bac9f71e39d">d_theoryArray</a>;</div>
<div class="line"><a name="l00103"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a5e85f73e319fbd8745c66852cfc1cad5"> 103</a></span>  <a class="code" href="classCVC3_1_1TheoryQuant.html" title="This theory handles quantifiers.">TheoryQuant</a>* <a class="code" href="classCVC3_1_1Translator.html#a5e85f73e319fbd8745c66852cfc1cad5">d_theoryQuant</a>;</div>
<div class="line"><a name="l00104"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a0ce73787e0363fc66f6e653cbec219f6"> 104</a></span>  <a class="code" href="classCVC3_1_1TheoryRecords.html" title="This theory handles records.">TheoryRecords</a>* <a class="code" href="classCVC3_1_1Translator.html#a0ce73787e0363fc66f6e653cbec219f6">d_theoryRecords</a>;</div>
<div class="line"><a name="l00105"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a3fbe66e1fdb7b24735146f6e15d6c9da"> 105</a></span>  <a class="code" href="classCVC3_1_1TheorySimulate.html" title=""Theory" of symbolic simulation.">TheorySimulate</a>* <a class="code" href="classCVC3_1_1Translator.html#a3fbe66e1fdb7b24735146f6e15d6c9da">d_theorySimulate</a>;</div>
<div class="line"><a name="l00106"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#aef70b07a6df14699d8f5bc24c6e93ae9"> 106</a></span>  <a class="code" href="classCVC3_1_1TheoryBitvector.html" title="Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG)">TheoryBitvector</a>* <a class="code" href="classCVC3_1_1Translator.html#aef70b07a6df14699d8f5bc24c6e93ae9">d_theoryBitvector</a>;</div>
<div class="line"><a name="l00107"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#ad4a063f628068060febbdff159af1eb3"> 107</a></span>  <a class="code" href="classCVC3_1_1TheoryDatatype.html" title="This theory handles datatypes.">TheoryDatatype</a>* <a class="code" href="classCVC3_1_1Translator.html#ad4a063f628068060febbdff159af1eb3">d_theoryDatatype</a>;</div>
<div class="line"><a name="l00108"></a><span class="lineno"> 108</span> </div>
<div class="line"><a name="l00109"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a703373c20b6092dd4ca97566921c2583"> 109</a></span>  std::vector<Expr> <a class="code" href="classCVC3_1_1Translator.html#a703373c20b6092dd4ca97566921c2583">d_dumpExprs</a>;</div>
<div class="line"><a name="l00110"></a><span class="lineno"> 110</span> </div>
<div class="line"><a name="l00111"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a607f817315c4f3140610420f97172c41"> 111</a></span>  std::map<std::string, Type>* <a class="code" href="classCVC3_1_1Translator.html#a607f817315c4f3140610420f97172c41">d_arrayConvertMap</a>;</div>
<div class="line"><a name="l00112"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a3fc40e37980968ff8859c1634c006749"> 112</a></span>  <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>* <a class="code" href="classCVC3_1_1Translator.html#a3fc40e37980968ff8859c1634c006749">d_indexType</a>;</div>
<div class="line"><a name="l00113"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#ac142228e58539d53376555542fa357fc"> 113</a></span>  <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>* <a class="code" href="classCVC3_1_1Translator.html#ac142228e58539d53376555542fa357fc">d_elementType</a>;</div>
<div class="line"><a name="l00114"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a77ec037bfce2d8e0d98ed1f7c4fef2c0"> 114</a></span>  <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>* <a class="code" href="classCVC3_1_1Translator.html#a77ec037bfce2d8e0d98ed1f7c4fef2c0">d_arrayType</a>;</div>
<div class="line"><a name="l00115"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a0dc704ddbd08fdeddd838280539e31bd"> 115</a></span>  std::vector<Expr> <a class="code" href="classCVC3_1_1Translator.html#a0dc704ddbd08fdeddd838280539e31bd">d_equalities</a>;</div>
<div class="line"><a name="l00116"></a><span class="lineno"> 116</span> </div>
<div class="line"><a name="l00117"></a><span class="lineno"> 117</span>  <span class="comment">// Name of benchmark in SMT-LIB</span></div>
<div class="line"><a name="l00118"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a7e45d1878196924bef7ab146613975a1"> 118</a></span>  std::string <a class="code" href="classCVC3_1_1Translator.html#a7e45d1878196924bef7ab146613975a1">d_benchName</a>;</div>
<div class="line"><a name="l00119"></a><span class="lineno"> 119</span>  <span class="comment">// Status of benchmark in SMT-LIB</span></div>
<div class="line"><a name="l00120"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a270ac8683f5505f82e207f3238aef007"> 120</a></span>  std::string <a class="code" href="classCVC3_1_1Translator.html#a270ac8683f5505f82e207f3238aef007">d_status</a>;</div>
<div class="line"><a name="l00121"></a><span class="lineno"> 121</span>  <span class="comment">// Source of benchmark in SMT-LIB</span></div>
<div class="line"><a name="l00122"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a2181217309457039aab4b190e523f390"> 122</a></span>  std::string <a class="code" href="classCVC3_1_1Translator.html#a2181217309457039aab4b190e523f390">d_source</a>;</div>
<div class="line"><a name="l00123"></a><span class="lineno"> 123</span> </div>
<div class="line"><a name="l00124"></a><span class="lineno"> 124</span>  std::string <a class="code" href="classCVC3_1_1Translator.html#aa1ff667f344c04df1ff5a6b50cd96e0a">fileToSMTLIBIdentifier</a>(<span class="keyword">const</span> std::string& filename);</div>
<div class="line"><a name="l00125"></a><span class="lineno"> 125</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1Translator.html#aed0fe44184d5d994a340d7006136a6dc">preprocessRec</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a>& cache);</div>
<div class="line"><a name="l00126"></a><span class="lineno"> 126</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1Translator.html#a6cad6b15357c5baf43a287be1a762a26">preprocess</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a>& cache);</div>
<div class="line"><a name="l00127"></a><span class="lineno"> 127</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1Translator.html#a8643ae389927052297fef525045211ac">preprocess2Rec</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a>& cache, <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> desiredType);</div>
<div class="line"><a name="l00128"></a><span class="lineno"> 128</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1Translator.html#ab0934eb91855a58064402f48bf4b4ad5">preprocess2</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a>& cache);</div>
<div class="line"><a name="l00129"></a><span class="lineno"> 129</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#aa41988d7a85be9e3b68a053ef1db50b6">containsArray</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00130"></a><span class="lineno"> 130</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1Translator.html#a5e42669a5a6f0a69ae33fde3ccedb8bb">processType</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00131"></a><span class="lineno"> 131</span> </div>
<div class="line"><a name="l00132"></a><span class="lineno"> 132</span>  <span class="comment">/*</span></div>
<div class="line"><a name="l00133"></a><span class="lineno"> 133</span> <span class="comment"> Expr spassPreprocess(const Expr& e, ExprMap<Expr>& mapping,</span></div>
<div class="line"><a name="l00134"></a><span class="lineno"> 134</span> <span class="comment"> std::vector<Expr>& functions,</span></div>
<div class="line"><a name="l00135"></a><span class="lineno"> 135</span> <span class="comment"> std::vector<Expr>& predicates);</span></div>
<div class="line"><a name="l00136"></a><span class="lineno"> 136</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00137"></a><span class="lineno"> 137</span> </div>
<div class="line"><a name="l00138"></a><span class="lineno"> 138</span> <span class="keyword">public</span>:</div>
<div class="line"><a name="l00139"></a><span class="lineno"> 139</span>  <span class="comment">// Constructors</span></div>
<div class="line"><a name="l00140"></a><span class="lineno"> 140</span>  <a class="code" href="classCVC3_1_1Translator.html#a23f150cc9a6b041d95b801bcdb5c9b5b">Translator</a>(<a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a>* em,</div>
<div class="line"><a name="l00141"></a><span class="lineno"> 141</span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>& translate,</div>
<div class="line"><a name="l00142"></a><span class="lineno"> 142</span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>& real2int,</div>
<div class="line"><a name="l00143"></a><span class="lineno"> 143</span>  <span class="keyword">const</span> <span class="keywordtype">bool</span>& convertArith,</div>
<div class="line"><a name="l00144"></a><span class="lineno"> 144</span>  <span class="keyword">const</span> std::string& convertToDiff,</div>
<div class="line"><a name="l00145"></a><span class="lineno"> 145</span>  <span class="keywordtype">bool</span> iteLiftArith,</div>
<div class="line"><a name="l00146"></a><span class="lineno"> 146</span>  <span class="keyword">const</span> std::string& expResult,</div>
<div class="line"><a name="l00147"></a><span class="lineno"> 147</span>  <span class="keyword">const</span> std::string& <a class="code" href="classCVC3_1_1Translator.html#af1a89762818192869c5d2161dab0a167">category</a>,</div>
<div class="line"><a name="l00148"></a><span class="lineno"> 148</span>  <span class="keywordtype">bool</span> convertArray,</div>
<div class="line"><a name="l00149"></a><span class="lineno"> 149</span>  <span class="keywordtype">bool</span> combineAssump,</div>
<div class="line"><a name="l00150"></a><span class="lineno"> 150</span>  <span class="keywordtype">int</span> convertToBV);</div>
<div class="line"><a name="l00151"></a><span class="lineno"> 151</span>  <a class="code" href="classCVC3_1_1Translator.html#a9c262ba866126a6a35e979a64d7e3518">~Translator</a>();</div>
<div class="line"><a name="l00152"></a><span class="lineno"> 152</span> </div>
<div class="line"><a name="l00153"></a><span class="lineno"> 153</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#ad0209b8b429fc08f7cd500aae0f35792">start</a>(<span class="keyword">const</span> std::string& dumpFile);<span class="comment"></span></div>
<div class="line"><a name="l00154"></a><span class="lineno"> 154</span> <span class="comment"> /*! Dump the expression in the current output language</span></div>
<div class="line"><a name="l00155"></a><span class="lineno"> 155</span> <span class="comment"> \param dumpOnly When false, the expression is output both when</span></div>
<div class="line"><a name="l00156"></a><span class="lineno"> 156</span> <span class="comment"> translating and when producing a trace of commands. When true, the</span></div>
<div class="line"><a name="l00157"></a><span class="lineno"> 157</span> <span class="comment"> expression is only output when producing a trace of commands</span></div>
<div class="line"><a name="l00158"></a><span class="lineno"> 158</span> <span class="comment"> (i.e. ignored during translation).</span></div>
<div class="line"><a name="l00159"></a><span class="lineno"> 159</span> <span class="comment"> */</span></div>
<div class="line"><a name="l00160"></a><span class="lineno"> 160</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#a2085a4f56a069befeaf2de05d78312a0">dump</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, <span class="keywordtype">bool</span> dumpOnly = <span class="keyword">false</span>);</div>
<div class="line"><a name="l00161"></a><span class="lineno"> 161</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#ad7100f7c31841078e4d298aa415694e0">dumpAssertion</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00162"></a><span class="lineno"> 162</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#a0642e4129e907824a8ac54d4cb89462f">dumpQuery</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00163"></a><span class="lineno"> 163</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#abafa3e4622d8ef21e29d79c7efb20053">dumpQueryResult</a>(<a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> qres);</div>
<div class="line"><a name="l00164"></a><span class="lineno"> 164</span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#a444765aa6bbf793c1ddbc66e9fb829fe">finish</a>();</div>
<div class="line"><a name="l00165"></a><span class="lineno"> 165</span> </div>
<div class="line"><a name="l00166"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#ae54e65770cca9121bd7edb3066db0cca"> 166</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#ae54e65770cca9121bd7edb3066db0cca">setTheoryCore</a>(<a class="code" href="classCVC3_1_1TheoryCore.html" title="This theory handles the built-in logical connectives plus equality. It also handles the registration ...">TheoryCore</a>* theoryCore) { <a class="code" href="classCVC3_1_1Translator.html#a1379b7c9235c804f32ab5ce19d86a907">d_theoryCore</a> = theoryCore; }</div>
<div class="line"><a name="l00167"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#ac90246c6882f3afb6dfa2c1cd28bee77"> 167</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#ac90246c6882f3afb6dfa2c1cd28bee77">setTheoryUF</a>(<a class="code" href="classCVC3_1_1TheoryUF.html" title="This theory handles uninterpreted functions.">TheoryUF</a>* theoryUF) { <a class="code" href="classCVC3_1_1Translator.html#a67f2340f940914d63aea99462eced2ad">d_theoryUF</a> = theoryUF; }</div>
<div class="line"><a name="l00168"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a56398996b69a8ae5f2d483cac21c06b4"> 168</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#a56398996b69a8ae5f2d483cac21c06b4">setTheoryArith</a>(<a class="code" href="classCVC3_1_1TheoryArith.html" title="This theory handles basic linear arithmetic.">TheoryArith</a>* theoryArith) { <a class="code" href="classCVC3_1_1Translator.html#a0d360419c4e9e9ee9ac8e8af126534d2">d_theoryArith</a> = theoryArith; }</div>
<div class="line"><a name="l00169"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#ae98b6dcd49033de9e7af75bf832ed907"> 169</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#ae98b6dcd49033de9e7af75bf832ed907">setTheoryArray</a>(<a class="code" href="classCVC3_1_1TheoryArray.html" title="This theory handles arrays.">TheoryArray</a>* theoryArray) { <a class="code" href="classCVC3_1_1Translator.html#a9b8dc03475b2e90380f82bac9f71e39d">d_theoryArray</a> = theoryArray; }</div>
<div class="line"><a name="l00170"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#afa7244fb9f0b749548fe1702238a1d29"> 170</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#afa7244fb9f0b749548fe1702238a1d29">setTheoryQuant</a>(<a class="code" href="classCVC3_1_1TheoryQuant.html" title="This theory handles quantifiers.">TheoryQuant</a>* theoryQuant) { <a class="code" href="classCVC3_1_1Translator.html#a5e85f73e319fbd8745c66852cfc1cad5">d_theoryQuant</a> = theoryQuant; }</div>
<div class="line"><a name="l00171"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a072d9f51dc77cf2e1d1c4b7ebafd4d1d"> 171</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#a072d9f51dc77cf2e1d1c4b7ebafd4d1d">setTheoryRecords</a>(<a class="code" href="classCVC3_1_1TheoryRecords.html" title="This theory handles records.">TheoryRecords</a>* theoryRecords) { <a class="code" href="classCVC3_1_1Translator.html#a0ce73787e0363fc66f6e653cbec219f6">d_theoryRecords</a> = theoryRecords; }</div>
<div class="line"><a name="l00172"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a8c47c28bbcfb39b3dc8244eda47a5dc9"> 172</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#a8c47c28bbcfb39b3dc8244eda47a5dc9">setTheorySimulate</a>(<a class="code" href="classCVC3_1_1TheorySimulate.html" title=""Theory" of symbolic simulation.">TheorySimulate</a>* theorySimulate) { <a class="code" href="classCVC3_1_1Translator.html#a3fbe66e1fdb7b24735146f6e15d6c9da">d_theorySimulate</a> = theorySimulate; }</div>
<div class="line"><a name="l00173"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a87f9011a441dd3c772c0efc8d73e8548"> 173</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#a87f9011a441dd3c772c0efc8d73e8548">setTheoryBitvector</a>(<a class="code" href="classCVC3_1_1TheoryBitvector.html" title="Theory of bitvectors of known length \ (operations include: @,[i:j],[i],+,.,BVAND,BVNEG)">TheoryBitvector</a>* theoryBitvector) { <a class="code" href="classCVC3_1_1Translator.html#aef70b07a6df14699d8f5bc24c6e93ae9">d_theoryBitvector</a> = theoryBitvector; }</div>
<div class="line"><a name="l00174"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a9fdb4320a2310af16ef6caacdff8ab5c"> 174</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#a9fdb4320a2310af16ef6caacdff8ab5c">setTheoryDatatype</a>(<a class="code" href="classCVC3_1_1TheoryDatatype.html" title="This theory handles datatypes.">TheoryDatatype</a>* theoryDatatype) { <a class="code" href="classCVC3_1_1Translator.html#ad4a063f628068060febbdff159af1eb3">d_theoryDatatype</a> = theoryDatatype; }</div>
<div class="line"><a name="l00175"></a><span class="lineno"> 175</span> </div>
<div class="line"><a name="l00176"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a9db51995d5dc21b254bfeb5381b4ce5a"> 176</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#a9db51995d5dc21b254bfeb5381b4ce5a">setBenchName</a>(std::string name) { <a class="code" href="classCVC3_1_1Translator.html#a7e45d1878196924bef7ab146613975a1">d_benchName</a> = name; }</div>
<div class="line"><a name="l00177"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#ad5c28f74006f791727b15d17a3a20650"> 177</a></span>  std::string <a class="code" href="classCVC3_1_1Translator.html#ad5c28f74006f791727b15d17a3a20650">benchName</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Translator.html#a7e45d1878196924bef7ab146613975a1">d_benchName</a>; }</div>
<div class="line"><a name="l00178"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#a4c9d948f111bd360e937b170a2c95120"> 178</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#a4c9d948f111bd360e937b170a2c95120">setStatus</a>(std::string <a class="code" href="classCVC3_1_1Translator.html#aee4bdef7291181744580934a93849b64">status</a>) { <a class="code" href="classCVC3_1_1Translator.html#a270ac8683f5505f82e207f3238aef007">d_status</a> = <a class="code" href="classCVC3_1_1Translator.html#aee4bdef7291181744580934a93849b64">status</a>; }</div>
<div class="line"><a name="l00179"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#aee4bdef7291181744580934a93849b64"> 179</a></span>  std::string <a class="code" href="classCVC3_1_1Translator.html#aee4bdef7291181744580934a93849b64">status</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Translator.html#a270ac8683f5505f82e207f3238aef007">d_status</a>; }</div>
<div class="line"><a name="l00180"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#ac9c933a8ce7265f0463c8556c8eb624c"> 180</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#ac9c933a8ce7265f0463c8556c8eb624c">setSource</a>(std::string <a class="code" href="classCVC3_1_1Translator.html#ad57a63292d37aa81d56c3102edd99f2b">source</a>) { <a class="code" href="classCVC3_1_1Translator.html#a2181217309457039aab4b190e523f390">d_source</a> = <a class="code" href="classCVC3_1_1Translator.html#ad57a63292d37aa81d56c3102edd99f2b">source</a>; }</div>
<div class="line"><a name="l00181"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#ad57a63292d37aa81d56c3102edd99f2b"> 181</a></span>  std::string <a class="code" href="classCVC3_1_1Translator.html#ad57a63292d37aa81d56c3102edd99f2b">source</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Translator.html#a2181217309457039aab4b190e523f390">d_source</a>; }</div>
<div class="line"><a name="l00182"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#aed753d381e5cec7619b8324a7588b874"> 182</a></span>  <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#aed753d381e5cec7619b8324a7588b874">setCategory</a>(std::string <a class="code" href="classCVC3_1_1Translator.html#af1a89762818192869c5d2161dab0a167">category</a>) { <a class="code" href="classCVC3_1_1Translator.html#a4a4f7719dd2741c94c88111015846099">d_category</a> = <a class="code" href="classCVC3_1_1Translator.html#af1a89762818192869c5d2161dab0a167">category</a>; }</div>
<div class="line"><a name="l00183"></a><span class="lineno"><a class="code" href="classCVC3_1_1Translator.html#af1a89762818192869c5d2161dab0a167"> 183</a></span>  std::string <a class="code" href="classCVC3_1_1Translator.html#af1a89762818192869c5d2161dab0a167">category</a>() { <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Translator.html#a4a4f7719dd2741c94c88111015846099">d_category</a>; }</div>
<div class="line"><a name="l00184"></a><span class="lineno"> 184</span> </div>
<div class="line"><a name="l00185"></a><span class="lineno"> 185</span>  <span class="keyword">const</span> std::string <a class="code" href="classCVC3_1_1Translator.html#a0ee4f6a5cf7bb40bfe341e4b99f06810">fixConstName</a>(<span class="keyword">const</span> std::string& s);</div>
<div class="line"><a name="l00186"></a><span class="lineno"> 186</span>  <span class="keyword">const</span> std::string <a class="code" href="classCVC3_1_1Translator.html#a6821f774dda2d0964fde109b29de20a8">escapeSymbol</a>(<span class="keyword">const</span> std::string& s);</div>
<div class="line"><a name="l00187"></a><span class="lineno"> 187</span>  <span class="keyword">const</span> std::string <a class="code" href="classCVC3_1_1Translator.html#a90238a14586a6582a741bebebce13010">quoteAnnotation</a>(<span class="keyword">const</span> std::string& s);<span class="comment"></span></div>
<div class="line"><a name="l00188"></a><span class="lineno"> 188</span> <span class="comment"> //! Returns true if expression has been printed</span></div>
<div class="line"><a name="l00189"></a><span class="lineno"> 189</span> <span class="comment"></span><span class="comment"> /*! If false is returned, array theory should print expression as usual */</span></div>
<div class="line"><a name="l00190"></a><span class="lineno"> 190</span>  <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#ab562bf78b184a0039093ce0dba0770d0" title="Returns true if expression has been printed.">printArrayExpr</a>(<a class="code" href="classCVC3_1_1ExprStream.html" title="Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!">ExprStream</a>& os, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e);</div>
<div class="line"><a name="l00191"></a><span class="lineno"> 191</span> </div>
<div class="line"><a name="l00192"></a><span class="lineno"> 192</span>  <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="classCVC3_1_1Translator.html#a89f83c6d0dcc3416b7b5facd68753e80">zeroVar</a>();</div>
<div class="line"><a name="l00193"></a><span class="lineno"> 193</span> </div>
<div class="line"><a name="l00194"></a><span class="lineno"> 194</span> }; <span class="comment">// end of class Translator</span></div>
<div class="line"><a name="l00195"></a><span class="lineno"> 195</span> </div>
<div class="line"><a name="l00196"></a><span class="lineno"> 196</span> } <span class="comment">// end of namespace CVC3 </span></div>
<div class="line"><a name="l00197"></a><span class="lineno"> 197</span> </div>
<div class="line"><a name="l00198"></a><span class="lineno"> 198</span> <span class="preprocessor">#endif</span></div>
</div><!-- fragment --></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:16 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
