src/util/abstract_value.h

   1 /*********************                                                        */
   2 /*! \file abstract_value.h
   3  ** \verbatim
   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
  11  **
  12  ** \brief Representation of abstract values
  13  **
  14  ** Representation of abstract values.
  15  **/
  16
  17 #include "cvc4_public.h"
  18
  19 #pragma once
  20
  21 #include <iosfwd>
  22
  23 #include "util/integer.h"
  24
  25 namespace CVC4 {
  26
  27 class CVC4_PUBLIC AbstractValue {
  28   const Integer d_index;
  29
  30 public:
  31
  32   AbstractValue(Integer index) throw(IllegalArgumentException);
  33
  34   ~AbstractValue() throw() {}
  35
  36   const Integer& getIndex() const throw() {
  37     return d_index;
  38   }
  39
  40   bool operator==(const AbstractValue& val) const throw() {
  41     return d_index == val.d_index;
  42   }
  43   bool operator!=(const AbstractValue& val) const throw() {
  44     return !(*this == val);
  45   }
  46
  47   bool operator<(const AbstractValue& val) const throw() {
  48     return d_index < val.d_index;
  49   }
  50   bool operator<=(const AbstractValue& val) const throw() {
  51     return d_index <= val.d_index;
  52   }
  53   bool operator>(const AbstractValue& val) const throw() {
  54     return !(*this <= val);
  55   }
  56   bool operator>=(const AbstractValue& val) const throw() {
  57     return !(*this < val);
  58   }
  59
  60 };/* class AbstractValue */
  61
  62 std::ostream& operator<<(std::ostream& out, const AbstractValue& val) CVC4_PUBLIC;
  63
  64 /**
  65  * Hash function for the BitVector constants.
  66  */
  67 struct CVC4_PUBLIC AbstractValueHashFunction {
  68   inline size_t operator()(const AbstractValue& val) const {
  69     return IntegerHashFunction()(val.getIndex());
  70   }
  71 };/* struct AbstractValueHashFunction */
  72
  73 }/* CVC4 namespace */