CVC3

expr_value.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file expr_value.h
00004  * 
00005  * Author: Sergey Berezin
00006  * 
00007  * Created: Fri Feb  7 15:07:18 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  * Class ExprValue: the value holding class of Expr.  No one should
00019  * use it directly; use Expr API instead.  To enforce that, the
00020  * constructors are made protected, and only Expr, ExprManager, and
00021  * subclasses can use them.
00022  */
00023 /*****************************************************************************/
00024 
00025 // *** HACK ATTACK *** (trick from Aaron Stump's code)
00026 
00027 // In order to inline the Expr constructors (for efficiency), this
00028 // file (expr_value.h) must be included in expr.h.  However, we also
00029 // need to include expr.h here, hence, circular dependency.  A way to
00030 // break it is to include expr_value.h in the middle of expr.h after
00031 // the definition of class Expr, but before the definition of its
00032 // inlined methods.  So, expr.h included below will also suck in
00033 // expr_value.h recursively, meaning that we then should skip the rest
00034 // of the file (since it's already been included). 
00035 
00036 // That's why expr.h is outside of #ifndef.  The same is true for
00037 // type.h and theorem.h.
00038 
00039 #ifndef _cvc3__expr_h_
00040 #include "expr.h"
00041 #endif
00042 
00043 #ifndef _cvc3__expr_value_h_
00044 #define _cvc3__expr_value_h_
00045 
00046 #include "theorem.h"
00047 #include "type.h"
00048 
00049 // The prime number used in the hash function for a vector of elements
00050 #define PRIME 131
00051 
00052 namespace CVC3 {
00053   
00054 /*****************************************************************************/
00055 /*!
00056  *\class ExprValue
00057  *\brief The base class for holding the actual data in expressions
00058  * 
00059  *
00060  * Author: Sergey Berezin
00061  *
00062  * Created: long time ago
00063  *
00064  * \anchor ExprValue The base class just holds the operator.
00065  * All the additional data resides in subclasses.
00066  * 
00067  */
00068 /*****************************************************************************/
00069 class CVC_DLL ExprValue {
00070   friend class Expr;
00071   friend class Expr::iterator;
00072   friend class ExprManager;
00073   friend class ::CInterface;
00074   friend class ExprApply;
00075   friend class Theorem;
00076   friend class ExprClosure;
00077 
00078   //! Unique expression id
00079   ExprIndex d_index;
00080 
00081   //! Reference counter for garbage collection
00082   unsigned d_refcount;
00083   
00084   //! Cached hash value (initially 0)
00085   size_t d_hash; 
00086 
00087   //! The find attribute (may be NULL)
00088   CDO<Theorem>* d_find;
00089 
00090   //! Equality between this term and next term in ring of all terms in the equivalence class
00091   CDO<Theorem>* d_eqNext;
00092 
00093   //! The cached type of the expression (may be Null)
00094   Type d_type;
00095 
00096   //! The cached TCC of the expression (may be Null)
00097   //  Expr d_tcc;
00098 
00099   //! Subtyping predicate for the expression and all subexpressions
00100   //  Theorem d_subtypePred;
00101 
00102   //! Notify list may be NULL (== no such attribute)
00103   NotifyList* d_notifyList;
00104 
00105   //! For caching calls to Simplify
00106   Theorem d_simpCache;
00107 
00108   //! For checking whether simplify cache is valid
00109   unsigned d_simpCacheTag;
00110 
00111   //! context-dependent bit-vector for flags that are context-dependent
00112   CDFlags d_dynamicFlags;
00113 
00114   //! Size of dag rooted at this expression
00115   Unsigned d_size;
00116 
00117   //! Which child has the largest height
00118   //  int d_highestKid;
00119 
00120   //! Most distant expression we were simplified *from*
00121   //  Expr d_simpFrom;
00122 
00123   //! Generic flag for marking expressions (e.g. in DAG traversal)
00124   unsigned d_flag;
00125 
00126 protected:
00127   /*! @brief The kind of the expression.  In particular, it determines which
00128    * subclass of ExprValue is used to store the expression. */
00129   int d_kind;
00130 
00131   //! Our expr. manager
00132   ExprManager* d_em;
00133 
00134   // End of data members
00135 
00136 private:
00137 
00138   //! Set the ExprIndex
00139   void setIndex(ExprIndex idx) { d_index = idx; }
00140 
00141   //! Increment reference counter
00142   void incRefcount() { ++d_refcount; }
00143 
00144   //! Decrement reference counter
00145   void decRefcount() {
00146     // Cannot be DebugAssert, since we are called in a destructor
00147     // and should not throw an exception
00148     IF_DEBUG(FatalAssert(d_refcount > 0, "Mis-handled the ref. counting");)
00149     if((--d_refcount) == 0) d_em->gc(this);
00150   }
00151 
00152   //! Caching hash function
00153   /*! Do NOT implement it in subclasses! Implement computeHash() instead.
00154    */
00155   size_t hash() const {
00156     if (d_hash == 0)
00157       const_cast<ExprValue*>(this)->d_hash = computeHash();
00158     return d_hash;
00159   }
00160 
00161   //! Return DAG-size of Expr
00162   Unsigned getSize() const {
00163     if (d_flag == d_em->getFlag()) return 0;
00164     const_cast<ExprValue*>(this)->d_flag = d_em->getFlag();
00165     return computeSize();
00166   }
00167 
00168   //! Return child with greatest height
00169   //  int getHighestKid() const { return d_highestKid; }
00170 
00171   //! Get Expr simplified to obtain this expr
00172   //  const Expr& getSimpFrom() const { return d_simpFrom; }
00173 
00174   //! Set Expr simplified to obtain this expr
00175   //  void setSimpFrom(const Expr& simpFrom) { d_simpFrom = simpFrom; }
00176 
00177 protected:
00178 
00179   // Static hash functions.  They don't depend on the context
00180   // (ExprManager and such), so it is still thread-safe to have them
00181   // static.
00182   static std::hash<char*> s_charHash;
00183   static std::hash<long int> s_intHash;
00184 
00185   static size_t pointerHash(void* p) { return s_intHash((long int)p); }
00186   // Hash function for subclasses with children
00187   static size_t hash(const int kind, const std::vector<Expr>& kids);
00188   // Hash function for kinds
00189   static size_t hash(const int n) { return s_intHash((long int)n); }
00190 
00191   // Size function for subclasses with children
00192   static Unsigned sizeWithChildren(const std::vector<Expr>& kids);
00193 
00194   //! Return the memory manager (for the benefit of subclasses)
00195   MemoryManager* getMM(size_t MMIndex) {
00196     DebugAssert(d_em!=NULL, "ExprValue::getMM()");
00197     return d_em->getMM(MMIndex);
00198   }
00199 
00200   //! Make a clean copy of itself using the given ExprManager
00201   ExprValue* rebuild(ExprManager* em) const
00202     { return copy(em, 0); }
00203 
00204   //! Make a clean copy of the expr using the given ExprManager
00205   Expr rebuild(Expr e, ExprManager* em) const
00206     { return em->rebuildRec(e); }
00207 
00208   // Protected API
00209 
00210   //! Non-caching hash function which actually computes the hash.
00211   /*! This is the method that all subclasses should implement */
00212   virtual size_t computeHash() const { return hash(d_kind); }
00213 
00214   //! Non-caching size function which actually computes the size.
00215   /*! This is the method that all subclasses should implement */
00216   virtual Unsigned computeSize() const { return 1; }
00217 
00218   //! Make a clean copy of itself using the given ExprManager
00219   virtual ExprValue* copy(ExprManager* em, ExprIndex idx) const;
00220 
00221 public:
00222   //! Constructor
00223   ExprValue(ExprManager* em, int kind, ExprIndex idx = 0)
00224     : d_index(idx), d_refcount(0),
00225       d_hash(0), d_find(NULL), d_eqNext(NULL), d_notifyList(NULL),
00226       d_simpCacheTag(0),
00227       d_dynamicFlags(em->getCurrentContext()),
00228       d_size(0),
00229       //      d_height(0), d_highestKid(-1),
00230       d_flag(0), d_kind(kind), d_em(em)
00231   {
00232     DebugAssert(em != NULL, "NULL ExprManager is given to ExprValue()");
00233     DebugAssert(em->isKindRegistered(kind),
00234                 ("ExprValue(kind = " + int2string(kind)
00235                  + ")): kind is not registered").c_str());
00236     DebugAssert(kind != APPLY, "Only ExprApply should have APPLY kind");
00237 // #ifdef _CVC3_DEBUG_MODE //added by yeting, just hold a place to put my breakpoints in gdb
00238 //     if(idx != 0){
00239 //       TRACE("expr", "expr created ", idx, "");//the line added by yeting
00240 //       //      char * a;
00241 //       //      a="a";
00242 //       //      a[999999]=255;
00243 //     }
00244 // #endif
00245   }
00246   //! Destructor
00247   virtual ~ExprValue();
00248 
00249   //! Get the kind of the expression
00250   int getKind() const { return d_kind; }
00251 
00252   //! Overload operator new
00253   void* operator new(size_t size, MemoryManager* mm)
00254     { return mm->newData(size); }
00255   void operator delete(void* pMem, MemoryManager* mm) {
00256     mm->deleteData(pMem);
00257   }
00258 
00259   //! Overload operator delete
00260   void operator delete(void*) { }
00261 
00262   //! Get unique memory manager ID
00263   virtual size_t getMMIndex() const { return EXPR_VALUE; }
00264 
00265   //! Equality between any two ExprValue objects (including subclasses)
00266   virtual bool operator==(const ExprValue& ev2) const;
00267 
00268   // Testers
00269 
00270   //! Test whether the expression is a generic subclass
00271   /*!
00272    * \return 0 for the core classes, and getMMIndex() value for
00273    * generic subclasses (those defined in DPs)
00274    */
00275   virtual const ExprValue* getExprValue() const
00276     { throw Exception("Illegal call to getExprValue()"); }
00277   //! String expression tester
00278   virtual bool isString() const { return false; }
00279   //! Rational number expression tester
00280   virtual bool isRational() const { return false; }
00281   //! Uninterpreted constants
00282   virtual bool isVar() const { return false; }
00283   //! Application of another expression
00284   virtual bool isApply() const { return false; }
00285   //! Special named symbol
00286   virtual bool isSymbol() const { return false; }
00287   //! A LAMBDA-expression or a quantifier
00288   virtual bool isClosure() const { return false; }
00289   //! Special Expr holding a theorem
00290   virtual bool isTheorem() const { return false; }
00291 
00292   //! Get kids: by default, returns a ref to an empty vector
00293   virtual const std::vector<Expr>& getKids() const
00294     { return d_em->getEmptyVector(); }
00295 
00296   // Methods to access leaf data in subclasses
00297 
00298   //! Default arity = 0
00299   virtual unsigned arity() const { return 0; }
00300 
00301   //! Special attributes for uninterpreted functions
00302   virtual CDO<Theorem>* getSig() const {
00303     DebugAssert(false, "getSig() is called on ExprValue");
00304     return NULL;
00305   }
00306 
00307   virtual CDO<Theorem>* getRep() const {
00308     DebugAssert(false, "getRep() is called on ExprValue");
00309     return NULL;
00310   }
00311 
00312   virtual void setSig(CDO<Theorem>* sig) {
00313     DebugAssert(false, "setSig() is called on ExprValue");
00314   }
00315 
00316   virtual void setRep(CDO<Theorem>* rep) {
00317     DebugAssert(false, "setRep() is called on ExprValue");
00318   }
00319 
00320   virtual const std::string& getUid() const { 
00321     static std::string null;
00322     DebugAssert(false, "ExprValue::getUid() called in base class");
00323     return null;
00324   }
00325 
00326   virtual const std::string& getString() const {
00327     DebugAssert(false, "getString() is called on ExprValue");
00328     static std::string s("");
00329     return s;
00330   }
00331 
00332   virtual const Rational& getRational() const {
00333     DebugAssert(false, "getRational() is called on ExprValue");
00334     static Rational r(0);
00335     return r;
00336   }
00337 
00338   //! Returns the string name of UCONST and BOUND_VAR expr's.
00339   virtual const std::string& getName() const {
00340     static std::string ret = "";
00341     DebugAssert(false, "getName() is called on ExprValue");
00342     return ret;
00343   }
00344 
00345   //! Returns the original Boolean variable (for BoolVarExprValue)
00346   virtual const Expr& getVar() const {
00347     DebugAssert(false, "getVar() is called on ExprValue");
00348     static Expr null;
00349     return null;
00350   }
00351 
00352   //! Get the Op from an Apply Expr
00353   virtual Op getOp() const {
00354     DebugAssert(false, "getOp() is called on ExprValue");
00355     return Op(NULL_KIND);
00356   }
00357 
00358   virtual const std::vector<Expr>& getVars() const  {
00359     DebugAssert(false, "getVars() is called on ExprValue");
00360     static std::vector<Expr> null;
00361     return null;
00362   }
00363 
00364   virtual const Expr& getBody() const {
00365     DebugAssert(false, "getBody() is called on ExprValue");
00366     static Expr null;
00367     return null;
00368   }
00369 
00370   virtual void setTriggers(const std::vector<std::vector<Expr> >& triggers) {
00371     DebugAssert(false, "setTriggers() is called on ExprValue");
00372   }
00373 
00374   virtual const std::vector<std::vector<Expr> >& getTriggers() const { //by yeting
00375     DebugAssert(false, "getTrigs() is called on ExprValue");
00376     static std::vector<std::vector<Expr> > null;
00377     return null;
00378   }
00379 
00380 
00381   virtual const Expr& getExistential() const {
00382     DebugAssert(false, "getExistential() is called on ExprValue");
00383     static Expr null;
00384     return null;
00385   }
00386   virtual int getBoundIndex() const {
00387     DebugAssert(false, "getIndex() is called on ExprValue");
00388     return 0;
00389   }
00390 
00391   virtual const std::vector<std::string>& getFields() const {
00392     DebugAssert(false, "getFields() is called on ExprValue");
00393     static std::vector<std::string> null;
00394     return null;
00395   }
00396   virtual const std::string& getField() const {
00397     DebugAssert(false, "getField() is called on ExprValue");
00398     static std::string null;
00399     return null;
00400   }
00401   virtual int getTupleIndex() const {
00402     DebugAssert(false, "getTupleIndex() is called on ExprValue");
00403     return 0;
00404   }
00405   virtual const Theorem& getTheorem() const {
00406     static Theorem null;
00407     DebugAssert(false, "getTheorem() is called on ExprValue");
00408     return null;
00409   }
00410 
00411 }; // end of class ExprValue
00412 
00413 // Class ExprNode; it's an expression with children
00414 class CVC_DLL ExprNode: public ExprValue {
00415   friend class Expr;
00416   friend class ExprManager;
00417 
00418 protected:
00419   //! Vector of children
00420   std::vector<Expr> d_children;
00421 
00422   // Special attributes for helping with congruence closure
00423   CDO<Theorem>* d_sig;
00424   CDO<Theorem>* d_rep;
00425 
00426 private:
00427 
00428   //! Tell ExprManager who we are
00429   size_t getMMIndex() const { return EXPR_NODE; }
00430 
00431 protected:
00432   //! Return number of children
00433   unsigned arity() const { return d_children.size(); }
00434 
00435   //! Return reference to children
00436   std::vector<Expr>& getKids1() { return d_children; }
00437 
00438   //! Return reference to children
00439   const std::vector<Expr>& getKids() const { return d_children; }
00440 
00441   //! Use our static hash() for the member method
00442   size_t computeHash() const {
00443     return ExprValue::hash(d_kind, d_children);
00444   }
00445 
00446   //! Use our static sizeWithChildren() for the member method
00447   Unsigned computeSize() const {
00448     return ExprValue::sizeWithChildren(d_children);
00449   }
00450 
00451   //! Make a clean copy of itself using the given memory manager
00452   virtual ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const;
00453 
00454 public:
00455   //! Constructor
00456   ExprNode(ExprManager* em, int kind, ExprIndex idx = 0)
00457     : ExprValue(em, kind, idx), d_sig(NULL), d_rep(NULL) { }
00458   //! Constructor
00459   ExprNode(ExprManager* em, int kind, const std::vector<Expr>& kids,
00460            ExprIndex idx = 0)
00461     : ExprValue(em, kind, idx), d_children(kids), d_sig(NULL), d_rep(NULL) { }
00462   //! Destructor
00463   virtual ~ExprNode();
00464     
00465   //! Overload operator new
00466   void* operator new(size_t size, MemoryManager* mm)
00467     { return mm->newData(size); }
00468   void operator delete(void* pMem, MemoryManager* mm) {
00469     mm->deleteData(pMem);
00470   }
00471 
00472   //! Overload operator delete
00473   void operator delete(void*) { }
00474 
00475   //! Compare with another ExprValue
00476   virtual bool operator==(const ExprValue& ev2) const;
00477 
00478   virtual CDO<Theorem>* getSig() const { return d_sig; }
00479   virtual CDO<Theorem>* getRep() const { return d_rep; }
00480 
00481   virtual void setRep(CDO<Theorem>* rep) { d_rep = rep; }
00482   virtual void setSig(CDO<Theorem>* sig) { d_sig = sig; }
00483 
00484 }; // end of class ExprNode
00485 
00486 // Class ExprNodeTmp; special version of ExprNode for Expr constructor
00487 class ExprNodeTmp: public ExprValue {
00488   friend class Expr;
00489   friend class ExprManager;
00490 
00491 protected:
00492   //! Vector of children
00493   const std::vector<Expr>& d_children;
00494 
00495 private:
00496 
00497   //! Tell ExprManager who we are
00498   size_t getMMIndex() const { return EXPR_NODE; }
00499 
00500 protected:
00501   //! Return number of children
00502   unsigned arity() const { return d_children.size(); }
00503 
00504   //! Return reference to children
00505   const std::vector<Expr>& getKids() const { return d_children; }
00506 
00507   //! Use our static hash() for the member method
00508   size_t computeHash() const {
00509     return ExprValue::hash(d_kind, d_children);
00510   }
00511 
00512   //! Use our static sizeWithChildren() for the member method
00513   Unsigned computeSize() const {
00514     return ExprValue::sizeWithChildren(d_children);
00515   }
00516 
00517   //! Make a clean copy of itself using the given memory manager
00518   virtual ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const;
00519 
00520 public:
00521   //! Constructor
00522   ExprNodeTmp(ExprManager* em, int kind, const std::vector<Expr>& kids)
00523     : ExprValue(em, kind, 0), d_children(kids) { }
00524 
00525   //! Destructor
00526   virtual ~ExprNodeTmp() {}
00527     
00528   //! Compare with another ExprValue
00529   virtual bool operator==(const ExprValue& ev2) const;
00530 
00531 }; // end of class ExprNodeTmp
00532 
00533 // Special version for Expr Constructor
00534 class ExprApplyTmp: public ExprNodeTmp {
00535   friend class Expr;
00536   friend class ExprManager;
00537 private:
00538   Expr d_opExpr;
00539 protected:
00540   size_t getMMIndex() const { return EXPR_APPLY; }
00541   size_t computeHash() const {
00542     return PRIME*ExprNodeTmp::computeHash() + d_opExpr.hash();
00543   }
00544   Op getOp() const { return Op(d_opExpr); }
00545   bool isApply() const { return true; }
00546   // Make a clean copy of itself using the given memory manager
00547   ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const;
00548 public:
00549   // Constructor
00550   ExprApplyTmp(ExprManager* em, const Op& op,
00551                const std::vector<Expr>& kids)
00552     : ExprNodeTmp(em, NULL_KIND, kids), d_opExpr(op.getExpr())
00553   { DebugAssert(!op.getExpr().isNull(), "Expected non-null Op");
00554     d_kind = APPLY; }
00555   virtual ~ExprApplyTmp() { }
00556 
00557   bool operator==(const ExprValue& ev2) const;
00558 }; // end of class ExprApply
00559 
00560 class CVC_DLL ExprApply: public ExprNode {
00561   friend class Expr;
00562   friend class ExprManager;
00563 private:
00564   Expr d_opExpr;
00565 protected:
00566   size_t getMMIndex() const { return EXPR_APPLY; }
00567   size_t computeHash() const {
00568     return PRIME*ExprNode::computeHash() + d_opExpr.hash();
00569   }
00570   Op getOp() const { return Op(d_opExpr); }
00571   bool isApply() const { return true; }
00572   // Make a clean copy of itself using the given memory manager
00573   ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const;
00574 public:
00575   // Constructor
00576   ExprApply(ExprManager* em, const Op& op, ExprIndex idx = 0)
00577     : ExprNode(em, NULL_KIND, idx), d_opExpr(op.getExpr())
00578   { DebugAssert(!op.getExpr().isNull(), "Expected non-null Op");
00579     d_kind = APPLY; }
00580   ExprApply(ExprManager* em, const Op& op,
00581             const std::vector<Expr>& kids, ExprIndex idx = 0)
00582     : ExprNode(em, NULL_KIND, kids, idx), d_opExpr(op.getExpr())
00583   { DebugAssert(!op.getExpr().isNull(), "Expected non-null Op");
00584     d_kind = APPLY; }
00585   virtual ~ExprApply() { }
00586 
00587   bool operator==(const ExprValue& ev2) const;
00588   // Memory management
00589   void* operator new(size_t size, MemoryManager* mm) {
00590     return mm->newData(size);
00591   }
00592   void operator delete(void* pMem, MemoryManager* mm) {
00593     mm->deleteData(pMem);
00594   }
00595   void operator delete(void*) { }
00596 }; // end of class ExprApply
00597 
00598 /*****************************************************************************/
00599 /*!
00600  *\class NamedExprValue
00601  *\brief NamedExprValue
00602  *
00603  * Author: Clark Barrett
00604  *
00605  * Created: Thu Dec  2 23:18:17 2004
00606  *
00607  * Subclass of ExprValue for kinds that have a name associated with them.
00608  */
00609 /*****************************************************************************/
00610 
00611 // class NamedExprValue : public ExprNode {
00612 //   friend class Expr;
00613 //   friend class ExprManager;
00614 
00615 // private:
00616 //   std::string d_name;
00617 
00618 // protected:
00619 
00620 //   ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const {
00621 //     return new(em->getMM(getMMIndex()))
00622 //       NamedExprValue(d_em, d_kind, d_name, d_children, idx);
00623 //   }
00624 
00625 //   ExprValue* copy(ExprManager* em, const std::vector<Expr>& kids,
00626 //            ExprIndex idx = 0) const {
00627 //     return new(em->getMM(getMMIndex()))
00628 //       NamedExprValue(d_em, d_kind, d_name, kids, idx);
00629 //   }
00630 
00631 //   size_t computeHash() const {
00632 //     return s_charHash(d_name.c_str())*PRIME + ExprNode::computeHash();
00633 //   }
00634 
00635 //   size_t getMMIndex() const { return EXPR_NAMED; }
00636 
00637 // public:
00638 //   // Constructor
00639 //   NamedExprValue(ExprManager *em, int kind, const std::string& name,
00640 //                  const std::vector<Expr>& kids, ExprIndex idx = 0)
00641 //     : ExprNode(em, kind, kids, idx), d_name(name) { }
00642 //   // virtual ~NamedExprValue();
00643 //   bool operator==(const ExprValue& ev2) const {
00644 //     if(getMMIndex() != ev2.getMMIndex()) return false;
00645 //     return (getName() == ev2.getName())
00646 //       && ExprNode::operator==(ev2);
00647 //   }
00648 
00649 //   const std::string& getName() const { return d_name; }
00650 
00651 //   // Memory management
00652 //   void* operator new(size_t size, MemoryManager* mm) {
00653 //     return mm->newData(size);
00654 //   }
00655 //   void operator delete(void*) { }
00656 // }; // end of class NamedExprValue
00657 
00658 // Leaf expressions
00659 class ExprString: public ExprValue {
00660   friend class Expr;
00661   friend class ExprManager;
00662 private:
00663   std::string d_str;
00664 
00665   // Hash function for this subclass
00666   static size_t hash(const std::string& str) {
00667     return s_charHash(str.c_str());
00668   }
00669 
00670   // Tell ExprManager who we are
00671   virtual size_t getMMIndex() const { return EXPR_STRING; }
00672 
00673 protected:
00674   // Use our static hash() for the member method
00675   virtual size_t computeHash() const { return hash(d_str); }
00676 
00677   virtual bool isString() const { return true; }
00678   virtual const std::string& getString() const { return d_str; }
00679 
00680   //! Make a clean copy of itself using the given memory manager
00681   virtual ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const;
00682 public:
00683   // Constructor
00684   ExprString(ExprManager* em, const std::string& s, ExprIndex idx = 0)
00685     : ExprValue(em, STRING_EXPR, idx), d_str(s) { }
00686   // Destructor
00687   virtual ~ExprString() { }
00688 
00689   virtual bool operator==(const ExprValue& ev2) const;
00690   // Memory management
00691   void* operator new(size_t size, MemoryManager* mm) {
00692     return mm->newData(size);
00693   }
00694   void operator delete(void* pMem, MemoryManager* mm) {
00695     mm->deleteData(pMem);
00696   }
00697   void operator delete(void*) { }
00698 }; // end of class ExprString
00699 
00700 class ExprSkolem: public ExprValue {
00701   friend class Expr;
00702   friend class ExprManager;
00703 private:
00704   Expr d_quant; //!< The quantified expression to skolemize
00705   int d_idx; //!< Variable index in the quantified expression
00706   const Expr& getExistential() const {return d_quant;}
00707   int getBoundIndex() const {return d_idx;}
00708 
00709   // Tell ExprManager who we are
00710   size_t getMMIndex() const { return EXPR_SKOLEM;}
00711 
00712 protected:
00713   size_t computeHash() const {
00714     size_t res = getExistential().getBody().hash();
00715     res = PRIME*res + getBoundIndex();
00716     return res;
00717   }
00718 
00719   bool operator==(const ExprValue& ev2) const;
00720 
00721   //! Make a clean copy of itself using the given memory manager
00722   ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const;
00723   bool isVar() const { return true; }
00724    
00725 public:
00726   // Constructor
00727   ExprSkolem(ExprManager* em, int index, const Expr& exist, ExprIndex idx = 0)
00728     : ExprValue(em, SKOLEM_VAR, idx), d_quant(exist), d_idx(index) { }
00729   // Destructor
00730   virtual ~ExprSkolem() { }
00731   // Memory management
00732   void* operator new(size_t size, MemoryManager* mm) {
00733     return mm->newData(size);
00734   }
00735   void operator delete(void* pMem, MemoryManager* mm) {
00736     mm->deleteData(pMem);
00737   }
00738   void operator delete(void*) { }
00739 }; // end of class ExprSkolem
00740 
00741 class ExprRational: public ExprValue {
00742   friend class Expr;
00743   friend class ExprManager;
00744 private:
00745   Rational d_r;
00746 
00747   virtual const Rational& getRational() const { return d_r; }
00748 
00749   // Hash function for this subclass
00750   static size_t hash(const Rational& r) {
00751     return s_charHash(r.toString().c_str());
00752   }
00753 
00754   // Tell ExprManager who we are
00755   virtual size_t getMMIndex() const { return EXPR_RATIONAL; }
00756 
00757 protected:
00758 
00759   virtual size_t computeHash() const { return hash(d_r); }
00760   virtual bool operator==(const ExprValue& ev2) const;
00761   //! Make a clean copy of itself using the given memory manager
00762   virtual ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const;
00763   virtual bool isRational() const { return true; }
00764 
00765 public:
00766   // Constructor
00767   ExprRational(ExprManager* em, const Rational& r, ExprIndex idx = 0)
00768     : ExprValue(em, RATIONAL_EXPR, idx), d_r(r) { }
00769   // Destructor
00770   virtual ~ExprRational() { }
00771   // Memory management
00772   void* operator new(size_t size, MemoryManager* mm) {
00773     return mm->newData(size);
00774   }
00775   void operator delete(void* pMem, MemoryManager* mm) {
00776     mm->deleteData(pMem);
00777   }
00778   void operator delete(void*) { }
00779 }; // end of class ExprRational
00780 
00781 // Uninterpreted constants (variables)
00782 class ExprVar: public ExprValue {
00783   friend class Expr;
00784   friend class ExprManager;
00785 private:
00786   std::string d_name;
00787 
00788   virtual const std::string& getName() const { return d_name; }
00789 
00790   // Tell ExprManager who we are
00791   virtual size_t getMMIndex() const { return EXPR_UCONST; }
00792 protected:
00793 
00794   virtual size_t computeHash() const {
00795     return s_charHash(d_name.c_str());
00796   }
00797   virtual bool isVar() const { return true; }
00798 
00799   //! Make a clean copy of itself using the given memory manager
00800   virtual ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const;
00801 
00802 public:
00803   // Constructor
00804   ExprVar(ExprManager *em, const std::string& name, ExprIndex idx = 0)
00805     : ExprValue(em, UCONST, idx), d_name(name) { }
00806   // Destructor
00807   virtual ~ExprVar() { }
00808 
00809   virtual bool operator==(const ExprValue& ev2) const;
00810   // Memory management
00811   void* operator new(size_t size, MemoryManager* mm) {
00812     return mm->newData(size);
00813   }
00814   void operator delete(void* pMem, MemoryManager* mm) {
00815     mm->deleteData(pMem);
00816   }
00817   void operator delete(void*) { }
00818 }; // end of class ExprVar
00819 
00820 // Interpreted symbols: similar to UCONST, but returns false for isVar().
00821 class ExprSymbol: public ExprValue {
00822   friend class Expr;
00823   friend class ExprManager;
00824 private:
00825   std::string d_name;
00826 
00827   virtual const std::string& getName() const { return d_name; }
00828 
00829   // Tell ExprManager who we are
00830   virtual size_t getMMIndex() const { return EXPR_SYMBOL; }
00831 protected:
00832 
00833   virtual size_t computeHash() const {
00834     return s_charHash(d_name.c_str())*PRIME + s_intHash(d_kind);
00835   }
00836   //! Make a clean copy of itself using the given memory manager
00837   virtual ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const;
00838   bool isSymbol() const { return true; }
00839 
00840 public:
00841   // Constructor
00842   ExprSymbol(ExprManager *em, int kind, const std::string& name,
00843              ExprIndex idx = 0)
00844     : ExprValue(em, kind, idx), d_name(name) { }
00845   // Destructor
00846   virtual ~ExprSymbol() { }
00847 
00848   virtual bool operator==(const ExprValue& ev2) const;
00849   // Memory management
00850   void* operator new(size_t size, MemoryManager* mm) {
00851     return mm->newData(size);
00852   }
00853   void operator delete(void* pMem, MemoryManager* mm) {
00854     mm->deleteData(pMem);
00855   }
00856   void operator delete(void*) { }
00857 }; // end of class ExprSymbol
00858 
00859 class ExprBoundVar: public ExprValue {
00860   friend class Expr;
00861   friend class ExprManager;
00862 private:
00863   std::string d_name;
00864   std::string d_uid;
00865 
00866   virtual const std::string& getName() const { return d_name; }
00867   virtual const std::string& getUid() const { return d_uid; }
00868 
00869   // Tell ExprManager who we are
00870   virtual size_t getMMIndex() const { return EXPR_BOUND_VAR; }
00871 protected:
00872 
00873   virtual size_t computeHash() const {
00874     return s_charHash(d_name.c_str())*PRIME + s_charHash(d_uid.c_str());
00875   }
00876   virtual bool isVar() const { return true; }
00877   //! Make a clean copy of itself using the given memory manager
00878   virtual ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const;
00879 
00880 public:
00881   // Constructor
00882   ExprBoundVar(ExprManager *em, const std::string& name,
00883                const std::string& uid, ExprIndex idx = 0)
00884     : ExprValue(em, BOUND_VAR, idx), d_name(name), d_uid(uid) { }
00885   // Destructor
00886   virtual ~ExprBoundVar() { }
00887 
00888   virtual bool operator==(const ExprValue& ev2) const;
00889   // Memory management
00890   void* operator new(size_t size, MemoryManager* mm) {
00891     return mm->newData(size);
00892   }
00893   void operator delete(void* pMem, MemoryManager* mm) {
00894     mm->deleteData(pMem);
00895   }
00896   void operator delete(void*) { }
00897 }; // end of class ExprBoundVar
00898 
00899 /*! @brief A "closure" expression which binds variables used in the
00900   "body".  Used by LAMBDA and quantifiers. */
00901 class ExprClosure: public ExprValue {
00902   friend class Expr;
00903   friend class ExprManager;
00904 private:
00905   //! Bound variables
00906   std::vector<Expr> d_vars;
00907   //! The body of the quantifier/lambda
00908   Expr d_body;
00909   //! Manual triggers. // added by yeting
00910   // Note that due to expr caching, only the most recent triggers specified for a given formula will be used.
00911   std::vector<std::vector<Expr> > d_manual_triggers;
00912   //! Tell ExprManager who we are
00913   virtual size_t getMMIndex() const { return EXPR_CLOSURE; }
00914 
00915   virtual const std::vector<Expr>& getVars() const { return d_vars; }
00916   virtual const Expr& getBody() const { return d_body; }
00917   virtual void setTriggers(const std::vector<std::vector<Expr> >& triggers) { d_manual_triggers = triggers; }
00918   virtual const std::vector<std::vector<Expr> >&  getTriggers() const { return d_manual_triggers; }
00919 
00920 protected:
00921 
00922   size_t computeHash() const;
00923   Unsigned computeSize() const { return d_body.d_expr->getSize() + 1; }
00924   //! Make a clean copy of itself using the given memory manager
00925   ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const;
00926 
00927 public:
00928   // Constructor
00929   ExprClosure(ExprManager *em, int kind, const Expr& var,
00930               const Expr& body, ExprIndex idx = 0)
00931     : ExprValue(em, kind, idx), d_body(body) { d_vars.push_back(var); }
00932 
00933   ExprClosure(ExprManager *em, int kind, const std::vector<Expr>& vars,
00934               const Expr& body, ExprIndex idx = 0)
00935     : ExprValue(em, kind, idx), d_vars(vars), d_body(body) { }
00936 
00937   ExprClosure(ExprManager *em, int kind, const std::vector<Expr>& vars, 
00938               const Expr& body, const std::vector<std::vector<Expr> >&  trigs, ExprIndex idx = 0)
00939     : ExprValue(em, kind, idx), d_vars(vars), d_body(body),  d_manual_triggers(trigs) { }
00940 
00941   // Destructor
00942   virtual ~ExprClosure() { }
00943 
00944   bool operator==(const ExprValue& ev2) const;
00945   // Memory management
00946   void* operator new(size_t size, MemoryManager* mm) {
00947     return mm->newData(size);
00948   }
00949   void operator delete(void* pMem, MemoryManager* mm) {
00950     mm->deleteData(pMem);
00951   }
00952   void operator delete(void*) { }
00953   virtual bool isClosure() const { return true; }
00954 }; // end of class ExprClosure
00955 
00956 
00957 } // end of namespace CVC3
00958 
00959 #endif