addLiteral(Lit l, bool invert=false) | SAT::CNF_Formula | [inline] |
begin() const | SAT::CD_CNF_Formula | [inline, virtual] |
CD_CNF_Formula(CVCL::Context *context) | SAT::CD_CNF_Formula | [inline] |
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] |
d_formula | SAT::CD_CNF_Formula | [private] |
d_numVars | SAT::CD_CNF_Formula | [private] |
empty() const | SAT::CD_CNF_Formula | [inline, virtual] |
end() const | SAT::CD_CNF_Formula | [inline, virtual] |
getCurrentClause() | SAT::CNF_Formula | [inline] |
newClause() | SAT::CD_CNF_Formula | [virtual] |
numClauses() const | SAT::CD_CNF_Formula | [inline, virtual] |
numVars() const | SAT::CD_CNF_Formula | [inline, virtual] |
operator+=(const CNF_Formula &cnf) | SAT::CNF_Formula | |
operator+=(const Clause &c) | SAT::CNF_Formula | |
operator[](int i) const | SAT::CD_CNF_Formula | [inline, virtual] |
print() const | SAT::CNF_Formula | |
registerUnit() | SAT::CD_CNF_Formula | [virtual] |
setNumVars(unsigned numVars) | SAT::CD_CNF_Formula | [inline, private, virtual] |
~CD_CNF_Formula() | SAT::CD_CNF_Formula | [inline] |
~CNF_Formula() | SAT::CNF_Formula | [inline, virtual] |