CVC3::ExprTransform Member List

This is the complete list of members for CVC3::ExprTransform, including all inherited members.

AckConstraints(T_ack_map &ack_map, T_name_map &name_map)CVC3::ExprTransform
ANNames(T_ack_map &ack_map, T_type_map &type_map)CVC3::ExprTransform
B_formula_map typedefCVC3::ExprTransform
B_name_map typedefCVC3::ExprTransform
B_Term_map typedefCVC3::ExprTransform
B_Term_Map_Deleter(B_Term_map &Map)CVC3::ExprTransform
B_type_map typedefCVC3::ExprTransform
BryantNames(T_generator_map &generator_map, B_type_map &type_map)CVC3::ExprTransform
BuildBryantMaps(const Expr &e, T_generator_map &generator_map, B_Term_map &X_generator_map, B_type_map &type_map, std::vector< Expr > &Pred_vec, std::set< Expr > &P_terms, std::set< Expr > &G_terms, B_Term_map &P_term_map, B_Term_map &G_term_map, std::set< Expr > &SeenBefore, std::set< Expr > &ITE_Added)CVC3::ExprTransform
BuildMap(const Expr &e, T_ack_map &ack_map, T_type_map &type_map, std::set< Expr > &SeenBefore)CVC3::ExprTransform
ConstrainedConstraints(std::set< Expr > &Not_replaced_set, T_generator_map &Constrained_map, B_name_map &name_map, B_Term_map &Creation_map, std::set< Expr > &Constrained_set, std::set< Expr > &UnConstrained_set, std::set< Expr > &P_constrained_set)CVC3::ExprTransform
ConstrainedConstraints(T_generator_map &Constrained_map, B_name_map &name_map, B_Term_map &Creation_map, std::set< Expr > &Constrained_set, std::set< Expr > &UnConstrained_set, std::set< Expr > &P_constrained_set)CVC3::ExprTransform
CountSubTerms(const Expr &e, int &counter)CVC3::ExprTransform
d_budgetLimitCVC3::ExprTransform [private]
d_commonRulesCVC3::ExprTransform [private]
d_coreCVC3::ExprTransform [private]
d_newPPCacheCVC3::ExprTransform [private]
d_pushNegCacheCVC3::ExprTransform [private]
d_rulesCVC3::ExprTransform [private]
d_theoryArithCVC3::ExprTransform [private]
doackermann(const Expr &T)CVC3::ExprTransform
dobryant(const Expr &T)CVC3::ExprTransform
ExprTransform(TheoryCore *core)CVC3::ExprTransform
Get_ITEs(B_formula_map &instance_map, std::set< Expr > &Not_replaced_set, B_Term_map &P_term_map, T_ITE_vec &ITE_vec, B_Term_map &Creation_map, B_name_map &name_map, T_ITE_map &ITE_map)CVC3::ExprTransform
GetAckSwap(const Expr &orig, std::vector< Expr > &OldAck, std::vector< Expr > &NewAck, T_name_map &name_map, T_ack_map &ack_map, std::set< Expr > &SeenBefore)CVC3::ExprTransform
GetFormulaMap(const Expr &e, std::set< Expr > &formula_map, std::set< Expr > &G_terms, int &size, int negations)CVC3::ExprTransform
GetGTerms2(std::set< Expr > &formula_map, std::set< Expr > &G_terms)CVC3::ExprTransform
GetOrderedTerms(B_formula_map &instance_map, B_name_map &name_map, B_Term_map &X_term_map, T_ITE_vec &ITE_vec, std::set< Expr > &G_terms, std::set< Expr > &X_terms, std::vector< Expr > &Pred_vec, std::vector< Expr > &sortedOps, std::vector< Expr > &Constrained_vec, std::vector< Expr > &UnConstrained_vec, std::set< Expr > &Constrained_set, std::set< Expr > &UnConstrained_set, B_Term_map &G_term_map, B_Term_map &P_term_map, std::set< Expr > &SeenBefore, std::set< Expr > &ITE_Added)CVC3::ExprTransform
GetOrdering(B_Term_map &X_generator_map, B_Term_map &G_term_map, B_Term_map &P_Term_map)CVC3::ExprTransform
GetPEqs(const Expr &e, B_name_map &name_map, std::set< Expr > &P_constrained_set, std::set< Expr > &Constrained_set, T_generator_map &Constrained_map, std::set< Expr > &SeenBefore)CVC3::ExprTransform
GetSortedOpVec(B_Term_map &X_generator_map, B_Term_map &X_term_map, B_Term_map &P_term_map, std::set< Expr > &P_terms, std::set< Expr > &G_terms, std::set< Expr > &X_terms, std::vector< Expr > &sortedOps, std::set< Expr > &SeenBefore)CVC3::ExprTransform
GetSub_vec(T_ITE_vec &ITE_vec, const Expr &e, std::set< Expr > &ITE_Added)CVC3::ExprTransform
ITE_generator(Expr &Orig, Expr &Value, B_Term_map &Creation_map, B_name_map &name_map, T_ITE_map &ITE_map)CVC3::ExprTransform
NEW_formula_map typedefCVC3::ExprTransform
NewBryantVar(const int a, const int b)CVC3::ExprTransform
newPP(const Expr &e, int &budget)CVC3::ExprTransform
newPPrec(const Expr &e, int &budget)CVC3::ExprTransform
NewVar(const int a, const int b)CVC3::ExprTransform
PredConstrainer(std::set< Expr > &Not_replaced_set, const Expr &e, const Expr &Pred, int location, B_name_map &name_map, std::set< Expr > &SeenBefore, std::set< Expr > &Constrained_set, T_generator_map &Constrained_map, std::set< Expr > &P_constrained_set)CVC3::ExprTransform
PredConstrainTester(std::set< Expr > &Not_replaced_set, const Expr &e, B_name_map &name_map, std::vector< Expr > &Pred_vec, std::set< Expr > &Constrained_set, std::set< Expr > &P_constrained_set, T_generator_map &Constrained_map)CVC3::ExprTransform
preprocess(const Expr &e)CVC3::ExprTransform
preprocess(const Theorem &thm)CVC3::ExprTransform
pushNegation(const Expr &e)CVC3::ExprTransform
pushNegation1(const Expr &e)CVC3::ExprTransform
pushNegationRec(const Expr &e, bool neg)CVC3::ExprTransform
pushNegationRec(const Theorem &e, bool neg)CVC3::ExprTransform
RemoveFunctionApps(const Expr &orig, std::set< Expr > &Not_replaced_set, std::vector< Expr > &Old, std::vector< Expr > &New, T_ITE_map &ITE_map, std::set< Expr > &SeenBefore)CVC3::ExprTransform
setTheoryArith(TheoryArith *arith)CVC3::ExprTransform [inline]
simplifyWithCare(const Expr &e)CVC3::ExprTransform
smartSimplify(const Expr &e, ExprMap< bool > &cache)CVC3::ExprTransform
specialSimplify(const Expr &e, ExprHashMap< Theorem > &cache)CVC3::ExprTransform
substitute(const Expr &e, ExprHashMap< Theorem > &substTable, ExprHashMap< Theorem > &cache)CVC3::ExprTransform [private]
T_ack_map typedefCVC3::ExprTransform
T_generator_map typedefCVC3::ExprTransform
T_generator_Map_Deleter(T_generator_map &Map)CVC3::ExprTransform
T_ITE_map typedefCVC3::ExprTransform
T_ITE_vec typedefCVC3::ExprTransform
T_name_map typedefCVC3::ExprTransform
T_type_map typedefCVC3::ExprTransform
updateQueue(ExprMap< std::set< Expr > * > &queue, const Expr &e, const std::set< Expr > &careSet)CVC3::ExprTransform [private]
~ExprTransform()CVC3::ExprTransform [inline]

Generated on Wed Nov 18 16:14:59 2009 for CVC3 by  doxygen 1.5.2