<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: CVC3::Assumptions Class Reference</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
<tbody>
<tr style="height: 56px;">
<td style="padding-left: 0.5em;">
<div id="projectname">CVC3
</div>
</td>
</tr>
</tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
<div id="navrow1" class="tabs">
<ul class="tablist">
<li><a href="index.html"><span>Main Page</span></a></li>
<li><a href="pages.html"><span>Related Pages</span></a></li>
<li><a href="modules.html"><span>Modules</span></a></li>
<li><a href="namespaces.html"><span>Namespaces</span></a></li>
<li class="current"><a href="annotated.html"><span>Classes</span></a></li>
<li><a href="files.html"><span>Files</span></a></li>
</ul>
</div>
<div id="navrow2" class="tabs2">
<ul class="tablist">
<li><a href="annotated.html"><span>Class List</span></a></li>
<li><a href="classes.html"><span>Class Index</span></a></li>
<li><a href="inherits.html"><span>Class Hierarchy</span></a></li>
<li><a href="functions.html"><span>Class Members</span></a></li>
</ul>
</div>
<div id="nav-path" class="navpath">
<ul>
<li class="navelem"><a class="el" href="namespaceCVC3.html">CVC3</a></li><li class="navelem"><a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a></li> </ul>
</div>
</div><!-- top -->
<div class="header">
<div class="summary">
<a href="#nested-classes">Classes</a> |
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pub-static-methods">Static Public Member Functions</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#pri-static-methods">Static Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> |
<a href="#pri-static-attribs">Static Private Attributes</a> |
<a href="#friends">Friends</a> |
<a href="classCVC3_1_1Assumptions-members.html">List of all members</a> </div>
<div class="headertitle">
<div class="title">CVC3::Assumptions Class Reference</div> </div>
</div><!--header-->
<div class="contents">
<p><code>#include <<a class="el" href="assumptions_8h_source.html">assumptions.h</a>></code></p>
<div class="dynheader">
Collaboration diagram for CVC3::Assumptions:</div>
<div class="dyncontent">
<div class="center"><img src="classCVC3_1_1Assumptions__coll__graph.gif" border="0" usemap="#CVC3_1_1Assumptions_coll__map" alt="Collaboration graph"/></div>
<map name="CVC3_1_1Assumptions_coll__map" id="CVC3_1_1Assumptions_coll__map">
</map>
</div>
<table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="nested-classes"></a>
Classes</h2></td></tr>
<tr class="memitem:"><td class="memItemLeft" align="right" valign="top">class  </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions_1_1iterator.html">iterator</a></td></tr>
<tr class="memdesc:"><td class="mdescLeft"> </td><td class="mdescRight">Iterator for the <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a>: points to class <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>. <a href="classCVC3_1_1Assumptions_1_1iterator.html#details">More...</a><br/></td></tr>
<tr class="separator:"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-methods"></a>
Public Member Functions</h2></td></tr>
<tr class="memitem:a48495ccaf5ba3bd448712573b1cd2d51"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a48495ccaf5ba3bd448712573b1cd2d51">Assumptions</a> ()</td></tr>
<tr class="memdesc:a48495ccaf5ba3bd448712573b1cd2d51"><td class="mdescLeft"> </td><td class="mdescRight">Default constructor: no value is created. <a href="#a48495ccaf5ba3bd448712573b1cd2d51"></a><br/></td></tr>
<tr class="separator:a48495ccaf5ba3bd448712573b1cd2d51"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a816544e449b0c1d46513933a6e4dad30"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a816544e449b0c1d46513933a6e4dad30">Assumptions</a> (const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &v)</td></tr>
<tr class="memdesc:a816544e449b0c1d46513933a6e4dad30"><td class="mdescLeft"> </td><td class="mdescRight">Constructor from a vector of theorems. <a href="#a816544e449b0c1d46513933a6e4dad30"></a><br/></td></tr>
<tr class="separator:a816544e449b0c1d46513933a6e4dad30"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a057ea30fb46ac9c437fa78fc533c08d1"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a057ea30fb46ac9c437fa78fc533c08d1">Assumptions</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t)</td></tr>
<tr class="memdesc:a057ea30fb46ac9c437fa78fc533c08d1"><td class="mdescLeft"> </td><td class="mdescRight">Constructor for one theorem (common case) <a href="#a057ea30fb46ac9c437fa78fc533c08d1"></a><br/></td></tr>
<tr class="separator:a057ea30fb46ac9c437fa78fc533c08d1"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a98b093589b515e8c2e3e571f37a029c5"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a98b093589b515e8c2e3e571f37a029c5">Assumptions</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t1, const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t2)</td></tr>
<tr class="memdesc:a98b093589b515e8c2e3e571f37a029c5"><td class="mdescLeft"> </td><td class="mdescRight">Constructor for two theorems (common case) <a href="#a98b093589b515e8c2e3e571f37a029c5"></a><br/></td></tr>
<tr class="separator:a98b093589b515e8c2e3e571f37a029c5"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ae2a8910654b704d67450b80ca5caf538"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#ae2a8910654b704d67450b80ca5caf538">~Assumptions</a> ()</td></tr>
<tr class="separator:ae2a8910654b704d67450b80ca5caf538"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aaf50a6162028fb8210e5ee992712769f"><td class="memItemLeft" align="right" valign="top"> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#aaf50a6162028fb8210e5ee992712769f">Assumptions</a> (const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> &assump)</td></tr>
<tr class="separator:aaf50a6162028fb8210e5ee992712769f"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a9813efe16db162994c6b2aece8d950fb"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a9813efe16db162994c6b2aece8d950fb">operator=</a> (const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> &assump)</td></tr>
<tr class="separator:a9813efe16db162994c6b2aece8d950fb"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a519110edce1cffe144c636e404a29ff4"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a519110edce1cffe144c636e404a29ff4">add1</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t)</td></tr>
<tr class="separator:a519110edce1cffe144c636e404a29ff4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a47ed07591d1311e7fe2a0df8165a2c56"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a47ed07591d1311e7fe2a0df8165a2c56">add</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &t)</td></tr>
<tr class="separator:a47ed07591d1311e7fe2a0df8165a2c56"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab9cabf6c8400905fa896e73e2dc60010"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#ab9cabf6c8400905fa896e73e2dc60010">add</a> (const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> &a)</td></tr>
<tr class="separator:ab9cabf6c8400905fa896e73e2dc60010"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab34a834ee653d1b34f042a6202c05b13"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#ab34a834ee653d1b34f042a6202c05b13">clear</a> ()</td></tr>
<tr class="separator:ab34a834ee653d1b34f042a6202c05b13"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ad6687116416453b9120a6e97141b631d"><td class="memItemLeft" align="right" valign="top">unsigned </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#ad6687116416453b9120a6e97141b631d">size</a> () const </td></tr>
<tr class="separator:ad6687116416453b9120a6e97141b631d"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a37da34b71944a11667d6af0fbd45651b"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a37da34b71944a11667d6af0fbd45651b">empty</a> () const </td></tr>
<tr class="separator:a37da34b71944a11667d6af0fbd45651b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a247df9fd4650ca8c58b3524bb6d393f4"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a247df9fd4650ca8c58b3524bb6d393f4">getFirst</a> ()</td></tr>
<tr class="separator:a247df9fd4650ca8c58b3524bb6d393f4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ab1e6eca463ad7b98c0c2d2d31bb5d1dd"><td class="memItemLeft" align="right" valign="top">std::string </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#ab1e6eca463ad7b98c0c2d2d31bb5d1dd">toString</a> () const </td></tr>
<tr class="separator:ab1e6eca463ad7b98c0c2d2d31bb5d1dd"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:afefe1857c30806381eb0f8f7fa3d88c4"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#afefe1857c30806381eb0f8f7fa3d88c4">print</a> () const </td></tr>
<tr class="separator:afefe1857c30806381eb0f8f7fa3d88c4"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a6acec430850e6bcc418d2c65e164a520"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a6acec430850e6bcc418d2c65e164a520">operator[]</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e) const </td></tr>
<tr class="separator:a6acec430850e6bcc418d2c65e164a520"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:acafacf59eb34d2e188931a016a87c61b"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#acafacf59eb34d2e188931a016a87c61b">find</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e) const </td></tr>
<tr class="separator:acafacf59eb34d2e188931a016a87c61b"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:ac3e7d0e1796c83edf687aac063bdba06"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Assumptions_1_1iterator.html">iterator</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#ac3e7d0e1796c83edf687aac063bdba06">begin</a> () const </td></tr>
<tr class="separator:ac3e7d0e1796c83edf687aac063bdba06"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:afc875bbe97e4e2d74a2cdc824f783bfb"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Assumptions_1_1iterator.html">iterator</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#afc875bbe97e4e2d74a2cdc824f783bfb">end</a> () const </td></tr>
<tr class="separator:afc875bbe97e4e2d74a2cdc824f783bfb"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pub-static-methods"></a>
Static Public Member Functions</h2></td></tr>
<tr class="memitem:af309a39e2e013cc62b6d94c5812ad86b"><td class="memItemLeft" align="right" valign="top">static const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#af309a39e2e013cc62b6d94c5812ad86b">emptyAssump</a> ()</td></tr>
<tr class="separator:af309a39e2e013cc62b6d94c5812ad86b"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-methods"></a>
Private Member Functions</h2></td></tr>
<tr class="memitem:a9d4f8e2ab0bee667188a42f1e0ab1a98"><td class="memItemLeft" align="right" valign="top">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a9d4f8e2ab0bee667188a42f1e0ab1a98">findTheorem</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e) const </td></tr>
<tr class="separator:a9d4f8e2ab0bee667188a42f1e0ab1a98"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a72ece655220d8976c4090006eb7b0b40"><td class="memItemLeft" align="right" valign="top">void </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a72ece655220d8976c4090006eb7b0b40">add</a> (const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &thms)</td></tr>
<tr class="separator:a72ece655220d8976c4090006eb7b0b40"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-static-methods"></a>
Static Private Member Functions</h2></td></tr>
<tr class="memitem:a2fd592d43e21629722887fe7b812b8b6"><td class="memItemLeft" align="right" valign="top">static bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a2fd592d43e21629722887fe7b812b8b6">findExpr</a> (const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> &a, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &gamma)</td></tr>
<tr class="separator:a2fd592d43e21629722887fe7b812b8b6"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a2aee19965a0ec1adcd927f7c40b7064f"><td class="memItemLeft" align="right" valign="top">static bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a2aee19965a0ec1adcd927f7c40b7064f">findExprs</a> (const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> &a, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &es, std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &gamma)</td></tr>
<tr class="separator:a2aee19965a0ec1adcd927f7c40b7064f"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-attribs"></a>
Private Attributes</h2></td></tr>
<tr class="memitem:a510d7d883844766ec1fd9003bbf6d66c"><td class="memItemLeft" align="right" valign="top">std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a510d7d883844766ec1fd9003bbf6d66c">d_vector</a></td></tr>
<tr class="separator:a510d7d883844766ec1fd9003bbf6d66c"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="pri-static-attribs"></a>
Static Private Attributes</h2></td></tr>
<tr class="memitem:a660c863825a5efd492db1b93769efbfe"><td class="memItemLeft" align="right" valign="top">static <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a660c863825a5efd492db1b93769efbfe">s_empty</a></td></tr>
<tr class="separator:a660c863825a5efd492db1b93769efbfe"><td class="memSeparator" colspan="2"> </td></tr>
</table><table class="memberdecls">
<tr class="heading"><td colspan="2"><h2 class="groupheader"><a name="friends"></a>
Friends</h2></td></tr>
<tr class="memitem:ae7979a5513c61abea383d419bb38b32a"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#ae7979a5513c61abea383d419bb38b32a">operator-</a> (const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> &a, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)</td></tr>
<tr class="memdesc:ae7979a5513c61abea383d419bb38b32a"><td class="mdescLeft"> </td><td class="mdescRight">Returns all (recursive) assumptions except e. <a href="#ae7979a5513c61abea383d419bb38b32a"></a><br/></td></tr>
<tr class="separator:ae7979a5513c61abea383d419bb38b32a"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:aa5544d92518ce9547a38c6cf28f32329"><td class="memItemLeft" align="right" valign="top"><a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#aa5544d92518ce9547a38c6cf28f32329">operator-</a> (const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> &a, const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &es)</td></tr>
<tr class="memdesc:aa5544d92518ce9547a38c6cf28f32329"><td class="mdescLeft"> </td><td class="mdescRight">Returns all (recursive) assumptions except those in es. <a href="#aa5544d92518ce9547a38c6cf28f32329"></a><br/></td></tr>
<tr class="separator:aa5544d92518ce9547a38c6cf28f32329"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a00df12f458d21e3fb60a5d53b7eede49"><td class="memItemLeft" align="right" valign="top">std::ostream & </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a00df12f458d21e3fb60a5d53b7eede49">operator<<</a> (std::ostream &os, const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> &assump)</td></tr>
<tr class="separator:a00df12f458d21e3fb60a5d53b7eede49"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a80f32d3c8b6067fd975edfdb901ef404"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a80f32d3c8b6067fd975edfdb901ef404">operator==</a> (const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> &a1, const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> &a2)</td></tr>
<tr class="separator:a80f32d3c8b6067fd975edfdb901ef404"><td class="memSeparator" colspan="2"> </td></tr>
<tr class="memitem:a1f01e3a71cd2e93b28adc84ba99c46d2"><td class="memItemLeft" align="right" valign="top">bool </td><td class="memItemRight" valign="bottom"><a class="el" href="classCVC3_1_1Assumptions.html#a1f01e3a71cd2e93b28adc84ba99c46d2">operator!=</a> (const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> &a1, const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> &a2)</td></tr>
<tr class="separator:a1f01e3a71cd2e93b28adc84ba99c46d2"><td class="memSeparator" colspan="2"> </td></tr>
</table>
<a name="details" id="details"></a><h2 class="groupheader">Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00046">46</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
</div><h2 class="groupheader">Constructor & Destructor Documentation</h2>
<a class="anchor" id="a48495ccaf5ba3bd448712573b1cd2d51"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CVC3::Assumptions::Assumptions </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Default constructor: no value is created. </p>
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00067">67</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
</div>
</div>
<a class="anchor" id="a816544e449b0c1d46513933a6e4dad30"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">Assumptions::Assumptions </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>v</em></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Constructor from a vector of theorems. </p>
<p>Definition at line <a class="el" href="assumptions_8cpp_source.html#l00127">127</a> of file <a class="el" href="assumptions_8cpp_source.html">assumptions.cpp</a>.</p>
<p>References <a class="el" href="search__fast_8cpp_source.html#l01096">TheoremEq()</a>.</p>
</div>
</div>
<a class="anchor" id="a057ea30fb46ac9c437fa78fc533c08d1"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CVC3::Assumptions::Assumptions </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Constructor for one theorem (common case) </p>
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00071">71</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00048">d_vector</a>.</p>
</div>
</div>
<a class="anchor" id="a98b093589b515e8c2e3e571f37a029c5"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">Assumptions::Assumptions </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Constructor for two theorems (common case) </p>
<p>Definition at line <a class="el" href="assumptions_8cpp_source.html#l00149">149</a> of file <a class="el" href="assumptions_8cpp_source.html">assumptions.cpp</a>.</p>
<p>References <a class="el" href="expr_8cpp_source.html#l00597">CVC3::compare()</a>, <a class="el" href="assumptions_8h_source.html#l00095">empty()</a>, and <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>.</p>
</div>
</div>
<a class="anchor" id="ae2a8910654b704d67450b80ca5caf538"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CVC3::Assumptions::~Assumptions </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00076">76</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
</div>
</div>
<a class="anchor" id="aaf50a6162028fb8210e5ee992712769f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">CVC3::Assumptions::Assumptions </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td>
<td class="paramname"><em>assump</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00078">78</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Function Documentation</h2>
<a class="anchor" id="a9d4f8e2ab0bee667188a42f1e0ab1a98"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & Assumptions::findTheorem </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8cpp_source.html#l00034">34</a> of file <a class="el" href="assumptions_8cpp_source.html">assumptions.cpp</a>.</p>
<p>References <a class="el" href="expr_8cpp_source.html#l00597">CVC3::compare()</a>, <a class="el" href="assumptions_8cpp_source.html#l00034">findTheorem()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8h_source.html#l00164">CVC3::Theorem::isNull()</a>, and <a class="el" href="theorem_8cpp_source.html#l00429">CVC3::Theorem::setFlag()</a>.</p>
<p>Referenced by <a class="el" href="assumptions_8cpp_source.html#l00034">findTheorem()</a>.</p>
</div>
</div>
<a class="anchor" id="a2fd592d43e21629722887fe7b812b8b6"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool Assumptions::findExpr </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td>
<td class="paramname"><em>a</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>gamma</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">static</span><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8cpp_source.html#l00058">58</a> of file <a class="el" href="assumptions_8cpp_source.html">assumptions.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00151">begin()</a>, <a class="el" href="assumptions_8h_source.html#l00152">end()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00441">CVC3::Theorem::getCachedValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00395">CVC3::Theorem::isAssump()</a>, <a class="el" href="theorem_8cpp_source.html#l00416">CVC3::Theorem::isFlagged()</a>, <a class="el" href="theorem_8h_source.html#l00171">CVC3::Theorem::isRefl()</a>, <a class="el" href="theorem_8cpp_source.html#l00435">CVC3::Theorem::setCachedValue()</a>, and <a class="el" href="theorem_8cpp_source.html#l00429">CVC3::Theorem::setFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="a2aee19965a0ec1adcd927f7c40b7064f"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool Assumptions::findExprs </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td>
<td class="paramname"><em>a</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>es</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>gamma</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">static</span><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8cpp_source.html#l00092">92</a> of file <a class="el" href="assumptions_8cpp_source.html">assumptions.cpp</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00151">begin()</a>, <a class="el" href="assumptions_8h_source.html#l00152">end()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem_8cpp_source.html#l00441">CVC3::Theorem::getCachedValue()</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="theorem_8cpp_source.html#l00395">CVC3::Theorem::isAssump()</a>, <a class="el" href="theorem_8cpp_source.html#l00416">CVC3::Theorem::isFlagged()</a>, <a class="el" href="theorem_8h_source.html#l00171">CVC3::Theorem::isRefl()</a>, <a class="el" href="theorem_8cpp_source.html#l00435">CVC3::Theorem::setCachedValue()</a>, and <a class="el" href="theorem_8cpp_source.html#l00429">CVC3::Theorem::setFlag()</a>.</p>
</div>
</div>
<a class="anchor" id="a72ece655220d8976c4090006eb7b0b40"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void Assumptions::add </td>
<td>(</td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>thms</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8cpp_source.html#l00200">200</a> of file <a class="el" href="assumptions_8cpp_source.html">assumptions.cpp</a>.</p>
<p>References <a class="el" href="expr_8cpp_source.html#l00597">CVC3::compare()</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="debug_8h_source.html#l00406">IF_DEBUG</a>.</p>
<p>Referenced by <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03775">CVC3::ArithTheoremProducerOld::addInequalities()</a>, <a class="el" href="arith__theorem__producer3_8cpp_source.html#l02774">CVC3::ArithTheoremProducer3::clashingBounds()</a>, <a class="el" href="arith__theorem__producer_8cpp_source.html#l02865">CVC3::ArithTheoremProducer::clashingBounds()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l02976">CVC3::ArithTheoremProducerOld::clashingBounds()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00744">CVC3::SearchEngineTheoremProducer::confAndrAF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00711">CVC3::SearchEngineTheoremProducer::confAndrAT()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00834">CVC3::SearchEngineTheoremProducer::confIffr()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01059">CVC3::SearchEngineTheoremProducer::confIterIfThen()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01012">CVC3::SearchEngineTheoremProducer::confIterThenElse()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01109">CVC3::SearchEngineTheoremProducer::conflictRule()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00375">CVC3::SearchEngineTheoremProducer::cutRule()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03369">CVC3::ArithTheoremProducerOld::cycleConflict()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00085">CVC3::CommonTheoremProducer::implIntro3()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03742">CVC3::ArithTheoremProducerOld::implyDiffLogicBothBounds()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03388">CVC3::ArithTheoremProducerOld::implyEqualities()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03516">CVC3::ArithTheoremProducerOld::implyNegatedInequalityDiffLogic()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03494">CVC3::ArithTheoremProducerOld::implyWeakerInequalityDiffLogic()</a>, <a class="el" href="arith__theorem__producer__old_8cpp_source.html#l03697">CVC3::ArithTheoremProducerOld::nonLinearIneqSignSplit()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00593">CVC3::SearchEngineTheoremProducer::propAndrAT()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00651">CVC3::SearchEngineTheoremProducer::propAndrLF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00681">CVC3::SearchEngineTheoremProducer::propAndrRF()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00782">CVC3::SearchEngineTheoremProducer::propIffr()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00923">CVC3::SearchEngineTheoremProducer::propIterIfThen()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00881">CVC3::SearchEngineTheoremProducer::propIterIte()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l00970">CVC3::SearchEngineTheoremProducer::propIterThen()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00055">CVC3::CommonTheoremProducer::queryTCC()</a>, and <a class="el" href="search__theorem__producer_8cpp_source.html#l00511">CVC3::SearchEngineTheoremProducer::unitProp()</a>.</p>
</div>
</div>
<a class="anchor" id="a9813efe16db162994c6b2aece8d950fb"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a>& CVC3::Assumptions::operator= </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td>
<td class="paramname"><em>assump</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00080">80</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00048">d_vector</a>.</p>
</div>
</div>
<a class="anchor" id="af309a39e2e013cc62b6d94c5812ad86b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">static const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a>& CVC3::Assumptions::emptyAssump </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span><span class="mlabel">static</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00083">83</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00049">s_empty</a>.</p>
<p>Referenced by <a class="el" href="common__theorem__producer_8cpp_source.html#l01298">CVC3::CommonTheoremProducer::ackermann()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00245">CVC3::CoreTheoremProducer::andDistributivityRule()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00383">CVC3::CoreTheoremProducer::AndToIte()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06324">CVC3::BitvectorTheoremProducer::bitblastBVMult()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06407">CVC3::BitvectorTheoremProducer::bitblastBVPlus()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00142">CVC3::BitvectorTheoremProducer::bitBlastEqnRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01575">CVC3::BitvectorTheoremProducer::bitExtractBitwise()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01829">CVC3::BitvectorTheoremProducer::bitExtractBVASHR()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01775">CVC3::BitvectorTheoremProducer::bitExtractBVLSHR()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01141">CVC3::BitvectorTheoremProducer::bitExtractBVMult()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01256">CVC3::BitvectorTheoremProducer::bitExtractBVPlus()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01337">CVC3::BitvectorTheoremProducer::bitExtractBVPlusPreComputed()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01721">CVC3::BitvectorTheoremProducer::bitExtractBVSHL()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01017">CVC3::BitvectorTheoremProducer::bitExtractConcatenation()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00977">CVC3::BitvectorTheoremProducer::bitExtractConstant()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01074">CVC3::BitvectorTheoremProducer::bitExtractConstBVMult()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01206">CVC3::BitvectorTheoremProducer::bitExtractExtraction()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01619">CVC3::BitvectorTheoremProducer::bitExtractFixedLeftShift()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01668">CVC3::BitvectorTheoremProducer::bitExtractFixedRightShift()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01539">CVC3::BitvectorTheoremProducer::bitExtractNot()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00948">CVC3::BitvectorTheoremProducer::bitExtractRewrite()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00380">CVC3::BitvectorTheoremProducer::bitExtractSXRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02922">CVC3::BitvectorTheoremProducer::bitwiseConcat()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02842">CVC3::BitvectorTheoremProducer::bitwiseConst()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03068">CVC3::BitvectorTheoremProducer::bitwiseConstElim()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02970">CVC3::BitvectorTheoremProducer::bitwiseFlatten()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02155">CVC3::BitvectorTheoremProducer::bvashrToConcat()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00704">CVC3::BitvectorTheoremProducer::bvConstIneqn()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03503">CVC3::BitvectorTheoremProducer::bvConstMultAssocRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02107">CVC3::BitvectorTheoremProducer::bvlshrToConcat()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04619">CVC3::BitvectorTheoremProducer::BVMult_order_subterms()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03541">CVC3::BitvectorTheoremProducer::bvMultAssocRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04128">CVC3::BitvectorTheoremProducer::bvmultBVUminus()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03329">CVC3::BitvectorTheoremProducer::bvmultConst()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03615">CVC3::BitvectorTheoremProducer::bvMultDistRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01497">CVC3::BitvectorTheoremProducer::bvPlusAssociativityRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03290">CVC3::BitvectorTheoremProducer::bvplusConst()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02318">CVC3::BitvectorTheoremProducer::bvplusZeroConcatRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06462">CVC3::BitvectorTheoremProducer::bvSDivRewrite()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02135">CVC3::BitvectorTheoremProducer::bvShiftZero()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02068">CVC3::BitvectorTheoremProducer::bvshlSplit()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02033">CVC3::BitvectorTheoremProducer::bvshlToConcat()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06574">CVC3::BitvectorTheoremProducer::bvSModRewrite()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06518">CVC3::BitvectorTheoremProducer::bvSRemRewrite()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06243">CVC3::BitvectorTheoremProducer::bvUDivConst()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06272">CVC3::BitvectorTheoremProducer::bvUDivTheorem()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04011">CVC3::BitvectorTheoremProducer::bvuminusBVConst()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04038">CVC3::BitvectorTheoremProducer::bvuminusBVMult()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04174">CVC3::BitvectorTheoremProducer::bvuminusBVPlus()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04084">CVC3::BitvectorTheoremProducer::bvuminusBVUminus()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03989">CVC3::BitvectorTheoremProducer::bvuminusToBVPlus()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04105">CVC3::BitvectorTheoremProducer::bvuminusVar()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06201">CVC3::BitvectorTheoremProducer::bvURemConst()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06229">CVC3::BitvectorTheoremProducer::bvURemRewrite()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l05692">CVC3::BitvectorTheoremProducer::canonBVEQ()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04770">CVC3::BitvectorTheoremProducer::canonBVMult()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l05559">CVC3::BitvectorTheoremProducer::canonBVPlus()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l05587">CVC3::BitvectorTheoremProducer::canonBVUMinus()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03865">CVC3::BitvectorTheoremProducer::combineLikeTermsRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03195">CVC3::BitvectorTheoremProducer::concatConst()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03217">CVC3::BitvectorTheoremProducer::concatFlatten()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03239">CVC3::BitvectorTheoremProducer::concatMergeExtract()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06675">CVC3::BitvectorTheoremProducer::constEq()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02270">CVC3::BitvectorTheoremProducer::constMultToPlus()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01968">CVC3::BitvectorTheoremProducer::constWidthLeftShiftToConcat()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04882">CVC3::BitvectorTheoremProducer::distributive_rule()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00670">CVC3::CoreTheoremProducer::dummyTheorem()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01893">CVC3::BitvectorTheoremProducer::eqConst()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00580">CVC3::CommonTheoremProducer::excludedMiddle()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02532">CVC3::BitvectorTheoremProducer::extractBitwise()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04209">CVC3::BitvectorTheoremProducer::extractBVMult()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04241">CVC3::BitvectorTheoremProducer::extractBVPlus()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02465">CVC3::BitvectorTheoremProducer::extractConcat()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02365">CVC3::BitvectorTheoremProducer::extractConst()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02421">CVC3::BitvectorTheoremProducer::extractExtract()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02397">CVC3::BitvectorTheoremProducer::extractWhole()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03655">CVC3::BitvectorTheoremProducer::flattenBVPlus()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03403">CVC3::BitvectorTheoremProducer::flipBVMult()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00762">CVC3::BitvectorTheoremProducer::generalIneqn()</a>, <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>, <a class="el" href="theorem__value_8h_source.html#l00526">CVC3::RWTheoremValue::getAssumptionsRef()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00297">CVC3::SearchImplBase::getAssumptionsUsed()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00565">CVC3::CoreTheoremProducer::iffAndDistrib()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00543">CVC3::CoreTheoremProducer::iffOrDistrib()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00423">CVC3::CoreTheoremProducer::IffToIte()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00588">CVC3::CoreTheoremProducer::ifLiftUnaryRule()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00439">CVC3::CoreTheoremProducer::ImpToIte()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00264">CVC3::ArrayTheoremProducer::interchangeIndices()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04371">CVC3::BitvectorTheoremProducer::isolate_var()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02627">CVC3::BitvectorTheoremProducer::iteBVnegRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02591">CVC3::BitvectorTheoremProducer::iteExtractRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01944">CVC3::BitvectorTheoremProducer::leftShiftToConcat()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00658">CVC3::BitvectorTheoremProducer::lhsEqRhsIneqn()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03916">CVC3::BitvectorTheoremProducer::lhsMinusRhsRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04687">CVC3::BitvectorTheoremProducer::liftConcatBVMult()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04924">CVC3::BitvectorTheoremProducer::liftConcatBVPlus()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01359">CVC3::CommonTheoremProducer::liftOneITE()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00319">CVC3::ArrayTheoremProducer::liftReadIte()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04343">CVC3::BitvectorTheoremProducer::MarkNonSolvableEq()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02744">CVC3::BitvectorTheoremProducer::negBVand()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02766">CVC3::BitvectorTheoremProducer::negBVor()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02815">CVC3::BitvectorTheoremProducer::negBVxnor()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02789">CVC3::BitvectorTheoremProducer::negBVxor()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02678">CVC3::BitvectorTheoremProducer::negConcat()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02655">CVC3::BitvectorTheoremProducer::negConst()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02719">CVC3::BitvectorTheoremProducer::negElim()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02703">CVC3::BitvectorTheoremProducer::negNeg()</a>, <a class="el" href="theorem__producer_8h_source.html#l00129">CVC3::TheoremProducer::newAssumption()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00606">CVC3::BitvectorTheoremProducer::notBVEQ1Rule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00631">CVC3::BitvectorTheoremProducer::notBVLTRule()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00328">CVC3::CoreTheoremProducer::NotToIte()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06653">CVC3::BitvectorTheoremProducer::oneBVAND()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03378">CVC3::BitvectorTheoremProducer::oneCoeffBVMult()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00202">CVC3::CoreTheoremProducer::orDistributivityRule()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00345">CVC3::CoreTheoremProducer::OrToIte()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00305">CVC3::BitvectorTheoremProducer::padBVLTRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03479">CVC3::BitvectorTheoremProducer::padBVMult()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03449">CVC3::BitvectorTheoremProducer::padBVPlus()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00397">CVC3::BitvectorTheoremProducer::padBVSLTRule()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00284">CVC3::ArrayTheoremProducer::readArrayLiteral()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06109">CVC3::BitvectorTheoremProducer::repeatRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00989">CVC3::CommonTheoremProducer::rewriteAnd()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00621">CVC3::CoreTheoremProducer::rewriteAndSubterms()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02226">CVC3::BitvectorTheoremProducer::rewriteBVCOMP()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02241">CVC3::BitvectorTheoremProducer::rewriteBVSub()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00297">CVC3::CoreTheoremProducer::rewriteDistinct()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00941">CVC3::CommonTheoremProducer::rewriteIff()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00285">CVC3::CoreTheoremProducer::rewriteImplies()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00186">CVC3::CoreTheoremProducer::rewriteIteBool()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00516">CVC3::CoreTheoremProducer::rewriteIteCond()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00863">CVC3::CommonTheoremProducer::rewriteIteFalse()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00885">CVC3::CommonTheoremProducer::rewriteIteSame()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00479">CVC3::CoreTheoremProducer::rewriteIteToAnd()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00491">CVC3::CoreTheoremProducer::rewriteIteToIff()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00503">CVC3::CoreTheoremProducer::rewriteIteToImp()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00455">CVC3::CoreTheoremProducer::rewriteIteToNot()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00467">CVC3::CoreTheoremProducer::rewriteIteToOr()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00841">CVC3::CommonTheoremProducer::rewriteIteTrue()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00064">CVC3::CoreTheoremProducer::rewriteLetDecl()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02196">CVC3::BitvectorTheoremProducer::rewriteNAND()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02211">CVC3::BitvectorTheoremProducer::rewriteNOR()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00075">CVC3::CoreTheoremProducer::rewriteNotAnd()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01117">CVC3::CommonTheoremProducer::rewriteNotExists()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01078">CVC3::CommonTheoremProducer::rewriteNotFalse()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01102">CVC3::CommonTheoremProducer::rewriteNotForall()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00110">CVC3::CoreTheoremProducer::rewriteNotIff()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00123">CVC3::CoreTheoremProducer::rewriteNotIte()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01090">CVC3::CommonTheoremProducer::rewriteNotNot()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00093">CVC3::CoreTheoremProducer::rewriteNotOr()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01066">CVC3::CommonTheoremProducer::rewriteNotTrue()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01028">CVC3::CommonTheoremProducer::rewriteOr()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00647">CVC3::CoreTheoremProducer::rewriteOrSubterms()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00149">CVC3::ArrayTheoremProducer::rewriteReadWrite()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00173">CVC3::ArrayTheoremProducer::rewriteReadWrite2()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00244">CVC3::ArrayTheoremProducer::rewriteRedundantWrite2()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00168">CVC3::CommonTheoremProducer::rewriteReflexivity()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00070">CVC3::ArrayTheoremProducer::rewriteSameStore()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00221">CVC3::CommonTheoremProducer::rewriteUsingSymmetry()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00122">CVC3::ArrayTheoremProducer::rewriteWriteWrite()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02181">CVC3::BitvectorTheoremProducer::rewriteXNOR()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l02001">CVC3::BitvectorTheoremProducer::rightShiftToConcat()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06142">CVC3::BitvectorTheoremProducer::rotlRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06173">CVC3::BitvectorTheoremProducer::rotrRule()</a>, <a class="el" href="search__theorem__producer_8cpp_source.html#l01419">CVC3::SearchEngineTheoremProducer::satProof()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00437">CVC3::BitvectorTheoremProducer::signBVLTRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00339">CVC3::BitvectorTheoremProducer::signExtendRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01145">CVC3::CommonTheoremProducer::skolemizeRewrite()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01165">CVC3::CommonTheoremProducer::skolemizeRewriteVar()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06713">CVC3::BitvectorTheoremProducer::solveExtractOverlap()</a>, <a class="el" href="array__theorem__producer_8cpp_source.html#l00363">CVC3::ArrayTheoremProducer::splitOnConstants()</a>, <a class="el" href="core__theorem__producer_8cpp_source.html#l00052">CVC3::CoreTheoremProducer::typePred()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l04277">CVC3::BitvectorTheoremProducer::typePredBit()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l01202">CVC3::CommonTheoremProducer::varIntroRule()</a>, <a class="el" href="common__theorem__producer_8cpp_source.html#l00922">CVC3::CommonTheoremProducer::xorToIff()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06631">CVC3::BitvectorTheoremProducer::zeroBVOR()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l03356">CVC3::BitvectorTheoremProducer::zeroCoeffBVMult()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l06081">CVC3::BitvectorTheoremProducer::zeroExtendRule()</a>, <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l00686">CVC3::BitvectorTheoremProducer::zeroLeq()</a>, and <a class="el" href="bitvector__theorem__producer_8cpp_source.html#l01470">CVC3::BitvectorTheoremProducer::zeroPaddingRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a519110edce1cffe144c636e404a29ff4"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::Assumptions::add1 </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00085">85</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00048">d_vector</a>, and <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>.</p>
</div>
</div>
<a class="anchor" id="a47ed07591d1311e7fe2a0df8165a2c56"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Assumptions::add </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>t</em></td><td>)</td>
<td></td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8cpp_source.html#l00190">190</a> of file <a class="el" href="assumptions_8cpp_source.html">assumptions.cpp</a>.</p>
<p>References <a class="el" href="expr_8cpp_source.html#l00597">CVC3::compare()</a>, <a class="el" href="assumptions_8h_source.html#l00095">empty()</a>, and <a class="el" href="theorem_8cpp_source.html#l00385">CVC3::Theorem::getAssumptionsRef()</a>.</p>
</div>
</div>
<a class="anchor" id="ab9cabf6c8400905fa896e73e2dc60010"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::Assumptions::add </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td>
<td class="paramname"><em>a</em></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00090">90</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00090">add()</a>, and <a class="el" href="assumptions_8h_source.html#l00048">d_vector</a>.</p>
<p>Referenced by <a class="el" href="assumptions_8h_source.html#l00090">add()</a>.</p>
</div>
</div>
<a class="anchor" id="ab34a834ee653d1b34f042a6202c05b13"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">void CVC3::Assumptions::clear </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00092">92</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00048">d_vector</a>.</p>
</div>
</div>
<a class="anchor" id="ad6687116416453b9120a6e97141b631d"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">unsigned CVC3::Assumptions::size </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00094">94</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00048">d_vector</a>.</p>
<p>Referenced by <a class="el" href="theorem_8cpp_source.html#l00320">CVC3::Theorem::getAssumptionsAndCongRec()</a>, and <a class="el" href="assumptions_8h_source.html#l00098">getFirst()</a>.</p>
</div>
</div>
<a class="anchor" id="a37da34b71944a11667d6af0fbd45651b"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool CVC3::Assumptions::empty </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00095">95</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00048">d_vector</a>.</p>
<p>Referenced by <a class="el" href="assumptions_8cpp_source.html#l00190">add()</a>, <a class="el" href="assumptions_8cpp_source.html#l00149">Assumptions()</a>, <a class="el" href="vcl_8cpp_source.html#l00381">CVC3::VCL::getAssumptions()</a>, <a class="el" href="theorem__value_8h_source.html#l00444">CVC3::RWTheoremValue::init()</a>, and <a class="el" href="theorem__value_8h_source.html#l00354">CVC3::RegTheoremValue::RegTheoremValue()</a>.</p>
</div>
</div>
<a class="anchor" id="a247df9fd4650ca8c58b3524bb6d393f4"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>& CVC3::Assumptions::getFirst </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00098">98</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00048">d_vector</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, and <a class="el" href="assumptions_8h_source.html#l00094">size()</a>.</p>
</div>
</div>
<a class="anchor" id="ab1e6eca463ad7b98c0c2d2d31bb5d1dd"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">string Assumptions::toString </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8cpp_source.html#l00250">250</a> of file <a class="el" href="assumptions_8cpp_source.html">assumptions.cpp</a>.</p>
<p>Referenced by <a class="el" href="theory__quant_8cpp_source.html#l08621">CVC3::TheoryQuant::notifyInconsistent()</a>, and <a class="el" href="theorem__value_8h_source.html#l00325">CVC3::TheoremValue::toString()</a>.</p>
</div>
</div>
<a class="anchor" id="afefe1857c30806381eb0f8f7fa3d88c4"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void Assumptions::print </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8cpp_source.html#l00257">257</a> of file <a class="el" href="assumptions_8cpp_source.html">assumptions.cpp</a>.</p>
<p>References <a class="el" href="expr__stream_8cpp_source.html#l00353">std::endl()</a>.</p>
</div>
</div>
<a class="anchor" id="a6acec430850e6bcc418d2c65e164a520"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & Assumptions::operator[] </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td> const</td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8cpp_source.html#l00263">263</a> of file <a class="el" href="assumptions_8cpp_source.html">assumptions.cpp</a>.</p>
<p>References <a class="el" href="theorem_8cpp_source.html#l00422">CVC3::Theorem::clearAllFlags()</a>.</p>
</div>
</div>
<a class="anchor" id="acafacf59eb34d2e188931a016a87c61b"></a>
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & Assumptions::find </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em></td><td>)</td>
<td> const</td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8cpp_source.html#l00271">271</a> of file <a class="el" href="assumptions_8cpp_source.html">assumptions.cpp</a>.</p>
<p>References <a class="el" href="expr_8cpp_source.html#l00597">CVC3::compare()</a>.</p>
</div>
</div>
<a class="anchor" id="ac3e7d0e1796c83edf687aac063bdba06"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Assumptions_1_1iterator.html">iterator</a> CVC3::Assumptions::begin </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00151">151</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00048">d_vector</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="assumptions_8cpp_source.html#l00058">findExpr()</a>, <a class="el" href="assumptions_8cpp_source.html#l00092">findExprs()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08653">CVC3::TheoryQuant::findInstAssumptions()</a>, <a class="el" href="vcl_8cpp_source.html#l00381">CVC3::VCL::getAssumptions()</a>, <a class="el" href="theorem_8cpp_source.html#l00320">CVC3::Theorem::getAssumptionsAndCongRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00259">CVC3::Theorem::getAssumptionsRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00309">CVC3::Theorem::GetSatAssumptions()</a>, <a class="el" href="theorem_8cpp_source.html#l00288">CVC3::Theorem::GetSatAssumptionsRec()</a>, <a class="el" href="theorem__value_8h_source.html#l00444">CVC3::RWTheoremValue::init()</a>, <a class="el" href="assumptions_8cpp_source.html#l00301">CVC3::operator-()</a>, <a class="el" href="theorem_8cpp_source.html#l00516">CVC3::Theorem::recursivePrint()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>.</p>
</div>
</div>
<a class="anchor" id="afc875bbe97e4e2d74a2cdc824f783bfb"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Assumptions_1_1iterator.html">iterator</a> CVC3::Assumptions::end </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td> const</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">inline</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00152">152</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
<p>References <a class="el" href="assumptions_8h_source.html#l00048">d_vector</a>.</p>
<p>Referenced by <a class="el" href="search__fast_8cpp_source.html#l01266">CVC3::SearchEngineFast::analyzeUIPs()</a>, <a class="el" href="assumptions_8cpp_source.html#l00058">findExpr()</a>, <a class="el" href="assumptions_8cpp_source.html#l00092">findExprs()</a>, <a class="el" href="theory__quant_8cpp_source.html#l08653">CVC3::TheoryQuant::findInstAssumptions()</a>, <a class="el" href="vcl_8cpp_source.html#l00381">CVC3::VCL::getAssumptions()</a>, <a class="el" href="theorem_8cpp_source.html#l00320">CVC3::Theorem::getAssumptionsAndCongRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00259">CVC3::Theorem::getAssumptionsRec()</a>, <a class="el" href="theorem_8cpp_source.html#l00309">CVC3::Theorem::GetSatAssumptions()</a>, <a class="el" href="theorem_8cpp_source.html#l00288">CVC3::Theorem::GetSatAssumptionsRec()</a>, <a class="el" href="theorem__value_8h_source.html#l00444">CVC3::RWTheoremValue::init()</a>, <a class="el" href="assumptions_8cpp_source.html#l00301">CVC3::operator-()</a>, <a class="el" href="theorem_8cpp_source.html#l00516">CVC3::Theorem::recursivePrint()</a>, and <a class="el" href="search__fast_8cpp_source.html#l01837">CVC3::SearchEngineFast::traceConflict()</a>.</p>
</div>
</div>
<h2 class="groupheader">Friends And Related Function Documentation</h2>
<a class="anchor" id="ae7979a5513c61abea383d419bb38b32a"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> operator- </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td>
<td class="paramname"><em>a</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>e</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Returns all (recursive) assumptions except e. </p>
<p>Definition at line <a class="el" href="assumptions_8cpp_source.html#l00301">301</a> of file <a class="el" href="assumptions_8cpp_source.html">assumptions.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="aa5544d92518ce9547a38c6cf28f32329"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> operator- </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td>
<td class="paramname"><em>a</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>es</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Returns all (recursive) assumptions except those in es. </p>
<p>Definition at line <a class="el" href="assumptions_8cpp_source.html#l00311">311</a> of file <a class="el" href="assumptions_8cpp_source.html">assumptions.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a00df12f458d21e3fb60a5d53b7eede49"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::ostream& operator<< </td>
<td>(</td>
<td class="paramtype">std::ostream & </td>
<td class="paramname"><em>os</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td>
<td class="paramname"><em>assump</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8cpp_source.html#l00321">321</a> of file <a class="el" href="assumptions_8cpp_source.html">assumptions.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a80f32d3c8b6067fd975edfdb901ef404"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool operator== </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td>
<td class="paramname"><em>a1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td>
<td class="paramname"><em>a2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00166">166</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
</div>
</div>
<a class="anchor" id="a1f01e3a71cd2e93b28adc84ba99c46d2"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">bool <a class="el" href="namespaceCVC3.html#a836d1b9fc2aa13791ad282f3a2d4551e">operator!</a>= </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td>
<td class="paramname"><em>a1</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> & </td>
<td class="paramname"><em>a2</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">friend</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00168">168</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
</div>
</div>
<h2 class="groupheader">Member Data Documentation</h2>
<a class="anchor" id="a510d7d883844766ec1fd9003bbf6d66c"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname">std::vector<<a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>> CVC3::Assumptions::d_vector</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00048">48</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
<p>Referenced by <a class="el" href="assumptions_8h_source.html#l00090">add()</a>, <a class="el" href="assumptions_8h_source.html#l00085">add1()</a>, <a class="el" href="assumptions_8h_source.html#l00071">Assumptions()</a>, <a class="el" href="assumptions_8h_source.html#l00151">begin()</a>, <a class="el" href="assumptions_8h_source.html#l00092">clear()</a>, <a class="el" href="assumptions_8h_source.html#l00095">empty()</a>, <a class="el" href="assumptions_8h_source.html#l00152">end()</a>, <a class="el" href="assumptions_8h_source.html#l00098">getFirst()</a>, <a class="el" href="assumptions_8cpp_source.html#l00321">CVC3::operator<<()</a>, <a class="el" href="assumptions_8h_source.html#l00080">operator=()</a>, and <a class="el" href="assumptions_8h_source.html#l00094">size()</a>.</p>
</div>
</div>
<a class="anchor" id="a660c863825a5efd492db1b93769efbfe"></a>
<div class="memitem">
<div class="memproto">
<table class="mlabels">
<tr>
<td class="mlabels-left">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Assumptions.html">Assumptions</a> Assumptions::s_empty</td>
</tr>
</table>
</td>
<td class="mlabels-right">
<span class="mlabels"><span class="mlabel">static</span><span class="mlabel">private</span></span> </td>
</tr>
</table>
</div><div class="memdoc">
<p>Definition at line <a class="el" href="assumptions_8h_source.html#l00049">49</a> of file <a class="el" href="assumptions_8h_source.html">assumptions.h</a>.</p>
<p>Referenced by <a class="el" href="assumptions_8h_source.html#l00083">emptyAssump()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="assumptions_8h_source.html">assumptions.h</a></li>
<li><a class="el" href="assumptions_8cpp_source.html">assumptions.cpp</a></li>
</ul>
</div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:17 for CVC3 by  <a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>
