CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theory_bitvector
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
Generated on Sat May 18 2013 12:01:23 for CVC3 by
1.8.3.1