22 #ifndef _cvc3__include__expr_transform_h_
23 #define _cvc3__include__expr_transform_h_
31 class CommonProofRules;
62 typedef std::map< std::pair< Expr, ExprTransform::CParameter >,
Expr >
T_name_map;
63 typedef std::map< Expr, std::set< ExprTransform::CParameter >* >
T_ack_map;
74 std::string
NewVar(
const int a,
const int b);
75 B_name_map
BryantNames(T_generator_map& generator_map, B_type_map& type_map);
78 void 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,
79 B_name_map& name_map, T_ITE_map& ITE_map);
82 void 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);
84 void 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);
87 Expr 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);
89 void 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);
90 void 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);
91 void GetFormulaMap(
const Expr& e, std::set<Expr>& formula_map, std::set<Expr>& G_terms,
int& size,
int negations);
92 void GetGTerms2(std::set<Expr>& formula_map, std::set<Expr>& G_terms);
93 void GetSub_vec(T_ITE_vec& ITE_vec,
const Expr& e, std::set<Expr>& ITE_Added);
95 void 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);
96 void 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);
98 Expr 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);
102 void 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);
104 void GetOrdering(B_Term_map& X_generator_map, B_Term_map& G_term_map, B_Term_map& P_Term_map);
114 T_name_map
ANNames(T_ack_map& ack_map, T_type_map& type_map);
116 void 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);
117 void BuildMap(
const Expr& e, T_ack_map& ack_map, T_type_map& type_map, std::set< Expr >& SeenBefore);
151 const std::set<Expr>& careSet);
Data structure of expressions in CVC3.
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
This theory handles basic linear arithmetic.
Definition of the API to expression package. See class Expr for details.