Sophie

Sophie

distrib > PLD > th > x86_64 > by-pkgid > 9f869ff92bf81fc4b13902b2b85811f8 > files > 267

cvc3-doc-2.4.1-1.noarch.rpm

<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/xhtml;charset=UTF-8"/>
<meta http-equiv="X-UA-Compatible" content="IE=9"/>
<title>CVC3: Member List</title>
<link href="tabs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="jquery.js"></script>
<script type="text/javascript" src="dynsections.js"></script>
<link href="doxygen.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="top"><!-- do not remove this div, it is closed by doxygen! -->
<div id="titlearea">
<table cellspacing="0" cellpadding="0">
 <tbody>
 <tr style="height: 56px;">
  <td style="padding-left: 0.5em;">
   <div id="projectname">CVC3
   </div>
  </td>
 </tr>
 </tbody>
</table>
</div>
<!-- end header part -->
<!-- Generated by Doxygen 1.8.2 -->
  <div id="navrow1" class="tabs">
    <ul class="tablist">
      <li><a href="index.html"><span>Main&#160;Page</span></a></li>
      <li><a href="pages.html"><span>Related&#160;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&#160;List</span></a></li>
      <li><a href="classes.html"><span>Class&#160;Index</span></a></li>
      <li><a href="inherits.html"><span>Class&#160;Hierarchy</span></a></li>
      <li><a href="functions.html"><span>Class&#160;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_1CommonProofRules.html">CommonProofRules</a></li>  </ul>
</div>
</div><!-- top -->
<div class="header">
  <div class="headertitle">
<div class="title">CVC3::CommonProofRules Member List</div>  </div>
</div><!--header-->
<div class="contents">

