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);
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);
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);
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);
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);
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.