39 #ifndef _cvc3__expr_h_
43 #ifndef _cvc3__expr_value_h_
44 #define _cvc3__expr_value_h_
73 friend class ::CInterface;
149 if((--d_refcount) == 0) d_em->gc(
this);
157 const_cast<ExprValue*
>(
this)->d_hash = computeHash();
163 if (d_flag == d_em->getFlag())
return 0;
164 const_cast<ExprValue*
>(
this)->d_flag = d_em->getFlag();
165 return computeSize();
185 static size_t pointerHash(
void* p) {
return s_intHash((
long int)p); }
187 static size_t hash(
const int kind,
const std::vector<Expr>& kids);
189 static size_t hash(
const int n) {
return s_intHash((
long int)n); }
192 static Unsigned sizeWithChildren(
const std::vector<Expr>& kids);
197 return d_em->getMM(MMIndex);
202 {
return copy(em, 0); }
224 : d_index(idx), d_refcount(0),
225 d_hash(0), d_find(NULL), d_eqNext(NULL), d_notifyList(NULL),
227 d_dynamicFlags(em->getCurrentContext()),
230 d_flag(0), d_kind(kind), d_em(em)
232 DebugAssert(em != NULL,
"NULL ExprManager is given to ExprValue()");
235 +
")): kind is not registered").c_str());
254 {
return mm->newData(size); }
256 mm->deleteData(pMem);
260 void operator delete(
void*) { }
276 {
throw Exception(
"Illegal call to getExprValue()"); }
282 virtual bool isVar()
const {
return false; }
284 virtual bool isApply()
const {
return false; }
293 virtual const std::vector<Expr>&
getKids()
const
294 {
return d_em->getEmptyVector(); }
299 virtual unsigned arity()
const {
return 0; }
303 DebugAssert(
false,
"getSig() is called on ExprValue");
308 DebugAssert(
false,
"getRep() is called on ExprValue");
313 DebugAssert(
false,
"setSig() is called on ExprValue");
317 DebugAssert(
false,
"setRep() is called on ExprValue");
320 virtual const std::string&
getUid()
const {
321 static std::string null;
322 DebugAssert(
false,
"ExprValue::getUid() called in base class");
327 DebugAssert(
false,
"getString() is called on ExprValue");
328 static std::string s(
"");
333 DebugAssert(
false,
"getRational() is called on ExprValue");
340 static std::string ret =
"";
341 DebugAssert(
false,
"getName() is called on ExprValue");
347 DebugAssert(
false,
"getVar() is called on ExprValue");
354 DebugAssert(
false,
"getOp() is called on ExprValue");
358 virtual const std::vector<Expr>&
getVars()
const {
359 DebugAssert(
false,
"getVars() is called on ExprValue");
360 static std::vector<Expr> null;
365 DebugAssert(
false,
"getBody() is called on ExprValue");
370 virtual void setTriggers(
const std::vector<std::vector<Expr> >& triggers) {
371 DebugAssert(
false,
"setTriggers() is called on ExprValue");
374 virtual const std::vector<std::vector<Expr> >&
getTriggers()
const {
375 DebugAssert(
false,
"getTrigs() is called on ExprValue");
376 static std::vector<std::vector<Expr> > null;
382 DebugAssert(
false,
"getExistential() is called on ExprValue");
387 DebugAssert(
false,
"getIndex() is called on ExprValue");
391 virtual const std::vector<std::string>&
getFields()
const {
392 DebugAssert(
false,
"getFields() is called on ExprValue");
393 static std::vector<std::string> null;
397 DebugAssert(
false,
"getField() is called on ExprValue");
398 static std::string null;
402 DebugAssert(
false,
"getTupleIndex() is called on ExprValue");
407 DebugAssert(
false,
"getTheorem() is called on ExprValue");
433 unsigned arity()
const {
return d_children.size(); }
436 std::vector<Expr>&
getKids1() {
return d_children; }
439 const std::vector<Expr>&
getKids()
const {
return d_children; }
457 :
ExprValue(em, kind, idx), d_sig(NULL), d_rep(NULL) { }
461 :
ExprValue(em, kind, idx), d_children(kids), d_sig(NULL), d_rep(NULL) { }
467 {
return mm->newData(size); }
469 mm->deleteData(pMem);
473 void operator delete(
void*) { }
551 const std::vector<Expr>& kids)
581 const std::vector<Expr>& kids,
ExprIndex idx = 0)
590 return mm->newData(size);
593 mm->deleteData(pMem);
595 void operator delete(
void*) { }
666 static size_t hash(
const std::string& str) {
692 return mm->newData(size);
695 mm->deleteData(pMem);
697 void operator delete(
void*) { }
733 return mm->newData(size);
736 mm->deleteData(pMem);
738 void operator delete(
void*) { }
773 return mm->newData(size);
776 mm->deleteData(pMem);
778 void operator delete(
void*) { }
797 virtual bool isVar()
const {
return true; }
812 return mm->newData(size);
815 mm->deleteData(pMem);
817 void operator delete(
void*) { }
851 return mm->newData(size);
854 mm->deleteData(pMem);
856 void operator delete(
void*) { }
876 virtual bool isVar()
const {
return true; }
883 const std::string& uid,
ExprIndex idx = 0)
891 return mm->newData(size);
894 mm->deleteData(pMem);
896 void operator delete(
void*) { }
938 const Expr& body,
const std::vector<std::vector<Expr> >& trigs,
ExprIndex idx = 0)
947 return mm->newData(size);
950 mm->deleteData(pMem);
952 void operator delete(
void*) { }