| addAssumption(const CVC3::Theorem &thm, CNF_Formula &cnf) | SAT::CNF_Manager | |
| addLemma(CVC3::Theorem thm, CNF_Formula &cnf) | SAT::CNF_Manager | |
| CNF_Manager(CVC3::TheoremManager *tm, CVC3::Statistics &statistics, const CVC3::CLFlags &flags) | SAT::CNF_Manager | |
| concreteExpr(const CVC3::Expr &e, const Lit &literal) | SAT::CNF_Manager | [private] |
| concreteLit(Lit l, bool checkTranslated=true) | SAT::CNF_Manager | [inline] |
| concreteVar(Var v) | 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, CNF_Formula &cnf) | SAT::CNF_Manager | |
| createProofRules(CVC3::TheoremManager *tm, const CVC3::CLFlags &) | 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_flags | SAT::CNF_Manager | [private] |
| d_iteMap | SAT::CNF_Manager | [private] |
| d_minimizeClauses | SAT::CNF_Manager | [private] |
| d_nullExpr | 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(Var c, unsigned i) | SAT::CNF_Manager | [inline] |
| getFanout(Var c, unsigned i) | SAT::CNF_Manager | [inline] |
| numFanins(Var c) | SAT::CNF_Manager | [inline] |
| numFanouts(Var 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 | |
