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_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