src/util/record.h

   1 /*********************                                                        */
   2 /*! \file record.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-2013  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 A class representing a Record definition
  13  **
  14  ** A class representing a Record definition.
  15  **/
  16
  17 #include "cvc4_public.h"
  18
  19 #ifndef __CVC4__RECORD_H
  20 #define __CVC4__RECORD_H
  21
  22 #include <iostream>
  23 #include <string>
  24 #include <vector>
  25 #include <utility>
  26 #include "util/hash.h"
  27
  28 namespace CVC4 {
  29
  30 class CVC4_PUBLIC Record;
  31
  32 // operators for record select and update
  33
  34 class CVC4_PUBLIC RecordSelect {
  35   std::string d_field;
  36 public:
  37   RecordSelect(const std::string& field) throw() : d_field(field) { }
  38   std::string getField() const throw() { return d_field; }
  39   bool operator==(const RecordSelect& t) const throw() { return d_field == t.d_field; }
  40   bool operator!=(const RecordSelect& t) const throw() { return d_field != t.d_field; }
  41 };/* class RecordSelect */
  42
  43 class CVC4_PUBLIC RecordUpdate {
  44   std::string d_field;
  45 public:
  46   RecordUpdate(const std::string& field) throw() : d_field(field) { }
  47   std::string getField() const throw() { return d_field; }
  48   bool operator==(const RecordUpdate& t) const throw() { return d_field == t.d_field; }
  49   bool operator!=(const RecordUpdate& t) const throw() { return d_field != t.d_field; }
  50 };/* class RecordUpdate */
  51
  52 struct CVC4_PUBLIC RecordSelectHashFunction {
  53   inline size_t operator()(const RecordSelect& t) const {
  54     return StringHashFunction()(t.getField());
  55   }
  56 };/* struct RecordSelectHashFunction */
  57
  58 struct CVC4_PUBLIC RecordUpdateHashFunction {
  59   inline size_t operator()(const RecordUpdate& t) const {
  60     return StringHashFunction()(t.getField());
  61   }
  62 };/* struct RecordUpdateHashFunction */
  63
  64 std::ostream& operator<<(std::ostream& out, const RecordSelect& t) CVC4_PUBLIC;
  65 std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) CVC4_PUBLIC;
  66
  67 inline std::ostream& operator<<(std::ostream& out, const RecordSelect& t) {
  68   return out << "[" << t.getField() << "]";
  69 }
  70
  71 inline std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) {
  72   return out << "[" << t.getField() << "]";
  73 }
  74
  75 }/* CVC4 namespace */
  76
  77 #include "expr/expr.h"
  78 #include "expr/type.h"
  79
  80 namespace CVC4 {
  81
  82 // now an actual record definition
  83
  84 class CVC4_PUBLIC Record {
  85   std::vector< std::pair<std::string, Type> > d_fields;
  86
  87 public:
  88
  89   typedef std::vector< std::pair<std::string, Type> >::const_iterator const_iterator;
  90   typedef const_iterator iterator;
  91
  92   Record(const std::vector< std::pair<std::string, Type> >& fields) :
  93     d_fields(fields) {
  94     CheckArgument(! fields.empty(), fields, "fields in record description cannot be empty");
  95   }
  96
  97   const_iterator find(std::string name) const {
  98     const_iterator i;
  99     for(i = begin(); i != end(); ++i) {
 100       if((*i).first == name) {
 101         break;
 102       }
 103     }
 104     return i;
 105   }
 106
 107   size_t getIndex(std::string name) const {
 108     const_iterator i = find(name);
 109     CheckArgument(i != end(), name, "requested field `%s' does not exist in record", name.c_str());
 110     return i - begin();
 111   }
 112
 113   size_t getNumFields() const {
 114     return d_fields.size();
 115   }
 116
 117   const_iterator begin() const {
 118     return d_fields.begin();
 119   }
 120
 121   const_iterator end() const {
 122     return d_fields.end();
 123   }
 124
 125   std::pair<std::string, Type> operator[](size_t index) const {
 126     CheckArgument(index < d_fields.size(), index, "index out of bounds for record type");
 127     return d_fields[index];
 128   }
 129
 130   bool operator==(const Record& r) const {
 131     return d_fields == r.d_fields;
 132   }
 133
 134   bool operator!=(const Record& r) const {
 135     return !(*this == r);
 136   }
 137
 138 };/* class Record */
 139
 140 struct CVC4_PUBLIC RecordHashFunction {
 141   inline size_t operator()(const Record& r) const {
 142     size_t n = 0;
 143     for(Record::iterator i = r.begin(); i != r.end(); ++i) {
 144       n = (n << 3) ^ TypeHashFunction()((*i).second);
 145     }
 146     return n;
 147   }
 148 };/* struct RecordHashFunction */
 149
 150 std::ostream& operator<<(std::ostream& os, const Record& r) CVC4_PUBLIC;
 151
 152 }/* CVC4 namespace */
 153
 154 #endif /* __CVC4__RECORD_H */