, 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 typedef | CVC3::ExprTransform | |
| B_name_map typedef | CVC3::ExprTransform | |
| B_Term_map typedef | CVC3::ExprTransform | |
| B_Term_Map_Deleter(B_Term_map &Map) | CVC3::ExprTransform | |
| B_type_map typedef | CVC3::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_budgetLimit | CVC3::ExprTransform | [private] |
| d_commonRules | CVC3::ExprTransform | [private] |
| d_core | CVC3::ExprTransform | [private] |
| d_newPPCache | CVC3::ExprTransform | [private] |
| d_pushNegCache | CVC3::ExprTransform | [private] |
| d_rules | CVC3::ExprTransform | [private] |
| d_theoryArith | CVC3::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 typedef | CVC3::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 typedef | CVC3::ExprTransform | |
| T_generator_map typedef | CVC3::ExprTransform | |
| T_generator_Map_Deleter(T_generator_map &Map) | CVC3::ExprTransform | |
| T_ITE_map typedef | CVC3::ExprTransform | |
| T_ITE_vec typedef | CVC3::ExprTransform | |
| T_name_map typedef | CVC3::ExprTransform | |
| T_type_map typedef | CVC3::ExprTransform | |
| updateQueue(ExprMap< std::set< Expr > * > &queue, const Expr &e, const std::set< Expr > &careSet) | CVC3::ExprTransform | [private] |
| ~ExprTransform() | CVC3::ExprTransform | [inline] |
