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_Manager [private]
concreteLit(Lit l, bool checkTranslated=true)SAT::CNF_Manager [inline]
concreteThm(const CVC3::Expr &e)SAT::CNF_Manager [private]
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_bottomScopeSAT::CNF_Manager [private]
d_clauseIdNextSAT::CNF_Manager [private]
d_cnfCallbackSAT::CNF_Manager [private]
d_cnfVarsSAT::CNF_Manager [private]
d_commonRulesSAT::CNF_Manager [private]
d_flagsSAT::CNF_Manager [private]
d_iteMapSAT::CNF_Manager [private]
d_minimizeClausesSAT::CNF_Manager [private]
d_nullExprSAT::CNF_Manager [private]
d_rulesSAT::CNF_Manager [private]
d_statisticsSAT::CNF_Manager [private]
d_translateQueueFlagsSAT::CNF_Manager [private]
d_translateQueueThmsSAT::CNF_Manager [private]
d_translateQueueVarsSAT::CNF_Manager [private]
d_varInfoSAT::CNF_Manager [private]
d_vcSAT::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