<!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: translator.h Source File</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><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 class="header">
<div class="headertitle">
<div class="title">translator.h</div> </div>
</div>
<div class="contents">
<a href="translator_8h.html">Go to the documentation of this file.</a><div class="fragment"><pre class="fragment"><a name="l00001"></a>00001 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00002"></a>00002 <span class="comment">/*!</span>
<a name="l00003"></a>00003 <span class="comment"> * \file translator.h</span>
<a name="l00004"></a>00004 <span class="comment"> * \brief An exception to be thrown by the smtlib translator.</span>
<a name="l00005"></a>00005 <span class="comment"> * </span>
<a name="l00006"></a>00006 <span class="comment"> * Author: Clark Barrett</span>
<a name="l00007"></a>00007 <span class="comment"> * </span>
<a name="l00008"></a>00008 <span class="comment"> * Created: Sat Jun 25 18:03:09 2005</span>
<a name="l00009"></a>00009 <span class="comment"> *</span>
<a name="l00010"></a>00010 <span class="comment"> * <hr></span>
<a name="l00011"></a>00011 <span class="comment"> *</span>
<a name="l00012"></a>00012 <span class="comment"> * License to use, copy, modify, sell and/or distribute this software</span>
<a name="l00013"></a>00013 <span class="comment"> * and its documentation for any purpose is hereby granted without</span>
<a name="l00014"></a>00014 <span class="comment"> * royalty, subject to the terms and conditions defined in the \ref</span>
<a name="l00015"></a>00015 <span class="comment"> * LICENSE file provided with this distribution.</span>
<a name="l00016"></a>00016 <span class="comment"> * </span>
<a name="l00017"></a>00017 <span class="comment"> * <hr></span>
<a name="l00018"></a>00018 <span class="comment"> * </span>
<a name="l00019"></a>00019 <span class="comment"> */</span>
<a name="l00020"></a>00020 <span class="comment">/*****************************************************************************/</span>
<a name="l00021"></a>00021
<a name="l00022"></a>00022 <span class="preprocessor">#ifndef _cvc3__translator_h_</span>
<a name="l00023"></a>00023 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__translator_h_</span>
<a name="l00024"></a>00024 <span class="preprocessor"></span>
<a name="l00025"></a>00025 <span class="preprocessor">#include <string></span>
<a name="l00026"></a>00026 <span class="preprocessor">#include <fstream></span>
<a name="l00027"></a>00027 <span class="preprocessor">#include <vector></span>
<a name="l00028"></a>00028 <span class="preprocessor">#include <map></span>
<a name="l00029"></a>00029 <span class="preprocessor">#include "<a class="code" href="queryresult_8h.html" title="enumerated type for result of queries">queryresult.h</a>"</span>
<a name="l00030"></a>00030 <span class="preprocessor">#include "<a class="code" href="compat__hash__map_8h.html">compat_hash_map.h</a>"</span>
<a name="l00031"></a>00031
<a name="l00032"></a>00032 <span class="keyword">namespace </span>CVC3 {
<a name="l00033"></a>00033
<a name="l00034"></a>00034 <span class="keyword">class </span>Expr;
<a name="l00035"></a>00035 <span class="keyword">template</span> <<span class="keyword">class</span> Data> <span class="keyword">class </span>ExprMap;
<a name="l00036"></a>00036 <span class="keyword">class </span>Type;
<a name="l00037"></a>00037 <span class="keyword">class </span>ExprManager;
<a name="l00038"></a>00038 <span class="keyword">class </span>ExprStream;
<a name="l00039"></a>00039 <span class="keyword">class </span>TheoryCore;
<a name="l00040"></a>00040 <span class="keyword">class </span>TheoryUF;
<a name="l00041"></a>00041 <span class="keyword">class </span>TheoryArith;
<a name="l00042"></a>00042 <span class="keyword">class </span>TheoryArray;
<a name="l00043"></a>00043 <span class="keyword">class </span>TheoryQuant;
<a name="l00044"></a>00044 <span class="keyword">class </span>TheoryRecords;
<a name="l00045"></a>00045 <span class="keyword">class </span>TheorySimulate;
<a name="l00046"></a>00046 <span class="keyword">class </span>TheoryBitvector;
<a name="l00047"></a>00047 <span class="keyword">class </span>TheoryDatatype;
<a name="l00048"></a>00048 <span class="keyword">template</span> <<span class="keyword">class</span> Data> <span class="keyword">class </span>ExprMap;
<a name="l00049"></a>00049 <span class="comment"></span>
<a name="l00050"></a>00050 <span class="comment">//! Used to keep track of which subset of arith is being used</span>
<a name="l00051"></a><a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7c">00051</a> <span class="comment"></span><span class="keyword">typedef</span> <span class="keyword">enum</span> {
<a name="l00052"></a><a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7ca5b626d14a049953c62f0cb7d44c0e465">00052</a> <a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7ca5b626d14a049953c62f0cb7d44c0e465">NOT_USED</a> = 0,
<a name="l00053"></a><a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7ca39f089c20d31c9fa12e8f7adad7f13bd">00053</a> <a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7ca39f089c20d31c9fa12e8f7adad7f13bd">TERMS_ONLY</a>,
<a name="l00054"></a><a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7cadf2229be3becac5a1196d6b5d0b5810d">00054</a> <a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7cadf2229be3becac5a1196d6b5d0b5810d">DIFF_ONLY</a>,
<a name="l00055"></a><a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7ca807972dafe8919cb23e79c536f1f1fc1">00055</a> <a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7ca807972dafe8919cb23e79c536f1f1fc1">LINEAR</a>,
<a name="l00056"></a><a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7caf73c1418f111cce667132ba34c016977">00056</a> <a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7caf73c1418f111cce667132ba34c016977">NONLINEAR</a>
<a name="l00057"></a>00057 } <a class="code" href="namespaceCVC3.html#acd059edbc777fc934dbf17c57b8bce7c" title="Used to keep track of which subset of arith is being used.">ArithLang</a>;
<a name="l00058"></a>00058
<a name="l00059"></a>00059 <span class="comment">//All the translation code should go here</span>
<a name="l00060"></a><a class="code" href="classCVC3_1_1Translator.html">00060</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Translator.html">Translator</a> {
<a name="l00061"></a><a class="code" href="classCVC3_1_1Translator.html#a913d9fbcdfbb4d17e3864a74480b0611">00061</a> <a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a>* <a class="code" href="classCVC3_1_1Translator.html#a913d9fbcdfbb4d17e3864a74480b0611">d_em</a>;
<a name="l00062"></a><a class="code" href="classCVC3_1_1Translator.html#a62b1d8ae4ec79cfb22725dd4635d59de">00062</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>& <a class="code" href="classCVC3_1_1Translator.html#a62b1d8ae4ec79cfb22725dd4635d59de">d_translate</a>;
<a name="l00063"></a><a class="code" href="classCVC3_1_1Translator.html#a54add6521f2f005b84cdd129d64764f2">00063</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>& <a class="code" href="classCVC3_1_1Translator.html#a54add6521f2f005b84cdd129d64764f2">d_real2int</a>;
<a name="l00064"></a><a class="code" href="classCVC3_1_1Translator.html#a4f578f10a492640eec9ff8de157cc521">00064</a> <span class="keyword">const</span> <span class="keywordtype">bool</span>& <a class="code" href="classCVC3_1_1Translator.html#a4f578f10a492640eec9ff8de157cc521">d_convertArith</a>;
<a name="l00065"></a><a class="code" href="classCVC3_1_1Translator.html#ac20944f0dfa8772fd1e4c1ad757bf9da">00065</a> <span class="keyword">const</span> std::string& <a class="code" href="classCVC3_1_1Translator.html#ac20944f0dfa8772fd1e4c1ad757bf9da">d_convertToDiff</a>;
<a name="l00066"></a><a class="code" href="classCVC3_1_1Translator.html#afd9c853a8d17a1c7905bb007f1494ce0">00066</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#afd9c853a8d17a1c7905bb007f1494ce0">d_iteLiftArith</a>;
<a name="l00067"></a><a class="code" href="classCVC3_1_1Translator.html#a755c43c5f5be61e8c3c034dccaef33ba">00067</a> <span class="keyword">const</span> std::string& <a class="code" href="classCVC3_1_1Translator.html#a755c43c5f5be61e8c3c034dccaef33ba">d_expResult</a>;
<a name="l00068"></a><a class="code" href="classCVC3_1_1Translator.html#a4a4f7719dd2741c94c88111015846099">00068</a> std::string <a class="code" href="classCVC3_1_1Translator.html#a4a4f7719dd2741c94c88111015846099">d_category</a>;
<a name="l00069"></a><a class="code" href="classCVC3_1_1Translator.html#ab09c1e81131dfc2d3a4da1f859a8108e">00069</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#ab09c1e81131dfc2d3a4da1f859a8108e">d_convertArray</a>;
<a name="l00070"></a><a class="code" href="classCVC3_1_1Translator.html#a72b7aff947a816fbf26f7a97ce0f5fdd">00070</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#a72b7aff947a816fbf26f7a97ce0f5fdd">d_combineAssump</a>;
<a name="l00071"></a>00071 <span class="comment"></span>
<a name="l00072"></a>00072 <span class="comment"> /** Private class for hashing strings; copied from ExprManager */</span>
<a name="l00073"></a><a class="code" href="classCVC3_1_1Translator_1_1HashString.html">00073</a> <span class="keyword">class </span><a class="code" href="classCVC3_1_1Translator_1_1HashString.html">HashString</a> {
<a name="l00074"></a><a class="code" href="classCVC3_1_1Translator_1_1HashString.html#ad5f8c6bb2644a17c3ea9bd826b953b59">00074</a> <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>;
<a name="l00075"></a>00075 <span class="keyword">public</span>:
<a name="l00076"></a><a class="code" href="classCVC3_1_1Translator_1_1HashString.html#a36e4809b34f6b9e4b8f6da780ff9e351">00076</a> <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>{
<a name="l00077"></a>00077 <span class="keywordflow">return</span> <a class="code" href="classCVC3_1_1Translator_1_1HashString.html#ad5f8c6bb2644a17c3ea9bd826b953b59">h</a>(const_cast<char*>(s.c_str()));
<a name="l00078"></a>00078 }
<a name="l00079"></a>00079 };
<a name="l00080"></a><a class="code" href="classCVC3_1_1Translator.html#ad81beb93ee2668558c897398ce68fa44">00080</a> <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>;
<a name="l00081"></a>00081 <span class="comment"></span>
<a name="l00082"></a>00082 <span class="comment"> //! The log file for top-level API calls in the CVC3 input language</span>
<a name="l00083"></a><a class="code" href="classCVC3_1_1Translator.html#a61574c04bd74489b4438ca890f3ec7b4">00083</a> <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>;
<a name="l00084"></a><a class="code" href="classCVC3_1_1Translator.html#a78a511690ef1f3421862b39dad9d02f7">00084</a> std::ofstream <a class="code" href="classCVC3_1_1Translator.html#a78a511690ef1f3421862b39dad9d02f7">d_osdumpFile</a>;
<a name="l00085"></a><a class="code" href="classCVC3_1_1Translator.html#ac55f4fdc4bbb29ccd09dfda38a6eeb91">00085</a> std::ifstream <a class="code" href="classCVC3_1_1Translator.html#ac55f4fdc4bbb29ccd09dfda38a6eeb91">d_tmpFile</a>;
<a name="l00086"></a><a class="code" href="classCVC3_1_1Translator.html#a86e279b67edf39d32056d279a4f9de3b">00086</a> <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>;
<a name="l00087"></a>00087
<a name="l00088"></a><a class="code" href="classCVC3_1_1Translator.html#a290235a7047226a6564add8ef5ad1f10">00088</a> <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>;
<a name="l00089"></a><a class="code" href="classCVC3_1_1Translator.html#a706c02509ddc23d60d43f38af6497139">00089</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#a706c02509ddc23d60d43f38af6497139">d_realUsed</a>;
<a name="l00090"></a><a class="code" href="classCVC3_1_1Translator.html#a18db4e99db8f78e67992cb3cf68dee28">00090</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#a18db4e99db8f78e67992cb3cf68dee28">d_intUsed</a>;
<a name="l00091"></a><a class="code" href="classCVC3_1_1Translator.html#a2e326c83175674acde79b1e33fe391b7">00091</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#a2e326c83175674acde79b1e33fe391b7">d_intConstUsed</a>;
<a name="l00092"></a><a class="code" href="classCVC3_1_1Translator.html#aa6d9fb46298801972cb082ec6eb9918d">00092</a> <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>;
<a name="l00093"></a><a class="code" href="classCVC3_1_1Translator.html#a939bf8530ea41cd0e0c9f8621e17569d">00093</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#a939bf8530ea41cd0e0c9f8621e17569d">d_UFIDL_ok</a>;
<a name="l00094"></a><a class="code" href="classCVC3_1_1Translator.html#a2adf399cb0475894d8b4ea870aaf4547">00094</a> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1Translator.html#a2adf399cb0475894d8b4ea870aaf4547">d_arithUsed</a>;
<a name="l00095"></a>00095
<a name="l00096"></a><a class="code" href="classCVC3_1_1Translator.html#abff660525da18bbe419aed68df4d8564">00096</a> <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>;
<a name="l00097"></a><a class="code" href="classCVC3_1_1Translator.html#a53fdab56fe2f1e821b3f36c2641ae462">00097</a> <span class="keywordtype">int</span> <a class="code" href="classCVC3_1_1Translator.html#a53fdab56fe2f1e821b3f36c2641ae462">d_convertToBV</a>;
<a name="l00098"></a>00098
<a name="l00099"></a><a class="code" href="classCVC3_1_1Translator.html#a1379b7c9235c804f32ab5ce19d86a907">00099</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>* <a class="code" href="classCVC3_1_1Translator.html#a1379b7c9235c804f32ab5ce19d86a907">d_theoryCore</a>;
<a name="l00100"></a><a class="code" href="classCVC3_1_1Translator.html#a67f2340f940914d63aea99462eced2ad">00100</a> <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>;
<a name="l00101"></a><a class="code" href="classCVC3_1_1Translator.html#a0d360419c4e9e9ee9ac8e8af126534d2">00101</a> <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>;
<a name="l00102"></a><a class="code" href="classCVC3_1_1Translator.html#a9b8dc03475b2e90380f82bac9f71e39d">00102</a> <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>;
<a name="l00103"></a><a class="code" href="classCVC3_1_1Translator.html#a5e85f73e319fbd8745c66852cfc1cad5">00103</a> <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>;
<a name="l00104"></a><a class="code" href="classCVC3_1_1Translator.html#a0ce73787e0363fc66f6e653cbec219f6">00104</a> <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>;
<a name="l00105"></a><a class="code" href="classCVC3_1_1Translator.html#a3fbe66e1fdb7b24735146f6e15d6c9da">00105</a> <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>;
<a name="l00106"></a><a class="code" href="classCVC3_1_1Translator.html#aef70b07a6df14699d8f5bc24c6e93ae9">00106</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>* <a class="code" href="classCVC3_1_1Translator.html#aef70b07a6df14699d8f5bc24c6e93ae9">d_theoryBitvector</a>;
<a name="l00107"></a><a class="code" href="classCVC3_1_1Translator.html#ad4a063f628068060febbdff159af1eb3">00107</a> <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>;
<a name="l00108"></a>00108
<a name="l00109"></a><a class="code" href="classCVC3_1_1Translator.html#a703373c20b6092dd4ca97566921c2583">00109</a> std::vector<Expr> <a class="code" href="classCVC3_1_1Translator.html#a703373c20b6092dd4ca97566921c2583">d_dumpExprs</a>;
<a name="l00110"></a>00110
<a name="l00111"></a><a class="code" href="classCVC3_1_1Translator.html#a607f817315c4f3140610420f97172c41">00111</a> std::map<std::string, Type>* <a class="code" href="classCVC3_1_1Translator.html#a607f817315c4f3140610420f97172c41">d_arrayConvertMap</a>;
<a name="l00112"></a><a class="code" href="classCVC3_1_1Translator.html#a3fc40e37980968ff8859c1634c006749">00112</a> <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>;
<a name="l00113"></a><a class="code" href="classCVC3_1_1Translator.html#ac142228e58539d53376555542fa357fc">00113</a> <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>;
<a name="l00114"></a><a class="code" href="classCVC3_1_1Translator.html#a77ec037bfce2d8e0d98ed1f7c4fef2c0">00114</a> <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>;
<a name="l00115"></a><a class="code" href="classCVC3_1_1Translator.html#a0dc704ddbd08fdeddd838280539e31bd">00115</a> std::vector<Expr> <a class="code" href="classCVC3_1_1Translator.html#a0dc704ddbd08fdeddd838280539e31bd">d_equalities</a>;
<a name="l00116"></a>00116
<a name="l00117"></a>00117 <span class="comment">// Name of benchmark in SMT-LIB</span>
<a name="l00118"></a><a class="code" href="classCVC3_1_1Translator.html#a7e45d1878196924bef7ab146613975a1">00118</a> std::string <a class="code" href="classCVC3_1_1Translator.html#a7e45d1878196924bef7ab146613975a1">d_benchName</a>;
<a name="l00119"></a>00119 <span class="comment">// Status of benchmark in SMT-LIB</span>
<a name="l00120"></a><a class="code" href="classCVC3_1_1Translator.html#a270ac8683f5505f82e207f3238aef007">00120</a> std::string <a class="code" href="classCVC3_1_1Translator.html#a270ac8683f5505f82e207f3238aef007">d_status</a>;
<a name="l00121"></a>00121 <span class="comment">// Source of benchmark in SMT-LIB</span>
<a name="l00122"></a><a class="code" href="classCVC3_1_1Translator.html#a2181217309457039aab4b190e523f390">00122</a> std::string <a class="code" href="classCVC3_1_1Translator.html#a2181217309457039aab4b190e523f390">d_source</a>;
<a name="l00123"></a>00123
<a name="l00124"></a>00124 std::string <a class="code" href="classCVC3_1_1Translator.html#aa1ff667f344c04df1ff5a6b50cd96e0a">fileToSMTLIBIdentifier</a>(<span class="keyword">const</span> std::string& filename);
<a name="l00125"></a>00125 <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);
<a name="l00126"></a>00126 <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);
<a name="l00127"></a>00127 <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);
<a name="l00128"></a>00128 <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);
<a name="l00129"></a>00129 <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);
<a name="l00130"></a>00130 <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);
<a name="l00131"></a>00131
<a name="l00132"></a>00132 <span class="comment">/*</span>
<a name="l00133"></a>00133 <span class="comment"> Expr spassPreprocess(const Expr& e, ExprMap<Expr>& mapping,</span>
<a name="l00134"></a>00134 <span class="comment"> std::vector<Expr>& functions,</span>
<a name="l00135"></a>00135 <span class="comment"> std::vector<Expr>& predicates);</span>
<a name="l00136"></a>00136 <span class="comment"> */</span>
<a name="l00137"></a>00137
<a name="l00138"></a>00138 <span class="keyword">public</span>:
<a name="l00139"></a>00139 <span class="comment">// Constructors</span>
<a name="l00140"></a>00140 <a class="code" href="classCVC3_1_1Translator.html#a23f150cc9a6b041d95b801bcdb5c9b5b">Translator</a>(<a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a>* em,
<a name="l00141"></a>00141 <span class="keyword">const</span> <span class="keywordtype">bool</span>& translate,
<a name="l00142"></a>00142 <span class="keyword">const</span> <span class="keywordtype">bool</span>& real2int,
<a name="l00143"></a>00143 <span class="keyword">const</span> <span class="keywordtype">bool</span>& convertArith,
<a name="l00144"></a>00144 <span class="keyword">const</span> std::string& convertToDiff,
<a name="l00145"></a>00145 <span class="keywordtype">bool</span> iteLiftArith,
<a name="l00146"></a>00146 <span class="keyword">const</span> std::string& expResult,
<a name="l00147"></a>00147 <span class="keyword">const</span> std::string& <a class="code" href="classCVC3_1_1Translator.html#af1a89762818192869c5d2161dab0a167">category</a>,
<a name="l00148"></a>00148 <span class="keywordtype">bool</span> convertArray,
<a name="l00149"></a>00149 <span class="keywordtype">bool</span> combineAssump,
<a name="l00150"></a>00150 <span class="keywordtype">int</span> convertToBV);
<a name="l00151"></a>00151 <a class="code" href="classCVC3_1_1Translator.html#a9c262ba866126a6a35e979a64d7e3518">~Translator</a>();
<a name="l00152"></a>00152
<a name="l00153"></a>00153 <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>
<a name="l00154"></a>00154 <span class="comment"> /*! Dump the expression in the current output language</span>
<a name="l00155"></a>00155 <span class="comment"> \param dumpOnly When false, the expression is output both when</span>
<a name="l00156"></a>00156 <span class="comment"> translating and when producing a trace of commands. When true, the</span>
<a name="l00157"></a>00157 <span class="comment"> expression is only output when producing a trace of commands</span>
<a name="l00158"></a>00158 <span class="comment"> (i.e. ignored during translation).</span>
<a name="l00159"></a>00159 <span class="comment"> */</span>
<a name="l00160"></a>00160 <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>);
<a name="l00161"></a>00161 <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);
<a name="l00162"></a>00162 <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);
<a name="l00163"></a>00163 <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);
<a name="l00164"></a>00164 <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1Translator.html#a444765aa6bbf793c1ddbc66e9fb829fe">finish</a>();
<a name="l00165"></a>00165
<a name="l00166"></a><a class="code" href="classCVC3_1_1Translator.html#ae54e65770cca9121bd7edb3066db0cca">00166</a> <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; }
<a name="l00167"></a><a class="code" href="classCVC3_1_1Translator.html#ac90246c6882f3afb6dfa2c1cd28bee77">00167</a> <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; }
<a name="l00168"></a><a class="code" href="classCVC3_1_1Translator.html#a56398996b69a8ae5f2d483cac21c06b4">00168</a> <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; }
<a name="l00169"></a><a class="code" href="classCVC3_1_1Translator.html#ae98b6dcd49033de9e7af75bf832ed907">00169</a> <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; }
<a name="l00170"></a><a class="code" href="classCVC3_1_1Translator.html#afa7244fb9f0b749548fe1702238a1d29">00170</a> <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; }
<a name="l00171"></a><a class="code" href="classCVC3_1_1Translator.html#a072d9f51dc77cf2e1d1c4b7ebafd4d1d">00171</a> <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; }
<a name="l00172"></a><a class="code" href="classCVC3_1_1Translator.html#a8c47c28bbcfb39b3dc8244eda47a5dc9">00172</a> <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; }
<a name="l00173"></a><a class="code" href="classCVC3_1_1Translator.html#a87f9011a441dd3c772c0efc8d73e8548">00173</a> <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; }
<a name="l00174"></a><a class="code" href="classCVC3_1_1Translator.html#a9fdb4320a2310af16ef6caacdff8ab5c">00174</a> <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; }
<a name="l00175"></a>00175
<a name="l00176"></a><a class="code" href="classCVC3_1_1Translator.html#a9db51995d5dc21b254bfeb5381b4ce5a">00176</a> <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; }
<a name="l00177"></a><a class="code" href="classCVC3_1_1Translator.html#ad5c28f74006f791727b15d17a3a20650">00177</a> 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>; }
<a name="l00178"></a><a class="code" href="classCVC3_1_1Translator.html#a4c9d948f111bd360e937b170a2c95120">00178</a> <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>; }
<a name="l00179"></a><a class="code" href="classCVC3_1_1Translator.html#aee4bdef7291181744580934a93849b64">00179</a> 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>; }
<a name="l00180"></a><a class="code" href="classCVC3_1_1Translator.html#ac9c933a8ce7265f0463c8556c8eb624c">00180</a> <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>; }
<a name="l00181"></a><a class="code" href="classCVC3_1_1Translator.html#ad57a63292d37aa81d56c3102edd99f2b">00181</a> 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>; }
<a name="l00182"></a><a class="code" href="classCVC3_1_1Translator.html#aed753d381e5cec7619b8324a7588b874">00182</a> <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>; }
<a name="l00183"></a><a class="code" href="classCVC3_1_1Translator.html#af1a89762818192869c5d2161dab0a167">00183</a> 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>; }
<a name="l00184"></a>00184
<a name="l00185"></a>00185 <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);
<a name="l00186"></a>00186 <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);
<a name="l00187"></a>00187 <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>
<a name="l00188"></a>00188 <span class="comment"> //! Returns true if expression has been printed</span>
<a name="l00189"></a>00189 <span class="comment"></span><span class="comment"> /*! If false is returned, array theory should print expression as usual */</span>
<a name="l00190"></a>00190 <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);
<a name="l00191"></a>00191
<a name="l00192"></a>00192 <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>();
<a name="l00193"></a>00193
<a name="l00194"></a>00194 }; <span class="comment">// end of class Translator</span>
<a name="l00195"></a>00195
<a name="l00196"></a>00196 } <span class="comment">// end of namespace CVC3 </span>
<a name="l00197"></a>00197
<a name="l00198"></a>00198 <span class="preprocessor">#endif</span>
</pre></div></div>
</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>
