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);
virtual Op getOp() const
Get the Op from an Apply Expr.
virtual size_t getMMIndex() const
Get unique memory manager ID.
virtual const Rational & getRational() const
long unsigned ExprIndex
Expression index type.
MS C++ specific settings.
int getKind() const
Get the kind of the expression.
#define DebugAssert(cond, str)
bool operator==(const Expr &e1, const Expr &e2)
MemoryManager * getMM(size_t MMIndex)
Return a MemoryManager for the given ExprValue type.
virtual const std::string & getName() const
Returns the string name of UCONST and BOUND_VAR expr's.
virtual const std::vector< Expr > & getKids() const
Get kids: by default, returns a ref to an empty vector.
virtual int getBoundIndex() const
virtual const std::string & getString() const
A "closure" expression which binds variables used in the "body". Used by LAMBDA and quantifiers...
virtual const std::vector< Expr > & getVars() const
virtual const Expr & getExistential() const
int d_kind
The kind of the expression. In particular, it determines which subclass of ExprValue is used to store...
The base class for holding the actual data in expressions.
virtual const std::string & getUid() const
virtual const Expr & getBody() const