<!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: vcl.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">vcl.h</div> </div>
</div>
<div class="contents">
<a href="vcl_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 vcl.h</span>
<a name="l00004"></a>00004 <span class="comment"> * \brief Main implementation of ValidityChecker for CVC3.</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: Wed Dec 11 14:40:39 2002</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__include__vcl_h_</span>
<a name="l00023"></a>00023 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__vcl_h_</span>
<a name="l00024"></a>00024 <span class="preprocessor"></span>
<a name="l00025"></a>00025 <span class="preprocessor">#include <queue></span>
<a name="l00026"></a>00026
<a name="l00027"></a>00027 <span class="preprocessor">#include "<a class="code" href="vc_8h.html" title="Generic API for a validity checker.">vc.h</a>"</span>
<a name="l00028"></a>00028 <span class="preprocessor">#include "<a class="code" href="command__line__flags_8h.html">command_line_flags.h</a>"</span>
<a name="l00029"></a>00029 <span class="preprocessor">#include "<a class="code" href="statistics_8h.html" title="Description: Counters and flags for collecting run-time statistics.">statistics.h</a>"</span>
<a name="l00030"></a>00030 <span class="preprocessor">#include "<a class="code" href="cdmap_8h.html">cdmap.h</a>"</span>
<a name="l00031"></a>00031 <span class="preprocessor">#include "<a class="code" href="cdlist_8h.html">cdlist.h</a>"</span>
<a name="l00032"></a>00032
<a name="l00033"></a>00033 <span class="keyword">namespace </span>CVC3 {
<a name="l00034"></a>00034
<a name="l00035"></a>00035 <span class="keyword">class </span>SearchEngine;
<a name="l00036"></a>00036 <span class="keyword">class </span>Theory;
<a name="l00037"></a>00037 <span class="keyword">class </span>TheoryCore;
<a name="l00038"></a>00038 <span class="keyword">class </span>TheoryUF;
<a name="l00039"></a>00039 <span class="keyword">class </span>TheoryArith;
<a name="l00040"></a>00040 <span class="keyword">class </span>TheoryArray;
<a name="l00041"></a>00041 <span class="keyword">class </span>TheoryQuant;
<a name="l00042"></a>00042 <span class="keyword">class </span>TheoryRecords;
<a name="l00043"></a>00043 <span class="keyword">class </span>TheorySimulate;
<a name="l00044"></a>00044 <span class="keyword">class </span>TheoryBitvector;
<a name="l00045"></a>00045 <span class="keyword">class </span>TheoryDatatype;
<a name="l00046"></a>00046 <span class="keyword">class </span>Translator;
<a name="l00047"></a>00047
<a name="l00048"></a><a class="code" href="classCVC3_1_1VCL.html">00048</a> <span class="keyword">class </span><a class="code" href="os_8h.html#a0035aac6379df39aa69feba98b2751ba">CVC_DLL</a> <a class="code" href="classCVC3_1_1VCL.html">VCL</a> : <span class="keyword">public</span> <a class="code" href="classCVC3_1_1ValidityChecker.html" title="Generic API for a validity checker.">ValidityChecker</a> {
<a name="l00049"></a>00049 <span class="comment"></span>
<a name="l00050"></a>00050 <span class="comment"> //! Pointers to main system components</span>
<a name="l00051"></a><a class="code" href="classCVC3_1_1VCL.html#a82e3b0230008233cddbb44489238097f">00051</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a>* <a class="code" href="classCVC3_1_1VCL.html#a82e3b0230008233cddbb44489238097f" title="Pointers to main system components.">d_em</a>;
<a name="l00052"></a><a class="code" href="classCVC3_1_1VCL.html#a2b40a6191db7398dc35d7294ef7f5cf5">00052</a> <a class="code" href="classCVC3_1_1ContextManager.html" title="Manager for multiple contexts. Also holds current context.">ContextManager</a>* <a class="code" href="classCVC3_1_1VCL.html#a2b40a6191db7398dc35d7294ef7f5cf5">d_cm</a>;
<a name="l00053"></a><a class="code" href="classCVC3_1_1VCL.html#ae2de028959c8cb591ece07d6a0ad6fd2">00053</a> <a class="code" href="classCVC3_1_1TheoremManager.html">TheoremManager</a>* <a class="code" href="classCVC3_1_1VCL.html#ae2de028959c8cb591ece07d6a0ad6fd2">d_tm</a>;
<a name="l00054"></a><a class="code" href="classCVC3_1_1VCL.html#ab21d710d786fc113e73da60c2201f237">00054</a> <a class="code" href="classCVC3_1_1SearchEngine.html" title="API to to a generic proof search engine.">SearchEngine</a>* <a class="code" href="classCVC3_1_1VCL.html#ab21d710d786fc113e73da60c2201f237">d_se</a>;
<a name="l00055"></a>00055 <span class="comment"></span>
<a name="l00056"></a>00056 <span class="comment"> //! Pointers to theories</span>
<a name="l00057"></a><a class="code" href="classCVC3_1_1VCL.html#a83c1ecc49a06d59154fcec151115ee41">00057</a> <span class="comment"></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_1VCL.html#a83c1ecc49a06d59154fcec151115ee41" title="Pointers to theories.">d_theoryCore</a>;
<a name="l00058"></a><a class="code" href="classCVC3_1_1VCL.html#a36a31c39519edb4c051724d0fe684e9f">00058</a> <a class="code" href="classCVC3_1_1TheoryUF.html" title="This theory handles uninterpreted functions.">TheoryUF</a>* <a class="code" href="classCVC3_1_1VCL.html#a36a31c39519edb4c051724d0fe684e9f">d_theoryUF</a>;
<a name="l00059"></a><a class="code" href="classCVC3_1_1VCL.html#a7ecdb7ee559f64dad9c090985ac6c64b">00059</a> <a class="code" href="classCVC3_1_1TheoryArith.html" title="This theory handles basic linear arithmetic.">TheoryArith</a>* <a class="code" href="classCVC3_1_1VCL.html#a7ecdb7ee559f64dad9c090985ac6c64b">d_theoryArith</a>;
<a name="l00060"></a><a class="code" href="classCVC3_1_1VCL.html#a7bef1476e19d2ac7c3e39f108cff1438">00060</a> <a class="code" href="classCVC3_1_1TheoryArray.html" title="This theory handles arrays.">TheoryArray</a>* <a class="code" href="classCVC3_1_1VCL.html#a7bef1476e19d2ac7c3e39f108cff1438">d_theoryArray</a>;
<a name="l00061"></a><a class="code" href="classCVC3_1_1VCL.html#a67512d691a8bbdfcf5a599beb6d881db">00061</a> <a class="code" href="classCVC3_1_1TheoryQuant.html" title="This theory handles quantifiers.">TheoryQuant</a>* <a class="code" href="classCVC3_1_1VCL.html#a67512d691a8bbdfcf5a599beb6d881db">d_theoryQuant</a>;
<a name="l00062"></a><a class="code" href="classCVC3_1_1VCL.html#af0fa33ca11ef9598d27baa79a20b7d06">00062</a> <a class="code" href="classCVC3_1_1TheoryRecords.html" title="This theory handles records.">TheoryRecords</a>* <a class="code" href="classCVC3_1_1VCL.html#af0fa33ca11ef9598d27baa79a20b7d06">d_theoryRecords</a>;
<a name="l00063"></a><a class="code" href="classCVC3_1_1VCL.html#a4c9b122ddd801eea777472c9f49aa6dd">00063</a> <a class="code" href="classCVC3_1_1TheorySimulate.html" title=""Theory" of symbolic simulation.">TheorySimulate</a>* <a class="code" href="classCVC3_1_1VCL.html#a4c9b122ddd801eea777472c9f49aa6dd">d_theorySimulate</a>;
<a name="l00064"></a><a class="code" href="classCVC3_1_1VCL.html#a4feddacffa44b4ecffd88dd1c1ef5f5f">00064</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_1VCL.html#a4feddacffa44b4ecffd88dd1c1ef5f5f">d_theoryBitvector</a>;
<a name="l00065"></a><a class="code" href="classCVC3_1_1VCL.html#ab8fd0353a6ebea5268cb6bf75e43edbb">00065</a> <a class="code" href="classCVC3_1_1TheoryDatatype.html" title="This theory handles datatypes.">TheoryDatatype</a>* <a class="code" href="classCVC3_1_1VCL.html#ab8fd0353a6ebea5268cb6bf75e43edbb">d_theoryDatatype</a>;
<a name="l00066"></a><a class="code" href="classCVC3_1_1VCL.html#a283c9912783c441bba4b59339c5e6f53">00066</a> <a class="code" href="classCVC3_1_1Translator.html">Translator</a>* <a class="code" href="classCVC3_1_1VCL.html#a283c9912783c441bba4b59339c5e6f53">d_translator</a>;
<a name="l00067"></a>00067 <span class="comment"></span>
<a name="l00068"></a>00068 <span class="comment"> //! All theories are stored in this common vector</span>
<a name="l00069"></a>00069 <span class="comment"></span><span class="comment"> /*! This includes TheoryCore and TheoryArith. */</span>
<a name="l00070"></a><a class="code" href="classCVC3_1_1VCL.html#afa0de50278d9008bb8da2e53d1842810">00070</a> std::vector<Theory*> <a class="code" href="classCVC3_1_1VCL.html#afa0de50278d9008bb8da2e53d1842810" title="All theories are stored in this common vector.">d_theories</a>;
<a name="l00071"></a>00071 <span class="comment"></span>
<a name="l00072"></a>00072 <span class="comment"> //! Command line flags</span>
<a name="l00073"></a><a class="code" href="classCVC3_1_1VCL.html#ac56c9b24bf7e95089f59acd4b8795aef">00073</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CLFlags.html">CLFlags</a> *<a class="code" href="classCVC3_1_1VCL.html#ac56c9b24bf7e95089f59acd4b8795aef" title="Command line flags.">d_flags</a>;
<a name="l00074"></a>00074 <span class="comment"></span>
<a name="l00075"></a>00075 <span class="comment"> //! User-level view of the scope stack</span>
<a name="l00076"></a><a class="code" href="classCVC3_1_1VCL.html#ac5d3b29754d41125c6f0eec7de1f8fd3">00076</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<int></a> *<a class="code" href="classCVC3_1_1VCL.html#ac5d3b29754d41125c6f0eec7de1f8fd3" title="User-level view of the scope stack.">d_stackLevel</a>;
<a name="l00077"></a>00077 <span class="comment"></span>
<a name="l00078"></a>00078 <span class="comment"> //! True iff we've pushed the stack artificially to avoid polluting context</span>
<a name="l00079"></a><a class="code" href="classCVC3_1_1VCL.html#a98a4d96994e90f013ce7ddeeaea617e9">00079</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1VCL.html#a98a4d96994e90f013ce7ddeeaea617e9" title="True iff we've pushed the stack artificially to avoid polluting context.">d_modelStackPushed</a>;
<a name="l00080"></a>00080 <span class="comment"></span>
<a name="l00081"></a>00081 <span class="comment"> //! Run-time statistics</span>
<a name="l00082"></a><a class="code" href="classCVC3_1_1VCL.html#a3c7c5a1be001f03b02670ddbc5ff8c5e">00082</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Statistics.html">Statistics</a>* <a class="code" href="classCVC3_1_1VCL.html#a3c7c5a1be001f03b02670ddbc5ff8c5e" title="Run-time statistics.">d_statistics</a>;
<a name="l00083"></a>00083 <span class="comment"></span>
<a name="l00084"></a>00084 <span class="comment"> //! Next index for user assertion</span>
<a name="l00085"></a><a class="code" href="classCVC3_1_1VCL.html#a453046f429f9d2529b00be9c0e573ac7">00085</a> <span class="comment"></span> <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1VCL.html#a453046f429f9d2529b00be9c0e573ac7" title="Next index for user assertion.">d_nextIdx</a>;
<a name="l00086"></a>00086 <span class="comment"></span>
<a name="l00087"></a>00087 <span class="comment"> //! Structure to hold user assertions indexed by declaration order</span>
<a name="l00088"></a><a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html">00088</a> <span class="comment"></span> <span class="keyword">class </span><a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html" title="Structure to hold user assertions indexed by declaration order.">UserAssertion</a> {
<a name="l00089"></a><a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a3e6183b9fdd461f7e1b1d704b1751c2e">00089</a> <span class="keywordtype">size_t</span> <a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a3e6183b9fdd461f7e1b1d704b1751c2e">d_idx</a>;
<a name="l00090"></a><a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a4038959756477796af0e6f4b31fc68a7">00090</a> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a4038959756477796af0e6f4b31fc68a7">d_thm</a>; <span class="comment">//! The theorem of the assertion (a |- a)</span>
<a name="l00091"></a><a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a5981395e9cace8a82d04c7d87af51987">00091</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a5981395e9cace8a82d04c7d87af51987" title="The theorem of the assertion (a |- a)">d_tcc</a>; <span class="comment">//! The proof of its TCC</span>
<a name="l00092"></a>00092 <span class="comment"></span> <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00093"></a>00093 <span class="comment"> //! Default constructor</span>
<a name="l00094"></a><a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a46d21bf4dced20a940cd8ce7a97bf4d6">00094</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a46d21bf4dced20a940cd8ce7a97bf4d6" title="The proof of its TCC.">UserAssertion</a>() { }<span class="comment"></span>
<a name="l00095"></a>00095 <span class="comment"> //! Constructor</span>
<a name="l00096"></a><a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a9c30539ff3e1ed2e1e7f12c6f79bf044">00096</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html" title="Structure to hold user assertions indexed by declaration order.">UserAssertion</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& tcc, <span class="keywordtype">size_t</span> idx)
<a name="l00097"></a>00097 : d_idx(idx), d_thm(thm), d_tcc(tcc) { }<span class="comment"></span>
<a name="l00098"></a>00098 <span class="comment"> //! Fetching a Theorem</span>
<a name="l00099"></a><a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a8c05436295f391cff8bccebb84cbaa85">00099</a> <span class="comment"></span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& <a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a8c05436295f391cff8bccebb84cbaa85" title="Fetching a Theorem.">thm</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_thm; }<span class="comment"></span>
<a name="l00100"></a>00100 <span class="comment"> //! Fetching a TCC</span>
<a name="l00101"></a><a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#ac5de0496e0c784b9e13d4ab3b11df704">00101</a> <span class="comment"></span> <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& <a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#ac5de0496e0c784b9e13d4ab3b11df704" title="Fetching a TCC.">tcc</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> d_tcc; }<span class="comment"></span>
<a name="l00102"></a>00102 <span class="comment"> //! Auto-conversion to Theorem</span>
<a name="l00103"></a><a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a4561409bc4658862f764f885d97d777d">00103</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a4561409bc4658862f764f885d97d777d" title="Auto-conversion to Theorem.">operator Theorem</a>() { <span class="keywordflow">return</span> d_thm; }<span class="comment"></span>
<a name="l00104"></a>00104 <span class="comment"> //! Comparison for use in std::map, to sort in declaration order</span>
<a name="l00105"></a><a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a38a8db7aa6489d8fc093448c61017ac7">00105</a> <span class="comment"></span> <span class="keyword">friend</span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a38a8db7aa6489d8fc093448c61017ac7" title="Comparison for use in std::map, to sort in declaration order.">operator<</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html" title="Structure to hold user assertions indexed by declaration order.">UserAssertion</a>& a1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html" title="Structure to hold user assertions indexed by declaration order.">UserAssertion</a>& a2) {
<a name="l00106"></a>00106 <span class="keywordflow">return</span> (a1.<a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a3e6183b9fdd461f7e1b1d704b1751c2e">d_idx</a> < a2.<a class="code" href="classCVC3_1_1VCL_1_1UserAssertion.html#a3e6183b9fdd461f7e1b1d704b1751c2e">d_idx</a>);
<a name="l00107"></a>00107 }
<a name="l00108"></a>00108 };
<a name="l00109"></a>00109 <span class="comment"></span>
<a name="l00110"></a>00110 <span class="comment"> //! Backtracking map of user assertions</span>
<a name="l00111"></a><a class="code" href="classCVC3_1_1VCL.html#a00dfc7df82e450d5eaabce47f33657eb">00111</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDMap.html">CDMap<Expr,UserAssertion></a>* <a class="code" href="classCVC3_1_1VCL.html#a00dfc7df82e450d5eaabce47f33657eb" title="Backtracking map of user assertions.">d_userAssertions</a>;
<a name="l00112"></a>00112 <span class="comment"></span>
<a name="l00113"></a>00113 <span class="comment"> //! Backtracking map of assertions when assertion batching is on</span>
<a name="l00114"></a><a class="code" href="classCVC3_1_1VCL.html#aa6c54159235f97cb9efc0e759070776a">00114</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDList.html">CDList<Expr></a>* <a class="code" href="classCVC3_1_1VCL.html#aa6c54159235f97cb9efc0e759070776a" title="Backtracking map of assertions when assertion batching is on.">d_batchedAssertions</a>;
<a name="l00115"></a>00115 <span class="comment"></span>
<a name="l00116"></a>00116 <span class="comment"> //! Index into batched Assertions</span>
<a name="l00117"></a><a class="code" href="classCVC3_1_1VCL.html#ac8ea2beb5efa17c968e7312db331ef83">00117</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1CDO.html">CDO<unsigned></a>* <a class="code" href="classCVC3_1_1VCL.html#ac8ea2beb5efa17c968e7312db331ef83" title="Index into batched Assertions.">d_batchedAssertionsIdx</a>;
<a name="l00118"></a>00118 <span class="comment"></span>
<a name="l00119"></a>00119 <span class="comment"> //! Result of the last query()</span>
<a name="l00120"></a>00120 <span class="comment"></span><span class="comment"> /*! Saved for printing assumptions and proofs. Normally it is</span>
<a name="l00121"></a>00121 <span class="comment"> * Theorem3, but query() on a TCC returns a 2-valued Theorem. */</span>
<a name="l00122"></a><a class="code" href="classCVC3_1_1VCL.html#ac7b0947fe5b3c9c737828be483ba27de">00122</a> <a class="code" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a> <a class="code" href="classCVC3_1_1VCL.html#ac7b0947fe5b3c9c737828be483ba27de" title="Result of the last query()">d_lastQuery</a>;
<a name="l00123"></a>00123 <span class="comment"></span>
<a name="l00124"></a>00124 <span class="comment"> //! Result of the last query(e, true) (for a TCC).</span>
<a name="l00125"></a><a class="code" href="classCVC3_1_1VCL.html#a1a8b62c258a4104da2ee425761e06d34">00125</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="code" href="classCVC3_1_1VCL.html#a1a8b62c258a4104da2ee425761e06d34" title="Result of the last query(e, true) (for a TCC).">d_lastQueryTCC</a>;
<a name="l00126"></a>00126 <span class="comment"></span>
<a name="l00127"></a>00127 <span class="comment"> //! Closure of the last query(e): |- Gamma => e</span>
<a name="l00128"></a><a class="code" href="classCVC3_1_1VCL.html#a44bab91924f750908ea96a44feb37a15">00128</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a> <a class="code" href="classCVC3_1_1VCL.html#a44bab91924f750908ea96a44feb37a15" title="Closure of the last query(e): |- Gamma => e.">d_lastClosure</a>;
<a name="l00129"></a>00129 <span class="comment"></span>
<a name="l00130"></a>00130 <span class="comment"> //! Whether to dump a trace (or a translated version)</span>
<a name="l00131"></a><a class="code" href="classCVC3_1_1VCL.html#af81bf916ed823bb6578a35fb555a4a5a">00131</a> <span class="comment"></span> <span class="keywordtype">bool</span> <a class="code" href="classCVC3_1_1VCL.html#af81bf916ed823bb6578a35fb555a4a5a" title="Whether to dump a trace (or a translated version)">d_dump</a>;
<a name="l00132"></a>00132
<a name="l00133"></a>00133 <span class="comment">// Private methods</span>
<a name="l00134"></a>00134 <span class="comment"></span>
<a name="l00135"></a>00135 <span class="comment"> //! Construct the closure "|-_3 Gamma => phi" of thm = "Gamma |-_3 phi"</span>
<a name="l00136"></a>00136 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a> deriveClosure(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem3.html" title="Theorem3.">Theorem3</a>& thm);
<a name="l00137"></a>00137 <span class="comment"></span>
<a name="l00138"></a>00138 <span class="comment"> //! Recursive assumption graph traversal to find user assumptions</span>
<a name="l00139"></a>00139 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00140"></a>00140 <span class="comment"> * If an assumption has a TCC, traverse the proof of TCC and add its</span>
<a name="l00141"></a>00141 <span class="comment"> * assumptions to the set recursively.</span>
<a name="l00142"></a>00142 <span class="comment"> */</span>
<a name="l00143"></a>00143 <span class="keywordtype">void</span> getAssumptionsRec(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a>& thm,
<a name="l00144"></a>00144 std::set<UserAssertion>& assumptions,
<a name="l00145"></a>00145 <span class="keywordtype">bool</span> addTCCs);
<a name="l00146"></a>00146 <span class="comment"></span>
<a name="l00147"></a>00147 <span class="comment"> //! Get set of user assertions from the set of assumptions</span>
<a name="l00148"></a>00148 <span class="comment"></span> <span class="keywordtype">void</span> getAssumptions(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Assumptions.html">Assumptions</a>& a, std::vector<Expr>& assumptions);
<a name="l00149"></a>00149 <span class="comment"></span>
<a name="l00150"></a>00150 <span class="comment"> //! Check the tcc</span>
<a name="l00151"></a>00151 <span class="comment"></span> <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> checkTCC(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& tcc);
<a name="l00152"></a>00152
<a name="l00153"></a>00153 <span class="preprocessor">#ifdef _CVC3_DEBUG_MODE</span>
<a name="l00154"></a>00154 <span class="preprocessor"></span><span class="comment"> //! Print an entry to the dump file: change of scope</span>
<a name="l00155"></a>00155 <span class="comment"></span> <span class="keywordtype">void</span> dumpTrace(<span class="keywordtype">int</span> scope);
<a name="l00156"></a>00156 <span class="preprocessor">#endif</span>
<a name="l00157"></a>00157 <span class="preprocessor"></span><span class="comment"></span>
<a name="l00158"></a>00158 <span class="comment"> //! Initialize everything except flags</span>
<a name="l00159"></a>00159 <span class="comment"></span> <span class="keywordtype">void</span> init(<span class="keywordtype">void</span>);<span class="comment"></span>
<a name="l00160"></a>00160 <span class="comment"> //! Destroy everything except flags</span>
<a name="l00161"></a>00161 <span class="comment"></span> <span class="keywordtype">void</span> destroy(<span class="keywordtype">void</span>);
<a name="l00162"></a>00162
<a name="l00163"></a>00163 <span class="keyword">public</span>:
<a name="l00164"></a>00164 <span class="comment">// Takes the vector of command line flags.</span>
<a name="l00165"></a>00165 <a class="code" href="classCVC3_1_1VCL.html">VCL</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1CLFlags.html">CLFlags</a>& flags);
<a name="l00166"></a>00166 ~<a class="code" href="classCVC3_1_1VCL.html">VCL</a>();
<a name="l00167"></a>00167
<a name="l00168"></a>00168 <span class="comment">// Implementation of vc.h virtual functions</span>
<a name="l00169"></a>00169
<a name="l00170"></a><a class="code" href="classCVC3_1_1VCL.html#a499633a949434b41a8555d0cf6e435f6">00170</a> <a class="code" href="classCVC3_1_1CLFlags.html">CLFlags</a>& <a class="code" href="classCVC3_1_1VCL.html#a499633a949434b41a8555d0cf6e435f6" title="Return the set of command-line flags.">getFlags</a>()<span class="keyword"> const </span>{ <span class="keywordflow">return</span> *d_flags; }
<a name="l00171"></a>00171 <span class="keywordtype">void</span> reprocessFlags();
<a name="l00172"></a>00172
<a name="l00173"></a>00173 <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>* core();
<a name="l00174"></a>00174
<a name="l00175"></a>00175 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> boolType();
<a name="l00176"></a>00176 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> realType();
<a name="l00177"></a>00177 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> intType();
<a name="l00178"></a>00178 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> subrangeType(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& l, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& r);
<a name="l00179"></a>00179 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> subtypeType(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& pred, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& witness);
<a name="l00180"></a>00180 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> tupleType(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type0, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type1);
<a name="l00181"></a>00181 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> tupleType(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type0, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type2);
<a name="l00182"></a>00182 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> tupleType(<span class="keyword">const</span> std::vector<Type>& types);
<a name="l00183"></a>00183 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> recordType(<span class="keyword">const</span> std::string& field, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type);
<a name="l00184"></a>00184 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> recordType(<span class="keyword">const</span> std::string& field0, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type0,
<a name="l00185"></a>00185 <span class="keyword">const</span> std::string& field1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type1);
<a name="l00186"></a>00186 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> recordType(<span class="keyword">const</span> std::string& field0, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type0,
<a name="l00187"></a>00187 <span class="keyword">const</span> std::string& field1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type1,
<a name="l00188"></a>00188 <span class="keyword">const</span> std::string& field2, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type2);
<a name="l00189"></a>00189 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> recordType(<span class="keyword">const</span> std::vector<std::string>& fields,
<a name="l00190"></a>00190 <span class="keyword">const</span> std::vector<Type>& types);
<a name="l00191"></a>00191 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> dataType(<span class="keyword">const</span> std::string& name,
<a name="l00192"></a>00192 <span class="keyword">const</span> std::string& constructor,
<a name="l00193"></a>00193 <span class="keyword">const</span> std::vector<std::string>& selectors,
<a name="l00194"></a>00194 <span class="keyword">const</span> std::vector<Expr>& types);
<a name="l00195"></a>00195 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> dataType(<span class="keyword">const</span> std::string& name,
<a name="l00196"></a>00196 <span class="keyword">const</span> std::vector<std::string>& constructors,
<a name="l00197"></a>00197 <span class="keyword">const</span> std::vector<std::vector<std::string> >& selectors,
<a name="l00198"></a>00198 <span class="keyword">const</span> std::vector<std::vector<Expr> >& types);
<a name="l00199"></a>00199 <span class="keywordtype">void</span> dataType(<span class="keyword">const</span> std::vector<std::string>& names,
<a name="l00200"></a>00200 <span class="keyword">const</span> std::vector<std::vector<std::string> >& constructors,
<a name="l00201"></a>00201 <span class="keyword">const</span> std::vector<std::vector<std::vector<std::string> > >& selectors,
<a name="l00202"></a>00202 <span class="keyword">const</span> std::vector<std::vector<std::vector<Expr> > >& types,
<a name="l00203"></a>00203 std::vector<Type>& returnTypes);
<a name="l00204"></a>00204 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> <a class="code" href="namespaceCVC3.html#a587d33ff63396be21a99bf4d744b2b98">arrayType</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& typeIndex, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& typeData);
<a name="l00205"></a>00205 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> bitvecType(<span class="keywordtype">int</span> n);
<a name="l00206"></a>00206 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> funType(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& typeDom, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& typeRan);
<a name="l00207"></a>00207 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> funType(<span class="keyword">const</span> std::vector<Type>& typeDom, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& typeRan);
<a name="l00208"></a>00208 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> createType(<span class="keyword">const</span> std::string& typeName);
<a name="l00209"></a>00209 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> createType(<span class="keyword">const</span> std::string& typeName, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& def);
<a name="l00210"></a>00210 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> lookupType(<span class="keyword">const</span> std::string& typeName);
<a name="l00211"></a>00211
<a name="l00212"></a><a class="code" href="classCVC3_1_1VCL.html#a811f456c7be235f67a45c9359475f770">00212</a> <a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a>* <a class="code" href="classCVC3_1_1VCL.html#a811f456c7be235f67a45c9359475f770" title="Return the ExprManager.">getEM</a>() { <span class="keywordflow">return</span> d_em; }
<a name="l00213"></a>00213 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> varExpr(<span class="keyword">const</span> std::string& name, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type);
<a name="l00214"></a>00214 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> varExpr(<span class="keyword">const</span> std::string& name, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& def);
<a name="l00215"></a>00215 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> lookupVar(<span class="keyword">const</span> std::string& name, <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>* type);
<a name="l00216"></a>00216 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> getType(<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="l00217"></a>00217 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> getBaseType(<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="l00218"></a>00218 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> getBaseType(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& e);
<a name="l00219"></a>00219 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> getTypePred(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>&t, <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="l00220"></a>00220 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> stringExpr(<span class="keyword">const</span> std::string& str);
<a name="l00221"></a>00221 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> idExpr(<span class="keyword">const</span> std::string& name);
<a name="l00222"></a>00222 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> listExpr(<span class="keyword">const</span> std::vector<Expr>& kids);
<a name="l00223"></a>00223 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> listExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e1);
<a name="l00224"></a>00224 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> listExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e2);
<a name="l00225"></a>00225 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> listExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e2, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e3);
<a name="l00226"></a>00226 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> listExpr(<span class="keyword">const</span> std::string& op, <span class="keyword">const</span> std::vector<Expr>& kids);
<a name="l00227"></a>00227 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> listExpr(<span class="keyword">const</span> std::string& op, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e1);
<a name="l00228"></a>00228 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> listExpr(<span class="keyword">const</span> std::string& op, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e1,
<a name="l00229"></a>00229 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e2);
<a name="l00230"></a>00230 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> listExpr(<span class="keyword">const</span> std::string& op, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e1,
<a name="l00231"></a>00231 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e2, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e3);
<a name="l00232"></a>00232 <span class="keywordtype">void</span> printExpr(<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="l00233"></a>00233 <span class="keywordtype">void</span> printExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e, std::ostream& os);
<a name="l00234"></a>00234 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> parseExpr(<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="l00235"></a>00235 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> parseType(<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="l00236"></a>00236 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> importExpr(<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="l00237"></a>00237 <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> importType(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& t);
<a name="l00238"></a>00238 <span class="keywordtype">void</span> cmdsFromString(<span class="keyword">const</span> std::string& s, <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e" title="Different input languages.">InputLanguage</a> lang);
<a name="l00239"></a>00239 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> exprFromString(<span class="keyword">const</span> std::string& s);
<a name="l00240"></a>00240
<a name="l00241"></a>00241 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> trueExpr();
<a name="l00242"></a>00242 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> falseExpr();
<a name="l00243"></a>00243 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> notExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& child);
<a name="l00244"></a>00244 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#ad4258158bba138eb54b9080af7f8223a">andExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#a82558b7a36c52f5d3211d5d14bed99d4">right</a>);
<a name="l00245"></a>00245 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#ad4258158bba138eb54b9080af7f8223a">andExpr</a>(<span class="keyword">const</span> std::vector<Expr>& children);
<a name="l00246"></a>00246 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#a30f30b6e20c174f21ae63acea8618294">orExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#a82558b7a36c52f5d3211d5d14bed99d4">right</a>);
<a name="l00247"></a>00247 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#a30f30b6e20c174f21ae63acea8618294">orExpr</a>(<span class="keyword">const</span> std::vector<Expr>& children);
<a name="l00248"></a>00248 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> impliesExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& hyp, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& conc);
<a name="l00249"></a>00249 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> iffExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#a82558b7a36c52f5d3211d5d14bed99d4">right</a>);
<a name="l00250"></a>00250 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> eqExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& child0, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& child1);
<a name="l00251"></a>00251 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> distinctExpr(<span class="keyword">const</span> std::vector<Expr>& children);
<a name="l00252"></a>00252 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> iteExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& ifpart, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& thenpart, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& elsepart);
<a name="l00253"></a>00253
<a name="l00254"></a>00254 <a class="code" href="classCVC3_1_1Op.html">Op</a> createOp(<span class="keyword">const</span> std::string& name, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type);
<a name="l00255"></a>00255 <a class="code" href="classCVC3_1_1Op.html">Op</a> createOp(<span class="keyword">const</span> std::string& name, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& def);
<a name="l00256"></a>00256 <a class="code" href="classCVC3_1_1Op.html">Op</a> lookupOp(<span class="keyword">const</span> std::string& name, <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>* type);
<a name="l00257"></a>00257 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> funExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Op.html">Op</a>& op, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& child);
<a name="l00258"></a>00258 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> funExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Op.html">Op</a>& op, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#a82558b7a36c52f5d3211d5d14bed99d4">right</a>);
<a name="l00259"></a>00259 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> funExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Op.html">Op</a>& op, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& child0, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& child1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& child2);
<a name="l00260"></a>00260 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> funExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Op.html">Op</a>& op, <span class="keyword">const</span> std::vector<Expr>& children);
<a name="l00261"></a>00261
<a name="l00262"></a>00262 <span class="keywordtype">bool</span> addPairToArithOrder(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& smaller, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& bigger);
<a name="l00263"></a>00263 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> ratExpr(<span class="keywordtype">int</span> n, <span class="keywordtype">int</span> d);
<a name="l00264"></a>00264 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> ratExpr(<span class="keyword">const</span> std::string& n, <span class="keyword">const</span> std::string& d, <span class="keywordtype">int</span> base);
<a name="l00265"></a>00265 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> ratExpr(<span class="keyword">const</span> std::string& n, <span class="keywordtype">int</span> base);
<a name="l00266"></a>00266 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#a8eccf9a3ce48e30b704c1b689bfe3eff">uminusExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& child);
<a name="l00267"></a>00267 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#accd3d7d38b0e04136afbc3e5191bc8bb">plusExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#a82558b7a36c52f5d3211d5d14bed99d4">right</a>);
<a name="l00268"></a>00268 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#accd3d7d38b0e04136afbc3e5191bc8bb">plusExpr</a>(<span class="keyword">const</span> std::vector<Expr>& children);
<a name="l00269"></a>00269 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#a9ba326c305c5aeb61de515009aaa61f8">minusExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#a82558b7a36c52f5d3211d5d14bed99d4">right</a>);
<a name="l00270"></a>00270 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#adb35e0739f86730543924dbc8211a778">multExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#a82558b7a36c52f5d3211d5d14bed99d4">right</a>);
<a name="l00271"></a>00271 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#aa123bf4eb1751181baf16c5e80b47740" title="Power (x^n, or base^{pow}) expressions.">powExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& x, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& n);
<a name="l00272"></a>00272 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#a36b5fb04640e2f95f74a58837ae04f68">divideExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#a82558b7a36c52f5d3211d5d14bed99d4">right</a>);
<a name="l00273"></a>00273 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#ac9ccba18a3c725634b1f8ba8e99e627f">ltExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#a82558b7a36c52f5d3211d5d14bed99d4">right</a>);
<a name="l00274"></a>00274 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#aebfd8a82800bd3dff4c8db461a52cdea">leExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#a82558b7a36c52f5d3211d5d14bed99d4">right</a>);
<a name="l00275"></a>00275 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#a8ad355d6650f2dfa754419c634e36afb">gtExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#a82558b7a36c52f5d3211d5d14bed99d4">right</a>);
<a name="l00276"></a>00276 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> <a class="code" href="namespaceCVC3.html#a520cf0df288be321d27ea6fa77ded2d2">geExpr</a>(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#ad93cb56673487974071ed3b75bf4ea83">left</a>, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& <a class="code" href="namespaceMiniSat.html#a82558b7a36c52f5d3211d5d14bed99d4">right</a>);
<a name="l00277"></a>00277
<a name="l00278"></a>00278 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> recordExpr(<span class="keyword">const</span> std::string& field, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& expr);
<a name="l00279"></a>00279 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> recordExpr(<span class="keyword">const</span> std::string& field0, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& expr0,
<a name="l00280"></a>00280 <span class="keyword">const</span> std::string& field1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& expr1);
<a name="l00281"></a>00281 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> recordExpr(<span class="keyword">const</span> std::string& field0, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& expr0,
<a name="l00282"></a>00282 <span class="keyword">const</span> std::string& field1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& expr1,
<a name="l00283"></a>00283 <span class="keyword">const</span> std::string& field2, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& expr2);
<a name="l00284"></a>00284 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> recordExpr(<span class="keyword">const</span> std::vector<std::string>& fields,
<a name="l00285"></a>00285 <span class="keyword">const</span> std::vector<Expr>& exprs);
<a name="l00286"></a>00286 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> recSelectExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& record, <span class="keyword">const</span> std::string& field);
<a name="l00287"></a>00287 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> recUpdateExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& record, <span class="keyword">const</span> std::string& field,
<a name="l00288"></a>00288 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& newValue);
<a name="l00289"></a>00289
<a name="l00290"></a>00290 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> readExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& array, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& index);
<a name="l00291"></a>00291 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> writeExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& array, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& index, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& newValue);
<a name="l00292"></a>00292
<a name="l00293"></a>00293 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVConstExpr(<span class="keyword">const</span> std::string& s, <span class="keywordtype">int</span> base);
<a name="l00294"></a>00294 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVConstExpr(<span class="keyword">const</span> std::vector<bool>& bits);
<a name="l00295"></a>00295 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVConstExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Rational.html">Rational</a>& r, <span class="keywordtype">int</span> len);
<a name="l00296"></a>00296 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newConcatExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00297"></a>00297 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newConcatExpr(<span class="keyword">const</span> std::vector<Expr>& kids);
<a name="l00298"></a>00298 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVExtractExpr(<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">int</span> hi, <span class="keywordtype">int</span> low);
<a name="l00299"></a>00299 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVNegExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1);
<a name="l00300"></a>00300 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVAndExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00301"></a>00301 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVAndExpr(<span class="keyword">const</span> std::vector<Expr>& kids);
<a name="l00302"></a>00302 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVOrExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00303"></a>00303 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVOrExpr(<span class="keyword">const</span> std::vector<Expr>& kids);
<a name="l00304"></a>00304 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVXorExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00305"></a>00305 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVXorExpr(<span class="keyword">const</span> std::vector<Expr>& kids);
<a name="l00306"></a>00306 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVXnorExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00307"></a>00307 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVXnorExpr(<span class="keyword">const</span> std::vector<Expr>& kids);
<a name="l00308"></a>00308 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVNandExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00309"></a>00309 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVNorExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00310"></a>00310 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVCompExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00311"></a>00311 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVLTExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00312"></a>00312 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVLEExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00313"></a>00313 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVSLTExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00314"></a>00314 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVSLEExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00315"></a>00315 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newSXExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keywordtype">int</span> len);
<a name="l00316"></a>00316 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVUminusExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1);
<a name="l00317"></a>00317 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVSubExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00318"></a>00318 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVPlusExpr(<span class="keywordtype">int</span> numbits, <span class="keyword">const</span> std::vector<Expr>& k);
<a name="l00319"></a>00319 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVPlusExpr(<span class="keywordtype">int</span> numbits, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00320"></a>00320 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVMultExpr(<span class="keywordtype">int</span> numbits, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00321"></a>00321 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVUDivExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00322"></a>00322 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVURemExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00323"></a>00323 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVSDivExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00324"></a>00324 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVSRemExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00325"></a>00325 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVSModExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00326"></a>00326 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newFixedLeftShiftExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keywordtype">int</span> r);
<a name="l00327"></a>00327 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newFixedConstWidthLeftShiftExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keywordtype">int</span> r);
<a name="l00328"></a>00328 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newFixedRightShiftExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keywordtype">int</span> r);
<a name="l00329"></a>00329 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVSHL(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00330"></a>00330 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVLSHR(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00331"></a>00331 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVASHR(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t1, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& t2);
<a name="l00332"></a>00332 <a class="code" href="classCVC3_1_1Rational.html">Rational</a> computeBVConst(<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="l00333"></a>00333
<a name="l00334"></a>00334 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> tupleExpr(<span class="keyword">const</span> std::vector<Expr>& exprs);
<a name="l00335"></a>00335 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> tupleSelectExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& tuple, <span class="keywordtype">int</span> index);
<a name="l00336"></a>00336 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> tupleUpdateExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& tuple, <span class="keywordtype">int</span> index, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& newValue);
<a name="l00337"></a>00337 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> datatypeConsExpr(<span class="keyword">const</span> std::string& constructor,
<a name="l00338"></a>00338 <span class="keyword">const</span> std::vector<Expr>& args);
<a name="l00339"></a>00339 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> datatypeSelExpr(<span class="keyword">const</span> std::string& selector, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& arg);
<a name="l00340"></a>00340 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> datatypeTestExpr(<span class="keyword">const</span> std::string& constructor, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& arg);
<a name="l00341"></a>00341 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> boundVarExpr(<span class="keyword">const</span> std::string& name, <span class="keyword">const</span> std::string& uid,
<a name="l00342"></a>00342 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type);
<a name="l00343"></a>00343 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> forallExpr(<span class="keyword">const</span> std::vector<Expr>& vars, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& body);
<a name="l00344"></a>00344 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> forallExpr(<span class="keyword">const</span> std::vector<Expr>& vars, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& body, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& trigger);
<a name="l00345"></a>00345 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> forallExpr(<span class="keyword">const</span> std::vector<Expr>& vars, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& body,
<a name="l00346"></a>00346 <span class="keyword">const</span> std::vector<Expr>& triggers);
<a name="l00347"></a>00347 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> forallExpr(<span class="keyword">const</span> std::vector<Expr>& vars, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& body,
<a name="l00348"></a>00348 <span class="keyword">const</span> std::vector<std::vector<Expr> >& triggers);
<a name="l00349"></a>00349
<a name="l00350"></a>00350 <span class="keywordtype">void</span> setTriggers(<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="keyword">const</span> std::vector<std::vector<Expr> >& triggers);
<a name="l00351"></a>00351 <span class="keywordtype">void</span> setTriggers(<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="keyword">const</span> std::vector<Expr>& triggers);
<a name="l00352"></a>00352 <span class="keywordtype">void</span> setTrigger(<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="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& trigger);
<a name="l00353"></a>00353 <span class="keywordtype">void</span> setMultiTrigger(<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="keyword">const</span> std::vector<Expr>& multiTrigger);
<a name="l00354"></a>00354
<a name="l00355"></a>00355 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> existsExpr(<span class="keyword">const</span> std::vector<Expr>& vars, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& body);
<a name="l00356"></a>00356 <a class="code" href="classCVC3_1_1Op.html">Op</a> lambdaExpr(<span class="keyword">const</span> std::vector<Expr>& vars, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& body);
<a name="l00357"></a>00357 <a class="code" href="classCVC3_1_1Op.html">Op</a> transClosure(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Op.html">Op</a>& op);
<a name="l00358"></a>00358 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> simulateExpr(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& f, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& s0,
<a name="l00359"></a>00359 <span class="keyword">const</span> std::vector<Expr>& inputs, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& n);
<a name="l00360"></a>00360
<a name="l00361"></a>00361 <span class="keywordtype">void</span> setResourceLimit(<span class="keywordtype">unsigned</span> limit);
<a name="l00362"></a>00362 <span class="keywordtype">void</span> setTimeLimit(<span class="keywordtype">unsigned</span> limit);
<a name="l00363"></a>00363 <span class="keywordtype">void</span> assertFormula(<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="l00364"></a>00364 <span class="keywordtype">void</span> registerAtom(<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="l00365"></a>00365 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> getImpliedLiteral();
<a name="l00366"></a>00366 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> simplify(<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="l00367"></a>00367 <a class="code" href="classCVC3_1_1Theorem.html">Theorem</a> simplifyThm(<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="l00368"></a>00368 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> query(<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="l00369"></a>00369 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> checkUnsat(<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="l00370"></a>00370 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> checkContinue();
<a name="l00371"></a>00371 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> restart(<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="l00372"></a>00372 <span class="keywordtype">void</span> returnFromCheck();
<a name="l00373"></a>00373 <span class="keywordtype">void</span> getUserAssumptions(std::vector<Expr>& assumptions);
<a name="l00374"></a>00374 <span class="keywordtype">void</span> getInternalAssumptions(std::vector<Expr>& assumptions);
<a name="l00375"></a>00375 <span class="keywordtype">void</span> getAssumptions(std::vector<Expr>& assumptions);
<a name="l00376"></a>00376 <span class="keywordtype">void</span> getAssumptionsUsed(std::vector<Expr>& assumptions);
<a name="l00377"></a>00377 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> getProofQuery();
<a name="l00378"></a>00378 <span class="keywordtype">void</span> getCounterExample(std::vector<Expr>& assumptions, <span class="keywordtype">bool</span> inOrder);
<a name="l00379"></a>00379 <span class="keywordtype">void</span> getConcreteModel(<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> & m);
<a name="l00380"></a>00380 <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> tryModelGeneration();
<a name="l00381"></a>00381 <a class="code" href="namespaceCVC3.html#a9d68f126b86e6fd08b3bc13a511df9bf">FormulaValue</a> value(<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="l00382"></a>00382 <span class="keywordtype">bool</span> inconsistent(std::vector<Expr>& assumptions);
<a name="l00383"></a>00383 <span class="keywordtype">bool</span> inconsistent();
<a name="l00384"></a>00384 <span class="keywordtype">bool</span> incomplete();
<a name="l00385"></a>00385 <span class="keywordtype">bool</span> incomplete(std::vector<std::string>& reasons);
<a name="l00386"></a>00386 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> getProof();
<a name="l00387"></a>00387 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> getAssignment();
<a name="l00388"></a>00388 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> getValue(<a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> e);
<a name="l00389"></a>00389 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> getTCC();
<a name="l00390"></a>00390 <span class="keywordtype">void</span> getAssumptionsTCC(std::vector<Expr>& assumptions);
<a name="l00391"></a>00391 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> getProofTCC();
<a name="l00392"></a>00392 <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> getClosure();
<a name="l00393"></a>00393 <a class="code" href="classCVC3_1_1Proof.html">Proof</a> getProofClosure();
<a name="l00394"></a>00394
<a name="l00395"></a>00395 <span class="keywordtype">int</span> stackLevel();
<a name="l00396"></a>00396 <span class="keywordtype">void</span> <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a>();
<a name="l00397"></a>00397 <span class="keywordtype">void</span> <a class="code" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be" title="Restore the indentation.">pop</a>();
<a name="l00398"></a>00398 <span class="keywordtype">void</span> popto(<span class="keywordtype">int</span> stackLevel);
<a name="l00399"></a>00399 <span class="keywordtype">int</span> scopeLevel();
<a name="l00400"></a>00400 <span class="keywordtype">void</span> pushScope();
<a name="l00401"></a>00401 <span class="keywordtype">void</span> popScope();
<a name="l00402"></a>00402 <span class="keywordtype">void</span> poptoScope(<span class="keywordtype">int</span> scopeLevel);
<a name="l00403"></a>00403 <a class="code" href="classCVC3_1_1Context.html">Context</a>* getCurrentContext();
<a name="l00404"></a>00404 <span class="keywordtype">void</span> <a class="code" href="group__ExprStream__Manip.html#ga90deb7348703ae1a59a11d9af77aa8ad" title="Reset the indentation to the default at this level.">reset</a>();
<a name="l00405"></a>00405 <span class="keywordtype">void</span> logAnnotation(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& annot);
<a name="l00406"></a>00406
<a name="l00407"></a>00407 <span class="keywordtype">void</span> loadFile(<span class="keyword">const</span> std::string& fileName,
<a name="l00408"></a>00408 <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e" title="Different input languages.">InputLanguage</a> lang = <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0eaa315c228d5c3290ce37df81524ed8e9a" title="Nice SAL-like language for manually written specs.">PRESENTATION_LANG</a>,
<a name="l00409"></a>00409 <span class="keywordtype">bool</span> interactive = <span class="keyword">false</span>,
<a name="l00410"></a>00410 <span class="keywordtype">bool</span> calledFromParser = <span class="keyword">false</span>);
<a name="l00411"></a>00411 <span class="keywordtype">void</span> loadFile(std::istream& is,
<a name="l00412"></a>00412 <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0e" title="Different input languages.">InputLanguage</a> lang = <a class="code" href="namespaceCVC3.html#a3aaaf7bc1fc47a4860ef6e59ddb0db0eaa315c228d5c3290ce37df81524ed8e9a" title="Nice SAL-like language for manually written specs.">PRESENTATION_LANG</a>,
<a name="l00413"></a>00413 <span class="keywordtype">bool</span> interactive = <span class="keyword">false</span>);
<a name="l00414"></a>00414
<a name="l00415"></a><a class="code" href="classCVC3_1_1VCL.html#a2c6c8bea5a7157b00fffc255feffcd22">00415</a> <a class="code" href="classCVC3_1_1Statistics.html">Statistics</a>& <a class="code" href="classCVC3_1_1VCL.html#a2c6c8bea5a7157b00fffc255feffcd22" title="Get statistics object.">getStatistics</a>() { <span class="keywordflow">return</span> *d_statistics; }
<a name="l00416"></a><a class="code" href="classCVC3_1_1VCL.html#a29fe4941b5cbb201d7918afeac0dc3cb">00416</a> <span class="keywordtype">void</span> <a class="code" href="classCVC3_1_1VCL.html#a29fe4941b5cbb201d7918afeac0dc3cb" title="Print collected statistics to stdout.">printStatistics</a>() { std::cout << *d_statistics << <a class="code" href="group__ExprStream__Manip.html#ga05b0ea7353ec24fa8e7e272d7a7875d8" title="Print the end-of-line.">std::endl</a>; }
<a name="l00417"></a>00417 <span class="keywordtype">unsigned</span> <span class="keywordtype">long</span> getMemory(<span class="keywordtype">int</span> verbosity = 0);
<a name="l00418"></a>00418
<a name="l00419"></a>00419 };
<a name="l00420"></a>00420
<a name="l00421"></a>00421 }
<a name="l00422"></a>00422
<a name="l00423"></a>00423 <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>
