src/util/abstract_value.h

   1 /*********************                                                        */
   2 /*! \file abstract_value.h
   3  ** \verbatim
   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
  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 "expr/type.h"
  22 #include <iostream>
  23
  24 namespace CVC4 {
  25
  26 class CVC4_PUBLIC AbstractValue {
  27   const Integer d_index;
  28
  29 public:
  30
  31   AbstractValue(Integer index) throw(IllegalArgumentException) :
  32     d_index(index) {
  33     CheckArgument(index >= 1, index, "index >= 1 required for abstract value, not `%s'", index.toString().c_str());
  34   }
  35
  36   ~AbstractValue() throw() {
  37   }
  38
  39   const Integer& getIndex() const throw() {
  40     return d_index;
  41   }
  42
  43   bool operator==(const AbstractValue& val) const throw() {
  44     return d_index == val.d_index;
  45   }
  46   bool operator!=(const AbstractValue& val) const throw() {
  47     return !(*this == val);
  48   }
  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 d_index <= val.d_index;
  55   }
  56   bool operator>(const AbstractValue& val) const throw() {
  57     return !(*this <= val);
  58   }
  59   bool operator>=(const AbstractValue& val) const throw() {
  60     return !(*this < val);
  61   }
  62
  63 };/* class AbstractValue */
  64
  65 std::ostream& operator<<(std::ostream& out, const AbstractValue& val) CVC4_PUBLIC;
  66
  67 /**
  68  * Hash function for the BitVector constants.
  69  */
  70 struct CVC4_PUBLIC AbstractValueHashFunction {
  71   inline size_t operator()(const AbstractValue& val) const {
  72     return IntegerHashFunction()(val.getIndex());
  73   }
  74 };/* struct AbstractValueHashFunction */
  75
  76 }/* CVC4 namespace */