CVC3  2.4.1
expr_transform.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file expr_transform.h
4  *\brief Generally Useful Expression Transformations
5  *
6  * Author: Clark Barrett
7  *
8  * Created: Fri Aug 5 16:11:51 2005
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #ifndef _cvc3__include__expr_transform_h_
23 #define _cvc3__include__expr_transform_h_
24 
25 #include "expr.h"
26 
27 namespace CVC3 {
28 
29  class VCL;
30  class TheoryCore;
31  class CommonProofRules;
32  class CoreProofRules;
33  class TheoryArith;
34 
36 
41 
42  //! Cache for pushNegation()
44  //! Cache for newPP
46  //! Budget limit for newPP
48 
49 public:
52 
53  void setTheoryArith(TheoryArith* arith) { d_theoryArith = arith; }
54 
55 // <UFTeam Junk>
56 
57  class CParameter;
58  //void get_atoms(std::set< Expr >& atoms, const Expr& e);
59  //Theorem do_static_learn(const Expr& e);
60 
61 
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;
64  typedef std::map< Expr, Type> T_type_map;
65  typedef std::map< std::pair< Expr, Expr>, Expr > B_name_map;
66  typedef std::map<Expr, Type> B_type_map;
67  typedef std::map< Expr, std::set<Expr>*> T_generator_map;
68  typedef std::map<Expr, std::vector<Expr>*> B_Term_map;
69  typedef std::map< Expr, Expr> T_ITE_map;
70  typedef std::map< Expr, int> B_formula_map;
71  typedef std::map<Expr, std::set<int>*> NEW_formula_map;
72  typedef std::vector<Expr> T_ITE_vec;
73  std::string NewBryantVar(const int a, const int b);
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);
76  Expr ITE_generator(Expr& Orig, Expr& Value, B_Term_map& Creation_map, B_name_map& name_map,
77  T_ITE_map& ITE_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);
80 
81 
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);
83 
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);
85 
86 
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);
88 
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);
94  //void GetOrderedTerms(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, B_Term_map& G_term_map, B_Term_map& P_term_map, std::set<Expr>& SeenBefore, 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);
97 
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);
99 
100 
101 
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);
103  int CountSubTerms(const Expr& e, int& counter);
104  void GetOrdering(B_Term_map& X_generator_map, B_Term_map& G_term_map, B_Term_map& P_Term_map);
105 
106  void B_Term_Map_Deleter(B_Term_map& Map);
108 
109 
110  Theorem dobryant(const Expr& T);
111 
112 
113 
114  T_name_map ANNames(T_ack_map& ack_map, T_type_map& type_map);
115  Expr AckConstraints(T_ack_map& ack_map, T_name_map& name_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);
118  Theorem doackermann(const Expr& T);
119 
120  // <UFTeam Junk>
121 
122 
123 
124  //! Simplification that avoids stack overflow
125  /*! Stack overflow is avoided by traversing the expression to depths that are
126  multiples of 5000 until the bottom is reached. Then, simplification is done
127  bottom-up.
128  */
129  Theorem smartSimplify(const Expr& e, ExprMap<bool>& cache);
130  Theorem preprocess(const Expr& e);
131  Theorem preprocess(const Theorem& thm);
132  //! Push all negations down to the leaves
133  Theorem pushNegation(const Expr& e);
134  //! Auxiliary recursive function for pushNegation().
135  Theorem pushNegationRec(const Expr& e, bool neg);
136  //! Its version for transitivity
137  Theorem pushNegationRec(const Theorem& e, bool neg);
138  //! Push negation one level down. Takes 'e' which is 'NOT e[0]'
139  Theorem pushNegation1(const Expr& e);
140  //! Helper for newPP
142  //! new preprocessing code
143  Theorem newPP(const Expr& e, int& budget);
144  //! main new preprocessing code
145  Theorem newPPrec(const Expr& e, int& budget);
146 
147 private:
148  //! Helper for simplifyWithCare
149  void updateQueue(ExprMap<std::set<Expr>* >& queue,
150  const Expr& e,
151  const std::set<Expr>& careSet);
152  //! Helper for simplifyWithCare
153  Theorem substitute(const Expr& e,
154  ExprHashMap<Theorem>& substTable,
155  ExprHashMap<Theorem>& cache);
156 public:
157  //! ITE simplification from Burch paper
158  Theorem simplifyWithCare(const Expr& e);
159 
160  /*@}*/ // end of preprocessor stuff
161 
162 };
163 
164 }
165 
166 #endif