<!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: CVC3::ExprTransform Class Reference</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 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="hierarchy.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_1ExprTransform.html">ExprTransform</a> </li>
</ul>
</div>
</div>
<div class="header">
<div class="summary">
<a href="#pub-types">Public Types</a> |
<a href="#pub-methods">Public Member Functions</a> |
<a href="#pri-methods">Private Member Functions</a> |
<a href="#pri-attribs">Private Attributes</a> </div>
<div class="headertitle">
<div class="title">CVC3::ExprTransform Class Reference</div> </div>
</div>
<div class="contents">
<!-- doxytag: class="CVC3::ExprTransform" -->
<p><code>#include <<a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>></code></p>
<p><a href="classCVC3_1_1ExprTransform-members.html">List of all members.</a></p>
<h2><a name="pub-types"></a>
Public Types</h2>
<ul>
<li>typedef std::map< std::pair<br class="typebreak"/>
< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <br class="typebreak"/>
ExprTransform::CParameter ><br class="typebreak"/>
, <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > <a class="el" href="classCVC3_1_1ExprTransform.html#ac97b921ef5da4a6f60b961984dc6100a">T_name_map</a>
<li>typedef std::map< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <br class="typebreak"/>
std::set<br class="typebreak"/>
< ExprTransform::CParameter > * > <a class="el" href="classCVC3_1_1ExprTransform.html#a6c748a11c5329f22edb08e2480e4d35d">T_ack_map</a>
<li>typedef std::map< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Type.html">Type</a> > <a class="el" href="classCVC3_1_1ExprTransform.html#a0497ad8dd16d60a11af24a3aa31de0a4">T_type_map</a>
<li>typedef std::map< std::pair<br class="typebreak"/>
< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Expr.html">Expr</a> >, <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > <a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a>
<li>typedef std::map< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Type.html">Type</a> > <a class="el" href="classCVC3_1_1ExprTransform.html#ad3d45dc36c7202bdfb6ae3296fd30ca0">B_type_map</a>
<li>typedef std::map< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <br class="typebreak"/>
std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > * > <a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a>
<li>typedef std::map< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <br class="typebreak"/>
std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > * > <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a>
<li>typedef std::map< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > <a class="el" href="classCVC3_1_1ExprTransform.html#a09e5e66e7ff199ea844d4ac6b0b5312c">T_ITE_map</a>
<li>typedef std::map< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, int > <a class="el" href="classCVC3_1_1ExprTransform.html#aa10792398a3dd7f79c5cc619585a599f">B_formula_map</a>
<li>typedef std::map< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <br class="typebreak"/>
std::set< int > * > <a class="el" href="classCVC3_1_1ExprTransform.html#a778f42e55a939714cfc796f8694c21b6">NEW_formula_map</a>
<li>typedef std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > <a class="el" href="classCVC3_1_1ExprTransform.html#aa711e6099dd934a9bc975cd8ca4c19f8">T_ITE_vec</a>
</ul>
<h2><a name="pub-methods"></a>
Public Member Functions</h2>
<ul>
<li><a class="el" href="classCVC3_1_1ExprTransform.html#a7bf5ddc9291a65cc5fa55af9f3a7f338">ExprTransform</a> (<a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> *core)
<li><a class="el" href="classCVC3_1_1ExprTransform.html#ab276e3bf371d8b726c801f2f6350bc3c">~ExprTransform</a> ()
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#af362794d5fd753e8d6ac6dab185eb424">setTheoryArith</a> (<a class="el" href="classCVC3_1_1TheoryArith.html">TheoryArith</a> *arith)
<li>std::string <a class="el" href="classCVC3_1_1ExprTransform.html#ae810dc60dbc0e66fcdcd75fd883db5cc">NewBryantVar</a> (const int a, const int b)
<li>std::string <a class="el" href="classCVC3_1_1ExprTransform.html#a08a24c302c7469e845fea47c6eb1bdab">NewVar</a> (const int a, const int b)
<li><a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> <a class="el" href="classCVC3_1_1ExprTransform.html#aa18644e8ddad65f85bba79b631a0b64f">BryantNames</a> (<a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a> &generator_map, <a class="el" href="classCVC3_1_1ExprTransform.html#ad3d45dc36c7202bdfb6ae3296fd30ca0">B_type_map</a> &type_map)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1ExprTransform.html#ab56e297f7c76c3f3dd25cb0fe2128743">ITE_generator</a> (<a class="el" href="classCVC3_1_1Expr.html">Expr</a> &Orig, <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &Value, <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &Creation_map, <a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> &name_map, <a class="el" href="classCVC3_1_1ExprTransform.html#a09e5e66e7ff199ea844d4ac6b0b5312c">T_ITE_map</a> &ITE_map)
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#a9b0513038a344188cd7ba64c439f0a90">Get_ITEs</a> (<a class="el" href="classCVC3_1_1ExprTransform.html#aa10792398a3dd7f79c5cc619585a599f">B_formula_map</a> &instance_map, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &Not_replaced_set, <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &P_term_map, <a class="el" href="classCVC3_1_1ExprTransform.html#aa711e6099dd934a9bc975cd8ca4c19f8">T_ITE_vec</a> &ITE_vec, <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &Creation_map, <a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> &name_map, <a class="el" href="classCVC3_1_1ExprTransform.html#a09e5e66e7ff199ea844d4ac6b0b5312c">T_ITE_map</a> &ITE_map)
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#a108f3c577d310fc31d33cf99d45c8f83">PredConstrainTester</a> (std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &Not_replaced_set, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> &name_map, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &Pred_vec, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &Constrained_set, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &P_constrained_set, <a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a> &Constrained_map)
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#a373ee038538a33ee19d424779c5be94a">PredConstrainer</a> (std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &Not_replaced_set, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &Pred, int location, <a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> &name_map, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &SeenBefore, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &Constrained_set, <a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a> &Constrained_map, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &P_constrained_set)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1ExprTransform.html#ae3bfa06061376f6a2bbd367da8ad6fed">ConstrainedConstraints</a> (std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &Not_replaced_set, <a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a> &Constrained_map, <a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> &name_map, <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &Creation_map, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &Constrained_set, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &UnConstrained_set, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &P_constrained_set)
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#a42100ea2839cf15346eab2c8ca29b744">RemoveFunctionApps</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &orig, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &Not_replaced_set, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &Old, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &New, <a class="el" href="classCVC3_1_1ExprTransform.html#a09e5e66e7ff199ea844d4ac6b0b5312c">T_ITE_map</a> &ITE_map, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &SeenBefore)
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#a1fd5200aed59c30782723933193e17e1">GetSortedOpVec</a> (<a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &X_generator_map, <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &X_term_map, <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &P_term_map, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &P_terms, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &G_terms, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &X_terms, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &sortedOps, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &SeenBefore)
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#aad34764272dd1294745101217847c037">GetFormulaMap</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &formula_map, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &G_terms, int &size, int negations)
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#ae234191fd5e1cf389b6db0d62fa14419">GetGTerms2</a> (std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &formula_map, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &G_terms)
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#aae8f759b318fc4e16a89e188cb11da79">GetSub_vec</a> (<a class="el" href="classCVC3_1_1ExprTransform.html#aa711e6099dd934a9bc975cd8ca4c19f8">T_ITE_vec</a> &ITE_vec, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &ITE_Added)
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#a6be37560bf3a9d8fb1770ff68903bbed">GetOrderedTerms</a> (<a class="el" href="classCVC3_1_1ExprTransform.html#aa10792398a3dd7f79c5cc619585a599f">B_formula_map</a> &instance_map, <a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> &name_map, <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &X_term_map, <a class="el" href="classCVC3_1_1ExprTransform.html#aa711e6099dd934a9bc975cd8ca4c19f8">T_ITE_vec</a> &ITE_vec, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &G_terms, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &X_terms, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &Pred_vec, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &sortedOps, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &Constrained_vec, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &UnConstrained_vec, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &Constrained_set, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &UnConstrained_set, <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &G_term_map, <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &P_term_map, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &SeenBefore, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &ITE_Added)
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#a2809937bb336aef64363212c5f69d443">GetPEqs</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> &name_map, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &P_constrained_set, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &Constrained_set, <a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a> &Constrained_map, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &SeenBefore)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1ExprTransform.html#a659a92b833ed5812ba515f85198e2cf8">ConstrainedConstraints</a> (<a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a> &Constrained_map, <a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> &name_map, <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &Creation_map, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &Constrained_set, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &UnConstrained_set, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &P_constrained_set)
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#a71108e36557a2682d8e321067c161e31">BuildBryantMaps</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a> &generator_map, <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &X_generator_map, <a class="el" href="classCVC3_1_1ExprTransform.html#ad3d45dc36c7202bdfb6ae3296fd30ca0">B_type_map</a> &type_map, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &Pred_vec, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &P_terms, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &G_terms, <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &P_term_map, <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &G_term_map, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &SeenBefore, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &ITE_Added)
<li>int <a class="el" href="classCVC3_1_1ExprTransform.html#a9dcc604aebee21513a723e7a4e1a19ab">CountSubTerms</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int &counter)
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#ad905aa95541bd87e9a1c14c385e1ce8c">GetOrdering</a> (<a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &X_generator_map, <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &G_term_map, <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &P_Term_map)
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#a8562ba510c6e4f2da2c2e57c56fd1200">B_Term_Map_Deleter</a> (<a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> &Map)
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#a442486c9c71341eaa3fb69f60e8d37f1">T_generator_Map_Deleter</a> (<a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a> &Map)
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ExprTransform.html#a4d3d970b0c48c6f5973fc150a8a63d5b">dobryant</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &T)
<li><a class="el" href="classCVC3_1_1ExprTransform.html#ac97b921ef5da4a6f60b961984dc6100a">T_name_map</a> <a class="el" href="classCVC3_1_1ExprTransform.html#aac9127480414753520986d861dae7fdf">ANNames</a> (<a class="el" href="classCVC3_1_1ExprTransform.html#a6c748a11c5329f22edb08e2480e4d35d">T_ack_map</a> &ack_map, <a class="el" href="classCVC3_1_1ExprTransform.html#a0497ad8dd16d60a11af24a3aa31de0a4">T_type_map</a> &type_map)
<li><a class="el" href="classCVC3_1_1Expr.html">Expr</a> <a class="el" href="classCVC3_1_1ExprTransform.html#aa93bd2d9e0e030afe292419128fbb118">AckConstraints</a> (<a class="el" href="classCVC3_1_1ExprTransform.html#a6c748a11c5329f22edb08e2480e4d35d">T_ack_map</a> &ack_map, <a class="el" href="classCVC3_1_1ExprTransform.html#ac97b921ef5da4a6f60b961984dc6100a">T_name_map</a> &name_map)
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#a7ef78e51553a7f71acb5c9440d39e934">GetAckSwap</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &orig, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &OldAck, std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &NewAck, <a class="el" href="classCVC3_1_1ExprTransform.html#ac97b921ef5da4a6f60b961984dc6100a">T_name_map</a> &name_map, <a class="el" href="classCVC3_1_1ExprTransform.html#a6c748a11c5329f22edb08e2480e4d35d">T_ack_map</a> &ack_map, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &SeenBefore)
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#adbeeb663fe9bd8a4ffb4ef990bd41b0a">BuildMap</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1ExprTransform.html#a6c748a11c5329f22edb08e2480e4d35d">T_ack_map</a> &ack_map, <a class="el" href="classCVC3_1_1ExprTransform.html#a0497ad8dd16d60a11af24a3aa31de0a4">T_type_map</a> &type_map, std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &SeenBefore)
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ExprTransform.html#a437c0fff15f026314984701a915ea956">doackermann</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &T)
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ExprTransform.html#aafc3b026dbacc81d82b75a45b702b0a4">smartSimplify</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > &cache)
<dl class="el"><dd class="mdescRight">Simplification that avoids stack overflow. <a href="#aafc3b026dbacc81d82b75a45b702b0a4"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ExprTransform.html#a39652560061ab1172040113d9dfa25f6">preprocess</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ExprTransform.html#aeb0a695de12cfa208e39f0b5a4bdeb56">preprocess</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &thm)
<li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ExprTransform.html#ab2757afee881751f99c86499400aef44">pushNegation</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Push all negations down to the leaves. <a href="#ab2757afee881751f99c86499400aef44"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ExprTransform.html#a8a34a76b702e026c8285f18893da7dbd">pushNegationRec</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, bool neg)
<dl class="el"><dd class="mdescRight">Auxiliary recursive function for <a class="el" href="classCVC3_1_1ExprTransform.html#ab2757afee881751f99c86499400aef44" title="Push all negations down to the leaves.">pushNegation()</a>. <a href="#a8a34a76b702e026c8285f18893da7dbd"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ExprTransform.html#aa247d13841a682165edb357895d78aa3">pushNegationRec</a> (const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> &e, bool neg)
<dl class="el"><dd class="mdescRight">Its version for transitivity. <a href="#aa247d13841a682165edb357895d78aa3"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ExprTransform.html#a5daaef4e405ec8c9bb7f6e6adbde27fa">pushNegation1</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">Push negation one level down. Takes 'e' which is 'NOT e[0]'. <a href="#a5daaef4e405ec8c9bb7f6e6adbde27fa"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ExprTransform.html#ac16db941bec1cf4ecb888a8fc3f1a0e9">specialSimplify</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &cache)
<dl class="el"><dd class="mdescRight">Helper for newPP. <a href="#ac16db941bec1cf4ecb888a8fc3f1a0e9"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ExprTransform.html#a10909e40663567172bcbf45bad521055">newPP</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int &budget)
<dl class="el"><dd class="mdescRight">new preprocessing code <a href="#a10909e40663567172bcbf45bad521055"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ExprTransform.html#a5817a5d8a33b01904fa7e06aa91061bb">newPPrec</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, int &budget)
<dl class="el"><dd class="mdescRight">main new preprocessing code <a href="#a5817a5d8a33b01904fa7e06aa91061bb"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ExprTransform.html#ad18b9697ac34575a40f106e48cfef5b4">simplifyWithCare</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e)
<dl class="el"><dd class="mdescRight">ITE simplification from Burch paper. <a href="#ad18b9697ac34575a40f106e48cfef5b4"></a><br/></dl></ul>
<h2><a name="pri-methods"></a>
Private Member Functions</h2>
<ul>
<li>void <a class="el" href="classCVC3_1_1ExprTransform.html#ad12aee56d7dd01276af2d993ce4676c9">updateQueue</a> (<a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > * > &queue, const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, const std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > &careSet)
<dl class="el"><dd class="mdescRight">Helper for simplifyWithCare. <a href="#ad12aee56d7dd01276af2d993ce4676c9"></a><br/></dl><li><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> <a class="el" href="classCVC3_1_1ExprTransform.html#ae1f3a46b2e09495bb5afe3ac46f23c2b">substitute</a> (const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> &e, <a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &substTable, <a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > &cache)
<dl class="el"><dd class="mdescRight">Helper for simplifyWithCare. <a href="#ae1f3a46b2e09495bb5afe3ac46f23c2b"></a><br/></dl></ul>
<h2><a name="pri-attribs"></a>
Private Attributes</h2>
<ul>
<li><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> * <a class="el" href="classCVC3_1_1ExprTransform.html#adf66a811cae797e64ae8ff25e922766a">d_core</a>
<li><a class="el" href="classCVC3_1_1TheoryArith.html">TheoryArith</a> * <a class="el" href="classCVC3_1_1ExprTransform.html#a741b9541234b906a8b74845e4c4d3c51">d_theoryArith</a>
<li><a class="el" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a> * <a class="el" href="classCVC3_1_1ExprTransform.html#aeea6bcb414f95c53d846ad7c684b1a5d">d_commonRules</a>
<li><a class="el" href="classCVC3_1_1CoreProofRules.html">CoreProofRules</a> * <a class="el" href="classCVC3_1_1ExprTransform.html#ae6bdbc5df7bd412e0594650d7ef02cc4">d_rules</a>
<li><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > <a class="el" href="classCVC3_1_1ExprTransform.html#a986331240196633d2d639867eb2b2850">d_pushNegCache</a>
<dl class="el"><dd class="mdescRight">Cache for <a class="el" href="classCVC3_1_1ExprTransform.html#ab2757afee881751f99c86499400aef44" title="Push all negations down to the leaves.">pushNegation()</a> <a href="#a986331240196633d2d639867eb2b2850"></a><br/></dl><li><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > <a class="el" href="classCVC3_1_1ExprTransform.html#a574575f8c65c604d6904c4654f2e48d6">d_newPPCache</a>
<dl class="el"><dd class="mdescRight">Cache for newPP. <a href="#a574575f8c65c604d6904c4654f2e48d6"></a><br/></dl><li>int <a class="el" href="classCVC3_1_1ExprTransform.html#a4228c9a8ee02c424c35bbd4bf3733cb8">d_budgetLimit</a>
<dl class="el"><dd class="mdescRight">Budget limit for newPP. <a href="#a4228c9a8ee02c424c35bbd4bf3733cb8"></a><br/></dl></ul>
<hr/><a name="details" id="details"></a><h2>Detailed Description</h2>
<div class="textblock">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00035">35</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
</div><hr/><h2>Member Typedef Documentation</h2>
<a class="anchor" id="ac97b921ef5da4a6f60b961984dc6100a"></a><!-- doxytag: member="CVC3::ExprTransform::T_name_map" ref="ac97b921ef5da4a6f60b961984dc6100a" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef std::map< std::pair< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, ExprTransform::CParameter >, <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > <a class="el" href="classCVC3_1_1ExprTransform.html#ac97b921ef5da4a6f60b961984dc6100a">CVC3::ExprTransform::T_name_map</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00057">57</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
</div>
</div>
<a class="anchor" id="a6c748a11c5329f22edb08e2480e4d35d"></a><!-- doxytag: member="CVC3::ExprTransform::T_ack_map" ref="a6c748a11c5329f22edb08e2480e4d35d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef std::map< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, std::set< ExprTransform::CParameter >* > <a class="el" href="classCVC3_1_1ExprTransform.html#a6c748a11c5329f22edb08e2480e4d35d">CVC3::ExprTransform::T_ack_map</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00063">63</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
</div>
</div>
<a class="anchor" id="a0497ad8dd16d60a11af24a3aa31de0a4"></a><!-- doxytag: member="CVC3::ExprTransform::T_type_map" ref="a0497ad8dd16d60a11af24a3aa31de0a4" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef std::map< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Type.html">Type</a>> <a class="el" href="classCVC3_1_1ExprTransform.html#a0497ad8dd16d60a11af24a3aa31de0a4">CVC3::ExprTransform::T_type_map</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00064">64</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
</div>
</div>
<a class="anchor" id="afd51977fd7d11cb567f22d5be92ef8b2"></a><!-- doxytag: member="CVC3::ExprTransform::B_name_map" ref="afd51977fd7d11cb567f22d5be92ef8b2" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef std::map< std::pair< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Expr.html">Expr</a>>, <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > <a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">CVC3::ExprTransform::B_name_map</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00065">65</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
</div>
</div>
<a class="anchor" id="ad3d45dc36c7202bdfb6ae3296fd30ca0"></a><!-- doxytag: member="CVC3::ExprTransform::B_type_map" ref="ad3d45dc36c7202bdfb6ae3296fd30ca0" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef std::map<<a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Type.html">Type</a>> <a class="el" href="classCVC3_1_1ExprTransform.html#ad3d45dc36c7202bdfb6ae3296fd30ca0">CVC3::ExprTransform::B_type_map</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00066">66</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
</div>
</div>
<a class="anchor" id="ae3037a0875b13d617c86cb543c1d4c30"></a><!-- doxytag: member="CVC3::ExprTransform::T_generator_map" ref="ae3037a0875b13d617c86cb543c1d4c30" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef std::map< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, std::set<<a class="el" href="classCVC3_1_1Expr.html">Expr</a>>*> <a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">CVC3::ExprTransform::T_generator_map</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00067">67</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
</div>
</div>
<a class="anchor" id="a473dadfb4e1638fd294871ce1c065eab"></a><!-- doxytag: member="CVC3::ExprTransform::B_Term_map" ref="a473dadfb4e1638fd294871ce1c065eab" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef std::map<<a class="el" href="classCVC3_1_1Expr.html">Expr</a>, std::vector<<a class="el" href="classCVC3_1_1Expr.html">Expr</a>>*> <a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">CVC3::ExprTransform::B_Term_map</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00068">68</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
</div>
</div>
<a class="anchor" id="a09e5e66e7ff199ea844d4ac6b0b5312c"></a><!-- doxytag: member="CVC3::ExprTransform::T_ITE_map" ref="a09e5e66e7ff199ea844d4ac6b0b5312c" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef std::map< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, <a class="el" href="classCVC3_1_1Expr.html">Expr</a>> <a class="el" href="classCVC3_1_1ExprTransform.html#a09e5e66e7ff199ea844d4ac6b0b5312c">CVC3::ExprTransform::T_ITE_map</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00069">69</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
</div>
</div>
<a class="anchor" id="aa10792398a3dd7f79c5cc619585a599f"></a><!-- doxytag: member="CVC3::ExprTransform::B_formula_map" ref="aa10792398a3dd7f79c5cc619585a599f" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef std::map< <a class="el" href="classCVC3_1_1Expr.html">Expr</a>, int> <a class="el" href="classCVC3_1_1ExprTransform.html#aa10792398a3dd7f79c5cc619585a599f">CVC3::ExprTransform::B_formula_map</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00070">70</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
</div>
</div>
<a class="anchor" id="a778f42e55a939714cfc796f8694c21b6"></a><!-- doxytag: member="CVC3::ExprTransform::NEW_formula_map" ref="a778f42e55a939714cfc796f8694c21b6" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef std::map<<a class="el" href="classCVC3_1_1Expr.html">Expr</a>, std::set<int>*> <a class="el" href="classCVC3_1_1ExprTransform.html#a778f42e55a939714cfc796f8694c21b6">CVC3::ExprTransform::NEW_formula_map</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00071">71</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
</div>
</div>
<a class="anchor" id="aa711e6099dd934a9bc975cd8ca4c19f8"></a><!-- doxytag: member="CVC3::ExprTransform::T_ITE_vec" ref="aa711e6099dd934a9bc975cd8ca4c19f8" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">typedef std::vector<<a class="el" href="classCVC3_1_1Expr.html">Expr</a>> <a class="el" href="classCVC3_1_1ExprTransform.html#aa711e6099dd934a9bc975cd8ca4c19f8">CVC3::ExprTransform::T_ITE_vec</a></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00072">72</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
</div>
</div>
<hr/><h2>Constructor & Destructor Documentation</h2>
<a class="anchor" id="a7bf5ddc9291a65cc5fa55af9f3a7f338"></a><!-- doxytag: member="CVC3::ExprTransform::ExprTransform" ref="a7bf5ddc9291a65cc5fa55af9f3a7f338" args="(TheoryCore *core)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">ExprTransform::ExprTransform </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a> * </td>
<td class="paramname"><em>core</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8cpp_source.html#l00034">34</a> of file <a class="el" href="expr__transform_8cpp_source.html">expr_transform.cpp</a>.</p>
<p>References <a class="el" href="expr__transform_8h_source.html#l00039">d_commonRules</a>, <a class="el" href="expr__transform_8h_source.html#l00037">d_core</a>, <a class="el" href="expr__transform_8h_source.html#l00040">d_rules</a>, <a class="el" href="theory_8h_source.html#l00096">CVC3::Theory::getCommonRules()</a>, and <a class="el" href="theory__core_8h_source.html#l00353">CVC3::TheoryCore::getCoreRules()</a>.</p>
</div>
</div>
<a class="anchor" id="ab276e3bf371d8b726c801f2f6350bc3c"></a><!-- doxytag: member="CVC3::ExprTransform::~ExprTransform" ref="ab276e3bf371d8b726c801f2f6350bc3c" args="()" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">CVC3::ExprTransform::~ExprTransform </td>
<td>(</td>
<td class="paramname"></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00051">51</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
</div>
</div>
<hr/><h2>Member Function Documentation</h2>
<a class="anchor" id="af362794d5fd753e8d6ac6dab185eb424"></a><!-- doxytag: member="CVC3::ExprTransform::setTheoryArith" ref="af362794d5fd753e8d6ac6dab185eb424" args="(TheoryArith *arith)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprTransform::setTheoryArith </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1TheoryArith.html">TheoryArith</a> * </td>
<td class="paramname"><em>arith</em></td><td>)</td>
<td><code> [inline]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00053">53</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
<p>References <a class="el" href="expr__transform_8h_source.html#l00038">d_theoryArith</a>.</p>
</div>
</div>
<a class="anchor" id="ae810dc60dbc0e66fcdcd75fd883db5cc"></a><!-- doxytag: member="CVC3::ExprTransform::NewBryantVar" ref="ae810dc60dbc0e66fcdcd75fd883db5cc" args="(const int a, const int b)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string ExprTransform::NewBryantVar </td>
<td>(</td>
<td class="paramtype">const int </td>
<td class="paramname"><em>a</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const int </td>
<td class="paramname"><em>b</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00025">25</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a08a24c302c7469e845fea47c6eb1bdab"></a><!-- doxytag: member="CVC3::ExprTransform::NewVar" ref="a08a24c302c7469e845fea47c6eb1bdab" args="(const int a, const int b)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">std::string CVC3::ExprTransform::NewVar </td>
<td>(</td>
<td class="paramtype">const int </td>
<td class="paramname"><em>a</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">const int </td>
<td class="paramname"><em>b</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
</div>
</div>
<a class="anchor" id="aa18644e8ddad65f85bba79b631a0b64f"></a><!-- doxytag: member="CVC3::ExprTransform::BryantNames" ref="aa18644e8ddad65f85bba79b631a0b64f" args="(T_generator_map &generator_map, B_type_map &type_map)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">ExprTransform::B_name_map</a> ExprTransform::BryantNames </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a> & </td>
<td class="paramname"><em>generator_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#ad3d45dc36c7202bdfb6ae3296fd30ca0">B_type_map</a> & </td>
<td class="paramname"><em>type_map</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00036">36</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="ab56e297f7c76c3f3dd25cb0fe2128743"></a><!-- doxytag: member="CVC3::ExprTransform::ITE_generator" ref="ab56e297f7c76c3f3dd25cb0fe2128743" args="(Expr &Orig, Expr &Value, B_Term_map &Creation_map, B_name_map &name_map, T_ITE_map &ITE_map)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> ExprTransform::ITE_generator </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>Orig</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>Value</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>Creation_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> & </td>
<td class="paramname"><em>name_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a09e5e66e7ff199ea844d4ac6b0b5312c">T_ITE_map</a> & </td>
<td class="paramname"><em>ITE_map</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00110">110</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00941">CVC3::Expr::andExpr()</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8h_source.html#l00929">CVC3::Expr::eqExpr()</a>, <a class="el" href="expr_8h_source.html#l01191">CVC3::Expr::getOpExpr()</a>, <a class="el" href="expr_8h_source.html#l01223">CVC3::Expr::isNull()</a>, and <a class="el" href="expr_8h_source.html#l00961">CVC3::Expr::iteExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="a9b0513038a344188cd7ba64c439f0a90"></a><!-- doxytag: member="CVC3::ExprTransform::Get_ITEs" ref="a9b0513038a344188cd7ba64c439f0a90" args="(B_formula_map &instance_map, std::set< Expr > &Not_replaced_set, B_Term_map &P_term_map, T_ITE_vec &ITE_vec, B_Term_map &Creation_map, B_name_map &name_map, T_ITE_map &ITE_map)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprTransform::Get_ITEs </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#aa10792398a3dd7f79c5cc619585a599f">B_formula_map</a> & </td>
<td class="paramname"><em>instance_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>Not_replaced_set</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>P_term_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#aa711e6099dd934a9bc975cd8ca4c19f8">T_ITE_vec</a> & </td>
<td class="paramname"><em>ITE_vec</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>Creation_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> & </td>
<td class="paramname"><em>name_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a09e5e66e7ff199ea844d4ac6b0b5312c">T_ITE_map</a> & </td>
<td class="paramname"><em>ITE_map</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00149">149</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
<p>References <a class="el" href="bryant_8cpp_source.html#l00012">LIMIT</a>.</p>
</div>
</div>
<a class="anchor" id="a108f3c577d310fc31d33cf99d45c8f83"></a><!-- doxytag: member="CVC3::ExprTransform::PredConstrainTester" ref="a108f3c577d310fc31d33cf99d45c8f83" args="(std::set< Expr > &Not_replaced_set, const Expr &e, B_name_map &name_map, std::vector< Expr > &Pred_vec, std::set< Expr > &Constrained_set, std::set< Expr > &P_constrained_set, T_generator_map &Constrained_map)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprTransform::PredConstrainTester </td>
<td>(</td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>Not_replaced_set</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"><a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> & </td>
<td class="paramname"><em>name_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>Pred_vec</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>Constrained_set</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>P_constrained_set</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a> & </td>
<td class="paramname"><em>Constrained_map</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00094">94</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a373ee038538a33ee19d424779c5be94a"></a><!-- doxytag: member="CVC3::ExprTransform::PredConstrainer" ref="a373ee038538a33ee19d424779c5be94a" args="(std::set< Expr > &Not_replaced_set, const Expr &e, const Expr &Pred, int location, B_name_map &name_map, std::set< Expr > &SeenBefore, std::set< Expr > &Constrained_set, T_generator_map &Constrained_map, std::set< Expr > &P_constrained_set)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprTransform::PredConstrainer </td>
<td>(</td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>Not_replaced_set</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">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>Pred</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>location</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> & </td>
<td class="paramname"><em>name_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>SeenBefore</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>Constrained_set</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a> & </td>
<td class="paramname"><em>Constrained_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>P_constrained_set</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00055">55</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8h_source.html#l01217">CVC3::Expr::end()</a>, <a class="el" href="expr_8h_source.html#l00929">CVC3::Expr::eqExpr()</a>, <a class="el" href="expr_8h_source.html#l01191">CVC3::Expr::getOpExpr()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, <a class="el" href="expr_8h_source.html#l01021">CVC3::Expr::isTerm()</a>, <a class="el" href="expr_8h_source.html#l00933">CVC3::Expr::notExpr()</a>, and <a class="el" href="kinds_8h_source.html#l00088">UFUNC</a>.</p>
</div>
</div>
<a class="anchor" id="ae3bfa06061376f6a2bbd367da8ad6fed"></a><!-- doxytag: member="CVC3::ExprTransform::ConstrainedConstraints" ref="ae3bfa06061376f6a2bbd367da8ad6fed" args="(std::set< Expr > &Not_replaced_set, T_generator_map &Constrained_map, B_name_map &name_map, B_Term_map &Creation_map, std::set< Expr > &Constrained_set, std::set< Expr > &UnConstrained_set, std::set< Expr > &P_constrained_set)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> ExprTransform::ConstrainedConstraints </td>
<td>(</td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>Not_replaced_set</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a> & </td>
<td class="paramname"><em>Constrained_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> & </td>
<td class="paramname"><em>name_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>Creation_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>Constrained_set</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>UnConstrained_set</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>P_constrained_set</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00442">442</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00941">CVC3::Expr::andExpr()</a>, <a class="el" href="expr_8h_source.html#l01211">CVC3::Expr::begin()</a>, <a class="el" href="expr_8h_source.html#l00929">CVC3::Expr::eqExpr()</a>, and <a class="el" href="expr_8h_source.html#l00933">CVC3::Expr::notExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="a42100ea2839cf15346eab2c8ca29b744"></a><!-- doxytag: member="CVC3::ExprTransform::RemoveFunctionApps" ref="a42100ea2839cf15346eab2c8ca29b744" args="(const Expr &orig, std::set< Expr > &Not_replaced_set, std::vector< Expr > &Old, std::vector< Expr > &New, T_ITE_map &ITE_map, std::set< Expr > &SeenBefore)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprTransform::RemoveFunctionApps </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>orig</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>Not_replaced_set</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>Old</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>New</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a09e5e66e7ff199ea844d4ac6b0b5312c">T_ITE_map</a> & </td>
<td class="paramname"><em>ITE_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>SeenBefore</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00185">185</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, and <a class="el" href="kinds_8h_source.html#l00088">UFUNC</a>.</p>
</div>
</div>
<a class="anchor" id="a1fd5200aed59c30782723933193e17e1"></a><!-- doxytag: member="CVC3::ExprTransform::GetSortedOpVec" ref="a1fd5200aed59c30782723933193e17e1" args="(B_Term_map &X_generator_map, B_Term_map &X_term_map, B_Term_map &P_term_map, std::set< Expr > &P_terms, std::set< Expr > &G_terms, std::set< Expr > &X_terms, std::vector< Expr > &sortedOps, std::set< Expr > &SeenBefore)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprTransform::GetSortedOpVec </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>X_generator_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>X_term_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>P_term_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>P_terms</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>G_terms</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>X_terms</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>sortedOps</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>SeenBefore</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00199">199</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="aad34764272dd1294745101217847c037"></a><!-- doxytag: member="CVC3::ExprTransform::GetFormulaMap" ref="aad34764272dd1294745101217847c037" args="(const Expr &e, std::set< Expr > &formula_map, std::set< Expr > &G_terms, int &size, int negations)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprTransform::GetFormulaMap </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::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>formula_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>G_terms</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int & </td>
<td class="paramname"><em>size</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">int </td>
<td class="paramname"><em>negations</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00252">252</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8h_source.html#l00419">CVC3::Expr::isEq()</a>, and <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>.</p>
</div>
</div>
<a class="anchor" id="ae234191fd5e1cf389b6db0d62fa14419"></a><!-- doxytag: member="CVC3::ExprTransform::GetGTerms2" ref="ae234191fd5e1cf389b6db0d62fa14419" args="(std::set< Expr > &formula_map, std::set< Expr > &G_terms)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprTransform::GetGTerms2 </td>
<td>(</td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>formula_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>G_terms</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00262">262</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="aae8f759b318fc4e16a89e188cb11da79"></a><!-- doxytag: member="CVC3::ExprTransform::GetSub_vec" ref="aae8f759b318fc4e16a89e188cb11da79" args="(T_ITE_vec &ITE_vec, const Expr &e, std::set< Expr > &ITE_Added)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprTransform::GetSub_vec </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#aa711e6099dd934a9bc975cd8ca4c19f8">T_ITE_vec</a> & </td>
<td class="paramname"><em>ITE_vec</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::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>ITE_Added</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00271">271</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, and <a class="el" href="expr_8h_source.html#l01021">CVC3::Expr::isTerm()</a>.</p>
</div>
</div>
<a class="anchor" id="a6be37560bf3a9d8fb1770ff68903bbed"></a><!-- doxytag: member="CVC3::ExprTransform::GetOrderedTerms" ref="a6be37560bf3a9d8fb1770ff68903bbed" args="(B_formula_map &instance_map, B_name_map &name_map, B_Term_map &X_term_map, T_ITE_vec &ITE_vec, std::set< Expr > &G_terms, std::set< Expr > &X_terms, std::vector< Expr > &Pred_vec, std::vector< Expr > &sortedOps, std::vector< Expr > &Constrained_vec, std::vector< Expr > &UnConstrained_vec, std::set< Expr > &Constrained_set, std::set< Expr > &UnConstrained_set, B_Term_map &G_term_map, B_Term_map &P_term_map, std::set< Expr > &SeenBefore, std::set< Expr > &ITE_Added)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprTransform::GetOrderedTerms </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#aa10792398a3dd7f79c5cc619585a599f">B_formula_map</a> & </td>
<td class="paramname"><em>instance_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> & </td>
<td class="paramname"><em>name_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>X_term_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#aa711e6099dd934a9bc975cd8ca4c19f8">T_ITE_vec</a> & </td>
<td class="paramname"><em>ITE_vec</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>G_terms</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>X_terms</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>Pred_vec</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>sortedOps</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>Constrained_vec</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>UnConstrained_vec</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>Constrained_set</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>UnConstrained_set</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>G_term_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>P_term_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>SeenBefore</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>ITE_Added</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00281">281</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a2809937bb336aef64363212c5f69d443"></a><!-- doxytag: member="CVC3::ExprTransform::GetPEqs" ref="a2809937bb336aef64363212c5f69d443" args="(const Expr &e, B_name_map &name_map, std::set< Expr > &P_constrained_set, std::set< Expr > &Constrained_set, T_generator_map &Constrained_map, std::set< Expr > &SeenBefore)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprTransform::GetPEqs </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"><a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> & </td>
<td class="paramname"><em>name_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>P_constrained_set</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>Constrained_set</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a> & </td>
<td class="paramname"><em>Constrained_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>SeenBefore</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00401">401</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8h_source.html#l00929">CVC3::Expr::eqExpr()</a>, <a class="el" href="expr_8h_source.html#l00419">CVC3::Expr::isEq()</a>, and <a class="el" href="expr_8h_source.html#l00933">CVC3::Expr::notExpr()</a>.</p>
</div>
</div>
<a class="anchor" id="a659a92b833ed5812ba515f85198e2cf8"></a><!-- doxytag: member="CVC3::ExprTransform::ConstrainedConstraints" ref="a659a92b833ed5812ba515f85198e2cf8" args="(T_generator_map &Constrained_map, B_name_map &name_map, B_Term_map &Creation_map, std::set< Expr > &Constrained_set, std::set< Expr > &UnConstrained_set, std::set< Expr > &P_constrained_set)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> CVC3::ExprTransform::ConstrainedConstraints </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a> & </td>
<td class="paramname"><em>Constrained_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#afd51977fd7d11cb567f22d5be92ef8b2">B_name_map</a> & </td>
<td class="paramname"><em>name_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>Creation_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>Constrained_set</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>UnConstrained_set</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>P_constrained_set</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
</div>
</div>
<a class="anchor" id="a71108e36557a2682d8e321067c161e31"></a><!-- doxytag: member="CVC3::ExprTransform::BuildBryantMaps" ref="a71108e36557a2682d8e321067c161e31" args="(const Expr &e, T_generator_map &generator_map, B_Term_map &X_generator_map, B_type_map &type_map, std::vector< Expr > &Pred_vec, std::set< Expr > &P_terms, std::set< Expr > &G_terms, B_Term_map &P_term_map, B_Term_map &G_term_map, std::set< Expr > &SeenBefore, std::set< Expr > &ITE_Added)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprTransform::BuildBryantMaps </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"><a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a> & </td>
<td class="paramname"><em>generator_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>X_generator_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#ad3d45dc36c7202bdfb6ae3296fd30ca0">B_type_map</a> & </td>
<td class="paramname"><em>type_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>Pred_vec</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>P_terms</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>G_terms</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>P_term_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>G_term_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>SeenBefore</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>ITE_Added</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00342">342</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8h_source.html#l01191">CVC3::Expr::getOpExpr()</a>, <a class="el" href="expr_8h_source.html#l01196">CVC3::Expr::getOpKind()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="expr_8h_source.html#l01014">CVC3::Expr::isApply()</a>, <a class="el" href="expr_8h_source.html#l01021">CVC3::Expr::isTerm()</a>, <a class="el" href="expr_8h_source.html#l01005">CVC3::Expr::isVar()</a>, and <a class="el" href="kinds_8h_source.html#l00088">UFUNC</a>.</p>
</div>
</div>
<a class="anchor" id="a9dcc604aebee21513a723e7a4e1a19ab"></a><!-- doxytag: member="CVC3::ExprTransform::CountSubTerms" ref="a9dcc604aebee21513a723e7a4e1a19ab" args="(const Expr &e, int &counter)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int ExprTransform::CountSubTerms </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">int & </td>
<td class="paramname"><em>counter</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00014">14</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>.</p>
</div>
</div>
<a class="anchor" id="ad905aa95541bd87e9a1c14c385e1ce8c"></a><!-- doxytag: member="CVC3::ExprTransform::GetOrdering" ref="ad905aa95541bd87e9a1c14c385e1ce8c" args="(B_Term_map &X_generator_map, B_Term_map &G_term_map, B_Term_map &P_Term_map)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprTransform::GetOrdering </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>X_generator_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>G_term_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>P_Term_map</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00493">493</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a8562ba510c6e4f2da2c2e57c56fd1200"></a><!-- doxytag: member="CVC3::ExprTransform::B_Term_Map_Deleter" ref="a8562ba510c6e4f2da2c2e57c56fd1200" args="(B_Term_map &Map)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprTransform::B_Term_Map_Deleter </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a473dadfb4e1638fd294871ce1c065eab">B_Term_map</a> & </td>
<td class="paramname"><em>Map</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00563">563</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a442486c9c71341eaa3fb69f60e8d37f1"></a><!-- doxytag: member="CVC3::ExprTransform::T_generator_Map_Deleter" ref="a442486c9c71341eaa3fb69f60e8d37f1" args="(T_generator_map &Map)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprTransform::T_generator_Map_Deleter </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#ae3037a0875b13d617c86cb543c1d4c30">T_generator_map</a> & </td>
<td class="paramname"><em>Map</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="bryant_8cpp_source.html#l00568">568</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
</div>
</div>
<a class="anchor" id="a4d3d970b0c48c6f5973fc150a8a63d5b"></a><!-- doxytag: member="CVC3::ExprTransform::dobryant" ref="a4d3d970b0c48c6f5973fc150a8a63d5b" args="(const Expr &T)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> ExprTransform::dobryant </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</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="bryant_8cpp_source.html#l00573">573</a> of file <a class="el" href="bryant_8cpp_source.html">bryant.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l00965">CVC3::Expr::iffExpr()</a>, <a class="el" href="expr_8h_source.html#l00969">CVC3::Expr::impExpr()</a>, <a class="el" href="bryant_8cpp_source.html#l00012">LIMIT</a>, <a class="el" href="expr_8h_source.html#l00933">CVC3::Expr::notExpr()</a>, and <a class="el" href="expr_8cpp_source.html#l00178">CVC3::Expr::substExpr()</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00079">preprocess()</a>.</p>
</div>
</div>
<a class="anchor" id="aac9127480414753520986d861dae7fdf"></a><!-- doxytag: member="CVC3::ExprTransform::ANNames" ref="aac9127480414753520986d861dae7fdf" args="(T_ack_map &ack_map, T_type_map &type_map)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprTransform.html#ac97b921ef5da4a6f60b961984dc6100a">T_name_map</a> CVC3::ExprTransform::ANNames </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a6c748a11c5329f22edb08e2480e4d35d">T_ack_map</a> & </td>
<td class="paramname"><em>ack_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a0497ad8dd16d60a11af24a3aa31de0a4">T_type_map</a> & </td>
<td class="paramname"><em>type_map</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
</div>
</div>
<a class="anchor" id="aa93bd2d9e0e030afe292419128fbb118"></a><!-- doxytag: member="CVC3::ExprTransform::AckConstraints" ref="aa93bd2d9e0e030afe292419128fbb118" args="(T_ack_map &ack_map, T_name_map &name_map)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Expr.html">Expr</a> CVC3::ExprTransform::AckConstraints </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a6c748a11c5329f22edb08e2480e4d35d">T_ack_map</a> & </td>
<td class="paramname"><em>ack_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#ac97b921ef5da4a6f60b961984dc6100a">T_name_map</a> & </td>
<td class="paramname"><em>name_map</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
</div>
</div>
<a class="anchor" id="a7ef78e51553a7f71acb5c9440d39e934"></a><!-- doxytag: member="CVC3::ExprTransform::GetAckSwap" ref="a7ef78e51553a7f71acb5c9440d39e934" args="(const Expr &orig, std::vector< Expr > &OldAck, std::vector< Expr > &NewAck, T_name_map &name_map, T_ack_map &ack_map, std::set< Expr > &SeenBefore)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprTransform::GetAckSwap </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>orig</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>OldAck</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::vector< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>NewAck</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#ac97b921ef5da4a6f60b961984dc6100a">T_name_map</a> & </td>
<td class="paramname"><em>name_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a6c748a11c5329f22edb08e2480e4d35d">T_ack_map</a> & </td>
<td class="paramname"><em>ack_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>SeenBefore</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
</div>
</div>
<a class="anchor" id="adbeeb663fe9bd8a4ffb4ef990bd41b0a"></a><!-- doxytag: member="CVC3::ExprTransform::BuildMap" ref="adbeeb663fe9bd8a4ffb4ef990bd41b0a" args="(const Expr &e, T_ack_map &ack_map, T_type_map &type_map, std::set< Expr > &SeenBefore)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void CVC3::ExprTransform::BuildMap </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"><a class="el" href="classCVC3_1_1ExprTransform.html#a6c748a11c5329f22edb08e2480e4d35d">T_ack_map</a> & </td>
<td class="paramname"><em>ack_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprTransform.html#a0497ad8dd16d60a11af24a3aa31de0a4">T_type_map</a> & </td>
<td class="paramname"><em>type_map</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>SeenBefore</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
</div>
</div>
<a class="anchor" id="a437c0fff15f026314984701a915ea956"></a><!-- doxytag: member="CVC3::ExprTransform::doackermann" ref="a437c0fff15f026314984701a915ea956" args="(const Expr &T)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> CVC3::ExprTransform::doackermann </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Expr.html">Expr</a> & </td>
<td class="paramname"><em>T</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
</div>
</div>
<a class="anchor" id="aafc3b026dbacc81d82b75a45b702b0a4"></a><!-- doxytag: member="CVC3::ExprTransform::smartSimplify" ref="aafc3b026dbacc81d82b75a45b702b0a4" args="(const Expr &e, ExprMap< bool > &cache)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> ExprTransform::smartSimplify </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"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< bool > & </td>
<td class="paramname"><em>cache</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Simplification that avoids stack overflow. </p>
<p>Stack overflow is avoided by traversing the expression to depths that are multiples of 5000 until the bottom is reached. Then, simplification is done bottom-up. </p>
<p>Definition at line <a class="el" href="expr__transform_8cpp_source.html#l00042">42</a> of file <a class="el" href="expr__transform_8cpp_source.html">expr_transform.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr__transform_8h_source.html#l00037">d_core</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="expr_8h_source.html#l01232">CVC3::Expr::hasFind()</a>, <a class="el" href="theory__core_8cpp_source.html#l00184">CVC3::TheoryCore::simplify()</a>, and <a class="el" href="expr_8h_source.html#l01294">CVC3::Expr::validSimpCache()</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00079">preprocess()</a>.</p>
</div>
</div>
<a class="anchor" id="a39652560061ab1172040113d9dfa25f6"></a><!-- doxytag: member="CVC3::ExprTransform::preprocess" ref="a39652560061ab1172040113d9dfa25f6" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> ExprTransform::preprocess </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></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8cpp_source.html#l00079">79</a> of file <a class="el" href="expr__transform_8cpp_source.html">expr_transform.cpp</a>.</p>
<p>References <a class="el" href="theory__core_8cpp_source.html#l00857">CVC3::TheoryCore::callTheoryPreprocess()</a>, <a class="el" href="theory__core_8h_source.html#l00366">CVC3::TheoryCore::clearInPP()</a>, <a class="el" href="expr__transform_8h_source.html#l00047">d_budgetLimit</a>, <a class="el" href="expr__transform_8h_source.html#l00039">d_commonRules</a>, <a class="el" href="expr__transform_8h_source.html#l00037">d_core</a>, <a class="el" href="bryant_8cpp_source.html#l00573">dobryant()</a>, <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, <a class="el" href="theory__core_8h_source.html#l00350">CVC3::TheoryCore::getFlags()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr__manager_8h_source.html#l00341">CVC3::ExprManager::invalidateSimpCache()</a>, <a class="el" href="theorem_8h_source.html#l00171">CVC3::Theorem::isRefl()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00282">newPP()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00127">pushNegation()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">CVC3::CommonProofRules::reflexivityRule()</a>, <a class="el" href="theory__core_8h_source.html#l00365">CVC3::TheoryCore::setInPP()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00476">simplifyWithCare()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00042">smartSimplify()</a>, and <a class="el" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a">CVC3::CommonProofRules::transitivityRule()</a>.</p>
<p>Referenced by <a class="el" href="search__simple_8cpp_source.html#l00165">CVC3::SearchSimple::checkValidInternal()</a>, <a class="el" href="search__fast_8cpp_source.html#l01697">CVC3::SearchEngineFast::checkValidInternal()</a>, <a class="el" href="theory__core_8cpp_source.html#l04320">CVC3::TheoryCore::getAssignment()</a>, <a class="el" href="theory__core_8cpp_source.html#l04333">CVC3::TheoryCore::getValue()</a>, <a class="el" href="search__impl__base_8cpp_source.html#l00141">CVC3::SearchImplBase::newUserAssumption()</a>, <a class="el" href="search__sat_8cpp_source.html#l01064">CVC3::SearchSat::newUserAssumptionInt()</a>, and <a class="el" href="expr__transform_8cpp_source.html#l00120">preprocess()</a>.</p>
</div>
</div>
<a class="anchor" id="aeb0a695de12cfa208e39f0b5a4bdeb56"></a><!-- doxytag: member="CVC3::ExprTransform::preprocess" ref="aeb0a695de12cfa208e39f0b5a4bdeb56" args="(const Theorem &thm)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> ExprTransform::preprocess </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>thm</em></td><td>)</td>
<td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8cpp_source.html#l00120">120</a> of file <a class="el" href="expr__transform_8cpp_source.html">expr_transform.cpp</a>.</p>
<p>References <a class="el" href="expr__transform_8h_source.html#l00039">d_commonRules</a>, <a class="el" href="theorem_8cpp_source.html#l00230">CVC3::Theorem::getExpr()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">CVC3::CommonProofRules::iffMP()</a>, and <a class="el" href="expr__transform_8cpp_source.html#l00079">preprocess()</a>.</p>
</div>
</div>
<a class="anchor" id="ab2757afee881751f99c86499400aef44"></a><!-- doxytag: member="CVC3::ExprTransform::pushNegation" ref="ab2757afee881751f99c86499400aef44" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> ExprTransform::pushNegation </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></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Push all negations down to the leaves. </p>
<p>Definition at line <a class="el" href="expr__transform_8cpp_source.html#l00127">127</a> of file <a class="el" href="expr__transform_8cpp_source.html">expr_transform.cpp</a>.</p>
<p>References <a class="el" href="expr__map_8h_source.html#l00175">CVC3::ExprMap< Data >::clear()</a>, <a class="el" href="expr__transform_8h_source.html#l00039">d_commonRules</a>, <a class="el" href="expr__transform_8h_source.html#l00043">d_pushNegCache</a>, <a class="el" href="expr_8h_source.html#l01021">CVC3::Expr::isTerm()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00141">pushNegationRec()</a>, and <a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">CVC3::CommonProofRules::reflexivityRule()</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00079">preprocess()</a>.</p>
</div>
</div>
<a class="anchor" id="a8a34a76b702e026c8285f18893da7dbd"></a><!-- doxytag: member="CVC3::ExprTransform::pushNegationRec" ref="a8a34a76b702e026c8285f18893da7dbd" args="(const Expr &e, bool neg)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> ExprTransform::pushNegationRec </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">bool </td>
<td class="paramname"><em>neg</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Auxiliary recursive function for <a class="el" href="classCVC3_1_1ExprTransform.html#ab2757afee881751f99c86499400aef44" title="Push all negations down to the leaves.">pushNegation()</a>. </p>
<p>Definition at line <a class="el" href="expr__transform_8cpp_source.html#l00141">141</a> of file <a class="el" href="expr__transform_8cpp_source.html">expr_transform.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00067">AND</a>, <a class="el" href="expr__transform_8h_source.html#l00039">d_commonRules</a>, <a class="el" href="expr__transform_8h_source.html#l00037">d_core</a>, <a class="el" href="expr__transform_8h_source.html#l00043">d_pushNegCache</a>, <a class="el" href="expr__transform_8h_source.html#l00040">d_rules</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="kinds_8h_source.html#l00036">FALSE_EXPR</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="kinds_8h_source.html#l00070">IFF</a>, <a class="el" href="kinds_8h_source.html#l00071">IMPLIES</a>, <a class="el" href="expr_8h_source.html#l01021">CVC3::Expr::isTerm()</a>, <a class="el" href="kinds_8h_source.html#l00081">ITE</a>, <a class="el" href="kinds_8h_source.html#l00227">LETDECL</a>, <a class="el" href="kinds_8h_source.html#l00066">NOT</a>, <a class="el" href="kinds_8h_source.html#l00068">OR</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">CVC3::CommonProofRules::reflexivityRule()</a>, <a class="el" href="theory_8h_source.html#l00673">CVC3::Theory::reflexivityRule()</a>, <a class="el" href="classCVC3_1_1CoreProofRules.html#a3389cd795acc4cee4b591c1488293963">CVC3::CoreProofRules::rewriteImplies()</a>, <a class="el" href="classCVC3_1_1CoreProofRules.html#acad687c3e6faa5709961210637c260da">CVC3::CoreProofRules::rewriteLetDecl()</a>, <a class="el" href="classCVC3_1_1CoreProofRules.html#ade3007866410b6565ee0ea1ff4c49a99">CVC3::CoreProofRules::rewriteNotAnd()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a30fa79637f4308e8e733015624293775">CVC3::CommonProofRules::rewriteNotFalse()</a>, <a class="el" href="classCVC3_1_1CoreProofRules.html#ac68942cf0c21011f9429042e279b4a54">CVC3::CoreProofRules::rewriteNotIte()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a8a04ff29591a019d4d4cf073c0987316">CVC3::CommonProofRules::rewriteNotNot()</a>, <a class="el" href="classCVC3_1_1CoreProofRules.html#aea875ee7355ae6aab01b84c176dbccf6">CVC3::CoreProofRules::rewriteNotOr()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#ad55b11590196fbd73d24daa1d0d6eeb1">CVC3::CommonProofRules::rewriteNotTrue()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f">CVC3::CommonProofRules::substitutivityRule()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, and <a class="el" href="kinds_8h_source.html#l00035">TRUE_EXPR</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00127">pushNegation()</a>, and <a class="el" href="expr__transform_8cpp_source.html#l00225">pushNegationRec()</a>.</p>
</div>
</div>
<a class="anchor" id="aa247d13841a682165edb357895d78aa3"></a><!-- doxytag: member="CVC3::ExprTransform::pushNegationRec" ref="aa247d13841a682165edb357895d78aa3" args="(const Theorem &e, bool neg)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> ExprTransform::pushNegationRec </td>
<td>(</td>
<td class="paramtype">const <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> & </td>
<td class="paramname"><em>e</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype">bool </td>
<td class="paramname"><em>neg</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Its version for transitivity. </p>
<p>Definition at line <a class="el" href="expr__transform_8cpp_source.html#l00225">225</a> of file <a class="el" href="expr__transform_8cpp_source.html">expr_transform.cpp</a>.</p>
<p>References <a class="el" href="expr__transform_8h_source.html#l00039">d_commonRules</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="theorem_8cpp_source.html#l00224">CVC3::Theorem::isRewrite()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00141">pushNegationRec()</a>, <a class="el" href="theorem_8h_source.html#l00404">CVC3::Theorem::toString()</a>, and <a class="el" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a">CVC3::CommonProofRules::transitivityRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a5daaef4e405ec8c9bb7f6e6adbde27fa"></a><!-- doxytag: member="CVC3::ExprTransform::pushNegation1" ref="a5daaef4e405ec8c9bb7f6e6adbde27fa" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> ExprTransform::pushNegation1 </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></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Push negation one level down. Takes 'e' which is 'NOT e[0]'. </p>
<p>Definition at line <a class="el" href="expr__transform_8cpp_source.html#l00239">239</a> of file <a class="el" href="expr__transform_8cpp_source.html">expr_transform.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00067">AND</a>, <a class="el" href="expr__transform_8h_source.html#l00039">d_commonRules</a>, <a class="el" href="expr__transform_8h_source.html#l00040">d_rules</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="kinds_8h_source.html#l00036">FALSE_EXPR</a>, <a class="el" href="expr_8h_source.html#l01183">CVC3::Expr::getOp()</a>, <a class="el" href="kinds_8h_source.html#l00071">IMPLIES</a>, <a class="el" href="expr_8h_source.html#l00420">CVC3::Expr::isNot()</a>, <a class="el" href="kinds_8h_source.html#l00081">ITE</a>, <a class="el" href="kinds_8h_source.html#l00227">LETDECL</a>, <a class="el" href="kinds_8h_source.html#l00066">NOT</a>, <a class="el" href="kinds_8h_source.html#l00068">OR</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">CVC3::CommonProofRules::reflexivityRule()</a>, <a class="el" href="classCVC3_1_1CoreProofRules.html#a3389cd795acc4cee4b591c1488293963">CVC3::CoreProofRules::rewriteImplies()</a>, <a class="el" href="classCVC3_1_1CoreProofRules.html#acad687c3e6faa5709961210637c260da">CVC3::CoreProofRules::rewriteLetDecl()</a>, <a class="el" href="classCVC3_1_1CoreProofRules.html#ade3007866410b6565ee0ea1ff4c49a99">CVC3::CoreProofRules::rewriteNotAnd()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a30fa79637f4308e8e733015624293775">CVC3::CommonProofRules::rewriteNotFalse()</a>, <a class="el" href="classCVC3_1_1CoreProofRules.html#ac68942cf0c21011f9429042e279b4a54">CVC3::CoreProofRules::rewriteNotIte()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a8a04ff29591a019d4d4cf073c0987316">CVC3::CommonProofRules::rewriteNotNot()</a>, <a class="el" href="classCVC3_1_1CoreProofRules.html#aea875ee7355ae6aab01b84c176dbccf6">CVC3::CoreProofRules::rewriteNotOr()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#ad55b11590196fbd73d24daa1d0d6eeb1">CVC3::CommonProofRules::rewriteNotTrue()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f">CVC3::CommonProofRules::substitutivityRule()</a>, <a class="el" href="expr_8cpp_source.html#l00344">CVC3::Expr::toString()</a>, <a class="el" href="kinds_8h_source.html#l00099">TRACE</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a">CVC3::CommonProofRules::transitivityRule()</a>, and <a class="el" href="kinds_8h_source.html#l00035">TRUE_EXPR</a>.</p>
</div>
</div>
<a class="anchor" id="ac16db941bec1cf4ecb888a8fc3f1a0e9"></a><!-- doxytag: member="CVC3::ExprTransform::specialSimplify" ref="ac16db941bec1cf4ecb888a8fc3f1a0e9" args="(const Expr &e, ExprHashMap< Theorem > &cache)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> ExprTransform::specialSimplify </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"><a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>cache</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Helper for newPP. </p>
<p>Definition at line <a class="el" href="expr__transform_8cpp_source.html#l00296">296</a> of file <a class="el" href="expr__transform_8cpp_source.html">expr_transform.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr__transform_8h_source.html#l00039">d_commonRules</a>, <a class="el" href="expr__transform_8h_source.html#l00037">d_core</a>, <a class="el" href="expr__map_8h_source.html#l00326">CVC3::ExprHashMap< Data >::end()</a>, <a class="el" href="expr__map_8h_source.html#l00329">CVC3::ExprHashMap< Data >::find()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="expr_8cpp_source.html#l00550">CVC3::Expr::isAtomic()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="theorem_8h_source.html#l00171">CVC3::Theorem::isRefl()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">CVC3::CommonProofRules::reflexivityRule()</a>, <a class="el" href="theory__core_8cpp_source.html#l00184">CVC3::TheoryCore::simplify()</a>, and <a class="el" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f">CVC3::CommonProofRules::substitutivityRule()</a>.</p>
</div>
</div>
<a class="anchor" id="a10909e40663567172bcbf45bad521055"></a><!-- doxytag: member="CVC3::ExprTransform::newPP" ref="a10909e40663567172bcbf45bad521055" args="(const Expr &e, int &budget)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> ExprTransform::newPP </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">int & </td>
<td class="paramname"><em>budget</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>new preprocessing code </p>
<p>Definition at line <a class="el" href="expr__transform_8cpp_source.html#l00282">282</a> of file <a class="el" href="expr__transform_8cpp_source.html">expr_transform.cpp</a>.</p>
<p>References <a class="el" href="expr__map_8h_source.html#l00175">CVC3::ExprMap< Data >::clear()</a>, <a class="el" href="expr__transform_8h_source.html#l00047">d_budgetLimit</a>, <a class="el" href="expr__transform_8h_source.html#l00039">d_commonRules</a>, <a class="el" href="expr__transform_8h_source.html#l00045">d_newPPCache</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01030">CVC3::Expr::getSize()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00334">newPPrec()</a>, and <a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">CVC3::CommonProofRules::reflexivityRule()</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00079">preprocess()</a>.</p>
</div>
</div>
<a class="anchor" id="a5817a5d8a33b01904fa7e06aa91061bb"></a><!-- doxytag: member="CVC3::ExprTransform::newPPrec" ref="a5817a5d8a33b01904fa7e06aa91061bb" args="(const Expr &e, int &budget)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> ExprTransform::newPPrec </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">int & </td>
<td class="paramname"><em>budget</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>main new preprocessing code </p>
<p>Definition at line <a class="el" href="expr__transform_8cpp_source.html#l00334">334</a> of file <a class="el" href="expr__transform_8cpp_source.html">expr_transform.cpp</a>.</p>
<p>References <a class="el" href="theory__core_8cpp_source.html#l03468">CVC3::TheoryCore::addFact()</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#ab4527c48e9f88d94d7ca076757a6f3ba">CVC3::CommonProofRules::assumpRule()</a>, <a class="el" href="expr_8cpp_source.html#l00525">CVC3::Expr::containsTermITE()</a>, <a class="el" href="expr__transform_8h_source.html#l00047">d_budgetLimit</a>, <a class="el" href="expr__transform_8h_source.html#l00039">d_commonRules</a>, <a class="el" href="expr__transform_8h_source.html#l00037">d_core</a>, <a class="el" href="expr__transform_8h_source.html#l00045">d_newPPCache</a>, <a class="el" href="expr__transform_8h_source.html#l00040">d_rules</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>, <a class="el" href="theory__core_8h_source.html#l00348">CVC3::TheoryCore::getCM()</a>, <a class="el" href="theorem_8cpp_source.html#l00246">CVC3::Theorem::getRHS()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00411">CVC3::Expr::isPropAtom()</a>, <a class="el" href="theorem_8h_source.html#l00171">CVC3::Theorem::isRefl()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a893a258d9f7d49acb5c8a8b5b8ec39b0">CVC3::CommonProofRules::liftOneITE()</a>, <a class="el" href="expr_8h_source.html#l00937">CVC3::Expr::negate()</a>, <a class="el" href="context_8h_source.html#l00402">CVC3::ContextManager::pop()</a>, <a class="el" href="context_8h_source.html#l00401">CVC3::ContextManager::push()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">CVC3::CommonProofRules::reflexivityRule()</a>, <a class="el" href="classCVC3_1_1CoreProofRules.html#a7912f66f5be7e05b0c85f15596747be4">CVC3::CoreProofRules::rewriteIteElse()</a>, <a class="el" href="classCVC3_1_1CoreProofRules.html#a8117a95eed02c35936f988d1c9c2bdab">CVC3::CoreProofRules::rewriteIteThen()</a>, <a class="el" href="theory__core_8cpp_source.html#l00184">CVC3::TheoryCore::simplify()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f">CVC3::CommonProofRules::substitutivityRule()</a>, and <a class="el" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a">CVC3::CommonProofRules::transitivityRule()</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00282">newPP()</a>.</p>
</div>
</div>
<a class="anchor" id="ad12aee56d7dd01276af2d993ce4676c9"></a><!-- doxytag: member="CVC3::ExprTransform::updateQueue" ref="ad12aee56d7dd01276af2d993ce4676c9" args="(ExprMap< std::set< Expr > * > &queue, const Expr &e, const std::set< Expr > &careSet)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">void ExprTransform::updateQueue </td>
<td>(</td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a>< std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > * > & </td>
<td class="paramname"><em>queue</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">const std::set< <a class="el" href="classCVC3_1_1Expr.html">Expr</a> > & </td>
<td class="paramname"><em>careSet</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Helper for simplifyWithCare. </p>
<p>Definition at line <a class="el" href="expr__transform_8cpp_source.html#l00413">413</a> of file <a class="el" href="expr__transform_8cpp_source.html">expr_transform.cpp</a>.</p>
<p>References <a class="el" href="expr__map_8h_source.html#l00194">CVC3::ExprMap< Data >::find()</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00476">simplifyWithCare()</a>.</p>
</div>
</div>
<a class="anchor" id="ae1f3a46b2e09495bb5afe3ac46f23c2b"></a><!-- doxytag: member="CVC3::ExprTransform::substitute" ref="ae1f3a46b2e09495bb5afe3ac46f23c2b" args="(const Expr &e, ExprHashMap< Theorem > &substTable, ExprHashMap< Theorem > &cache)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> ExprTransform::substitute </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"><a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>substTable</em>, </td>
</tr>
<tr>
<td class="paramkey"></td>
<td></td>
<td class="paramtype"><a class="el" href="classCVC3_1_1ExprHashMap.html">ExprHashMap</a>< <a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> > & </td>
<td class="paramname"><em>cache</em> </td>
</tr>
<tr>
<td></td>
<td>)</td>
<td></td><td><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Helper for simplifyWithCare. </p>
<p>Definition at line <a class="el" href="expr__transform_8cpp_source.html#l00434">434</a> of file <a class="el" href="expr__transform_8cpp_source.html">expr_transform.cpp</a>.</p>
<p>References <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr__transform_8h_source.html#l00039">d_commonRules</a>, <a class="el" href="expr__map_8h_source.html#l00326">CVC3::ExprHashMap< Data >::end()</a>, <a class="el" href="expr__map_8h_source.html#l00329">CVC3::ExprHashMap< Data >::find()</a>, <a class="el" href="expr_8cpp_source.html#l00550">CVC3::Expr::isAtomic()</a>, <a class="el" href="theorem_8h_source.html#l00171">CVC3::Theorem::isRefl()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">CVC3::CommonProofRules::reflexivityRule()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f">CVC3::CommonProofRules::substitutivityRule()</a>, and <a class="el" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a">CVC3::CommonProofRules::transitivityRule()</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00476">simplifyWithCare()</a>.</p>
</div>
</div>
<a class="anchor" id="ad18b9697ac34575a40f106e48cfef5b4"></a><!-- doxytag: member="CVC3::ExprTransform::simplifyWithCare" ref="ad18b9697ac34575a40f106e48cfef5b4" args="(const Expr &e)" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1Theorem.html">Theorem</a> ExprTransform::simplifyWithCare </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></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>ITE simplification from Burch paper. </p>
<p>Definition at line <a class="el" href="expr__transform_8cpp_source.html#l00476">476</a> of file <a class="el" href="expr__transform_8cpp_source.html">expr_transform.cpp</a>.</p>
<p>References <a class="el" href="kinds_8h_source.html#l00067">AND</a>, <a class="el" href="expr_8h_source.html#l01201">CVC3::Expr::arity()</a>, <a class="el" href="expr_8cpp_source.html#l00525">CVC3::Expr::containsTermITE()</a>, <a class="el" href="expr__transform_8h_source.html#l00039">d_commonRules</a>, <a class="el" href="expr__transform_8h_source.html#l00037">d_core</a>, <a class="el" href="expr__transform_8h_source.html#l00040">d_rules</a>, <a class="el" href="expr__transform_8h_source.html#l00038">d_theoryArith</a>, <a class="el" href="debug_8h_source.html#l00408">DebugAssert</a>, <a class="el" href="classCVC3_1_1CoreProofRules.html#a9592705bbf82393b7f6500fa33ead252">CVC3::CoreProofRules::dummyTheorem()</a>, <a class="el" href="expr__map_8h_source.html#l00170">CVC3::ExprMap< Data >::empty()</a>, <a class="el" href="expr__map_8h_source.html#l00191">CVC3::ExprMap< Data >::end()</a>, <a class="el" href="expr_8h_source.html#l00929">CVC3::Expr::eqExpr()</a>, <a class="el" href="expr__map_8h_source.html#l00178">CVC3::ExprMap< Data >::erase()</a>, <a class="el" href="expr__manager_8h_source.html#l00278">CVC3::ExprManager::falseExpr()</a>, <a class="el" href="theory_8h_source.html#l00090">CVC3::Theory::getEM()</a>, <a class="el" href="expr_8h_source.html#l01168">CVC3::Expr::getKind()</a>, <a class="el" href="expr_8h_source.html#l01259">CVC3::Expr::getType()</a>, <a class="el" href="expr_8h_source.html#l00965">CVC3::Expr::iffExpr()</a>, <a class="el" href="expr_8cpp_source.html#l00550">CVC3::Expr::isAtomic()</a>, <a class="el" href="expr_8cpp_source.html#l00571">CVC3::Expr::isAtomicFormula()</a>, <a class="el" href="type_8h_source.html#l00060">CVC3::Type::isBool()</a>, <a class="el" href="expr_8h_source.html#l00411">CVC3::Expr::isPropAtom()</a>, <a class="el" href="theorem_8h_source.html#l00171">CVC3::Theorem::isRefl()</a>, <a class="el" href="kinds_8h_source.html#l00081">ITE</a>, <a class="el" href="theory__arith_8cpp_source.html#l00294">CVC3::TheoryArith::leavesAreNumConst()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a893a258d9f7d49acb5c8a8b5b8ec39b0">CVC3::CommonProofRules::liftOneITE()</a>, <a class="el" href="kinds_8h_source.html#l00068">OR</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">CVC3::CommonProofRules::reflexivityRule()</a>, <a class="el" href="classCVC3_1_1CoreProofRules.html#a03f8a74b8b1b6d90ff23a0a6150c49d6">CVC3::CoreProofRules::rewriteIteCond()</a>, <a class="el" href="theory__core_8cpp_source.html#l00184">CVC3::TheoryCore::simplify()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00434">substitute()</a>, <a class="el" href="theory_8cpp_source.html#l00252">CVC3::Theory::theoryOf()</a>, <a class="el" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a">CVC3::CommonProofRules::transitivityRule()</a>, <a class="el" href="expr__manager_8h_source.html#l00280">CVC3::ExprManager::trueExpr()</a>, and <a class="el" href="expr__transform_8cpp_source.html#l00413">updateQueue()</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00079">preprocess()</a>.</p>
</div>
</div>
<hr/><h2>Member Data Documentation</h2>
<a class="anchor" id="adf66a811cae797e64ae8ff25e922766a"></a><!-- doxytag: member="CVC3::ExprTransform::d_core" ref="adf66a811cae797e64ae8ff25e922766a" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoryCore.html">TheoryCore</a>* <a class="el" href="classCVC3_1_1ExprTransform.html#adf66a811cae797e64ae8ff25e922766a">CVC3::ExprTransform::d_core</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00037">37</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00034">ExprTransform()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00334">newPPrec()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00079">preprocess()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00141">pushNegationRec()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00476">simplifyWithCare()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00042">smartSimplify()</a>, and <a class="el" href="expr__transform_8cpp_source.html#l00296">specialSimplify()</a>.</p>
</div>
</div>
<a class="anchor" id="a741b9541234b906a8b74845e4c4d3c51"></a><!-- doxytag: member="CVC3::ExprTransform::d_theoryArith" ref="a741b9541234b906a8b74845e4c4d3c51" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1TheoryArith.html">TheoryArith</a>* <a class="el" href="classCVC3_1_1ExprTransform.html#a741b9541234b906a8b74845e4c4d3c51">CVC3::ExprTransform::d_theoryArith</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00038">38</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8h_source.html#l00053">setTheoryArith()</a>, and <a class="el" href="expr__transform_8cpp_source.html#l00476">simplifyWithCare()</a>.</p>
</div>
</div>
<a class="anchor" id="aeea6bcb414f95c53d846ad7c684b1a5d"></a><!-- doxytag: member="CVC3::ExprTransform::d_commonRules" ref="aeea6bcb414f95c53d846ad7c684b1a5d" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CommonProofRules.html">CommonProofRules</a>* <a class="el" href="classCVC3_1_1ExprTransform.html#aeea6bcb414f95c53d846ad7c684b1a5d">CVC3::ExprTransform::d_commonRules</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00039">39</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00034">ExprTransform()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00282">newPP()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00334">newPPrec()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00079">preprocess()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00127">pushNegation()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00239">pushNegation1()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00141">pushNegationRec()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00476">simplifyWithCare()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00296">specialSimplify()</a>, and <a class="el" href="expr__transform_8cpp_source.html#l00434">substitute()</a>.</p>
</div>
</div>
<a class="anchor" id="ae6bdbc5df7bd412e0594650d7ef02cc4"></a><!-- doxytag: member="CVC3::ExprTransform::d_rules" ref="ae6bdbc5df7bd412e0594650d7ef02cc4" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1CoreProofRules.html">CoreProofRules</a>* <a class="el" href="classCVC3_1_1ExprTransform.html#ae6bdbc5df7bd412e0594650d7ef02cc4">CVC3::ExprTransform::d_rules</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00040">40</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00034">ExprTransform()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00334">newPPrec()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00239">pushNegation1()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00141">pushNegationRec()</a>, and <a class="el" href="expr__transform_8cpp_source.html#l00476">simplifyWithCare()</a>.</p>
</div>
</div>
<a class="anchor" id="a986331240196633d2d639867eb2b2850"></a><!-- doxytag: member="CVC3::ExprTransform::d_pushNegCache" ref="a986331240196633d2d639867eb2b2850" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a><<a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>> <a class="el" href="classCVC3_1_1ExprTransform.html#a986331240196633d2d639867eb2b2850">CVC3::ExprTransform::d_pushNegCache</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Cache for <a class="el" href="classCVC3_1_1ExprTransform.html#ab2757afee881751f99c86499400aef44" title="Push all negations down to the leaves.">pushNegation()</a> </p>
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00043">43</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00127">pushNegation()</a>, and <a class="el" href="expr__transform_8cpp_source.html#l00141">pushNegationRec()</a>.</p>
</div>
</div>
<a class="anchor" id="a574575f8c65c604d6904c4654f2e48d6"></a><!-- doxytag: member="CVC3::ExprTransform::d_newPPCache" ref="a574575f8c65c604d6904c4654f2e48d6" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname"><a class="el" href="classCVC3_1_1ExprMap.html">ExprMap</a><<a class="el" href="classCVC3_1_1Theorem.html">Theorem</a>> <a class="el" href="classCVC3_1_1ExprTransform.html#a574575f8c65c604d6904c4654f2e48d6">CVC3::ExprTransform::d_newPPCache</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Cache for newPP. </p>
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00045">45</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00282">newPP()</a>, and <a class="el" href="expr__transform_8cpp_source.html#l00334">newPPrec()</a>.</p>
</div>
</div>
<a class="anchor" id="a4228c9a8ee02c424c35bbd4bf3733cb8"></a><!-- doxytag: member="CVC3::ExprTransform::d_budgetLimit" ref="a4228c9a8ee02c424c35bbd4bf3733cb8" args="" -->
<div class="memitem">
<div class="memproto">
<table class="memname">
<tr>
<td class="memname">int <a class="el" href="classCVC3_1_1ExprTransform.html#a4228c9a8ee02c424c35bbd4bf3733cb8">CVC3::ExprTransform::d_budgetLimit</a><code> [private]</code></td>
</tr>
</table>
</div>
<div class="memdoc">
<p>Budget limit for newPP. </p>
<p>Definition at line <a class="el" href="expr__transform_8h_source.html#l00047">47</a> of file <a class="el" href="expr__transform_8h_source.html">expr_transform.h</a>.</p>
<p>Referenced by <a class="el" href="expr__transform_8cpp_source.html#l00282">newPP()</a>, <a class="el" href="expr__transform_8cpp_source.html#l00334">newPPrec()</a>, and <a class="el" href="expr__transform_8cpp_source.html#l00079">preprocess()</a>.</p>
</div>
</div>
<hr/>The documentation for this class was generated from the following files:<ul>
<li><a class="el" href="expr__transform_8h_source.html">expr_transform.h</a></li>
<li><a class="el" href="bryant_8cpp_source.html">bryant.cpp</a></li>
<li><a class="el" href="expr__transform_8cpp_source.html">expr_transform.cpp</a></li>
</ul>
</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>
