SAT::CNF_Manager Member List

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

addAssumption(const CVCL::Theorem &thm, CNF_Formula &cnf)	SAT::CNF_Manager
addLemma(const CVCL::Theorem &thm, CNF_Formula &cnf)	SAT::CNF_Manager
CNF_Manager(CVCL::TheoremManager *tm)	SAT::CNF_Manager
concreteLit(Lit l)	SAT::CNF_Manager	[inline]
convertLemma(const CVCL::Theorem &thm, Clause &c)	SAT::CNF_Manager
createProofRules(CVCL::TheoremManager *tm)	SAT::CNF_Manager	[private]
d_bottomScope	SAT::CNF_Manager	[private]
d_clauseIdNext	SAT::CNF_Manager	[private]
d_cnfVars	SAT::CNF_Manager	[private]
d_commonRules	SAT::CNF_Manager	[private]
d_iteMap	SAT::CNF_Manager	[private]
d_rules	SAT::CNF_Manager	[private]
d_theorems	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]
getCNFLit(const CVCL::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]
replaceITErec(const CVCL::Expr &e, Var v, bool translateOnly)	SAT::CNF_Manager	[private]
setBottomScope(int scope)	SAT::CNF_Manager	[inline]
translateExpr(const CVCL::Expr &e, CNF_Formula &cnf)	SAT::CNF_Manager	[private]
translateExprRec(const CVCL::Expr &e, CNF_Formula &cnf)	SAT::CNF_Manager	[private]
~CNF_Manager()	SAT::CNF_Manager

---