| assertLit(Lit l) | CVCL::SearchSatTheoryAPI | [inline, virtual] |
| checkConsistent(Clause &c, bool fullEffort) | CVCL::SearchSatTheoryAPI | [inline] |
| SAT::DPLLT::TheoryAPI::checkConsistent(Clause &c, bool fullEffort)=0 | SAT::DPLLT::TheoryAPI | [pure virtual] |
| d_cm | CVCL::SearchSatTheoryAPI | [private] |
| d_ss | CVCL::SearchSatTheoryAPI | [private] |
| getExplanation(Lit l, Clause &c) | CVCL::SearchSatTheoryAPI | [inline] |
| SAT::DPLLT::TheoryAPI::getExplanation(Lit l, Clause &c)=0 | SAT::DPLLT::TheoryAPI | [pure virtual] |
| getImplication() | CVCL::SearchSatTheoryAPI | [inline, virtual] |
| getNewClauses(CNF_Formula &cnf) | CVCL::SearchSatTheoryAPI | [inline, virtual] |
| pop() | CVCL::SearchSatTheoryAPI | [inline, virtual] |
| push() | CVCL::SearchSatTheoryAPI | [inline, virtual] |
| SearchSatTheoryAPI(SearchSat *ss) | CVCL::SearchSatTheoryAPI | [inline] |
| TheoryAPI() | SAT::DPLLT::TheoryAPI | [inline] |
| ~SearchSatTheoryAPI() | CVCL::SearchSatTheoryAPI | [inline] |
| ~TheoryAPI() | SAT::DPLLT::TheoryAPI | [inline, virtual] |
