<!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: vc.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">vc.h</div> </div>
</div>
<div class="contents">
<a href="vc_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 vc.h</span>
<a name="l00004"></a>00004 <span class="comment"> * \brief Generic API for a validity checker</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: Tue Nov 26 17:45:10 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__vc_h_</span>
<a name="l00023"></a>00023 <span class="preprocessor"></span><span class="preprocessor">#define _cvc3__include__vc_h_</span>
<a name="l00024"></a>00024 <span class="preprocessor"></span>
<a name="l00025"></a>00025 <span class="preprocessor">#include "<a class="code" href="os_8h.html" title="Abstraction over different operating systems.">os.h</a>"</span>
<a name="l00026"></a>00026 <span class="preprocessor">#include "<a class="code" href="queryresult_8h.html" title="enumerated type for result of queries">queryresult.h</a>"</span>
<a name="l00027"></a>00027 <span class="preprocessor">#include "<a class="code" href="expr_8h.html" title="Definition of the API to expression package. See class Expr for details.">expr.h</a>"</span>
<a name="l00028"></a>00028 <span class="preprocessor">#include "<a class="code" href="formula__value_8h.html" title="enumerated type for value of formulas">formula_value.h</a>"</span>
<a name="l00029"></a>00029
<a name="l00030"></a>00030 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00031"></a>00031 <span class="comment">/*! Note that this list of modules is very incomplete</span>
<a name="l00032"></a>00032 <span class="comment"> */</span>
<a name="l00033"></a>00033 <span class="comment">/*****************************************************************************/</span>
<a name="l00034"></a>00034
<a name="l00035"></a>00035 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00036"></a>00036 <span class="comment">/*!</span>
<a name="l00037"></a>00037 <span class="comment"> *\defgroup CVC3 CVC3</span>
<a name="l00038"></a>00038 <span class="comment"> *\brief The top level group which includes all of CVC3 documentation.</span>
<a name="l00039"></a>00039 <span class="comment"> *@{</span>
<a name="l00040"></a>00040 <span class="comment"> */</span>
<a name="l00041"></a>00041 <span class="comment">/*****************************************************************************/</span>
<a name="l00042"></a>00042
<a name="l00043"></a>00043 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00044"></a>00044 <span class="comment">/*!</span>
<a name="l00045"></a>00045 <span class="comment"> *\defgroup BuildingBlocks Building Blocks</span>
<a name="l00046"></a>00046 <span class="comment"> *\brief Code providing basic infrastructure</span>
<a name="l00047"></a>00047 <span class="comment"> */</span>
<a name="l00048"></a>00048 <span class="comment">/*****************************************************************************/</span>
<a name="l00049"></a>00049
<a name="l00050"></a>00050 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00051"></a>00051 <span class="comment">/*!</span>
<a name="l00052"></a>00052 <span class="comment"> *\defgroup VC Validity Checker</span>
<a name="l00053"></a>00053 <span class="comment"> *\brief The modules that make up the validity checker</span>
<a name="l00054"></a>00054 <span class="comment"> */</span>
<a name="l00055"></a>00055 <span class="comment">/*****************************************************************************/</span>
<a name="l00056"></a>00056 <span class="comment"></span>
<a name="l00057"></a>00057 <span class="comment">/*@}*/</span> <span class="comment">// end of group CVC3</span>
<a name="l00058"></a>00058
<a name="l00059"></a>00059 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00060"></a>00060 <span class="comment">/*!</span>
<a name="l00061"></a>00061 <span class="comment"> *\defgroup VC_API Validity Checker API</span>
<a name="l00062"></a>00062 <span class="comment"> * \ingroup VC</span>
<a name="l00063"></a>00063 <span class="comment"> *\brief The library interface of the validity checker (class ValidityChecker)</span>
<a name="l00064"></a>00064 <span class="comment"> */</span>
<a name="l00065"></a>00065 <span class="comment">/*****************************************************************************/</span>
<a name="l00066"></a>00066
<a name="l00067"></a>00067 <span class="keyword">namespace </span>CVC3 {
<a name="l00068"></a>00068
<a name="l00069"></a>00069 <span class="keyword">class </span>Context;
<a name="l00070"></a>00070 <span class="keyword">class </span>CLFlags;
<a name="l00071"></a>00071 <span class="keyword">class </span>Statistics;
<a name="l00072"></a>00072
<a name="l00073"></a>00073 <span class="comment">/*****************************************************************************/</span><span class="comment"></span>
<a name="l00074"></a>00074 <span class="comment">/*!</span>
<a name="l00075"></a>00075 <span class="comment"> *\class ValidityChecker</span>
<a name="l00076"></a>00076 <span class="comment"> *\brief Generic API for a validity checker</span>
<a name="l00077"></a>00077 <span class="comment"> *\ingroup VC_API</span>
<a name="l00078"></a>00078 <span class="comment"> *\anchor vc</span>
<a name="l00079"></a>00079 <span class="comment"> *</span>
<a name="l00080"></a>00080 <span class="comment"> * Author: Clark Barrett</span>
<a name="l00081"></a>00081 <span class="comment"> *</span>
<a name="l00082"></a>00082 <span class="comment"> * Created: Tue Nov 26 18:24:25 2002</span>
<a name="l00083"></a>00083 <span class="comment"> *</span>
<a name="l00084"></a>00084 <span class="comment"> * All terms and formulas are represented as expressions using the Expr class.</span>
<a name="l00085"></a>00085 <span class="comment"> * The notion of a context is also important. A context is a "background" set</span>
<a name="l00086"></a>00086 <span class="comment"> * of formulas which are assumed to be true or false. Formulas can be added to</span>
<a name="l00087"></a>00087 <span class="comment"> * the context explicitly, using assertFormula, or they may be added as part of</span>
<a name="l00088"></a>00088 <span class="comment"> * processing a query command. At any time, the current set of formulas making</span>
<a name="l00089"></a>00089 <span class="comment"> * up the context can be retrieved using getAssumptions.</span>
<a name="l00090"></a>00090 <span class="comment"> */</span>
<a name="l00091"></a>00091 <span class="comment">/*****************************************************************************/</span>
<a name="l00092"></a><a class="code" href="classCVC3_1_1ValidityChecker.html">00092</a> <span class="keyword">class </span><a class="code" href="os_8h.html#a0035aac6379df39aa69feba98b2751ba">CVC_DLL</a> <a class="code" href="classCVC3_1_1ValidityChecker.html" title="Generic API for a validity checker.">ValidityChecker</a> {
<a name="l00093"></a>00093
<a name="l00094"></a>00094 <span class="keyword">public</span>:<span class="comment"></span>
<a name="l00095"></a>00095 <span class="comment"> //! Constructor</span>
<a name="l00096"></a><a class="code" href="classCVC3_1_1ValidityChecker.html#a15399f370b5af3e31e1ee2add14470bf">00096</a> <span class="comment"></span> <a class="code" href="classCVC3_1_1ValidityChecker.html#a15399f370b5af3e31e1ee2add14470bf" title="Constructor.">ValidityChecker</a>() {}<span class="comment"></span>
<a name="l00097"></a>00097 <span class="comment"> //! Destructor</span>
<a name="l00098"></a><a class="code" href="classCVC3_1_1ValidityChecker.html#a4ba951ee63a5a1ffb804f282980a1a68">00098</a> <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1ValidityChecker.html#a4ba951ee63a5a1ffb804f282980a1a68" title="Destructor.">~ValidityChecker</a>() {}
<a name="l00099"></a>00099 <span class="comment"></span>
<a name="l00100"></a>00100 <span class="comment"> //! Return the set of command-line flags</span>
<a name="l00101"></a>00101 <span class="comment"></span><span class="comment"> /*! The flags are returned by reference, and if modified, will have an</span>
<a name="l00102"></a>00102 <span class="comment"> immediate effect on the subsequent commands. Note that not all flags will</span>
<a name="l00103"></a>00103 <span class="comment"> have such an effect; some flags are used only at initialization time (like</span>
<a name="l00104"></a>00104 <span class="comment"> "sat"), and therefore, will not take effect if modified after</span>
<a name="l00105"></a>00105 <span class="comment"> ValidityChecker is created.</span>
<a name="l00106"></a>00106 <span class="comment"> */</span>
<a name="l00107"></a>00107 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1CLFlags.html">CLFlags</a>& getFlags() <span class="keyword">const</span> = 0;<span class="comment"></span>
<a name="l00108"></a>00108 <span class="comment"> //! Force reprocessing of all flags</span>
<a name="l00109"></a>00109 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">void</span> reprocessFlags() = 0;
<a name="l00110"></a>00110
<a name="l00111"></a>00111 <span class="comment">/***************************************************************************/</span>
<a name="l00112"></a>00112 <span class="comment">/*</span>
<a name="l00113"></a>00113 <span class="comment"> * Static methods</span>
<a name="l00114"></a>00114 <span class="comment"> */</span>
<a name="l00115"></a>00115 <span class="comment">/***************************************************************************/</span>
<a name="l00116"></a>00116 <span class="comment"></span>
<a name="l00117"></a>00117 <span class="comment"> //! Create the set of command line flags with default values;</span>
<a name="l00118"></a>00118 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00119"></a>00119 <span class="comment"> \return the set of flags by value</span>
<a name="l00120"></a>00120 <span class="comment"> */</span>
<a name="l00121"></a>00121 <span class="keyword">static</span> <a class="code" href="classCVC3_1_1CLFlags.html">CLFlags</a> createFlags();<span class="comment"></span>
<a name="l00122"></a>00122 <span class="comment"> //! Create an instance of ValidityChecker</span>
<a name="l00123"></a>00123 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00124"></a>00124 <span class="comment"> \param flags is the set of command line flags.</span>
<a name="l00125"></a>00125 <span class="comment"> */</span>
<a name="l00126"></a>00126 <span class="keyword">static</span> <a class="code" href="classCVC3_1_1ValidityChecker.html" title="Generic API for a validity checker.">ValidityChecker</a>* create(<span class="keyword">const</span> <a class="code" href="classCVC3_1_1CLFlags.html">CLFlags</a>& flags);<span class="comment"></span>
<a name="l00127"></a>00127 <span class="comment"> //! Create an instance of ValidityChecker using default flag values.</span>
<a name="l00128"></a>00128 <span class="comment"></span> <span class="keyword">static</span> <a class="code" href="classCVC3_1_1ValidityChecker.html" title="Generic API for a validity checker.">ValidityChecker</a>* create();
<a name="l00129"></a>00129
<a name="l00130"></a>00130 <span class="comment">/***************************************************************************/</span><span class="comment"></span>
<a name="l00131"></a>00131 <span class="comment"> /*!</span>
<a name="l00132"></a>00132 <span class="comment"> *\name Type-related methods</span>
<a name="l00133"></a>00133 <span class="comment"> * Methods for creating and looking up types</span>
<a name="l00134"></a>00134 <span class="comment"> *\sa class Type</span>
<a name="l00135"></a>00135 <span class="comment"> *@{</span>
<a name="l00136"></a>00136 <span class="comment"> */</span>
<a name="l00137"></a>00137 <span class="comment">/***************************************************************************/</span>
<a name="l00138"></a>00138
<a name="l00139"></a>00139 <span class="comment">// Basic types</span>
<a name="l00140"></a>00140 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> boolType() = 0; <span class="comment">//!< Create type BOOLEAN</span>
<a name="l00141"></a>00141 <span class="comment"></span>
<a name="l00142"></a>00142 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> realType() = 0; <span class="comment">//!< Create type REAL</span>
<a name="l00143"></a>00143 <span class="comment"></span>
<a name="l00144"></a>00144 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> intType() = 0; <span class="comment">//!< Create type INT</span>
<a name="l00145"></a>00145 <span class="comment"></span><span class="comment"></span>
<a name="l00146"></a>00146 <span class="comment"> //! Create a subrange type [l..r]</span>
<a name="l00147"></a>00147 <span class="comment"></span><span class="comment"> /*! l and r can be Null; l=Null represents minus infinity, r=Null is</span>
<a name="l00148"></a>00148 <span class="comment"> * plus infinity.</span>
<a name="l00149"></a>00149 <span class="comment"> */</span>
<a name="l00150"></a>00150 <span class="keyword">virtual</span> <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) = 0;
<a name="l00151"></a>00151 <span class="comment"></span>
<a name="l00152"></a>00152 <span class="comment"> //! Creates a subtype defined by the given predicate</span>
<a name="l00153"></a>00153 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00154"></a>00154 <span class="comment"> * \param pred is a predicate taking one argument of type T and returning</span>
<a name="l00155"></a>00155 <span class="comment"> * Boolean. The resulting type is a subtype of T whose elements x are those</span>
<a name="l00156"></a>00156 <span class="comment"> * satisfying the predicate pred(x).</span>
<a name="l00157"></a>00157 <span class="comment"> *</span>
<a name="l00158"></a>00158 <span class="comment"> * \param witness is an expression of type T for which pred holds (if a Null</span>
<a name="l00159"></a>00159 <span class="comment"> * expression is passed as a witness, cvc will try to prove \f$\exists x. pred(x))\f$.</span>
<a name="l00160"></a>00160 <span class="comment"> * if the witness check fails, a TypecheckException is thrown.</span>
<a name="l00161"></a>00161 <span class="comment"> */</span>
<a name="l00162"></a>00162 <span class="keyword">virtual</span> <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) = 0;
<a name="l00163"></a>00163
<a name="l00164"></a>00164 <span class="comment">// Tuple types</span><span class="comment"></span>
<a name="l00165"></a>00165 <span class="comment"> //! 2-element tuple</span>
<a name="l00166"></a>00166 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00167"></a>00167 <span class="comment"></span>
<a name="l00168"></a>00168 <span class="comment"> //! 3-element tuple</span>
<a name="l00169"></a>00169 <span class="comment"></span> <span class="keyword">virtual</span> <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="l00170"></a>00170 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type2) = 0;<span class="comment"></span>
<a name="l00171"></a>00171 <span class="comment"> //! n-element tuple (from a vector of types)</span>
<a name="l00172"></a>00172 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00173"></a>00173
<a name="l00174"></a>00174 <span class="comment">// Record types</span><span class="comment"></span>
<a name="l00175"></a>00175 <span class="comment"> //! 1-element record</span>
<a name="l00176"></a>00176 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00177"></a>00177 <span class="comment"></span>
<a name="l00178"></a>00178 <span class="comment"> //! 2-element record</span>
<a name="l00179"></a>00179 <span class="comment"></span><span class="comment"> /*! Fields will be sorted automatically */</span>
<a name="l00180"></a>00180 <span class="keyword">virtual</span> <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="l00181"></a>00181 <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) = 0;<span class="comment"></span>
<a name="l00182"></a>00182 <span class="comment"> //! 3-element record</span>
<a name="l00183"></a>00183 <span class="comment"></span><span class="comment"> /*! Fields will be sorted automatically */</span>
<a name="l00184"></a>00184 <span class="keyword">virtual</span> <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 <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) = 0;<span class="comment"></span>
<a name="l00187"></a>00187 <span class="comment"> //! n-element record (fields and types must be of the same length)</span>
<a name="l00188"></a>00188 <span class="comment"></span><span class="comment"> /*! Fields will be sorted automatically */</span>
<a name="l00189"></a>00189 <span class="keyword">virtual</span> <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) = 0;
<a name="l00191"></a>00191
<a name="l00192"></a>00192 <span class="comment">// Datatypes</span>
<a name="l00193"></a>00193 <span class="comment"></span>
<a name="l00194"></a>00194 <span class="comment"> //! Single datatype, single constructor</span>
<a name="l00195"></a>00195 <span class="comment"></span><span class="comment"> /*! The types are either type exressions (obtained from a type with</span>
<a name="l00196"></a>00196 <span class="comment"> * getExpr()) or string expressions containing the name of (one of) the</span>
<a name="l00197"></a>00197 <span class="comment"> * dataType(s) being defined. */</span>
<a name="l00198"></a>00198 <span class="keyword">virtual</span> <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="l00199"></a>00199 <span class="keyword">const</span> std::string& constructor,
<a name="l00200"></a>00200 <span class="keyword">const</span> std::vector<std::string>& selectors,
<a name="l00201"></a>00201 <span class="keyword">const</span> std::vector<Expr>& types) = 0;
<a name="l00202"></a>00202 <span class="comment"></span>
<a name="l00203"></a>00203 <span class="comment"> //! Single datatype, multiple constructors</span>
<a name="l00204"></a>00204 <span class="comment"></span><span class="comment"> /*! The types are either type exressions (obtained from a type with</span>
<a name="l00205"></a>00205 <span class="comment"> * getExpr()) or string expressions containing the name of (one of) the</span>
<a name="l00206"></a>00206 <span class="comment"> * dataType(s) being defined. */</span>
<a name="l00207"></a>00207 <span class="keyword">virtual</span> <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="l00208"></a>00208 <span class="keyword">const</span> std::vector<std::string>& constructors,
<a name="l00209"></a>00209 <span class="keyword">const</span> std::vector<std::vector<std::string> >& selectors,
<a name="l00210"></a>00210 <span class="keyword">const</span> std::vector<std::vector<Expr> >& types) = 0;
<a name="l00211"></a>00211 <span class="comment"></span>
<a name="l00212"></a>00212 <span class="comment"> //! Multiple datatypes</span>
<a name="l00213"></a>00213 <span class="comment"></span><span class="comment"> /*! The types are either type exressions (obtained from a type with</span>
<a name="l00214"></a>00214 <span class="comment"> * getExpr()) or string expressions containing the name of (one of) the</span>
<a name="l00215"></a>00215 <span class="comment"> * dataType(s) being defined. */</span>
<a name="l00216"></a>00216 <span class="keyword">virtual</span> <span class="keywordtype">void</span> dataType(<span class="keyword">const</span> std::vector<std::string>& names,
<a name="l00217"></a>00217 <span class="keyword">const</span> std::vector<std::vector<std::string> >& constructors,
<a name="l00218"></a>00218 <span class="keyword">const</span> std::vector<std::vector<std::vector<std::string> > >& selectors,
<a name="l00219"></a>00219 <span class="keyword">const</span> std::vector<std::vector<std::vector<Expr> > >& types,
<a name="l00220"></a>00220 std::vector<Type>& returnTypes) = 0;
<a name="l00221"></a>00221 <span class="comment"></span>
<a name="l00222"></a>00222 <span class="comment"> //! Create an array type (ARRAY typeIndex OF typeData)</span>
<a name="l00223"></a>00223 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00224"></a>00224 <span class="comment"></span>
<a name="l00225"></a>00225 <span class="comment"> //! Create a bitvector type of length n</span>
<a name="l00226"></a>00226 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> bitvecType(<span class="keywordtype">int</span> n) = 0;
<a name="l00227"></a>00227 <span class="comment"></span>
<a name="l00228"></a>00228 <span class="comment"> //! Create a function type typeDom -> typeRan</span>
<a name="l00229"></a>00229 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00230"></a>00230 <span class="comment"></span>
<a name="l00231"></a>00231 <span class="comment"> //! Create a function type (t1,t2,...,tn) -> typeRan</span>
<a name="l00232"></a>00232 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00233"></a>00233 <span class="comment"></span>
<a name="l00234"></a>00234 <span class="comment"> //! Create named user-defined uninterpreted type</span>
<a name="l00235"></a>00235 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> createType(<span class="keyword">const</span> std::string& typeName) = 0;
<a name="l00236"></a>00236 <span class="comment"></span>
<a name="l00237"></a>00237 <span class="comment"> //! Create named user-defined interpreted type (type abbreviation)</span>
<a name="l00238"></a>00238 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00239"></a>00239 <span class="comment"></span>
<a name="l00240"></a>00240 <span class="comment"> //! Lookup a user-defined (uninterpreted) type by name. Returns Null if none.</span>
<a name="l00241"></a>00241 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a> lookupType(<span class="keyword">const</span> std::string& typeName) = 0;
<a name="l00242"></a>00242 <span class="comment"></span>
<a name="l00243"></a>00243 <span class="comment"> /*@}*/</span> <span class="comment">// End of Type-related methods</span>
<a name="l00244"></a>00244
<a name="l00245"></a>00245 <span class="comment">/***************************************************************************/</span><span class="comment"></span>
<a name="l00246"></a>00246 <span class="comment"> /*!</span>
<a name="l00247"></a>00247 <span class="comment"> *\name General Expr methods</span>
<a name="l00248"></a>00248 <span class="comment"> *\sa class Expr</span>
<a name="l00249"></a>00249 <span class="comment"> *\sa class ExprManager</span>
<a name="l00250"></a>00250 <span class="comment"> *@{</span>
<a name="l00251"></a>00251 <span class="comment"> */</span>
<a name="l00252"></a>00252 <span class="comment">/***************************************************************************/</span>
<a name="l00253"></a>00253 <span class="comment"></span>
<a name="l00254"></a>00254 <span class="comment"> //! Return the ExprManager</span>
<a name="l00255"></a>00255 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1ExprManager.html">ExprManager</a>* getEM() = 0;
<a name="l00256"></a>00256 <span class="comment"></span>
<a name="l00257"></a>00257 <span class="comment"> //! Create a variable with a given name and type</span>
<a name="l00258"></a>00258 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00259"></a>00259 <span class="comment"> \param name is the name of the variable</span>
<a name="l00260"></a>00260 <span class="comment"> \param type is its type. The type cannot be a function type.</span>
<a name="l00261"></a>00261 <span class="comment"> \return an Expr representation of a new variable</span>
<a name="l00262"></a>00262 <span class="comment"> */</span>
<a name="l00263"></a>00263 <span class="keyword">virtual</span> <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) = 0;
<a name="l00264"></a>00264 <span class="comment"></span>
<a name="l00265"></a>00265 <span class="comment"> //! Create a variable with a given name, type, and value</span>
<a name="l00266"></a>00266 <span class="comment"></span> <span class="keyword">virtual</span> <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="l00267"></a>00267 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& def) = 0;
<a name="l00268"></a>00268 <span class="comment"></span>
<a name="l00269"></a>00269 <span class="comment"> //! Get the variable associated with a name, and its type</span>
<a name="l00270"></a>00270 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00271"></a>00271 <span class="comment"> \param name is the variable name</span>
<a name="l00272"></a>00272 <span class="comment"> \param type is where the type value is returned</span>
<a name="l00273"></a>00273 <span class="comment"></span>
<a name="l00274"></a>00274 <span class="comment"> \return a variable by the name. If there is no such Expr, a NULL \</span>
<a name="l00275"></a>00275 <span class="comment"> Expr is returned.</span>
<a name="l00276"></a>00276 <span class="comment"> */</span>
<a name="l00277"></a>00277 <span class="keyword">virtual</span> <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) = 0;
<a name="l00278"></a>00278 <span class="comment"></span>
<a name="l00279"></a>00279 <span class="comment"> //! Get the type of the Expr.</span>
<a name="l00280"></a>00280 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00281"></a>00281 <span class="comment"></span>
<a name="l00282"></a>00282 <span class="comment"> //! Get the largest supertype of the Expr.</span>
<a name="l00283"></a>00283 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00284"></a>00284 <span class="comment"></span>
<a name="l00285"></a>00285 <span class="comment"> //! Get the largest supertype of the Type.</span>
<a name="l00286"></a>00286 <span class="comment"></span> <span class="keyword">virtual</span> <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>& t) = 0;
<a name="l00287"></a>00287 <span class="comment"></span>
<a name="l00288"></a>00288 <span class="comment"> //! Get the subtype predicate</span>
<a name="l00289"></a>00289 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00290"></a>00290 <span class="comment"></span>
<a name="l00291"></a>00291 <span class="comment"> //! Create a string Expr</span>
<a name="l00292"></a>00292 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00293"></a>00293 <span class="comment"></span>
<a name="l00294"></a>00294 <span class="comment"> //! Create an ID Expr</span>
<a name="l00295"></a>00295 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00296"></a>00296 <span class="comment"></span>
<a name="l00297"></a>00297 <span class="comment"> //! Create a list Expr</span>
<a name="l00298"></a>00298 <span class="comment"></span><span class="comment"> /*! Intermediate representation for DP-specific expressions.</span>
<a name="l00299"></a>00299 <span class="comment"> * Normally, the first element of the list is a string Expr</span>
<a name="l00300"></a>00300 <span class="comment"> * representing an operator, and the rest of the list are the</span>
<a name="l00301"></a>00301 <span class="comment"> * arguments. For example,</span>
<a name="l00302"></a>00302 <span class="comment"> *</span>
<a name="l00303"></a>00303 <span class="comment"> * kids.push_back(vc->stringExpr("PLUS"));</span>
<a name="l00304"></a>00304 <span class="comment"> * kids.push_back(x); // x and y are previously created Exprs</span>
<a name="l00305"></a>00305 <span class="comment"> * kids.push_back(y);</span>
<a name="l00306"></a>00306 <span class="comment"> * Expr lst = vc->listExpr(kids);</span>
<a name="l00307"></a>00307 <span class="comment"> *</span>
<a name="l00308"></a>00308 <span class="comment"> * Or, alternatively (using its overloaded version):</span>
<a name="l00309"></a>00309 <span class="comment"> *</span>
<a name="l00310"></a>00310 <span class="comment"> * Expr lst = vc->listExpr("PLUS", x, y);</span>
<a name="l00311"></a>00311 <span class="comment"> *</span>
<a name="l00312"></a>00312 <span class="comment"> * or</span>
<a name="l00313"></a>00313 <span class="comment"> *</span>
<a name="l00314"></a>00314 <span class="comment"> * vector<Expr> summands;</span>
<a name="l00315"></a>00315 <span class="comment"> * summands.push_back(x); summands.push_back(y); ...</span>
<a name="l00316"></a>00316 <span class="comment"> * Expr lst = vc->listExpr("PLUS", summands);</span>
<a name="l00317"></a>00317 <span class="comment"> */</span>
<a name="l00318"></a>00318 <span class="keyword">virtual</span> <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) = 0;
<a name="l00319"></a>00319 <span class="comment"></span>
<a name="l00320"></a>00320 <span class="comment"> //! Overloaded version of listExpr with one argument</span>
<a name="l00321"></a>00321 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00322"></a>00322 <span class="comment"></span>
<a name="l00323"></a>00323 <span class="comment"> //! Overloaded version of listExpr with two arguments</span>
<a name="l00324"></a>00324 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00325"></a>00325 <span class="comment"></span>
<a name="l00326"></a>00326 <span class="comment"> //! Overloaded version of listExpr with three arguments</span>
<a name="l00327"></a>00327 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00328"></a>00328 <span class="comment"></span>
<a name="l00329"></a>00329 <span class="comment"> //! Overloaded version of listExpr with string operator and many arguments</span>
<a name="l00330"></a>00330 <span class="comment"></span> <span class="keyword">virtual</span> <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,
<a name="l00331"></a>00331 <span class="keyword">const</span> std::vector<Expr>& kids) = 0;
<a name="l00332"></a>00332 <span class="comment"></span>
<a name="l00333"></a>00333 <span class="comment"> //! Overloaded version of listExpr with string operator and one argument</span>
<a name="l00334"></a>00334 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00335"></a>00335 <span class="comment"></span>
<a name="l00336"></a>00336 <span class="comment"> //! Overloaded version of listExpr with string operator and two arguments</span>
<a name="l00337"></a>00337 <span class="comment"></span> <span class="keyword">virtual</span> <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="l00338"></a>00338 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& e2) = 0;
<a name="l00339"></a>00339 <span class="comment"></span>
<a name="l00340"></a>00340 <span class="comment"> //! Overloaded version of listExpr with string operator and three arguments</span>
<a name="l00341"></a>00341 <span class="comment"></span> <span class="keyword">virtual</span> <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="l00342"></a>00342 <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) = 0;
<a name="l00343"></a>00343 <span class="comment"></span>
<a name="l00344"></a>00344 <span class="comment"> //! Prints e to the standard output</span>
<a name="l00345"></a>00345 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00346"></a>00346 <span class="comment"></span>
<a name="l00347"></a>00347 <span class="comment"> //! Prints e to the given ostream</span>
<a name="l00348"></a>00348 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00349"></a>00349 <span class="comment"></span>
<a name="l00350"></a>00350 <span class="comment"> //! Parse an expression using a Theory-specific parser</span>
<a name="l00351"></a>00351 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00352"></a>00352 <span class="comment"></span>
<a name="l00353"></a>00353 <span class="comment"> //! Parse a type expression using a Theory-specific parser</span>
<a name="l00354"></a>00354 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00355"></a>00355 <span class="comment"></span>
<a name="l00356"></a>00356 <span class="comment"> //! Import the Expr from another instance of ValidityChecker</span>
<a name="l00357"></a>00357 <span class="comment"></span><span class="comment"> /*! When expressions need to be passed among several instances of</span>
<a name="l00358"></a>00358 <span class="comment"> * ValidityChecker, they need to be explicitly imported into the</span>
<a name="l00359"></a>00359 <span class="comment"> * corresponding instance using this method. The return result is</span>
<a name="l00360"></a>00360 <span class="comment"> * an identical expression that belongs to the current instance of</span>
<a name="l00361"></a>00361 <span class="comment"> * ValidityChecker, and can be safely used as part of more complex</span>
<a name="l00362"></a>00362 <span class="comment"> * expressions from the same instance.</span>
<a name="l00363"></a>00363 <span class="comment"> */</span>
<a name="l00364"></a>00364 <span class="keyword">virtual</span> <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) = 0;
<a name="l00365"></a>00365 <span class="comment"></span>
<a name="l00366"></a>00366 <span class="comment"> //! Import the Type from another instance of ValidityChecker</span>
<a name="l00367"></a>00367 <span class="comment"></span><span class="comment"> /*! \sa getType() */</span>
<a name="l00368"></a>00368 <span class="keyword">virtual</span> <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) = 0;
<a name="l00369"></a>00369 <span class="comment"></span>
<a name="l00370"></a>00370 <span class="comment"> //! Parse a sequence of commands from a presentation language string</span>
<a name="l00371"></a>00371 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">void</span> cmdsFromString(<span class="keyword">const</span> std::string& s,
<a name="l00372"></a>00372 <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>) = 0;
<a name="l00373"></a>00373 <span class="comment"></span>
<a name="l00374"></a>00374 <span class="comment"> //! Parse an expression from a presentation language string</span>
<a name="l00375"></a>00375 <span class="comment"></span> <span class="keyword">virtual</span> <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& e) = 0;
<a name="l00376"></a>00376 <span class="comment"></span>
<a name="l00377"></a>00377 <span class="comment"> /*@}*/</span> <span class="comment">// End of General Expr Methods</span>
<a name="l00378"></a>00378
<a name="l00379"></a>00379 <span class="comment">/***************************************************************************/</span><span class="comment"></span>
<a name="l00380"></a>00380 <span class="comment"> /*!</span>
<a name="l00381"></a>00381 <span class="comment"> *\name Core expression methods</span>
<a name="l00382"></a>00382 <span class="comment"> * Methods for manipulating core expressions</span>
<a name="l00383"></a>00383 <span class="comment"> *</span>
<a name="l00384"></a>00384 <span class="comment"> * Except for equality and ite, the children provided as arguments must be of</span>
<a name="l00385"></a>00385 <span class="comment"> * type Boolean.</span>
<a name="l00386"></a>00386 <span class="comment"> *@{</span>
<a name="l00387"></a>00387 <span class="comment"> */</span>
<a name="l00388"></a>00388 <span class="comment">/***************************************************************************/</span>
<a name="l00389"></a>00389 <span class="comment"></span>
<a name="l00390"></a>00390 <span class="comment"> //! Return TRUE Expr</span>
<a name="l00391"></a>00391 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> trueExpr() = 0;
<a name="l00392"></a>00392 <span class="comment"></span>
<a name="l00393"></a>00393 <span class="comment"> //! Return FALSE Expr</span>
<a name="l00394"></a>00394 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> falseExpr() = 0;
<a name="l00395"></a>00395 <span class="comment"></span>
<a name="l00396"></a>00396 <span class="comment"> //! Create negation</span>
<a name="l00397"></a>00397 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00398"></a>00398 <span class="comment"></span>
<a name="l00399"></a>00399 <span class="comment"> //! Create 2-element conjunction</span>
<a name="l00400"></a>00400 <span class="comment"></span> <span class="keyword">virtual</span> <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>) = 0;
<a name="l00401"></a>00401 <span class="comment"></span>
<a name="l00402"></a>00402 <span class="comment"> //! Create n-element conjunction</span>
<a name="l00403"></a>00403 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00404"></a>00404 <span class="comment"></span>
<a name="l00405"></a>00405 <span class="comment"> //! Create 2-element disjunction</span>
<a name="l00406"></a>00406 <span class="comment"></span> <span class="keyword">virtual</span> <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>) = 0;
<a name="l00407"></a>00407 <span class="comment"></span>
<a name="l00408"></a>00408 <span class="comment"> //! Create n-element disjunction</span>
<a name="l00409"></a>00409 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00410"></a>00410 <span class="comment"></span>
<a name="l00411"></a>00411 <span class="comment"> //! Create Boolean implication</span>
<a name="l00412"></a>00412 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00413"></a>00413 <span class="comment"></span>
<a name="l00414"></a>00414 <span class="comment"> //! Create left IFF right (boolean equivalence)</span>
<a name="l00415"></a>00415 <span class="comment"></span> <span class="keyword">virtual</span> <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>) = 0;
<a name="l00416"></a>00416 <span class="comment"></span>
<a name="l00417"></a>00417 <span class="comment"> //! Create an equality expression.</span>
<a name="l00418"></a>00418 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00419"></a>00419 <span class="comment"> The two children must have the same type, and cannot be of type</span>
<a name="l00420"></a>00420 <span class="comment"> Boolean.</span>
<a name="l00421"></a>00421 <span class="comment"> */</span>
<a name="l00422"></a>00422 <span class="keyword">virtual</span> <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) = 0;
<a name="l00423"></a>00423 <span class="comment"></span>
<a name="l00424"></a>00424 <span class="comment"> //! Create IF ifpart THEN thenpart ELSE elsepart ENDIF</span>
<a name="l00425"></a>00425 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00426"></a>00426 <span class="comment"> \param ifpart must be of type Boolean.</span>
<a name="l00427"></a>00427 <span class="comment"> \param thenpart and \param elsepart must have the same type, which will</span>
<a name="l00428"></a>00428 <span class="comment"> also be the type of the ite expression.</span>
<a name="l00429"></a>00429 <span class="comment"> */</span>
<a name="l00430"></a>00430 <span class="keyword">virtual</span> <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,
<a name="l00431"></a>00431 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& elsepart) = 0;
<a name="l00432"></a>00432 <span class="comment"></span>
<a name="l00433"></a>00433 <span class="comment"> /**</span>
<a name="l00434"></a>00434 <span class="comment"> * Create an expression asserting that all the children are different.</span>
<a name="l00435"></a>00435 <span class="comment"> * @param children the children to be asserted different</span>
<a name="l00436"></a>00436 <span class="comment"> */</span>
<a name="l00437"></a>00437 <span class="keyword">virtual</span> <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) = 0;
<a name="l00438"></a>00438 <span class="comment"></span>
<a name="l00439"></a>00439 <span class="comment"> /*@}*/</span> <span class="comment">// End of Core expression methods</span>
<a name="l00440"></a>00440
<a name="l00441"></a>00441 <span class="comment">/***************************************************************************/</span><span class="comment"></span>
<a name="l00442"></a>00442 <span class="comment"> /*!</span>
<a name="l00443"></a>00443 <span class="comment"> *\name User-defined (uninterpreted) function methods</span>
<a name="l00444"></a>00444 <span class="comment"> * Methods for manipulating uninterpreted function expressions</span>
<a name="l00445"></a>00445 <span class="comment"> *@{</span>
<a name="l00446"></a>00446 <span class="comment"> */</span>
<a name="l00447"></a>00447 <span class="comment">/***************************************************************************/</span>
<a name="l00448"></a>00448 <span class="comment"></span>
<a name="l00449"></a>00449 <span class="comment"> //! Create a named uninterpreted function with a given type</span>
<a name="l00450"></a>00450 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00451"></a>00451 <span class="comment"> \param name is the new function's name (as ID Expr)</span>
<a name="l00452"></a>00452 <span class="comment"> \param type is a function type ( [range -> domain] )</span>
<a name="l00453"></a>00453 <span class="comment"> */</span>
<a name="l00454"></a>00454 <span class="keyword">virtual</span> <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) = 0;
<a name="l00455"></a>00455 <span class="comment"></span>
<a name="l00456"></a>00456 <span class="comment"> //! Create a named user-defined function with a given type</span>
<a name="l00457"></a>00457 <span class="comment"></span> <span class="keyword">virtual</span> <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="l00458"></a>00458 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& def) = 0;
<a name="l00459"></a>00459 <span class="comment"></span>
<a name="l00460"></a>00460 <span class="comment"> //! Get the Op associated with a name, and its type</span>
<a name="l00461"></a>00461 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00462"></a>00462 <span class="comment"> \param name is the operator name</span>
<a name="l00463"></a>00463 <span class="comment"> \param type is where the type value is returned</span>
<a name="l00464"></a>00464 <span class="comment"></span>
<a name="l00465"></a>00465 <span class="comment"> \return an Op by the name. If there is no such Op, a NULL \</span>
<a name="l00466"></a>00466 <span class="comment"> Op is returned.</span>
<a name="l00467"></a>00467 <span class="comment"> */</span>
<a name="l00468"></a>00468 <span class="keyword">virtual</span> <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) = 0;
<a name="l00469"></a>00469 <span class="comment"></span>
<a name="l00470"></a>00470 <span class="comment"> //! Unary function application (op must be of function type)</span>
<a name="l00471"></a>00471 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00472"></a>00472 <span class="comment"></span>
<a name="l00473"></a>00473 <span class="comment"> //! Binary function application (op must be of function type)</span>
<a name="l00474"></a>00474 <span class="comment"></span> <span class="keyword">virtual</span> <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>) = 0;
<a name="l00475"></a>00475 <span class="comment"></span>
<a name="l00476"></a>00476 <span class="comment"> //! Ternary function application (op must be of function type)</span>
<a name="l00477"></a>00477 <span class="comment"></span> <span class="keyword">virtual</span> <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,
<a name="l00478"></a>00478 <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) = 0;
<a name="l00479"></a>00479 <span class="comment"></span>
<a name="l00480"></a>00480 <span class="comment"> //! n-ary function application (op must be of function type)</span>
<a name="l00481"></a>00481 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00482"></a>00482 <span class="comment"></span>
<a name="l00483"></a>00483 <span class="comment"> /*@}*/</span> <span class="comment">// End of User-defined (uninterpreted) function methods</span>
<a name="l00484"></a>00484
<a name="l00485"></a>00485 <span class="comment">/***************************************************************************/</span><span class="comment"></span>
<a name="l00486"></a>00486 <span class="comment"> /*!</span>
<a name="l00487"></a>00487 <span class="comment"> *\name Arithmetic expression methods</span>
<a name="l00488"></a>00488 <span class="comment"> * Methods for manipulating arithmetic expressions</span>
<a name="l00489"></a>00489 <span class="comment"> *</span>
<a name="l00490"></a>00490 <span class="comment"> * These functions create arithmetic expressions. The children provided</span>
<a name="l00491"></a>00491 <span class="comment"> * as arguments must be of type Real.</span>
<a name="l00492"></a>00492 <span class="comment"> *@{</span>
<a name="l00493"></a>00493 <span class="comment"> */</span>
<a name="l00494"></a>00494 <span class="comment">/***************************************************************************/</span>
<a name="l00495"></a>00495 <span class="comment"></span>
<a name="l00496"></a>00496 <span class="comment"> /*!</span>
<a name="l00497"></a>00497 <span class="comment"> * Add the pair of variables to the variable ordering for aritmetic solving.</span>
<a name="l00498"></a>00498 <span class="comment"> * Terms that are not arithmetic will be ignored.</span>
<a name="l00499"></a>00499 <span class="comment"> * \param smaller the smaller variable</span>
<a name="l00500"></a>00500 <span class="comment"> * \param bigger the bigger variable</span>
<a name="l00501"></a>00501 <span class="comment"> */</span>
<a name="l00502"></a>00502 <span class="keyword">virtual</span> <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) = 0;
<a name="l00503"></a>00503 <span class="comment"></span>
<a name="l00504"></a>00504 <span class="comment"> //! Create a rational number with numerator n and denominator d.</span>
<a name="l00505"></a>00505 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00506"></a>00506 <span class="comment"> \param n the numerator</span>
<a name="l00507"></a>00507 <span class="comment"> \param d the denominator, cannot be 0.</span>
<a name="l00508"></a>00508 <span class="comment"> */</span>
<a name="l00509"></a>00509 <span class="keyword">virtual</span> <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 = 1) = 0;
<a name="l00510"></a>00510 <span class="comment"></span>
<a name="l00511"></a>00511 <span class="comment"> //! Create a rational number with numerator n and denominator d.</span>
<a name="l00512"></a>00512 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00513"></a>00513 <span class="comment"> Here n and d are given as strings. They are converted to</span>
<a name="l00514"></a>00514 <span class="comment"> arbitrary-precision integers according to the given base.</span>
<a name="l00515"></a>00515 <span class="comment"> */</span>
<a name="l00516"></a>00516 <span class="keyword">virtual</span> <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) = 0;
<a name="l00517"></a>00517 <span class="comment"></span>
<a name="l00518"></a>00518 <span class="comment"> //! Create a rational from a single string.</span>
<a name="l00519"></a>00519 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00520"></a>00520 <span class="comment"> \param n can be a string containing an integer, a pair of integers</span>
<a name="l00521"></a>00521 <span class="comment"> "nnn/ddd", or a number in the fixed or floating point format.</span>
<a name="l00522"></a>00522 <span class="comment"> \param base is the base in which to interpret the string.</span>
<a name="l00523"></a>00523 <span class="comment"> */</span>
<a name="l00524"></a>00524 <span class="keyword">virtual</span> <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 = 10) = 0;
<a name="l00525"></a>00525 <span class="comment"></span>
<a name="l00526"></a>00526 <span class="comment"> //! Unary minus.</span>
<a name="l00527"></a>00527 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00528"></a>00528 <span class="comment"></span>
<a name="l00529"></a>00529 <span class="comment"> //! Create 2-element sum (left + right)</span>
<a name="l00530"></a>00530 <span class="comment"></span> <span class="keyword">virtual</span> <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>) = 0;
<a name="l00531"></a>00531 <span class="comment"></span>
<a name="l00532"></a>00532 <span class="comment"> //! Create n-element sum</span>
<a name="l00533"></a>00533 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00534"></a>00534 <span class="comment"></span>
<a name="l00535"></a>00535 <span class="comment"> //! Make a difference (left - right)</span>
<a name="l00536"></a>00536 <span class="comment"></span> <span class="keyword">virtual</span> <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>) = 0;
<a name="l00537"></a>00537 <span class="comment"></span>
<a name="l00538"></a>00538 <span class="comment"> //! Create a product (left * right)</span>
<a name="l00539"></a>00539 <span class="comment"></span> <span class="keyword">virtual</span> <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>) = 0;
<a name="l00540"></a>00540 <span class="comment"></span>
<a name="l00541"></a>00541 <span class="comment"> //! Create a power expression (x ^ n); n must be integer</span>
<a name="l00542"></a>00542 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00543"></a>00543 <span class="comment"></span>
<a name="l00544"></a>00544 <span class="comment"> //! Create expression x / y</span>
<a name="l00545"></a>00545 <span class="comment"></span> <span class="keyword">virtual</span> <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>& numerator, <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& denominator) = 0;
<a name="l00546"></a>00546 <span class="comment"></span>
<a name="l00547"></a>00547 <span class="comment"> //! Create (left < right)</span>
<a name="l00548"></a>00548 <span class="comment"></span> <span class="keyword">virtual</span> <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>) = 0;
<a name="l00549"></a>00549 <span class="comment"></span>
<a name="l00550"></a>00550 <span class="comment"> //! Create (left <= right)</span>
<a name="l00551"></a>00551 <span class="comment"></span> <span class="keyword">virtual</span> <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>) = 0;
<a name="l00552"></a>00552 <span class="comment"></span>
<a name="l00553"></a>00553 <span class="comment"> //! Create (left > right)</span>
<a name="l00554"></a>00554 <span class="comment"></span> <span class="keyword">virtual</span> <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>) = 0;
<a name="l00555"></a>00555 <span class="comment"></span>
<a name="l00556"></a>00556 <span class="comment"> //! Create (left >= right)</span>
<a name="l00557"></a>00557 <span class="comment"></span> <span class="keyword">virtual</span> <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>) = 0;
<a name="l00558"></a>00558 <span class="comment"></span>
<a name="l00559"></a>00559 <span class="comment"> /*@}*/</span> <span class="comment">// End of Arithmetic expression methods</span>
<a name="l00560"></a>00560
<a name="l00561"></a>00561 <span class="comment">/***************************************************************************/</span><span class="comment"></span>
<a name="l00562"></a>00562 <span class="comment"> /*!</span>
<a name="l00563"></a>00563 <span class="comment"> *\name Record expression methods</span>
<a name="l00564"></a>00564 <span class="comment"> * Methods for manipulating record expressions</span>
<a name="l00565"></a>00565 <span class="comment"> *@{</span>
<a name="l00566"></a>00566 <span class="comment"> */</span>
<a name="l00567"></a>00567 <span class="comment">/***************************************************************************/</span>
<a name="l00568"></a>00568 <span class="comment"></span>
<a name="l00569"></a>00569 <span class="comment"> //! Create a 1-element record value (# field := expr #)</span>
<a name="l00570"></a>00570 <span class="comment"></span><span class="comment"> /*! Fields will be sorted automatically */</span>
<a name="l00571"></a>00571 <span class="keyword">virtual</span> <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) = 0;
<a name="l00572"></a>00572 <span class="comment"></span>
<a name="l00573"></a>00573 <span class="comment"> //! Create a 2-element record value (# field0 := expr0, field1 := expr1 #)</span>
<a name="l00574"></a>00574 <span class="comment"></span><span class="comment"> /*! Fields will be sorted automatically */</span>
<a name="l00575"></a>00575 <span class="keyword">virtual</span> <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="l00576"></a>00576 <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) = 0;
<a name="l00577"></a>00577 <span class="comment"></span>
<a name="l00578"></a>00578 <span class="comment"> //! Create a 3-element record value (# field_i := expr_i #)</span>
<a name="l00579"></a>00579 <span class="comment"></span><span class="comment"> /*! Fields will be sorted automatically */</span>
<a name="l00580"></a>00580 <span class="keyword">virtual</span> <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="l00581"></a>00581 <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="l00582"></a>00582 <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) = 0;
<a name="l00583"></a>00583 <span class="comment"></span>
<a name="l00584"></a>00584 <span class="comment"> //! Create an n-element record value (# field_i := expr_i #)</span>
<a name="l00585"></a>00585 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00586"></a>00586 <span class="comment"> * \param fields</span>
<a name="l00587"></a>00587 <span class="comment"> * \param exprs must be the same length as fields</span>
<a name="l00588"></a>00588 <span class="comment"> *</span>
<a name="l00589"></a>00589 <span class="comment"> * Fields will be sorted automatically</span>
<a name="l00590"></a>00590 <span class="comment"> */</span>
<a name="l00591"></a>00591 <span class="keyword">virtual</span> <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="l00592"></a>00592 <span class="keyword">const</span> std::vector<Expr>& exprs) = 0;
<a name="l00593"></a>00593 <span class="comment"></span>
<a name="l00594"></a>00594 <span class="comment"> //! Create record.field (field selection)</span>
<a name="l00595"></a>00595 <span class="comment"></span><span class="comment"> /*! Create an expression representing the selection of a field from</span>
<a name="l00596"></a>00596 <span class="comment"> a record. */</span>
<a name="l00597"></a>00597 <span class="keyword">virtual</span> <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) = 0;
<a name="l00598"></a>00598 <span class="comment"></span>
<a name="l00599"></a>00599 <span class="comment"> //! Record update; equivalent to "record WITH .field := newValue"</span>
<a name="l00600"></a>00600 <span class="comment"></span><span class="comment"> /*! Notice the `.' before field in the presentation language (and</span>
<a name="l00601"></a>00601 <span class="comment"> the comment above); this is to distinguish it from datatype</span>
<a name="l00602"></a>00602 <span class="comment"> update.</span>
<a name="l00603"></a>00603 <span class="comment"> */</span>
<a name="l00604"></a>00604 <span class="keyword">virtual</span> <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="l00605"></a>00605 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& newValue) = 0;
<a name="l00606"></a>00606 <span class="comment"></span>
<a name="l00607"></a>00607 <span class="comment"> /*@}*/</span> <span class="comment">// End of Record expression methods</span>
<a name="l00608"></a>00608
<a name="l00609"></a>00609 <span class="comment">/***************************************************************************/</span><span class="comment"></span>
<a name="l00610"></a>00610 <span class="comment"> /*!</span>
<a name="l00611"></a>00611 <span class="comment"> *\name Array expression methods</span>
<a name="l00612"></a>00612 <span class="comment"> * Methods for manipulating array expressions</span>
<a name="l00613"></a>00613 <span class="comment"> *@{</span>
<a name="l00614"></a>00614 <span class="comment"> */</span>
<a name="l00615"></a>00615 <span class="comment">/***************************************************************************/</span>
<a name="l00616"></a>00616 <span class="comment"></span>
<a name="l00617"></a>00617 <span class="comment"> //! Create an expression array[index] (array access)</span>
<a name="l00618"></a>00618 <span class="comment"></span><span class="comment"> /*! Create an expression for the value of array at the given index */</span>
<a name="l00619"></a>00619 <span class="keyword">virtual</span> <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) = 0;
<a name="l00620"></a>00620 <span class="comment"></span>
<a name="l00621"></a>00621 <span class="comment"> //! Array update; equivalent to "array WITH index := newValue"</span>
<a name="l00622"></a>00622 <span class="comment"></span> <span class="keyword">virtual</span> <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,
<a name="l00623"></a>00623 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& newValue) = 0;
<a name="l00624"></a>00624 <span class="comment"></span>
<a name="l00625"></a>00625 <span class="comment"> /*@}*/</span> <span class="comment">// End of Array expression methods</span>
<a name="l00626"></a>00626
<a name="l00627"></a>00627 <span class="comment">/***************************************************************************/</span><span class="comment"></span>
<a name="l00628"></a>00628 <span class="comment"> /*!</span>
<a name="l00629"></a>00629 <span class="comment"> *\name Bitvector expression methods</span>
<a name="l00630"></a>00630 <span class="comment"> * Methods for manipulating bitvector expressions</span>
<a name="l00631"></a>00631 <span class="comment"> *@{</span>
<a name="l00632"></a>00632 <span class="comment"> */</span>
<a name="l00633"></a>00633 <span class="comment">/***************************************************************************/</span>
<a name="l00634"></a>00634
<a name="l00635"></a>00635 <span class="comment">// Bitvector constants</span>
<a name="l00636"></a>00636 <span class="comment">// From a string of digits in a given base</span>
<a name="l00637"></a>00637 <span class="keyword">virtual</span> <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 = 2) = 0;
<a name="l00638"></a>00638 <span class="comment">// From a vector of bools</span>
<a name="l00639"></a>00639 <span class="keyword">virtual</span> <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) = 0;
<a name="l00640"></a>00640 <span class="comment">// From a rational: bitvector is of length 'len', or the min. needed length when len=0.</span>
<a name="l00641"></a>00641 <span class="keyword">virtual</span> <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 = 0) = 0;
<a name="l00642"></a>00642
<a name="l00643"></a>00643 <span class="comment">// Concat and extract</span>
<a name="l00644"></a>00644 <span class="keyword">virtual</span> <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) = 0;
<a name="l00645"></a>00645 <span class="keyword">virtual</span> <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) = 0;
<a name="l00646"></a>00646 <span class="keyword">virtual</span> <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) = 0;
<a name="l00647"></a>00647
<a name="l00648"></a>00648 <span class="comment">// Bitwise Boolean operators: Negation, And, Nand, Or, Nor, Xor, Xnor</span>
<a name="l00649"></a>00649 <span class="keyword">virtual</span> <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) = 0;
<a name="l00650"></a>00650
<a name="l00651"></a>00651 <span class="keyword">virtual</span> <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) = 0;
<a name="l00652"></a>00652 <span class="keyword">virtual</span> <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) = 0;
<a name="l00653"></a>00653
<a name="l00654"></a>00654 <span class="keyword">virtual</span> <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) = 0;
<a name="l00655"></a>00655 <span class="keyword">virtual</span> <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) = 0;
<a name="l00656"></a>00656
<a name="l00657"></a>00657 <span class="keyword">virtual</span> <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) = 0;
<a name="l00658"></a>00658 <span class="keyword">virtual</span> <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) = 0;
<a name="l00659"></a>00659
<a name="l00660"></a>00660 <span class="keyword">virtual</span> <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) = 0;
<a name="l00661"></a>00661 <span class="keyword">virtual</span> <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) = 0;
<a name="l00662"></a>00662
<a name="l00663"></a>00663 <span class="keyword">virtual</span> <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) = 0;
<a name="l00664"></a>00664 <span class="keyword">virtual</span> <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) = 0;
<a name="l00665"></a>00665 <span class="keyword">virtual</span> <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) = 0;
<a name="l00666"></a>00666
<a name="l00667"></a>00667 <span class="comment">// Unsigned bitvector inequalities</span>
<a name="l00668"></a>00668 <span class="keyword">virtual</span> <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) = 0;
<a name="l00669"></a>00669 <span class="keyword">virtual</span> <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) = 0;
<a name="l00670"></a>00670
<a name="l00671"></a>00671 <span class="comment">// Signed bitvector inequalities</span>
<a name="l00672"></a>00672 <span class="keyword">virtual</span> <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) = 0;
<a name="l00673"></a>00673 <span class="keyword">virtual</span> <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) = 0;
<a name="l00674"></a>00674
<a name="l00675"></a>00675 <span class="comment">// Sign-extend t1 to a total of len bits</span>
<a name="l00676"></a>00676 <span class="keyword">virtual</span> <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) = 0;
<a name="l00677"></a>00677
<a name="l00678"></a>00678 <span class="comment">// Bitvector arithmetic: unary minus, plus, subtract, multiply</span>
<a name="l00679"></a>00679 <span class="keyword">virtual</span> <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) = 0;
<a name="l00680"></a>00680 <span class="keyword">virtual</span> <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) = 0;<span class="comment"></span>
<a name="l00681"></a>00681 <span class="comment"> //! 'numbits' is the number of bits in the result</span>
<a name="l00682"></a>00682 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00683"></a>00683 <span class="keyword">virtual</span> <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) = 0;
<a name="l00684"></a>00684 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> newBVMultExpr(<span class="keywordtype">int</span> numbits,
<a name="l00685"></a>00685 <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) = 0;
<a name="l00686"></a>00686
<a name="l00687"></a>00687 <span class="keyword">virtual</span> <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) = 0;
<a name="l00688"></a>00688 <span class="keyword">virtual</span> <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) = 0;
<a name="l00689"></a>00689 <span class="keyword">virtual</span> <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) = 0;
<a name="l00690"></a>00690 <span class="keyword">virtual</span> <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) = 0;
<a name="l00691"></a>00691 <span class="keyword">virtual</span> <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) = 0;
<a name="l00692"></a>00692
<a name="l00693"></a>00693 <span class="comment">// Left shift by r bits: result is old size + r bits</span>
<a name="l00694"></a>00694 <span class="keyword">virtual</span> <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) = 0;
<a name="l00695"></a>00695 <span class="comment">// Left shift by r bits: result is same size as t1</span>
<a name="l00696"></a>00696 <span class="keyword">virtual</span> <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) = 0;
<a name="l00697"></a>00697 <span class="comment">// Logical right shift by r bits: result is same size as t1</span>
<a name="l00698"></a>00698 <span class="keyword">virtual</span> <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) = 0;
<a name="l00699"></a>00699 <span class="comment">// Left shift with shift parameter an arbitrary bit-vector expr</span>
<a name="l00700"></a>00700 <span class="keyword">virtual</span> <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) = 0;
<a name="l00701"></a>00701 <span class="comment">// Logical right shift with shift parameter an arbitrary bit-vector expr</span>
<a name="l00702"></a>00702 <span class="keyword">virtual</span> <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) = 0;
<a name="l00703"></a>00703 <span class="comment">// Arithmetic right shift with shift parameter an arbitrary bit-vector expr</span>
<a name="l00704"></a>00704 <span class="keyword">virtual</span> <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) = 0;
<a name="l00705"></a>00705 <span class="comment">// Get value of BV Constant</span>
<a name="l00706"></a>00706 <span class="keyword">virtual</span> <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) = 0;
<a name="l00707"></a>00707 <span class="comment"></span>
<a name="l00708"></a>00708 <span class="comment"> /*@}*/</span> <span class="comment">// End of Bitvector expression methods</span>
<a name="l00709"></a>00709
<a name="l00710"></a>00710 <span class="comment">/***************************************************************************/</span><span class="comment"></span>
<a name="l00711"></a>00711 <span class="comment"> /*!</span>
<a name="l00712"></a>00712 <span class="comment"> *\name Other expression methods</span>
<a name="l00713"></a>00713 <span class="comment"> * Methods for manipulating other kinds of expressions</span>
<a name="l00714"></a>00714 <span class="comment"> *@{</span>
<a name="l00715"></a>00715 <span class="comment"> */</span>
<a name="l00716"></a>00716 <span class="comment">/***************************************************************************/</span>
<a name="l00717"></a>00717 <span class="comment"></span>
<a name="l00718"></a>00718 <span class="comment"> //! Tuple expression</span>
<a name="l00719"></a>00719 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00720"></a>00720 <span class="comment"></span>
<a name="l00721"></a>00721 <span class="comment"> //! Tuple select; equivalent to "tuple.n", where n is an numeral (e.g. tup.5)</span>
<a name="l00722"></a>00722 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00723"></a>00723 <span class="comment"></span>
<a name="l00724"></a>00724 <span class="comment"> //! Tuple update; equivalent to "tuple WITH index := newValue"</span>
<a name="l00725"></a>00725 <span class="comment"></span> <span class="keyword">virtual</span> <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,
<a name="l00726"></a>00726 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& newValue) = 0;
<a name="l00727"></a>00727 <span class="comment"></span>
<a name="l00728"></a>00728 <span class="comment"> //! Datatype constructor expression</span>
<a name="l00729"></a>00729 <span class="comment"></span> <span class="keyword">virtual</span> <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, <span class="keyword">const</span> std::vector<Expr>& args) = 0;
<a name="l00730"></a>00730 <span class="comment"></span>
<a name="l00731"></a>00731 <span class="comment"> //! Datatype selector expression</span>
<a name="l00732"></a>00732 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00733"></a>00733 <span class="comment"></span>
<a name="l00734"></a>00734 <span class="comment"> //! Datatype tester expression</span>
<a name="l00735"></a>00735 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00736"></a>00736 <span class="comment"></span>
<a name="l00737"></a>00737 <span class="comment"> //! Create a bound variable with a given name, unique ID (uid) and type</span>
<a name="l00738"></a>00738 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00739"></a>00739 <span class="comment"> \param name is the name of the variable</span>
<a name="l00740"></a>00740 <span class="comment"> \param uid is the unique ID (a string), which must be unique for</span>
<a name="l00741"></a>00741 <span class="comment"> each variable</span>
<a name="l00742"></a>00742 <span class="comment"> \param type is its type. The type cannot be a function type.</span>
<a name="l00743"></a>00743 <span class="comment"> \return an Expr representation of a new variable</span>
<a name="l00744"></a>00744 <span class="comment"> */</span>
<a name="l00745"></a>00745 <span class="keyword">virtual</span> <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,
<a name="l00746"></a>00746 <span class="keyword">const</span> std::string& uid,
<a name="l00747"></a>00747 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Type.html" title="MS C++ specific settings.">Type</a>& type) = 0;
<a name="l00748"></a>00748 <span class="comment"></span>
<a name="l00749"></a>00749 <span class="comment"> //! Universal quantifier</span>
<a name="l00750"></a>00750 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;<span class="comment"></span>
<a name="l00751"></a>00751 <span class="comment"> //! Universal quantifier with a trigger</span>
<a name="l00752"></a>00752 <span class="comment"></span> <span class="keyword">virtual</span> <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="l00753"></a>00753 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& trigger) = 0;<span class="comment"></span>
<a name="l00754"></a>00754 <span class="comment"> //! Universal quantifier with a set of triggers.</span>
<a name="l00755"></a>00755 <span class="comment"></span> <span class="keyword">virtual</span> <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="l00756"></a>00756 <span class="keyword">const</span> std::vector<Expr>& triggers) = 0;<span class="comment"></span>
<a name="l00757"></a>00757 <span class="comment"> //! Universal quantifier with a set of multi-triggers.</span>
<a name="l00758"></a>00758 <span class="comment"></span> <span class="keyword">virtual</span> <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="l00759"></a>00759 <span class="keyword">const</span> std::vector<std::vector<Expr> >& triggers) = 0;
<a name="l00760"></a>00760 <span class="comment"></span>
<a name="l00761"></a>00761 <span class="comment"> //! Set triggers for quantifier instantiation</span>
<a name="l00762"></a>00762 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00763"></a>00763 <span class="comment"> * \param e the expression for which triggers are being set.</span>
<a name="l00764"></a>00764 <span class="comment"> * \param triggers Each item in triggers is a vector of Expr containing one</span>
<a name="l00765"></a>00765 <span class="comment"> * or more patterns. A pattern is a term or Atomic predicate sub-expression</span>
<a name="l00766"></a>00766 <span class="comment"> * of e. A vector containing more than one pattern is treated as a</span>
<a name="l00767"></a>00767 <span class="comment"> * multi-trigger. Patterns will be matched in the order they occur in</span>
<a name="l00768"></a>00768 <span class="comment"> * the vector.</span>
<a name="l00769"></a>00769 <span class="comment"> */</span>
<a name="l00770"></a>00770 <span class="keyword">virtual</span> <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) = 0;<span class="comment"></span>
<a name="l00771"></a>00771 <span class="comment"> //! Set triggers for quantifier instantiation (no multi-triggers)</span>
<a name="l00772"></a>00772 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;<span class="comment"></span>
<a name="l00773"></a>00773 <span class="comment"> //! Set a single trigger for quantifier instantiation</span>
<a name="l00774"></a>00774 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;<span class="comment"></span>
<a name="l00775"></a>00775 <span class="comment"> //! Set a single multi-trigger for quantifier instantiation</span>
<a name="l00776"></a>00776 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00777"></a>00777 <span class="comment"></span>
<a name="l00778"></a>00778 <span class="comment"> //! Existential quantifier</span>
<a name="l00779"></a>00779 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00780"></a>00780 <span class="comment"></span>
<a name="l00781"></a>00781 <span class="comment"> //! Lambda-expression</span>
<a name="l00782"></a>00782 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00783"></a>00783 <span class="comment"></span>
<a name="l00784"></a>00784 <span class="comment"> //! Transitive closure of a binary predicate</span>
<a name="l00785"></a>00785 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00786"></a>00786 <span class="comment"></span>
<a name="l00787"></a>00787 <span class="comment"> //! Symbolic simulation expression</span>
<a name="l00788"></a>00788 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00789"></a>00789 <span class="comment"> * \param f is the next state function (LAMBDA-expression)</span>
<a name="l00790"></a>00790 <span class="comment"> * \param s0 is the initial state</span>
<a name="l00791"></a>00791 <span class="comment"> * \param inputs is the vector of LAMBDA-expressions representing</span>
<a name="l00792"></a>00792 <span class="comment"> * the sequences of inputs to f</span>
<a name="l00793"></a>00793 <span class="comment"> * \param n is a constant, the number of cycles to run the simulation.</span>
<a name="l00794"></a>00794 <span class="comment"> */</span>
<a name="l00795"></a>00795 <span class="keyword">virtual</span> <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="l00796"></a>00796 <span class="keyword">const</span> std::vector<Expr>& inputs,
<a name="l00797"></a>00797 <span class="keyword">const</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a>& n) = 0;
<a name="l00798"></a>00798 <span class="comment"></span>
<a name="l00799"></a>00799 <span class="comment"> /*@}*/</span> <span class="comment">// End of Other expression methods</span>
<a name="l00800"></a>00800
<a name="l00801"></a>00801 <span class="comment">/***************************************************************************/</span><span class="comment"></span>
<a name="l00802"></a>00802 <span class="comment"> /*!</span>
<a name="l00803"></a>00803 <span class="comment"> *\name Validity checking methods</span>
<a name="l00804"></a>00804 <span class="comment"> * Methods related to validity checking</span>
<a name="l00805"></a>00805 <span class="comment"> *</span>
<a name="l00806"></a>00806 <span class="comment"> * This group includes methods for asserting formulas, checking</span>
<a name="l00807"></a>00807 <span class="comment"> * validity in the given logical context, manipulating the scope</span>
<a name="l00808"></a>00808 <span class="comment"> * level of the context, etc.</span>
<a name="l00809"></a>00809 <span class="comment"> *@{</span>
<a name="l00810"></a>00810 <span class="comment"> */</span>
<a name="l00811"></a>00811 <span class="comment">/***************************************************************************/</span>
<a name="l00812"></a>00812 <span class="comment"></span>
<a name="l00813"></a>00813 <span class="comment"> //! Set the resource limit (0==unlimited, 1==exhausted).</span>
<a name="l00814"></a>00814 <span class="comment"></span><span class="comment"> /*! Currently, the limit is the total number of processed facts. */</span>
<a name="l00815"></a>00815 <span class="keyword">virtual</span> <span class="keywordtype">void</span> setResourceLimit(<span class="keywordtype">unsigned</span> limit) = 0;
<a name="l00816"></a>00816 <span class="comment"></span>
<a name="l00817"></a>00817 <span class="comment"> //! Set a time limit in tenth of a second,</span>
<a name="l00818"></a>00818 <span class="comment"></span><span class="comment"> /*! counting the cpu time used by the current process from now on.</span>
<a name="l00819"></a>00819 <span class="comment"> * Currently, when the limit is reached, cvc3 tries to quickly</span>
<a name="l00820"></a>00820 <span class="comment"> * terminate, probably with the status unknown.</span>
<a name="l00821"></a>00821 <span class="comment"> */</span>
<a name="l00822"></a>00822 <span class="keyword">virtual</span> <span class="keywordtype">void</span> setTimeLimit(<span class="keywordtype">unsigned</span> limit) = 0;
<a name="l00823"></a>00823 <span class="comment"></span>
<a name="l00824"></a>00824 <span class="comment"> //! Assert a new formula in the current context.</span>
<a name="l00825"></a>00825 <span class="comment"></span><span class="comment"> /*! This creates the assumption e |- e. The formula must have Boolean type.</span>
<a name="l00826"></a>00826 <span class="comment"> */</span>
<a name="l00827"></a>00827 <span class="keyword">virtual</span> <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) = 0;
<a name="l00828"></a>00828 <span class="comment"></span>
<a name="l00829"></a>00829 <span class="comment"> //! Register an atomic formula of interest.</span>
<a name="l00830"></a>00830 <span class="comment"></span><span class="comment"> /*! Registered atoms are tracked by the decision procedures. If one of them</span>
<a name="l00831"></a>00831 <span class="comment"> is deduced to be true or false, it is added to a list of implied literals.</span>
<a name="l00832"></a>00832 <span class="comment"> Implied literals can be retrieved with the getImpliedLiteral function */</span>
<a name="l00833"></a>00833 <span class="keyword">virtual</span> <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) = 0;
<a name="l00834"></a>00834 <span class="comment"></span>
<a name="l00835"></a>00835 <span class="comment"> //! Return next literal implied by last assertion. Null Expr if none.</span>
<a name="l00836"></a>00836 <span class="comment"></span><span class="comment"> /*! Returned literals are either registered atomic formulas or their negation</span>
<a name="l00837"></a>00837 <span class="comment"> */</span>
<a name="l00838"></a>00838 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> getImpliedLiteral() = 0;
<a name="l00839"></a>00839 <span class="comment"></span>
<a name="l00840"></a>00840 <span class="comment"> //! Simplify e with respect to the current context</span>
<a name="l00841"></a>00841 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l00842"></a>00842 <span class="comment"></span>
<a name="l00843"></a>00843 <span class="comment"> //! Check validity of e in the current context.</span>
<a name="l00844"></a>00844 <span class="comment"></span><span class="comment"> /*! If it returns VALID, the scope and context are the same</span>
<a name="l00845"></a>00845 <span class="comment"> * as when called. If it returns INVALID, the context will be one which</span>
<a name="l00846"></a>00846 <span class="comment"> * falsifies the query. If it returns UNKNOWN, the context will falsify the</span>
<a name="l00847"></a>00847 <span class="comment"> * query, but the context may be inconsistent. Finally, if it returns</span>
<a name="l00848"></a>00848 <span class="comment"> * ABORT, the context will be one which satisfies as much as possible.</span>
<a name="l00849"></a>00849 <span class="comment"> *</span>
<a name="l00850"></a>00850 <span class="comment"> * \param e is the queried formula</span>
<a name="l00851"></a>00851 <span class="comment"> */</span>
<a name="l00852"></a>00852 <span class="keyword">virtual</span> <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) = 0;
<a name="l00853"></a>00853 <span class="comment"></span>
<a name="l00854"></a>00854 <span class="comment"> //! Check satisfiability of the expr in the current context.</span>
<a name="l00855"></a>00855 <span class="comment"></span><span class="comment"> /*! Equivalent to query(!e) */</span>
<a name="l00856"></a>00856 <span class="keyword">virtual</span> <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) = 0;
<a name="l00857"></a>00857 <span class="comment"></span>
<a name="l00858"></a>00858 <span class="comment"> //! Get the next model</span>
<a name="l00859"></a>00859 <span class="comment"></span><span class="comment"> /*! This method should only be called after a query which returns</span>
<a name="l00860"></a>00860 <span class="comment"> INVALID. Its return values are as for query(). */</span>
<a name="l00861"></a>00861 <span class="keyword">virtual</span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> checkContinue() = 0;
<a name="l00862"></a>00862 <span class="comment"></span>
<a name="l00863"></a>00863 <span class="comment"> //! Restart the most recent query with e as an additional assertion.</span>
<a name="l00864"></a>00864 <span class="comment"></span><span class="comment"> /*! This method should only be called after a query which returns</span>
<a name="l00865"></a>00865 <span class="comment"> INVALID. Its return values are as for query(). */</span>
<a name="l00866"></a>00866 <span class="keyword">virtual</span> <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) = 0;
<a name="l00867"></a>00867 <span class="comment"></span>
<a name="l00868"></a>00868 <span class="comment"> //! Returns to context immediately before last invalid query.</span>
<a name="l00869"></a>00869 <span class="comment"></span><span class="comment"> /*! This method should only be called after a query which returns false.</span>
<a name="l00870"></a>00870 <span class="comment"> */</span>
<a name="l00871"></a>00871 <span class="keyword">virtual</span> <span class="keywordtype">void</span> returnFromCheck() = 0;
<a name="l00872"></a>00872 <span class="comment"></span>
<a name="l00873"></a>00873 <span class="comment"> //! Get assumptions made by the user in this and all previous contexts.</span>
<a name="l00874"></a>00874 <span class="comment"></span><span class="comment"> /*! User assumptions are created either by calls to assertFormula or by a</span>
<a name="l00875"></a>00875 <span class="comment"> * call to query. In the latter case, the negated query is added as an</span>
<a name="l00876"></a>00876 <span class="comment"> * assumption.</span>
<a name="l00877"></a>00877 <span class="comment"> * \param assumptions should be empty on entry.</span>
<a name="l00878"></a>00878 <span class="comment"> */</span>
<a name="l00879"></a>00879 <span class="keyword">virtual</span> <span class="keywordtype">void</span> getUserAssumptions(std::vector<Expr>& assumptions) = 0;
<a name="l00880"></a>00880 <span class="comment"></span>
<a name="l00881"></a>00881 <span class="comment"> //! Get assumptions made internally in this and all previous contexts.</span>
<a name="l00882"></a>00882 <span class="comment"></span><span class="comment"> /*! Internal assumptions are literals assumed by the sat solver.</span>
<a name="l00883"></a>00883 <span class="comment"> * \param assumptions should be empty on entry.</span>
<a name="l00884"></a>00884 <span class="comment"> */</span>
<a name="l00885"></a>00885 <span class="keyword">virtual</span> <span class="keywordtype">void</span> getInternalAssumptions(std::vector<Expr>& assumptions) = 0;
<a name="l00886"></a>00886 <span class="comment"></span>
<a name="l00887"></a>00887 <span class="comment"> //! Get all assumptions made in this and all previous contexts.</span>
<a name="l00888"></a>00888 <span class="comment"></span><span class="comment"> /*! \param assumptions should be empty on entry.</span>
<a name="l00889"></a>00889 <span class="comment"> */</span>
<a name="l00890"></a>00890 <span class="keyword">virtual</span> <span class="keywordtype">void</span> getAssumptions(std::vector<Expr>& assumptions) = 0;
<a name="l00891"></a>00891 <span class="comment"></span>
<a name="l00892"></a>00892 <span class="comment"> //! Returns the set of assumptions used in the proof of queried formula.</span>
<a name="l00893"></a>00893 <span class="comment"></span><span class="comment"> /*! It returns a subset of getAssumptions(). If the last query was false</span>
<a name="l00894"></a>00894 <span class="comment"> * or there has not yet been a query, it does nothing.</span>
<a name="l00895"></a>00895 <span class="comment"> * NOTE: this functionality is not supported yet</span>
<a name="l00896"></a>00896 <span class="comment"> * \param assumptions should be empty on entry.</span>
<a name="l00897"></a>00897 <span class="comment"> */</span>
<a name="l00898"></a>00898 <span class="keyword">virtual</span> <span class="keywordtype">void</span> getAssumptionsUsed(std::vector<Expr>& assumptions) = 0;
<a name="l00899"></a>00899
<a name="l00900"></a>00900 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> getProofQuery() = 0;
<a name="l00901"></a>00901
<a name="l00902"></a>00902 <span class="comment"></span>
<a name="l00903"></a>00903 <span class="comment"> //! Return the internal assumptions that make the queried formula false.</span>
<a name="l00904"></a>00904 <span class="comment"></span><span class="comment"> /*! This method should only be called after a query which returns</span>
<a name="l00905"></a>00905 <span class="comment"> false. It will try to return the simplest possible subset of</span>
<a name="l00906"></a>00906 <span class="comment"> the internal assumptions sufficient to make the queried expression</span>
<a name="l00907"></a>00907 <span class="comment"> false.</span>
<a name="l00908"></a>00908 <span class="comment"> \param assumptions should be empty on entry.</span>
<a name="l00909"></a>00909 <span class="comment"> \param inOrder if true, returns the assumptions in the order they</span>
<a name="l00910"></a>00910 <span class="comment"> were made. This is slightly more expensive than inOrder = false.</span>
<a name="l00911"></a>00911 <span class="comment"> */</span>
<a name="l00912"></a>00912 <span class="keyword">virtual</span> <span class="keywordtype">void</span> getCounterExample(std::vector<Expr>& assumptions,
<a name="l00913"></a>00913 <span class="keywordtype">bool</span> inOrder=<span class="keyword">true</span>) = 0;
<a name="l00914"></a>00914 <span class="comment"></span>
<a name="l00915"></a>00915 <span class="comment"> //! Will assign concrete values to all user created variables</span>
<a name="l00916"></a>00916 <span class="comment"></span><span class="comment"> /*! This function should only be called after a query which return false.</span>
<a name="l00917"></a>00917 <span class="comment"> */</span>
<a name="l00918"></a>00918 <span class="keyword">virtual</span> <span class="keywordtype">void</span> getConcreteModel(<a class="code" href="classCVC3_1_1ExprMap.html">ExprMap<Expr></a> & m) = 0;
<a name="l00919"></a>00919 <span class="comment"></span>
<a name="l00920"></a>00920 <span class="comment"> //! If the result of the last query was UNKNOWN try to actually build the model</span>
<a name="l00921"></a>00921 <span class="comment"> //! to verify the result.</span>
<a name="l00922"></a>00922 <span class="comment"></span><span class="comment"> /*! This function should only be called after a query which return unknown.</span>
<a name="l00923"></a>00923 <span class="comment"> */</span>
<a name="l00924"></a>00924 <span class="keyword">virtual</span> <a class="code" href="namespaceCVC3.html#a060d21b3207cc3471e24f8dbcff3498b">QueryResult</a> tryModelGeneration() = 0;
<a name="l00925"></a>00925
<a name="l00926"></a>00926 <span class="comment">//:ALEX: returns the current truth value of a formula</span>
<a name="l00927"></a>00927 <span class="comment">// returns UNKNOWN_VAL if e is not associated</span>
<a name="l00928"></a>00928 <span class="comment">// with a boolean variable in the SAT module,</span>
<a name="l00929"></a>00929 <span class="comment">// i.e. if its value can not determined without search.</span>
<a name="l00930"></a>00930 <span class="keyword">virtual</span> <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) = 0;
<a name="l00931"></a>00931 <span class="comment"></span>
<a name="l00932"></a>00932 <span class="comment"> //! Returns true if the current context is inconsistent.</span>
<a name="l00933"></a>00933 <span class="comment"></span><span class="comment"> /*! Also returns a minimal set of assertions used to determine the</span>
<a name="l00934"></a>00934 <span class="comment"> inconsistency.</span>
<a name="l00935"></a>00935 <span class="comment"> \param assumptions should be empty on entry.</span>
<a name="l00936"></a>00936 <span class="comment"> */</span>
<a name="l00937"></a>00937 <span class="keyword">virtual</span> <span class="keywordtype">bool</span> inconsistent(std::vector<Expr>& assumptions) = 0;
<a name="l00938"></a>00938 <span class="comment"></span>
<a name="l00939"></a>00939 <span class="comment"> //! Returns true if the current context is inconsistent.</span>
<a name="l00940"></a>00940 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">bool</span> inconsistent() = 0;
<a name="l00941"></a>00941 <span class="comment"></span>
<a name="l00942"></a>00942 <span class="comment"> //! Returns true if the invalid result from last query() is imprecise</span>
<a name="l00943"></a>00943 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00944"></a>00944 <span class="comment"> * Some decision procedures in CVC are incomplete (quantifier</span>
<a name="l00945"></a>00945 <span class="comment"> * elimination, non-linear arithmetic, etc.). If any incomplete</span>
<a name="l00946"></a>00946 <span class="comment"> * features were used during the last query(), and the result is</span>
<a name="l00947"></a>00947 <span class="comment"> * "invalid" (query() returns false), then this result is</span>
<a name="l00948"></a>00948 <span class="comment"> * inconclusive. It means that the system gave up the search for</span>
<a name="l00949"></a>00949 <span class="comment"> * contradiction at some point.</span>
<a name="l00950"></a>00950 <span class="comment"> */</span>
<a name="l00951"></a>00951 <span class="keyword">virtual</span> <span class="keywordtype">bool</span> incomplete() = 0;
<a name="l00952"></a>00952 <span class="comment"></span>
<a name="l00953"></a>00953 <span class="comment"> //! Returns true if the invalid result from last query() is imprecise</span>
<a name="l00954"></a>00954 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l00955"></a>00955 <span class="comment"> * \sa incomplete()</span>
<a name="l00956"></a>00956 <span class="comment"> *</span>
<a name="l00957"></a>00957 <span class="comment"> * The argument is filled with the reasons for incompleteness (they</span>
<a name="l00958"></a>00958 <span class="comment"> * are intended to be shown to the end user).</span>
<a name="l00959"></a>00959 <span class="comment"> */</span>
<a name="l00960"></a>00960 <span class="keyword">virtual</span> <span class="keywordtype">bool</span> incomplete(std::vector<std::string>& reasons) = 0;
<a name="l00961"></a>00961 <span class="comment"></span>
<a name="l00962"></a>00962 <span class="comment"> //! Returns the proof term for the last proven query</span>
<a name="l00963"></a>00963 <span class="comment"></span><span class="comment"> /*! If there has not been a successful query, it should return a NULL proof</span>
<a name="l00964"></a>00964 <span class="comment"> */</span>
<a name="l00965"></a>00965 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Proof.html">Proof</a> getProof() = 0;
<a name="l00966"></a>00966 <span class="comment"></span>
<a name="l00967"></a>00967 <span class="comment"> //! Evaluate an expression and return a concrete value in the model</span>
<a name="l00968"></a>00968 <span class="comment"></span><span class="comment"> /*! If the last query was not invalid, should return NULL expr */</span>
<a name="l00969"></a>00969 <span class="keyword">virtual</span> <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) = 0;
<a name="l00970"></a>00970 <span class="comment"></span>
<a name="l00971"></a>00971 <span class="comment"> //! Returns the list of pairs (name value) for each :named attribute.</span>
<a name="l00972"></a>00972 <span class="comment"></span><span class="comment"> /*! If the last query was not invalid, should return NULL expr */</span>
<a name="l00973"></a>00973 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> getAssignment() = 0;
<a name="l00974"></a>00974 <span class="comment"></span>
<a name="l00975"></a>00975 <span class="comment"> //! Returns the TCC of the last assumption or query</span>
<a name="l00976"></a>00976 <span class="comment"></span><span class="comment"> /*! Returns Null if no assumptions or queries were performed. */</span>
<a name="l00977"></a>00977 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> getTCC() = 0;
<a name="l00978"></a>00978 <span class="comment"></span>
<a name="l00979"></a>00979 <span class="comment"> //! Return the set of assumptions used in the proof of the last TCC</span>
<a name="l00980"></a>00980 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">void</span> getAssumptionsTCC(std::vector<Expr>& assumptions) = 0;
<a name="l00981"></a>00981 <span class="comment"></span>
<a name="l00982"></a>00982 <span class="comment"> //! Returns the proof of TCC of the last assumption or query</span>
<a name="l00983"></a>00983 <span class="comment"></span><span class="comment"> /*! Returns Null if no assumptions or queries were performed. */</span>
<a name="l00984"></a>00984 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Proof.html">Proof</a> getProofTCC() = 0;
<a name="l00985"></a>00985 <span class="comment"></span>
<a name="l00986"></a>00986 <span class="comment"> //! After successful query, return its closure |- Gamma => phi</span>
<a name="l00987"></a>00987 <span class="comment"></span><span class="comment"> /*! Turn a valid query Gamma |- phi into an implication</span>
<a name="l00988"></a>00988 <span class="comment"> * |- Gamma => phi.</span>
<a name="l00989"></a>00989 <span class="comment"> *</span>
<a name="l00990"></a>00990 <span class="comment"> * Returns Null if last query was invalid.</span>
<a name="l00991"></a>00991 <span class="comment"> */</span>
<a name="l00992"></a>00992 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Expr.html" title="Data structure of expressions in CVC3.">Expr</a> getClosure() = 0;
<a name="l00993"></a>00993 <span class="comment"></span>
<a name="l00994"></a>00994 <span class="comment"> //! Construct a proof of the query closure |- Gamma => phi</span>
<a name="l00995"></a>00995 <span class="comment"></span><span class="comment"> /*! Returns Null if last query was Invalid. */</span>
<a name="l00996"></a>00996 <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Proof.html">Proof</a> getProofClosure() = 0;
<a name="l00997"></a>00997 <span class="comment"></span>
<a name="l00998"></a>00998 <span class="comment"> /*@}*/</span> <span class="comment">// End of Validity checking methods</span>
<a name="l00999"></a>00999
<a name="l01000"></a>01000 <span class="comment">/***************************************************************************/</span><span class="comment"></span>
<a name="l01001"></a>01001 <span class="comment"> /*!</span>
<a name="l01002"></a>01002 <span class="comment"> *\name Context methods</span>
<a name="l01003"></a>01003 <span class="comment"> * Methods for manipulating contexts</span>
<a name="l01004"></a>01004 <span class="comment"> *</span>
<a name="l01005"></a>01005 <span class="comment"> * Contexts support stack-based push and pop. There are two</span>
<a name="l01006"></a>01006 <span class="comment"> * separate notions of the current context stack. stackLevel(), push(),</span>
<a name="l01007"></a>01007 <span class="comment"> * pop(), and popto() work with the user-level notion of the stack.</span>
<a name="l01008"></a>01008 <span class="comment"> *</span>
<a name="l01009"></a>01009 <span class="comment"> * scopeLevel(), pushScope(), popScope(), and poptoScope() work with</span>
<a name="l01010"></a>01010 <span class="comment"> * the internal stack which is more fine-grained than the user</span>
<a name="l01011"></a>01011 <span class="comment"> * stack.</span>
<a name="l01012"></a>01012 <span class="comment"> *</span>
<a name="l01013"></a>01013 <span class="comment"> * Do not use the scope methods unless you know what you are doing.</span>
<a name="l01014"></a>01014 <span class="comment"> * *@{</span>
<a name="l01015"></a>01015 <span class="comment"> */</span>
<a name="l01016"></a>01016 <span class="comment">/***************************************************************************/</span>
<a name="l01017"></a>01017 <span class="comment"></span>
<a name="l01018"></a>01018 <span class="comment"> //! Returns the current stack level. Initial level is 0.</span>
<a name="l01019"></a>01019 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">int</span> stackLevel() = 0;
<a name="l01020"></a>01020 <span class="comment"></span>
<a name="l01021"></a>01021 <span class="comment"> //! Checkpoint the current context and increase the scope level</span>
<a name="l01022"></a>01022 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__ExprStream__Manip.html#ga2a0348c6d3f94f2f8febc6dd0a9c3218" title="Set the indentation to the current position.">push</a>() = 0;
<a name="l01023"></a>01023 <span class="comment"></span>
<a name="l01024"></a>01024 <span class="comment"> //! Restore the current context to its state at the last checkpoint</span>
<a name="l01025"></a>01025 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">void</span> <a class="code" href="group__ExprStream__Manip.html#gaddb050a787be87116afc51791293d3be" title="Restore the indentation.">pop</a>() = 0;
<a name="l01026"></a>01026 <span class="comment"></span>
<a name="l01027"></a>01027 <span class="comment"> //! Restore the current context to the given stackLevel.</span>
<a name="l01028"></a>01028 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l01029"></a>01029 <span class="comment"> \param stackLevel should be greater than or equal to 0 and less</span>
<a name="l01030"></a>01030 <span class="comment"> than or equal to the current scope level.</span>
<a name="l01031"></a>01031 <span class="comment"> */</span>
<a name="l01032"></a>01032 <span class="keyword">virtual</span> <span class="keywordtype">void</span> popto(<span class="keywordtype">int</span> stackLevel) = 0;
<a name="l01033"></a>01033 <span class="comment"></span>
<a name="l01034"></a>01034 <span class="comment"> //! Returns the current scope level. Initially, the scope level is 1.</span>
<a name="l01035"></a>01035 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">int</span> scopeLevel() = 0;
<a name="l01036"></a>01036 <span class="comment"></span>
<a name="l01037"></a>01037 <span class="comment"> /*! @brief Checkpoint the current context and increase the</span>
<a name="l01038"></a>01038 <span class="comment"> * <strong>internal</strong> scope level. Do not use unless you</span>
<a name="l01039"></a>01039 <span class="comment"> * know what you're doing!</span>
<a name="l01040"></a>01040 <span class="comment"> */</span>
<a name="l01041"></a>01041 <span class="keyword">virtual</span> <span class="keywordtype">void</span> pushScope() = 0;
<a name="l01042"></a>01042 <span class="comment"></span>
<a name="l01043"></a>01043 <span class="comment"> /*! @brief Restore the current context to its state at the last</span>
<a name="l01044"></a>01044 <span class="comment"> * <strong>internal</strong> checkpoint. Do not use unless you know</span>
<a name="l01045"></a>01045 <span class="comment"> * what you're doing!</span>
<a name="l01046"></a>01046 <span class="comment"> */</span>
<a name="l01047"></a>01047 <span class="keyword">virtual</span> <span class="keywordtype">void</span> popScope() = 0;
<a name="l01048"></a>01048 <span class="comment"></span>
<a name="l01049"></a>01049 <span class="comment"> //! Restore the current context to the given scopeLevel.</span>
<a name="l01050"></a>01050 <span class="comment"></span><span class="comment"> /*!</span>
<a name="l01051"></a>01051 <span class="comment"> \param scopeLevel should be less than or equal to the current scope level.</span>
<a name="l01052"></a>01052 <span class="comment"></span>
<a name="l01053"></a>01053 <span class="comment"> If scopeLevel is less than 1, then the current context is reset</span>
<a name="l01054"></a>01054 <span class="comment"> and the scope level is set to 1.</span>
<a name="l01055"></a>01055 <span class="comment"> */</span>
<a name="l01056"></a>01056 <span class="keyword">virtual</span> <span class="keywordtype">void</span> poptoScope(<span class="keywordtype">int</span> scopeLevel) = 0;
<a name="l01057"></a>01057 <span class="comment"></span>
<a name="l01058"></a>01058 <span class="comment"> //! Get the current context</span>
<a name="l01059"></a>01059 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Context.html">Context</a>* getCurrentContext() = 0;
<a name="l01060"></a>01060 <span class="comment"></span>
<a name="l01061"></a>01061 <span class="comment"> //! Destroy and recreate validity checker: resets everything except for flags</span>
<a name="l01062"></a>01062 <span class="comment"></span> <span class="keyword">virtual</span> <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>() = 0;
<a name="l01063"></a>01063 <span class="comment"></span>
<a name="l01064"></a>01064 <span class="comment"> //! Add an annotation to the current script - prints annot when translating</span>
<a name="l01065"></a>01065 <span class="comment"></span> <span class="keyword">virtual</span> <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) = 0;
<a name="l01066"></a>01066 <span class="comment"></span>
<a name="l01067"></a>01067 <span class="comment"> /*@}*/</span> <span class="comment">// End of Context methods</span>
<a name="l01068"></a>01068
<a name="l01069"></a>01069 <span class="comment">/***************************************************************************/</span><span class="comment"></span>
<a name="l01070"></a>01070 <span class="comment"> /*!</span>
<a name="l01071"></a>01071 <span class="comment"> *\name Reading files</span>
<a name="l01072"></a>01072 <span class="comment"> * Methods for reading external files</span>
<a name="l01073"></a>01073 <span class="comment"> *@{</span>
<a name="l01074"></a>01074 <span class="comment"> */</span>
<a name="l01075"></a>01075 <span class="comment">/***************************************************************************/</span>
<a name="l01076"></a>01076 <span class="comment"></span>
<a name="l01077"></a>01077 <span class="comment"> //! Read and execute the commands from a file given by name ("" means stdin)</span>
<a name="l01078"></a>01078 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">void</span> loadFile(<span class="keyword">const</span> std::string& fileName,
<a name="l01079"></a>01079 <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="l01080"></a>01080 <span class="keywordtype">bool</span> interactive = <span class="keyword">false</span>,
<a name="l01081"></a>01081 <span class="keywordtype">bool</span> calledFromParser = <span class="keyword">false</span>) = 0;
<a name="l01082"></a>01082 <span class="comment"></span>
<a name="l01083"></a>01083 <span class="comment"> //! Read and execute the commands from a stream</span>
<a name="l01084"></a>01084 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">void</span> loadFile(std::istream& is,
<a name="l01085"></a>01085 <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="l01086"></a>01086 <span class="keywordtype">bool</span> interactive = <span class="keyword">false</span>) = 0;
<a name="l01087"></a>01087 <span class="comment"></span>
<a name="l01088"></a>01088 <span class="comment"> /*@}*/</span> <span class="comment">// End of methods for reading files</span>
<a name="l01089"></a>01089
<a name="l01090"></a>01090 <span class="comment">/***************************************************************************/</span><span class="comment"></span>
<a name="l01091"></a>01091 <span class="comment"> /*!</span>
<a name="l01092"></a>01092 <span class="comment"> *\name Reporting Statistics</span>
<a name="l01093"></a>01093 <span class="comment"> * Methods for collecting and reporting run-time statistics</span>
<a name="l01094"></a>01094 <span class="comment"> *@{</span>
<a name="l01095"></a>01095 <span class="comment"> */</span>
<a name="l01096"></a>01096 <span class="comment">/***************************************************************************/</span>
<a name="l01097"></a>01097 <span class="comment"></span>
<a name="l01098"></a>01098 <span class="comment"> //! Get statistics object</span>
<a name="l01099"></a>01099 <span class="comment"></span> <span class="keyword">virtual</span> <a class="code" href="classCVC3_1_1Statistics.html">Statistics</a>& getStatistics() = 0;
<a name="l01100"></a>01100 <span class="comment"></span>
<a name="l01101"></a>01101 <span class="comment"> //! Print collected statistics to stdout</span>
<a name="l01102"></a>01102 <span class="comment"></span> <span class="keyword">virtual</span> <span class="keywordtype">void</span> printStatistics() = 0;
<a name="l01103"></a>01103 <span class="comment"></span>
<a name="l01104"></a>01104 <span class="comment"> /*@}*/</span> <span class="comment">// End of Statistics Methods</span>
<a name="l01105"></a>01105
<a name="l01106"></a>01106
<a name="l01107"></a>01107 }; <span class="comment">// End of class ValidityChecker</span>
<a name="l01108"></a>01108
<a name="l01109"></a>01109 } <span class="comment">// End of namespace CVC3</span>
<a name="l01110"></a>01110
<a name="l01111"></a>01111 <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>
