| CVC3 | 
| addLiteral(Lit l, bool invert=false) | SAT::CNF_Formula |  [inline] | 
| begin() const =0 | SAT::CNF_Formula |  [pure virtual] | 
| CNF_Formula() | SAT::CNF_Formula |  [inline] | 
| const_iterator typedef | SAT::CNF_Formula | |
| copy(const CNF_Formula &cnf) | SAT::CNF_Formula |  [protected] | 
| d_current | SAT::CNF_Formula |  [protected] | 
| empty() const =0 | SAT::CNF_Formula |  [pure virtual] | 
| end() const =0 | SAT::CNF_Formula |  [pure virtual] | 
| getCurrentClause() | SAT::CNF_Formula |  [inline] | 
| newClause()=0 | SAT::CNF_Formula |  [pure virtual] | 
| numClauses() const =0 | SAT::CNF_Formula |  [pure virtual] | 
| numVars() const =0 | SAT::CNF_Formula |  [pure virtual] | 
| operator+=(const CNF_Formula &cnf) | SAT::CNF_Formula | |
| operator+=(const Clause &c) | SAT::CNF_Formula | |
| operator[](int i) const =0 | SAT::CNF_Formula |  [pure virtual] | 
| print() const | SAT::CNF_Formula | |
| registerUnit()=0 | SAT::CNF_Formula |  [pure virtual] | 
| setNumVars(unsigned numVars)=0 | SAT::CNF_Formula |  [protected, pure virtual] | 
| ~CNF_Formula() | SAT::CNF_Formula |  [inline, virtual] | 
 1.7.3
 1.7.3