41 ExprValue::~ExprValue() {
56 if(d_notifyList != NULL) {
70 "ExprValue::operator==() called from a subclass");
74 return (d_kind == ev2.
d_kind);
80 "ExprValue::copy() called from a subclass");
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);
100 return new(em->
getMM(getMMIndex()))
ExprNode(em, d_kind, d_children, idx);
104 ExprNode::~ExprNode()
127 return (d_kind == ev2.
getKind())
128 && (getKids() == ev2.
getKids());
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);
140 return new(em->
getMM(getMMIndex()))
ExprNode(em, d_kind, d_children, idx);
166 return new(em->
getMM(getMMIndex()))
167 ExprSkolem(em, getBoundIndex(), rebuild(getExistential(), em), idx);
169 return new(em->
getMM(getMMIndex()))
170 ExprSkolem(em, getBoundIndex(), getExistential(), idx);
190 return (getKind() == ev2.
getKind() && getName() == ev2.
getName());
194 return new(em->
getMM(getMMIndex()))
ExprVar(em, d_name, idx);
202 return (getKind() == ev2.
getKind() && getName() == ev2.
getName());
206 return new(em->
getMM(getMMIndex()))
ExprSymbol(em, d_kind, d_name, idx);
215 && getUid() == ev2.
getUid());
227 return (getOp() == ev2.
getOp())
228 && (getKids() == ev2.
getKids());
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);
241 return new(em->
getMM(getMMIndex()))
250 return (getOp() == ev2.
getOp())
251 && (getKids() == ev2.
getKids());
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);
264 return new(em->
getMM(getMMIndex()))
273 return (getKind() == ev2.
getKind())
274 && (getBody() == ev2.
getBody())
275 && (getVars() == ev2.
getVars());
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));
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));
294 manual_trigs.push_back(cur_trig);
297 return new(em->
getMM(getMMIndex()))
298 ExprClosure(em, d_kind, vars, rebuild(d_body, em), manual_trigs, idx);
300 return new(em->
getMM(getMMIndex()))
301 ExprClosure(em, d_kind, d_vars, d_body, d_manual_triggers, idx);
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();
314 void* ptr = i->d_expr;
315 res = res*
PRIME + pointerHash(ptr);
322 Unsigned ExprValue::sizeWithChildren(
const std::vector<Expr>& kids)
325 for(vector<Expr>::const_iterator i=kids.begin(), iend=kids.end();
327 res += (*i).d_expr->getSize();
333 size_t ExprClosure::computeHash()
const {
334 return d_body.
hash()*
PRIME + ExprValue::hash(d_kind, d_vars);