CVC3
SAT::CNF_Manager Member List

This is the complete list of members for SAT::CNF_Manager, including all inherited members.

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_Managerprivate
concreteLit(Lit l, bool checkTranslated=true)SAT::CNF_Managerinline
concreteThm(const CVC3::Expr &e)SAT::CNF_Managerprivate
concreteVar(Var v)SAT::CNF_Managerinline
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_Managerprivate
d_bottomScopeSAT::CNF_Managerprivate
d_clauseIdNextSAT::CNF_Managerprivate
d_cnfCallbackSAT::CNF_Managerprivate
d_cnfVarsSAT::CNF_Managerprivate
d_commonRulesSAT::CNF_Managerprivate
d_flagsSAT::CNF_Managerprivate
d_iteMapSAT::CNF_Managerprivate
d_minimizeClausesSAT::CNF_Managerprivate
d_nullExprSAT::CNF_Managerprivate
d_rulesSAT::CNF_Managerprivate
d_statisticsSAT::CNF_Managerprivate
d_translateQueueFlagsSAT::CNF_Managerprivate
d_translateQueueThmsSAT::CNF_Managerprivate
d_translateQueueVarsSAT::CNF_Managerprivate
d_varInfoSAT::CNF_Managerprivate
d_vcSAT::CNF_Managerprivate
getCNFLit(const CVC3::Expr &e)SAT::CNF_Managerinline
getFanin(Var c, unsigned i)SAT::CNF_Managerinline
getFanout(Var c, unsigned i)SAT::CNF_Managerinline
numFanins(Var c)SAT::CNF_Managerinline
numFanouts(Var c)SAT::CNF_Managerinline
numVars()SAT::CNF_Managerinline
registerAtom(const CVC3::Expr &e, const CVC3::Theorem &thm)SAT::CNF_Managerprivate
registerCNFCallback(CNFCallback *cnfCallback)SAT::CNF_Managerinline
replaceITErec(const CVC3::Expr &e, Var v, bool translateOnly)SAT::CNF_Managerprivate
setBottomScope(int scope)SAT::CNF_Managerinline
translateExpr(const CVC3::Theorem &thmIn, CNF_Formula &cnf)SAT::CNF_Managerprivate
translateExprRec(const CVC3::Expr &e, CNF_Formula &cnf, const CVC3::Theorem &thmIn)SAT::CNF_Managerprivate
~CNF_Manager()SAT::CNF_Manager