CVC3
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