1 /********************* */
2 /*! \file abstract_value.h
4 ** Top contributors (to current version):
5 ** Morgan Deters, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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
;
31 AbstractValue(Integer index
);
33 const Integer
& getIndex() const { return d_index
; }
34 bool operator==(const AbstractValue
& val
) const
36 return d_index
== val
.d_index
;
38 bool operator!=(const AbstractValue
& val
) const { return !(*this == val
); }
39 bool operator<(const AbstractValue
& val
) const
41 return d_index
< val
.d_index
;
43 bool operator<=(const AbstractValue
& val
) const
45 return d_index
<= val
.d_index
;
47 bool operator>(const AbstractValue
& val
) const { return !(*this <= val
); }
48 bool operator>=(const AbstractValue
& val
) const { return !(*this < val
); }
49 };/* class AbstractValue */
51 std::ostream
& operator<<(std::ostream
& out
, const AbstractValue
& val
) CVC4_PUBLIC
;
54 * Hash function for the BitVector constants.
56 struct CVC4_PUBLIC AbstractValueHashFunction
{
57 inline size_t operator()(const AbstractValue
& val
) const {
58 return IntegerHashFunction()(val
.getIndex());
60 };/* struct AbstractValueHashFunction */