bitvector_expr_value.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file bitvector_expr_value.h
00004  *\brief Subclasses of ExprValue for bit-vector expressions
00005  *
00006  * Author: Sergey Berezin, Vijay Ganesh
00007  *
00008  * Created: Wed Jun 23 14:36:59 2004
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  * 
00019  */
00020 /*****************************************************************************/
00021 
00022 #ifndef _cvc3__theory_bitvector__bitvector_expr_value_h_
00023 #define _cvc3__theory_bitvector__bitvector_expr_value_h_
00024 
00025 #include "theory_bitvector.h"
00026 
00027 namespace CVC3 {
00028 
00029 ///////////////////////////////////////////////////////////////////////////////
00030 //class BVConstExpr
00031 ///////////////////////////////////////////////////////////////////////////////
00032 //! An expression subclass for bitvector constants.
00033 class BVConstExpr : public ExprValue {
00034 private:
00035   std::vector<bool> d_bvconst; //!< value of bitvector constant
00036   size_t d_MMIndex; //!< The registration index for ExprManager
00037  public:
00038   //! Constructor
00039   BVConstExpr(ExprManager* em, std::string bvconst,
00040         size_t mmIndex, ExprIndex idx = 0);
00041   
00042   //! Constructor
00043   BVConstExpr(ExprManager* em, std::vector<bool> bvconst,
00044         size_t mmIndex, ExprIndex idx = 0);
00045   
00046   ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const {
00047     return new(em->getMM(getMMIndex()))
00048       BVConstExpr(em, d_bvconst, d_MMIndex, idx);
00049   }
00050 
00051   size_t computeHash() const;
00052   size_t getMMIndex() const { return d_MMIndex; }
00053 
00054   const ExprValue* getExprValue() const { return this; }
00055   
00056   //! Only compare the bitvector constant, not the integer attribute
00057   bool operator==(const ExprValue& ev2) const {
00058     if(ev2.getMMIndex() != d_MMIndex) return false;
00059     return (d_bvconst == ((const BVConstExpr&)ev2).d_bvconst);
00060   }
00061   
00062   void* operator new(size_t size, MemoryManager* mm) {
00063     return mm->newData(size);
00064   }
00065   void operator delete(void* pMem, MemoryManager* mm) {
00066     mm->deleteData(pMem);
00067   }
00068 
00069   void operator delete(void*) { }
00070 
00071   unsigned size() const { return d_bvconst.size(); }
00072   bool getValue(int i) const
00073     { DebugAssert(0 <= i && (unsigned)i < size(), "out of bounds");
00074       return d_bvconst[i]; }
00075 
00076 }; //end of BVConstExpr
00077 
00078 } // end of namespace CVC3
00079 #endif

Generated on Tue Jul 3 14:33:34 2007 for CVC3 by  doxygen 1.5.1