CVC3
expr_value.cpp
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file expr_value.cpp
4  *
5  * Author: Sergey Berezin
6  *
7  * Created: Fri Feb 7 22:29:04 2003
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 #include "expr_value.h"
22 #include "notifylist.h"
23 
24 using namespace std;
25 
26 namespace CVC3 {
27 
28 ////////////////////////////////////////////////////////////////////////
29 // Class ExprValue static members
30 ////////////////////////////////////////////////////////////////////////
31 
32 std::hash<char*> ExprValue::s_charHash;
33 std::hash<long int> ExprValue::s_intHash;
34 
35 ////////////////////////////////////////////////////////////////////////
36 // Class ExprValue methods
37 ////////////////////////////////////////////////////////////////////////
38 
39 
40 // Destructor
41 ExprValue::~ExprValue() {
42  // Be careful deleting the attributes: first set them to NULL, then
43  // delete, to avoid circular destructor calls
44  if (d_find) {
45  CDO<Theorem>* find = d_find;
46  d_find = NULL;
47  delete find;
48  free(find);
49  }
50  if (d_eqNext) {
51  CDO<Theorem>* eqNext = d_eqNext;
52  d_eqNext = NULL;
53  delete eqNext;
54  free(eqNext);
55  }
56  if(d_notifyList != NULL) {
57  NotifyList* nl = d_notifyList;
58  d_notifyList = NULL;
59  delete nl;
60  }
61  // Set all smart pointers to Null
62  d_type = Type();
63  d_simpCache=Theorem();
64  // d_simpFrom=Expr();
65 }
66 
67 // Equality between any two ExprValue objects (including subclasses)
68 bool ExprValue::operator==(const ExprValue& ev2) const {
69  DebugAssert(getMMIndex() == EXPR_VALUE,
70  "ExprValue::operator==() called from a subclass");
71  if(getMMIndex() != ev2.getMMIndex())
72  return false;
73 
74  return (d_kind == ev2.d_kind);
75 }
76 
77 
78 ExprValue* ExprValue::copy(ExprManager* em, ExprIndex idx) const {
79  DebugAssert(getMMIndex() == EXPR_VALUE,
80  "ExprValue::copy() called from a subclass");
81  return new(em->getMM(EXPR_VALUE)) ExprValue(em, d_kind, idx);
82 }
83 
84 
85 bool ExprNodeTmp::operator==(const ExprValue& ev2) const {
86  return getMMIndex() == ev2.getMMIndex() &&
87  d_kind == ev2.getKind() &&
88  getKids() == ev2.getKids();
89 }
90 
91 ExprValue* ExprNodeTmp::copy(ExprManager* em, ExprIndex idx) const {
92  if (d_em != em) {
93  vector<Expr> children;
94  vector<Expr>::const_iterator
95  i = d_children.begin(), iend = d_children.end();
96  for (; i != iend; ++i)
97  children.push_back(rebuild(*i, em));
98  return new(em->getMM(getMMIndex())) ExprNode(em, d_kind, children, idx);
99  }
100  return new(em->getMM(getMMIndex())) ExprNode(em, d_kind, d_children, idx);
101 }
102 
103 
104 ExprNode::~ExprNode()
105 {
106  // Be careful deleting the attributes: first set them to NULL, then
107  // delete, to avoid circular destructor calls
108  if (d_sig) {
109  CDO<Theorem>* sig = d_sig;
110  d_sig = NULL;
111  delete sig;
112  free(sig);
113  }
114  if (d_rep) {
115  CDO<Theorem>* rep = d_rep;
116  d_rep = NULL;
117  delete rep;
118  free(rep);
119  }
120 }
121 
122 
123 bool ExprNode::operator==(const ExprValue& ev2) const {
124  if(getMMIndex() != ev2.getMMIndex())
125  return false;
126 
127  return (d_kind == ev2.getKind())
128  && (getKids() == ev2.getKids());
129 }
130 
131 ExprValue* ExprNode::copy(ExprManager* em, ExprIndex idx) const {
132  if (d_em != em) {
133  vector<Expr> children;
134  vector<Expr>::const_iterator
135  i = d_children.begin(), iend = d_children.end();
136  for (; i != iend; ++i)
137  children.push_back(rebuild(*i, em));
138  return new(em->getMM(getMMIndex())) ExprNode(em, d_kind, children, idx);
139  }
140  return new(em->getMM(getMMIndex())) ExprNode(em, d_kind, d_children, idx);
141 }
142 
143 
144 bool ExprString::operator==(const ExprValue& ev2) const {
145  if(getMMIndex() != ev2.getMMIndex())
146  return false;
147 
148  return (getString() == ev2.getString());
149 }
150 
151 ExprValue* ExprString::copy(ExprManager* em, ExprIndex idx) const {
152  return new(em->getMM(getMMIndex())) ExprString(em, d_str, idx);
153 }
154 
155 
156 bool ExprSkolem::operator==(const ExprValue& ev2) const {
157  if(getMMIndex() != ev2.getMMIndex())
158  return false;
159 
160  return (getBoundIndex() == ev2.getBoundIndex()
161  && getExistential() == ev2.getExistential());
162 }
163 
164 ExprValue* ExprSkolem::copy(ExprManager* em, ExprIndex idx) const {
165  if (d_em != em) {
166  return new(em->getMM(getMMIndex()))
167  ExprSkolem(em, getBoundIndex(), rebuild(getExistential(), em), idx);
168  }
169  return new(em->getMM(getMMIndex()))
170  ExprSkolem(em, getBoundIndex(), getExistential(), idx);
171 }
172 
173 
174 bool ExprRational::operator==(const ExprValue& ev2) const {
175  if(getMMIndex() != ev2.getMMIndex())
176  return false;
177 
178  return (getRational() == ev2.getRational());
179 }
180 
181 ExprValue* ExprRational::copy(ExprManager* em, ExprIndex idx) const {
182  return new(em->getMM(getMMIndex())) ExprRational(em, d_r, idx);
183 }
184 
185 
186 bool ExprVar::operator==(const ExprValue& ev2) const {
187  if(getMMIndex() != ev2.getMMIndex())
188  return false;
189 
190  return (getKind() == ev2.getKind() && getName() == ev2.getName());
191 }
192 
193 ExprValue* ExprVar::copy(ExprManager* em, ExprIndex idx) const {
194  return new(em->getMM(getMMIndex())) ExprVar(em, d_name, idx);
195 }
196 
197 
198 bool ExprSymbol::operator==(const ExprValue& ev2) const {
199  if(getMMIndex() != ev2.getMMIndex())
200  return false;
201 
202  return (getKind() == ev2.getKind() && getName() == ev2.getName());
203 }
204 
205 ExprValue* ExprSymbol::copy(ExprManager* em, ExprIndex idx) const {
206  return new(em->getMM(getMMIndex())) ExprSymbol(em, d_kind, d_name, idx);
207 }
208 
209 
210 bool ExprBoundVar::operator==(const ExprValue& ev2) const {
211  if(getMMIndex() != ev2.getMMIndex())
212  return false;
213 
214  return (getKind() == ev2.getKind() && getName() == ev2.getName()
215  && getUid() == ev2.getUid());
216 }
217 
218 ExprValue* ExprBoundVar::copy(ExprManager* em, ExprIndex idx) const {
219  return new(em->getMM(getMMIndex())) ExprBoundVar(em, d_name, d_uid, idx);
220 }
221 
222 
223 bool ExprApply::operator==(const ExprValue& ev2) const {
224  if(getMMIndex() != ev2.getMMIndex())
225  return false;
226 
227  return (getOp() == ev2.getOp())
228  && (getKids() == ev2.getKids());
229 }
230 
231 ExprValue* ExprApply::copy(ExprManager* em, ExprIndex idx) const {
232  if (d_em != em) {
233  vector<Expr> children;
234  vector<Expr>::const_iterator
235  i = d_children.begin(), iend = d_children.end();
236  for (; i != iend; ++i)
237  children.push_back(rebuild(*i, em));
238  return new(em->getMM(getMMIndex()))
239  ExprApply(em, Op(rebuild(d_opExpr, em)), children, idx);
240  }
241  return new(em->getMM(getMMIndex()))
242  ExprApply(em, Op(d_opExpr), d_children, idx);
243 }
244 
245 
246 bool ExprApplyTmp::operator==(const ExprValue& ev2) const {
247  if(getMMIndex() != ev2.getMMIndex())
248  return false;
249 
250  return (getOp() == ev2.getOp())
251  && (getKids() == ev2.getKids());
252 }
253 
254 ExprValue* ExprApplyTmp::copy(ExprManager* em, ExprIndex idx) const {
255  if (d_em != em) {
256  vector<Expr> children;
257  vector<Expr>::const_iterator
258  i = d_children.begin(), iend = d_children.end();
259  for (; i != iend; ++i)
260  children.push_back(rebuild(*i, em));
261  return new(em->getMM(getMMIndex()))
262  ExprApply(em, Op(rebuild(d_opExpr, em)), children, idx);
263  }
264  return new(em->getMM(getMMIndex()))
265  ExprApply(em, Op(d_opExpr), d_children, idx);
266 }
267 
268 
269 bool ExprClosure::operator==(const ExprValue& ev2) const {
270  if(getMMIndex() != ev2.getMMIndex())
271  return false;
272 
273  return (getKind() == ev2.getKind())
274  && (getBody() == ev2.getBody())
275  && (getVars() == ev2.getVars());
276 }
277 
278 ExprValue* ExprClosure::copy(ExprManager* em, ExprIndex idx) const {
279  if (d_em != em) {
280  vector<Expr> vars;
281  vector<Expr>::const_iterator i = d_vars.begin(), iend = d_vars.end();
282  for (; i != iend; ++i)
283  vars.push_back(rebuild(*i, em));
284 
285  vector<vector<Expr> > manual_trigs;
286  vector<vector<Expr> >::const_iterator j = d_manual_triggers.begin(), jend = d_manual_triggers.end();
287  for (; j != jend; ++j) {
288  vector<Expr >::const_iterator k = j->begin(), kend = j->end();
289  vector<Expr> cur_trig;
290  for (; k != kend; ++k){
291  cur_trig.push_back(rebuild(*k,em));
292  }
293  // manual_trigs.push_back(rebuild(*j, em));
294  manual_trigs.push_back(cur_trig);
295  }
296 
297  return new(em->getMM(getMMIndex()))
298  ExprClosure(em, d_kind, vars, rebuild(d_body, em), manual_trigs, idx);
299  }
300  return new(em->getMM(getMMIndex()))
301  ExprClosure(em, d_kind, d_vars, d_body, d_manual_triggers, idx);
302 }
303 
304 
305 ////////////////////////////////////////////////////////////////////////
306 // Methods of subclasses of ExprValue
307 ////////////////////////////////////////////////////////////////////////
308 
309 // Hash function for subclasses with kids.
310 size_t ExprValue::hash(const int kind, const std::vector<Expr>& kids) {
311  size_t res(s_intHash((long int)kind));
312  for(std::vector<Expr>::const_iterator i=kids.begin(), iend=kids.end();
313  i!=iend; ++i) {
314  void* ptr = i->d_expr;
315  res = res*PRIME + pointerHash(ptr);
316  }
317  return res;
318 }
319 
320 
321 // Size function for subclasses with kids.
322 Unsigned ExprValue::sizeWithChildren(const std::vector<Expr>& kids)
323 {
324  Unsigned res = 1;
325  for(vector<Expr>::const_iterator i=kids.begin(), iend=kids.end();
326  i!=iend; ++i) {
327  res += (*i).d_expr->getSize();
328  }
329  return res;
330 }
331 
332 
333 size_t ExprClosure::computeHash() const {
334  return d_body.hash()*PRIME + ExprValue::hash(d_kind, d_vars);
335 }
336 
337 
338 } // end of namespace CVC3