1 /********************* */
2 /*! \file abstract_value.h
4 ** Top contributors (to current version):
5 ** Morgan Deters, Paul Meng, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Representation of abstract values
14 ** Representation of abstract values.
17 #include "cvc4_public.h"
23 #include "util/integer.h"
27 class CVC4_PUBLIC AbstractValue
{
28 const Integer d_index
;
32 AbstractValue(Integer index
) throw(IllegalArgumentException
);
34 ~AbstractValue() throw() {}
36 const Integer
& getIndex() const throw() {
40 bool operator==(const AbstractValue
& val
) const throw() {
41 return d_index
== val
.d_index
;
43 bool operator!=(const AbstractValue
& val
) const throw() {
44 return !(*this == val
);
47 bool operator<(const AbstractValue
& val
) const throw() {
48 return d_index
< val
.d_index
;
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 !(*this <= val
);
56 bool operator>=(const AbstractValue
& val
) const throw() {
57 return !(*this < val
);
60 };/* class AbstractValue */
62 std::ostream
& operator<<(std::ostream
& out
, const AbstractValue
& val
) CVC4_PUBLIC
;
65 * Hash function for the BitVector constants.
67 struct CVC4_PUBLIC AbstractValueHashFunction
{
68 inline size_t operator()(const AbstractValue
& val
) const {
69 return IntegerHashFunction()(val
.getIndex());
71 };/* struct AbstractValueHashFunction */