1 /********************* */
2 /*! \file abstract_value.h
4 ** Original author: Morgan Deters
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Representation of abstract values
14 ** Representation of abstract values.
17 #include "cvc4_public.h"
21 #include "expr/type.h"
26 class CVC4_PUBLIC AbstractValue
{
27 const Integer d_index
;
31 AbstractValue(Integer index
) throw(IllegalArgumentException
) :
33 CheckArgument(index
>= 1, index
, "index >= 1 required for abstract value, not `%s'", index
.toString().c_str());
36 ~AbstractValue() throw() {
39 const Integer
& getIndex() const throw() {
43 bool operator==(const AbstractValue
& val
) const throw() {
44 return d_index
== val
.d_index
;
46 bool operator!=(const AbstractValue
& val
) const throw() {
47 return !(*this == val
);
50 bool operator<(const AbstractValue
& val
) const throw() {
51 return d_index
< val
.d_index
;
53 bool operator<=(const AbstractValue
& val
) const throw() {
54 return d_index
<= val
.d_index
;
56 bool operator>(const AbstractValue
& val
) const throw() {
57 return !(*this <= val
);
59 bool operator>=(const AbstractValue
& val
) const throw() {
60 return !(*this < val
);
63 };/* class AbstractValue */
65 std::ostream
& operator<<(std::ostream
& out
, const AbstractValue
& val
) CVC4_PUBLIC
;
68 * Hash function for the BitVector constants.
70 struct CVC4_PUBLIC AbstractValueHashFunction
{
71 inline size_t operator()(const AbstractValue
& val
) const {
72 return IntegerHashFunction()(val
.getIndex());
74 };/* struct AbstractValueHashFunction */