src/expr/codatatype_bound_variable.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * Representation of bound variables in codatatype values
  14  */
  15
  16 #include "expr/codatatype_bound_variable.h"
  17
  18 #include <algorithm>
  19 #include <iostream>
  20 #include <sstream>
  21 #include <string>
  22
  23 #include "base/check.h"
  24 #include "expr/type_node.h"
  25
  26 using namespace std;
  27
  28 namespace cvc5 {
  29
  30 CodatatypeBoundVariable::CodatatypeBoundVariable(const TypeNode& type,
  31                                                  Integer index)
  32     : d_type(new TypeNode(type)), d_index(index)
  33 {
  34   PrettyCheckArgument(type.isCodatatype(),
  35                       type,
  36                       "codatatype bound variables can only be created for "
  37                       "codatatype sorts, not `%s'",
  38                       type.toString().c_str());
  39   PrettyCheckArgument(
  40       index >= 0,
  41       index,
  42       "index >= 0 required for codatatype bound variable index, not `%s'",
  43       index.toString().c_str());
  44 }
  45
  46 CodatatypeBoundVariable::~CodatatypeBoundVariable() {}
  47
  48 CodatatypeBoundVariable::CodatatypeBoundVariable(
  49     const CodatatypeBoundVariable& other)
  50     : d_type(new TypeNode(other.getType())), d_index(other.getIndex())
  51 {
  52 }
  53
  54 const TypeNode& CodatatypeBoundVariable::getType() const { return *d_type; }
  55 const Integer& CodatatypeBoundVariable::getIndex() const { return d_index; }
  56 bool CodatatypeBoundVariable::operator==(
  57     const CodatatypeBoundVariable& cbv) const
  58 {
  59   return getType() == cbv.getType() && d_index == cbv.d_index;
  60 }
  61 bool CodatatypeBoundVariable::operator!=(
  62     const CodatatypeBoundVariable& cbv) const
  63 {
  64   return !(*this == cbv);
  65 }
  66
  67 bool CodatatypeBoundVariable::operator<(
  68     const CodatatypeBoundVariable& cbv) const
  69 {
  70   return getType() < cbv.getType()
  71          || (getType() == cbv.getType() && d_index < cbv.d_index);
  72 }
  73 bool CodatatypeBoundVariable::operator<=(
  74     const CodatatypeBoundVariable& cbv) const
  75 {
  76   return getType() < cbv.getType()
  77          || (getType() == cbv.getType() && d_index <= cbv.d_index);
  78 }
  79 bool CodatatypeBoundVariable::operator>(
  80     const CodatatypeBoundVariable& cbv) const
  81 {
  82   return !(*this <= cbv);
  83 }
  84 bool CodatatypeBoundVariable::operator>=(
  85     const CodatatypeBoundVariable& cbv) const
  86 {
  87   return !(*this < cbv);
  88 }
  89
  90 std::ostream& operator<<(std::ostream& out, const CodatatypeBoundVariable& cbv)
  91 {
  92   std::stringstream ss;
  93   ss << cbv.getType();
  94   std::string st(ss.str());
  95   // must remove delimiting quotes from the name of the type
  96   // this prevents us from printing symbols like |@cbv_|T|_n|
  97   std::string q("|");
  98   size_t pos;
  99   while ((pos = st.find(q)) != std::string::npos)
 100   {
 101     st.replace(pos, 1, "");
 102   }
 103   return out << "cbv_" << st.c_str() << "_" << cbv.getIndex();
 104 }
 105
 106 size_t CodatatypeBoundVariableHashFunction::operator()(
 107     const CodatatypeBoundVariable& cbv) const
 108 {
 109   return std::hash<TypeNode>()(cbv.getType())
 110          * IntegerHashFunction()(cbv.getIndex());
 111 }
 112
 113 }  // namespace cvc5