CVC3  2.4.1
bitvector_expr_value.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file bitvector_expr_value.h
4  *\brief Subclasses of ExprValue for bit-vector expressions
5  *
6  * Author: Sergey Berezin, Vijay Ganesh
7  *
8  * Created: Wed Jun 23 14:36:59 2004
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #ifndef _cvc3__theory_bitvector__bitvector_expr_value_h_
23 #define _cvc3__theory_bitvector__bitvector_expr_value_h_
24 
25 #include "theory_bitvector.h"
26 
27 namespace CVC3 {
28 
29 ///////////////////////////////////////////////////////////////////////////////
30 //class BVConstExpr
31 ///////////////////////////////////////////////////////////////////////////////
32 //! An expression subclass for bitvector constants.
33 class BVConstExpr : public ExprValue {
34 private:
35  std::vector<bool> d_bvconst; //!< value of bitvector constant
36  size_t d_MMIndex; //!< The registration index for ExprManager
37  public:
38  //! Constructor
39  BVConstExpr(ExprManager* em, std::string bvconst,
40  size_t mmIndex, ExprIndex idx = 0);
41 
42  //! Constructor
43  BVConstExpr(ExprManager* em, std::vector<bool> bvconst,
44  size_t mmIndex, ExprIndex idx = 0);
45 
46  ExprValue* copy(ExprManager* em, ExprIndex idx = 0) const {
47  return new(em->getMM(getMMIndex()))
48  BVConstExpr(em, d_bvconst, d_MMIndex, idx);
49  }
50 
51  size_t computeHash() const;
52  size_t getMMIndex() const { return d_MMIndex; }
53 
54  const ExprValue* getExprValue() const { return this; }
55 
56  //! Only compare the bitvector constant, not the integer attribute
57  bool operator==(const ExprValue& ev2) const {
58  if(ev2.getMMIndex() != d_MMIndex) return false;
59  return (d_bvconst == ((const BVConstExpr&)ev2).d_bvconst);
60  }
61 
62  void* operator new(size_t size, MemoryManager* mm) {
63  return mm->newData(size);
64  }
65  void operator delete(void* pMem, MemoryManager* mm) {
66  mm->deleteData(pMem);
67  }
68 
69  void operator delete(void*) { }
70 
71  unsigned size() const { return d_bvconst.size(); }
72  bool getValue(int i) const
73  { DebugAssert(0 <= i && (unsigned)i < size(), "out of bounds");
74  return d_bvconst[i]; }
75 
76 }; //end of BVConstExpr
77 
78 } // end of namespace CVC3
79 #endif
unsigned size() const
virtual size_t getMMIndex() const
Get unique memory manager ID.
Definition: expr_value.h:263
size_t getMMIndex() const
Get unique memory manager ID.
bool getValue(int i) const
long unsigned ExprIndex
Expression index type.
Definition: expr.h:87
#define DebugAssert(cond, str)
Definition: debug.h:408
std::vector< bool > d_bvconst
value of bitvector constant
MemoryManager * getMM(size_t MMIndex)
Return a MemoryManager for the given ExprValue type.
Definition: expr_manager.h:334
size_t d_MMIndex
The registration index for ExprManager.
An expression subclass for bitvector constants.
const ExprValue * getExprValue() const
Test whether the expression is a generic subclass.
Expression Manager.
Definition: expr_manager.h:58
bool operator==(const ExprValue &ev2) const
Only compare the bitvector constant, not the integer attribute.
BVConstExpr(ExprManager *em, std::string bvconst, size_t mmIndex, ExprIndex idx=0)
Constructor.
ExprValue * copy(ExprManager *em, ExprIndex idx=0) const
Make a clean copy of itself using the given ExprManager.
size_t computeHash() const
Non-caching hash function which actually computes the hash.
The base class for holding the actual data in expressions.
Definition: expr_value.h:69
Definition: expr.cpp:35