Sophie

Sophie

distrib > Fedora > 15 > i386 > by-pkgid > 583ffa4ba069126c3ba0bc565dc0485a > files > 759

cvc3-doc-2.4.1-1.fc15.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"/>
<title>CVC3: Member List</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&#160;<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&#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="hierarchy.html"><span>Class&#160;Hierarchy</span></a></li>
      <li><a href="functions.html"><span>Class&#160;Members</span></a></li>
    </ul>
  </div>
</div>
<div class="header">
  <div class="headertitle">
<div class="title">SatSolver Member List</div>  </div>
</div>
<div class="contents">
This is the complete list of members for <a class="el" href="classSatSolver.html">SatSolver</a>, including all inherited members.<table>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a1fb269f00fd9da8242e2bad01967f097">AddClause</a>(std::vector&lt; Lit &gt; &amp;lits)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a771730713d9da6f1161de299c6acc308">AddVariable</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#acf0e4f44556b7cfcea37100f92962fee">AddVariables</a>(int nvars)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a1a1ccd6ae244cce5f08fcdf2d4621fe0">BUDGET_EXCEEDED</a> enum value</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#ab4e73333fbc4b4372a18c66a40d4757f">Continue</a>()=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#aad67f64508f2560518d09449cd4e39ee">Create</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [static]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a833d889d53fa2dbd609dac14625a5325">DeleteClause</a>(Clause clause)</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#ae4127dad23cea8d60a6eb2f5d0072554">DisableClauseDeletion</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#aab2f83c7e7a2e0294904ff5c0fa3409d">EnableClauseDeletion</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a9ab0d5988fd6b737626eddfdfb3086ca">GetBudgetUsed</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a3f5dcfdd713812059fdcba94bc6be3c1">GetClause</a>(int clauseIndex)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#af0c71f214e5980cf6848abaeaa3dbf16">GetClauseLits</a>(Clause clause, std::vector&lt; Lit &gt; *lits)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a580f042cdf32047e73056dfd810226ad">GetFirstClause</a>()=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a6c62129375a3b6dda25ad2ba6c0a5696">GetFirstVar</a>()=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a74190d9fc4abdb54fc65c4efffdf75fc">GetMaxDLevel</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a409a256b9b590f8881690422ac34f566">GetMemUsed</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a61ca72083b23704e2007f0c4b7414ff1">GetNextClause</a>(Clause clause)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a2a175341a5ca6b28add0a1cac3e9bc8a">GetNextVar</a>(Var var)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#ab81836241806bc37ca6c5cfcd1a77df4">GetNumConflicts</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a2a416ee5b49d9cf91a57c5b9e71388b8">GetNumDecisions</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a6499994eb391919ce6542412e3e43d01">GetNumDeletedClauses</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#ab81eb4127972de38906425ba4babfadc">GetNumDeletedLiterals</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#af11d56356aa9a578f0baaa4cbcdc0b97">GetNumExtConflicts</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a45923d3ff1c6145198098d7e689c23f0">GetNumImplications</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a6f617ce6eae22b959f135d347776cb27">GetNumLiterals</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a7187c85c8fc08c253b97de67509af3f2">GetPhaseFromLit</a>(Lit lit)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a4af09fc1738959db1c0d197a4fbf8a6a">GetSATTime</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#ab1d30058d42aecba7708cb9e29cbda67">GetTotalTime</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#aebeecffca634f23d8c9b941b44b4cfe7">GetVar</a>(int varIndex)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a111b3a56be2feaae62bc57483f0aa9bf">GetVarAssignment</a>(Var var)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a505146a1fb5715620935ec31f909932f">GetVarFromLit</a>(Lit lit)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a78a8661d31ba8f3aca7e4c73a84f0bcf">GetVarIndex</a>(Var v)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a66bbef74a05f145e477adf37a1e1d116">MakeLit</a>(Var var, int phase)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#ad883af9527935afd6c8ad542ba119f4a">NumClauses</a>()=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a75ac3919b9d2794bd2443e32bb1f29fd">NumVariables</a>()=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a987b167d27ed988755362d6decb025d8">OUT_OF_MEMORY</a> enum value</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a1e57a5f44892f0ef08a487a1516030df">PrintStatistics</a>(std::ostream &amp;os=std::cout)</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a658bb40c580f149024c59509e9e3acd0">RegisterAssignmentHook</a>(void(*f)(void *, Var, int), void *cookie)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a76cc15252a711e8a9a21e49a30d7e920">RegisterDecisionHook</a>(Lit(*f)(void *, bool *), void *cookie)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a856cf7839d83dcc04ee421d2595fc671">RegisterDeductionHook</a>(void(*f)(void *), void *cookie)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a2f5308d9fdff97f882186073f05d8874">RegisterDLevelHook</a>(void(*f)(void *, int), void *cookie)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#ac64e81107b4b94fd1f6fb76b219a0517">Reset</a>()=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#aa05fce07f5c3363e2362a3b1de7795db">Restart</a>()=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a0dfc1321f3446be70349f35881144433">Satisfiable</a>(bool allowNewClauses=false)=0</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [pure virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a8bc290b76f93dd68bdc44d083a7c4e25">SATISFIABLE</a> enum value</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a362ed37d0180c370c2060628dc75dd32">SatSolver</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53">SATStatus</a> enum name</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a5310ac0594841d926d40d6ddb3d749b6">SATStatus</a> typedef</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#ab6c0375792fa61834acc0e059b0f0215">SetBudget</a>(int budget)</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#ae71ce584f847dd8f8cd79c15a1e18ac4">SetMemLimit</a>(int mem_limit)</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a2d799de14b8f73985474b6e6bb391799">SetRandomness</a>(int n)</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a49baebbc72ee8480ce9b15931fd6a087">SetRandSeed</a>(int seed)</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53a77f70e9dedb02009ba4ab7e6fbea1de3">UNKNOWN</a> enum value</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a09aef5b79042b31f37d0184667c34d53ad154fc26948177f01812d287e6340734">UNSATISFIABLE</a> enum value</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td></td></tr>
  <tr class="memlist"><td><a class="el" href="classSatSolver.html#a087f2258b1c1ccce271e826dc07d27e6">~SatSolver</a>()</td><td><a class="el" href="classSatSolver.html">SatSolver</a></td><td><code> [inline, virtual]</code></td></tr>
</table></div>
<hr class="footer"/><address class="footer"><small>Generated on Wed Sep 7 2011 for CVC3 by&#160;
<a href="http://www.doxygen.org/index.html">
<img class="footer" src="doxygen.png" alt="doxygen"/></a> 1.7.4 </small></address>
</body>
</html>