| addAssumption(const CVC3::Theorem &thm, CNF_Formula &cnf) | SAT::CNF_Manager | |
| addLemma(const CVC3::Theorem &thm, CNF_Formula &cnf) | SAT::CNF_Manager | |
| CNF_Manager(CVC3::TheoremManager *tm, CVC3::Statistics &statistics, bool minimizeClauses) | SAT::CNF_Manager | |
| concreteLit(Lit l, bool checkTranslated=true) | SAT::CNF_Manager | [inline] |
| cons(unsigned lb, unsigned ub, const CVC3::Expr &e2, std::vector< unsigned > &newLits) | SAT::CNF_Manager | |
| convertLemma(const CVC3::Theorem &thm, Clause &c) | SAT::CNF_Manager | |
| createProofRules(CVC3::TheoremManager *tm) | SAT::CNF_Manager | [private] |
| d_bottomScope | SAT::CNF_Manager | [private] |
| d_clauseIdNext | SAT::CNF_Manager | [private] |
| d_cnfCallback | SAT::CNF_Manager | [private] |
| d_cnfVars | SAT::CNF_Manager | [private] |
| d_commonRules | SAT::CNF_Manager | [private] |
| d_iteMap | SAT::CNF_Manager | [private] |
| d_minimizeClauses | SAT::CNF_Manager | [private] |
| d_rules | SAT::CNF_Manager | [private] |
| d_statistics | SAT::CNF_Manager | [private] |
| d_translateQueueFlags | SAT::CNF_Manager | [private] |
| d_translateQueueThms | SAT::CNF_Manager | [private] |
| d_translateQueueVars | SAT::CNF_Manager | [private] |
| d_varInfo | SAT::CNF_Manager | [private] |
| d_vc | SAT::CNF_Manager | [private] |
| getCNFLit(const CVC3::Expr &e) | SAT::CNF_Manager | [inline] |
| getFanin(Lit c, unsigned i) | SAT::CNF_Manager | [inline] |
| getFanout(Lit c, unsigned i) | SAT::CNF_Manager | [inline] |
| numFanins(Lit c) | SAT::CNF_Manager | [inline] |
| numFanouts(Lit c) | SAT::CNF_Manager | [inline] |
| numVars() | SAT::CNF_Manager | [inline] |
| registerAtom(const CVC3::Expr &e, const CVC3::Theorem &thm) | SAT::CNF_Manager | [private] |
| registerCNFCallback(CNFCallback *cnfCallback) | SAT::CNF_Manager | [inline] |
| replaceITErec(const CVC3::Expr &e, Var v, bool translateOnly) | SAT::CNF_Manager | [private] |
| setBottomScope(int scope) | SAT::CNF_Manager | [inline] |
| translateExpr(const CVC3::Theorem &thmIn, CNF_Formula &cnf) | SAT::CNF_Manager | [private] |
| translateExprRec(const CVC3::Expr &e, CNF_Formula &cnf, const CVC3::Theorem &thmIn) | SAT::CNF_Manager | [private] |
| ~CNF_Manager() | SAT::CNF_Manager | |