<p>This is the complete list of members for <a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a>, including all inherited members.</p>
<table class="directory">
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a484540b067da205d23b2fe263662cda2">ackermann</a>(const Expr &amp;e1, const Expr &amp;e2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a3f3592ac74d0aa0caa3b9224ea7e61f4">andElim</a>(const Theorem &amp;e, int i)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a4aa193bfeb969c96b63db39a70470015">andIntro</a>(const Theorem &amp;e1, const Theorem &amp;e2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a8fadf7698616e688d0db569b7db6e5fe">andIntro</a>(const std::vector&lt; Theorem &gt; &amp;es)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#ab4527c48e9f88d94d7ca076757a6f3ba">assumpRule</a>(const Expr &amp;a, int scope=-1)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a6f8068606f30fe7b2c405ddf5ce1a53b">clearSkolemAxioms</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a1074822d52c22daacaa78b34ac0635ba">contradictionRule</a>(const Theorem &amp;e, const Theorem &amp;not_e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#aec56ab0fbac82267ff202ae328fe801f">excludedMiddle</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#ac773341edabcc5091ca25af74fcb7653">getSkolemAxioms</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#af38f25446a561384c3de66392c4d3544">iffContrapositive</a>(const Theorem &amp;thm)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a11b56754024b56844336954cf789a63a">iffFalseElim</a>(const Theorem &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#aebbcd4a194e4fdca0bcd16143fb03a75">iffMP</a>(const Theorem &amp;e1, const Theorem &amp;e1_iff_e2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a5a56b6f9544841fe86255e5bc35e8449">iffNotFalse</a>(const Theorem &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#ae5a0a67c59ba15d84e900fdccc7653ca">iffTrue</a>(const Theorem &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#ad2edb920405666bf6e9d21ae496ff6b3">iffTrueElim</a>(const Theorem &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a69da48e244e1674f6b501ac4ef168feb">implContrapositive</a>(const Theorem &amp;thm)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a9292e13acd4b5ba2b215864022a22573">implIntro</a>(const Theorem &amp;phi, const std::vector&lt; Expr &gt; &amp;assump)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#afe561cfd6d5ee752fbc1c3cafe9b68a5">implIntro3</a>(const Theorem3 &amp;phi, const std::vector&lt; Expr &gt; &amp;assump, const std::vector&lt; Theorem &gt; &amp;tccs)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a86416b3ccec1ddf1ce534b53d6af1ec9">implMP</a>(const Theorem &amp;e1, const Theorem &amp;e1_impl_e2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a893a258d9f7d49acb5c8a8b5b8ec39b0">liftOneITE</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#ace6786234994faf89bc1b0ac8575278a">notNotElim</a>(const Theorem &amp;not_not_e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a34064eea86afa953b9229537b075a420">notToIff</a>(const Theorem &amp;not_e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a758fe978ff00099419c459914a0af5ba">queryTCC</a>(const Theorem &amp;phi, const Theorem &amp;D_phi)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a61c1fe56b4ed9744006883a7784ddb71">reflexivityRule</a>(const Expr &amp;a)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#afb2ae30738c04b088459281d259a6d3a">rewriteAnd</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a1d546d9530a3c15cd627a141137a8616">rewriteAnd</a>(const Theorem &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a5c50bf251b95dfc47ccfc6e8b51426c1">rewriteIff</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a95af3ce5ccd4212b15bac9b249004c48">rewriteIteFalse</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a6cb02a9489ef5ed4e548f49bbd07439f">rewriteIteSame</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a0e770e47e947275a69b4c9f225f8beb6">rewriteIteTrue</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a12d8ca9f5547fb3a3239d7dc6f53987c">rewriteNotExists</a>(const Expr &amp;existsExpr)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a30fa79637f4308e8e733015624293775">rewriteNotFalse</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#ad14f0ceb0d486ba3d78c2c3c6e47382a">rewriteNotForall</a>(const Expr &amp;forallExpr)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a8a04ff29591a019d4d4cf073c0987316">rewriteNotNot</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#ad55b11590196fbd73d24daa1d0d6eeb1">rewriteNotTrue</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#aa3cfb7d47a6d6bc84c85c7fa6a3e1242">rewriteOr</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a44474beaa5761147eb816db48c795c4b">rewriteOr</a>(const Theorem &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#ad078b5d25129b200fe04b20c5962aa34">rewriteReflexivity</a>(const Expr &amp;a_eq_a)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a338cafc978d9b6a447e8d58af42d7e5b">rewriteUsingSymmetry</a>(const Expr &amp;a1_eq_a2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a015539886185195ba5d98c60cd7e8f66">skolemize</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#aed771f6a74d1a336cc08bfcfaf8169da">skolemize</a>(const Theorem &amp;thm)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a8a2561e9e4763460c65dbebe10d2f281">skolemizeRewrite</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a4013a795d82cebb8b60ed67c094a7cba">skolemizeRewriteVar</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a776c827bb6e3b889234429c49ae9ad6f">substitutivityRule</a>(const Expr &amp;e, const Theorem &amp;thm)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#abd65b6e03c3c57174b94a955d12cf266">substitutivityRule</a>(const Expr &amp;e, const Theorem &amp;thm1, const Theorem &amp;thm2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#aa1d9df2568ac3efade63925834c752e6">substitutivityRule</a>(const Op &amp;op, const std::vector&lt; Theorem &gt; &amp;thms)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a23a0251820f022d14376c6e825291fa2">substitutivityRule</a>(const Expr &amp;e, const std::vector&lt; unsigned &gt; &amp;changed, const std::vector&lt; Theorem &gt; &amp;thms)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a5f4e51842d28b0ef5def4eecb65ae99c">substitutivityRule</a>(const Expr &amp;e, const int changed, const Theorem &amp;thm)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a0a87e88508f49b73037e0024afa841bf">symmetryRule</a>(const Theorem &amp;a1_eq_a2)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a4a4e90cd69ce24e83ba2c217907c277a">transitivityRule</a>(const Theorem &amp;a1_eq_a2, const Theorem &amp;a2_eq_a3)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a6e93694c76f7b567487bc8cae674ae5d">trueTheorem</a>()=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#aab746efc9d013643bccc065affa82992">varIntroRule</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a10fa187373ec24079c10874d8e804ecb">varIntroSkolem</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#ae25f68b7cceeeb25b41b1d2bcb1df8f3">xorToIff</a>(const Expr &amp;e)=0</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">pure virtual</span></td></tr>
  <tr class="even"><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html#a334ad50333e9323968df2bc286de7a8f">~CommonProofRules</a>()</td><td class="entry"><a class="el" href="classCVC3_1_1CommonProofRules.html">CVC3::CommonProofRules</a></td><td class="entry"><span class="mlabel">inline</span><span class="mlabel">virtual</span></td></tr>
</table></div><!-- contents -->
<!-- start footer part -->
<hr class="footer"/><address class="footer"><small>
Generated on Thu May 16 2013 13:25:17 for CVC3 by &#160;<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/>
</a> 1.8.2
</small></address>
</body>
</html>